Results 1 to 4 of 4
Like Tree1Thanks
  • 1 Post By ModusPonens

Math Help - Trying to prove Law of Excluded Middle in a Hilbert System

  1. #1
    Newbie
    Joined
    Nov 2012
    From
    Sydney
    Posts
    5

    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:

    H1.ϕϕ
    H2.ϕ(ψϕ)
    H3.(ϕ(ψξ))((ϕψ)(ϕξ))
    H4.(ϕψ)(ψϕ)

    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.
    Last edited by andrewkirk; November 1st 2012 at 03:02 AM. Reason: typo
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Member ModusPonens's Avatar
    Joined
    Aug 2010
    Posts
    125
    Thanks
    14

    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.
    Thanks from andrewkirk
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Nov 2012
    From
    Sydney
    Posts
    5

    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).
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Member ModusPonens's Avatar
    Joined
    Aug 2010
    Posts
    125
    Thanks
    14

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

    You're welcome, and thanks for the correction.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Hilbert System Proof. ( p /\ q ) -> (q /\ p )
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: October 7th 2012, 02:28 PM
  2. A proof involving the Law of Excluded Middle
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: October 23rd 2011, 09:31 AM
  3. Excluded middle
    Posted in the Discrete Math Forum
    Replies: 2
    Last Post: October 17th 2011, 01:18 AM
  4. [SOLVED] Proofs using Hilbert Axiomatic System
    Posted in the Discrete Math Forum
    Replies: 10
    Last Post: October 15th 2011, 11:37 AM
  5. Replies: 2
    Last Post: March 23rd 2010, 06:29 AM

Search Tags


/mathhelpforum @mathhelpforum