# Question about derivation of $\phi, \neg \phi \vdash \psi$ with constructive propositional logic system

I am trying to solve exercise 3.37b from Goldrei's logic book, with non-classical propositional axioms. The axioms are as follows:

Ax 1: $$(\phi \rightarrow (\psi \rightarrow \phi))$$
Ax 2: $$((\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \theta)))$$
Ax 3: $$((\phi \rightarrow \psi) \rightarrow ((\phi \rightarrow \neg \psi) \rightarrow \neg \phi))$$

I can derive $$\phi, \neg \phi \vdash \neg \psi$$ in the following manner:

1. $$\phi \rightarrow (\psi \rightarrow \phi)$$ (Ax 1)
2. $$\neg \phi \rightarrow (\psi \rightarrow \neg \phi)$$ (Ax 1)
3. $$(\psi \rightarrow \phi) \rightarrow ((\psi \rightarrow \neg \phi) \rightarrow \neg \psi)$$ (Ax 3)
4. $$\neg \psi$$ (MP 1,2,3 a few times with the assumptions)

But I don't see how to derive an arbitrary formula without a negation sign. In this proof system, it is not possible to derive $$\neg \neg \psi \vdash \psi$$.

• You can’t prove the sequent in question with those axioms. If $\neg \phi :=(\phi \to \bot)$, then you can change the last axiom to $((\psi \to \phi) \to ((\psi \to \neg \phi) \to (\psi \to \chi))$, or simply replace it with $\bot \to \chi$. Jul 3, 2023 at 4:14
• Interesting. Do you know how one would prove that the derivation isn't possible with those axioms? Would one use a quasi-truth assignment of 3 values for implication and negation? Jul 3, 2023 at 15:00
• Yes. You just have to make sure that modus ponens and all of the axioms are valid on that truth assignment, but that the sequent in question doesn’t follow from those axioms. Jul 3, 2023 at 16:25
• @PW_246 Did you personally use the quasi-truth assignment technique to come to the conclusion that $\psi$ wasn't derivable? Or did you use some other heuristic based on the structure of the axioms? Jul 3, 2023 at 18:25
• I used a tree system. It can also be shown by identifying a constructive sequent system that proves these axioms, but does not validate the sequent in question. Such a sequent calculus is that of Minimal Logic. Jul 3, 2023 at 18:35

There is an error in the book (I would notify this to Derek Goldrei, but I've seen that, sadly, he has passed away, R.I.P.).

With the given axiom

$$(\phi\rightarrow\psi)\rightarrow((\phi\rightarrow\neg\psi)\rightarrow\neg\phi)$$

which was introduced by Kolmogorov, a weak version of ex falso quodlibet can be proved, that is

$$\phi,\neg\phi\vdash\neg\psi$$

In order to prove

$$\phi,\neg\phi\vdash\psi$$

Heyting's axiom

$$\neg\phi\rightarrow(\phi\rightarrow\psi)$$

is needed.

I shall expand on this topic later.

As Goldrei goes on to explain in the book, the discussion is concerning intuitionistic logic.

Early on, Kolmogorov held that the principle of explosion (ex falso [sequitur] quodlibet) is not coherent with the intuitionistic stance. Talking about the system proposed by Hilbert, he says (see “On the Principle of Excluded Middle” in From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, edited by J.van Heijenoort, p. 421):

. . . the axiom now considered does not have and cannot have any intuitive foundation since it asserts something about the consequences of something impossible: we have to accept B if the true judgment A is regarded as false.

On this line of thought (for details, see Kolmogorov' article referred), he proposes the axiom which he calls the principle of contradiction, explaining its meaning as “if both the truth and the falsity of a certain judgment B follow from A, the judgment A itself is false” (ibid. p. 422):

$$\underbrace{(A\rightarrow B)}_{\text{B is true}}\rightarrow(\underbrace{(A\rightarrow\neg B)}_{\text{B is false}}\rightarrow\underbrace{\neg A)}_{\text{A is false}}$$

As stated in the answer, this axiom does not allow the (strong) explosion principle, but the weaker $$A,\neg A\vdash\neg B$$ is derivable.

Later, Kolmogorov agreed to Heyting's axiom

$$\neg A\rightarrow(A\rightarrow B)$$

which Heyting proposed in 1930 as expressing ex falso sequitur quodlibet. The now standard motivation for this axiom (thus, the acceptance of the principle of explosion in the strong sense) is explained by Troelstra and van Dalen in Constructivism in Mathematics: An Introduction (vol 1, p. 10) as

Another consequence is that $$\bot\rightarrow A$$ is generally provable: since there is no proof of $$\bot,\lambda a.a$$ (or any other mapping) may count as a proof of $$\bot\rightarrow A$$, since it has to be applied to an empty domain. The principle $$\bot\rightarrow A$$ (“ex falso sequitur quodlibet”) has sometimes been rejected as non-constructive (Johannson 1937); Heyting (1956, 7.1.3) regards it as an extra stipulation fixing the meaning and use of $$\bot,\rightarrow$$.

• Was this in the first or second volume of Constructivism in Mathematics? (You linked to the second volume.) Do you happen to know the page number? Jul 8, 2023 at 23:06
• Right. The first volume, p. 10; I've corrected it. Unfortunately, its online copy at archive.org is almost illegible. Jul 8, 2023 at 23:24