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

Question

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$.

Answer 1

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.

Addendum

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$.