Trying to prove Law of Excluded Middle in a Hilbert System

I am trying to prove (¬¬*ϕ)*→*ϕ *using only the Hilbert axioms, of which only the first four are relevant:

*H*1.*ϕ*→*ϕ*

*H*2.*ϕ*→(*ψ*→*ϕ*)

*H*3.(*ϕ*→(*ψ*→*ξ*))→((*ϕ*→*ψ*)→(*ϕ*→*ξ*))

*H*4.(¬*ϕ*→¬*ψ*)→(*ψ*→*ϕ*)

It seems like the proof should be straightforward, but I can't seem to even get started.

Clearly it has to use H4, as that's the only axiom involving the negation symbol.

Other than the above four axioms, I have the following available, which I have already proven:

- the Deduction Theorem: T⋃{
*ϕ*}⊢*ψ *iff T⊢(*ϕ*→*ψ*) - {a→b, b→c} ⊢ a→c (Transitivity of Implication)

Conjunction and dysjunction have been defined by

a∧b ≡¬(a→¬b)

a∨b≡(¬a)→b

and b→a∨b follows from the above by H2; But my proofs of the other main results for ∧ and∨: (a∧b →a; a∧b →b; a∧b≡b∧a; a→a∨b; a∨b≡b∨a) use versions of the Double Negation result we are trying to prove, so we can't use them

I haven't yet proved either form of proof by negation:

(a→(b∧¬b))→¬a; and (¬a→(b∧¬b))→a

I have a feeling that one or both of those is equivalent to what I want to prove.

I am hoping that it can be proved without needing to assume consistency. I guess it may be possible to prove a contradiction from assuming ¬( (¬¬*ϕ)*→*ϕ*), in which case an assumption of consistency allows us to conclude that ( (¬¬*ϕ)*→*ϕ*). But I've got the impression that it should be able to be proved without having to assume consistency. That's because Wikipedia's presentation of the axioms says that to restrict ourselves to intuitionistic logic we either omit H4, or use a weaker version of it. That suggests to me that H4 should be sufficient to prove things that an intuitionist approach cannot (such as what I'm trying to prove here), without having to make additional assumptions such as consistency.

Thank you for any suggestions anybody can offer.

Re: Trying to prove Law of Excluded Middle in a Hilbert System

1 ~~A->A Hyp

2 ~~A->(~~~~A->~~A) H2

3 ~~~~A->~~A MP1,2

4 (~~~~A->~~A)->(~A->~~~A) H4

5 ~A->~~~A MP3,4

6 (~A->~~~A)->(~~A->A) H4

7 ~~A->A MP5,6

8 A MP1,7

Apply the metatheorem of deduction and voila.

Re: Trying to prove Law of Excluded Middle in a Hilbert System

Thank you very much Modus Ponens.

It is a very nice proof. That's the first time I've ever seen somebody apply four negations to the same proposition!

By the way, I think you intended your first line to read ~~A, rather than (~~A->A).

Re: Trying to prove Law of Excluded Middle in a Hilbert System

You're welcome, and thanks for the correction.