Negationless intuitionism (Q1267080)

It is well known that there are serious obstacles to obtain constructive completeness results for intuitionistic (predicate) logic IL since completeness for IL with respect to intuitionistic validity implies a form of the Markov principle. The author studies so-called natural (also called intuitive or internal) interpretations of IL which are based on the Heyting interpretation of logically compound sentences. The author reviews results by Veldman, de Swart, Friedman, Troelstra and himself on so-called fallible Beth models for which intuitionistic proofs of completeness (and strong completeness where one has an arbitrary set of premises) of IL can be obtained. In fallible Beth models, \(\perp\) is allowed to be true at some node. From results due to Kreisel it is known that the theory of lawless sequences allows to connect Beth semantics and natural semantics. So ``the problem arises to seek an intuitive counterpart of fallible Beth semantics, so as to recover strong completeness for some intuitionistically acceptable extensions of natural semantics. The difficulty is that allowing \(\perp\) to be true in a natural interpretation amounts to allowing its possible intuitive provability, in disagreement with Heyting's clause 1'' (p. 168). Using the theory of lawless sequences, the author proves a strong completeness result for a negationless (Henkin-style) semantics for second-order intuitionistic logic. ``Negationless semantics'' here means that \(\perp\) is not interpreted according to its intended meaning but is treated as defined by \(\perp\;=_{df}\forall F\forall x F(x)\). In the final section of the paper, the author discusses the philosophical significance of lawless negationless semantics. Reviewer's remark: In Section 2 of the paper under review, the author proves that ``strong completeness is contradictory'' (and not only unprovable intuitionistically), which seems to be at odds with the well-known result that Markov's principle allows to prove strong completeness w.r.t. Beth models, which in turn -- using lawless sequences -- yields strong completeness for natural semantics [see, e.g., \textit{M. Dummett}, Elements of intuitionism (1977; Zbl 0358.02032)]. In the latter result, however, the set \(\Gamma\) of premises is given explicitly as an enumeration of formulas, whereas for the set \(\Gamma:= \{\perp: M\models A\vee\neg A\}\), used in the proof by the author, it is undecidable whether \(\Gamma\) is empty or the singleton set \(\{\perp\}\), which seems to be a bit artificial and in particular implies that one cannot decide whether a given proof-tree of a formula \(\varphi\) is actually a proof \(\Gamma\vdash\varphi\).