Results 1 to 11 of 11

Math Help - Proofs using Hilbert Axiomatic System

  1. #1
    Newbie chili5's Avatar
    Joined
    Mar 2009
    From
    Canada
    Posts
    17

    Proofs using Hilbert Axiomatic System

    I'm having trouble understanding how to go about coming up with these proofs. I understand that we have a list of axioms and a reference rule (Modus Ponens) to make use of and we have to use a combination of them to get down to what we are trying to prove.

    \vdash ((\neg p \rightarrow) \rightarrow p)

    I tried this:

    (\neg p \rightarrow p) \rightarrow ((\neg p \rightarrow \neg p) \rightarrow p) (by  Ax3)

    (\neg p \rightarrow p) \rightarrow (\neg p \rightarrow p) (by MP, 1)

    (\neg p \rightarrow p) \rightarrow p (by MP, 2, 1)

    But this doesn't seem right to me. It seems way too short. So what I'm confused about is how to actually go about these proofs. I'm still confused by what is meant by Modus Ponens.

    That was if A \rightarrow B and A then B. Does this just mean if I have A \rightarrow B that I can replace that with just B?
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proofs using Hilbert Axiomatic System

    I think you missed a part of the first formula. Also, can you write Axiom 3 because it is formulated in different ways? Finally, the second line of your derivation says by MP, 1, but Modus Ponens requires two premises.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie chili5's Avatar
    Joined
    Mar 2009
    From
    Canada
    Posts
    17

    Re: Proofs using Hilbert Axiomatic System

    Um no that is what I was given for the first formula. There isn't anything before the "turnstyle".

    And Axiom 3 is given as (\neg A \rightarrow B) \rightarrow ((\neg A \rightarrow \neg B) \rightarrow A))
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proofs using Hilbert Axiomatic System

    Quote Originally Posted by chili5 View Post
    \vdash ((\neg p \rightarrow) \rightarrow p)
    Implication cannot be followed by the right parenthesis.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Newbie chili5's Avatar
    Joined
    Mar 2009
    From
    Canada
    Posts
    17

    Re: Proofs using Hilbert Axiomatic System

    Oops. It is a ((\neg p) \rightarrow  p) \rightarrow p)
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proofs using Hilbert Axiomatic System

    If axiom 3 were

    (\neg A \rightarrow \neg B) \rightarrow ((\neg A \rightarrow B) \rightarrow A)),

    then we could take its instance

    (\neg p \rightarrow \neg p) \rightarrow ((\neg p \rightarrow p) \rightarrow p)),

    derive \neg p \rightarrow \neg p (see below) and derive (\neg p \rightarrow p) \rightarrow p) from the last two formulas by MP. As it is, it requires some thought.

    Here is a derivation of A -> A for any A.

    1. (A -> ((B -> A) -> A)) -> ((A -> (B -> A)) -> (A -> A)) Ax. 1
    2. A -> ((B -> A) -> A) Ax. 2
    3. (A -> (B -> A)) -> (A -> A) MP, 1, 2
    4. A -> (B -> A) Ax. 2
    5. A -> A MP, 3, 4

    As you see, Hilbert System is pretty awkward.

    Have you derived any other useful formulas, or have you proved any metatheorems, like the deduction theorem?

    That was if A \rightarrow B and A then B. Does this just mean if I have A \rightarrow B that I can replace that with just B?
    You don't replace anything; you just write new and new formulas. You are allowed to write B is you have A -> B and A already written.
    Follow Math Help Forum on Facebook and Google+

  7. #7
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proofs using Hilbert Axiomatic System

    It is easy to show ~p -> p |- p. Indeed, by axiom 3, (~p -> p) -> (~p -> ~p) -> p, so by using MP and the assumption (~p -> ~p) -> p. Next, ~p -> ~p is derivable in post #6, so p.

    Deduction theorem then claims that |- (~p -> p) -> p. To get a concrete derivation, it is possible to replay the proof of the deduction theorem in this concrete case. However, it seems that it would use formulas longer than a line and would have 11 steps even not counting the ~p -> ~p lemma. I am not sure it would help understand Hilbert system better. If you still need it, let us know.
    Follow Math Help Forum on Facebook and Google+

  8. #8
    Newbie chili5's Avatar
    Joined
    Mar 2009
    From
    Canada
    Posts
    17

    Re: Proofs using Hilbert Axiomatic System

    Don't know the deduction theorem yet. Still trying to figure out modus ponens.

    Here:


    1. (A -> ((B -> A) -> A)) -> ((A -> (B -> A)) -> (A -> A)) Ax. 1
    2. A -> ((B -> A) -> A) Ax. 2
    3. (A -> (B -> A)) -> (A -> A) MP, 1, 2

    How can you use Modens Ponus on line 3? So on line 1 you are making A = A, B = B -> A and C = A for Ax. 1. Then on line 1 you say A -> B and on line 2 you mention just A at the very beginning of line 2 which lets you use MP, yes? Then how do you just conclude B->A. I don't see how you arrive at line 3?
    Follow Math Help Forum on Facebook and Google+

  9. #9
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proofs using Hilbert Axiomatic System

    Modus Ponens lets you take two formulas: D -> E and D, where D and E are arbitrary formulas, and conclude E. Here you have

    1. (A -> ((B -> A) -> A)) -> ((A -> (B -> A)) -> (A -> A))
    2. (A -> ((B -> A) -> A))
    3. ((A -> (B -> A)) -> (A -> A)) MP 1, 2

    I.e., D = (A -> ((B -> A) -> A)) and E = ((A -> (B -> A)) -> (A -> A)).

    By the way, does your axiomatic system really make A -> ((B -> A) -> A) an instance of axiom 2? It's an instance of D -> (E -> D), which is usually called axiom 1. See, for example, this scan from another thread.
    Follow Math Help Forum on Facebook and Google+

  10. #10
    Newbie chili5's Avatar
    Joined
    Mar 2009
    From
    Canada
    Posts
    17

    Re: Proofs using Hilbert Axiomatic System

    Thank you so much! That is VERY helpful!

    Just one more thing if I write

    {\neg q} |- (p -> q) -> \neg p

    what does the {\neg q} before the turnstyle mean? Is that some kind of assumption? Like in the above proof there was nothing before the turnstyle so does that mean there are no assumptions being made?

    Then the next step is practice and to derive the deduction theorem yes?
    Follow Math Help Forum on Facebook and Google+

  11. #11
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Proofs using Hilbert Axiomatic System

    You are welcome.

    Quote Originally Posted by chili5 View Post
    {\neg q} |- (p -> q) -> \neg p

    what does the {\neg q} before the turnstyle mean? Is that some kind of assumption? Like in the above proof there was nothing before the turnstyle so does that mean there are no assumptions being made?
    Yes, formulas left of the turnstile can be used as if they were axioms, i.e., one can insert such formula in a derivation at any time.

    Quote Originally Posted by chili5 View Post
    Then the next step is practice and to derive the deduction theorem yes?
    Hilbert system is somewhat tricky. It is so minimalistic because it has only two connectives, three axioms and one inference rule, which makes it easy to prove (meta)theorems about it, like the deduction theorem or the soundness theorem. However, this also makes it pretty hard to derive some simple formulas, even p -> p. So, yes, one needs practice, but don't be surprised if you can't derive some obvious tautologies because it can indeed be tricky. Be sure to read a lot of example derivations in your textbook or lecture notes.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. System of Equation proofs
    Posted in the Algebra Forum
    Replies: 0
    Last Post: February 7th 2011, 05:28 PM
  2. Proof in axiomatic system (Prop. logic)
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: October 3rd 2010, 12:12 PM
  3. Axiomatic System Problem: Checking Models and Isomorphism
    Posted in the Advanced Math Topics Forum
    Replies: 7
    Last Post: September 8th 2010, 07:41 AM
  4. Replies: 7
    Last Post: September 6th 2010, 09:57 AM
  5. Axiomatic system...
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: September 9th 2009, 07:29 AM

/mathhelpforum @mathhelpforum