1. Not finding help here? Sign up for a free 30min tutor trial with Chegg Tutors
    Dismiss Notice
Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

A proof in the Hilbert-style axiom system

  1. Oct 25, 2016 #1
    1. The problem statement, all variables and given/known data
    Provide a complete formal proof that ## \vdash ((A \rightarrow B) \rightarrow C)
    \rightarrow (B \rightarrow C)##.
    2. Relevant equations
    I am only allowed to use modus ponens and these four 'sentential logic' axioms:
    A1 ## \neg \alpha \rightarrow (\alpha \rightarrow \beta)##
    A2 ##\beta \rightarrow (\alpha \rightarrow \beta)##
    A3 ##(\alpha \rightarrow \beta) \rightarrow ((\neg \alpha \rightarrow \beta) \rightarrow \beta)##
    A4 ##(\alpha \rightarrow (\beta \rightarrow \gamma )) \rightarrow ((\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma ))##

    3. The attempt at a solution
    I have no idea where to begin. I'm thinking about using axiom 2, but I don't know how I would proceed from there. The problem would become easy if I was allowed to 'add an antecedent', but I am not allowed to directly do that. Any help is appreciated. Please note that I am a new student to logic, and I have only studied zero-order logic until now, so kindly provide hints that I will be able to understand. (The homework is due tomorrow!)
     
  2. jcsd
  3. Oct 25, 2016 #2

    stevendaryl

    User Avatar
    Staff Emeritus
    Science Advisor

    These kind of proofs are much easier if you have the deduction theorem. What the deduction theorem says is that:

    If you can prove [itex]Y[/itex] using [itex]X[/itex] as an axiom, then you can prove [itex]X \rightarrow Y[/itex]​

    You don't have the deduction theorem, but you can use it as a strategy for finding the proof, as follows:

    A proof of [itex]S[/itex] is a sequence of statements [itex]S_1, S_2, ..., S_n[/itex] such that each statement is either an axiom, or follows from two previous statements by modus ponens, and such that the last statement is [itex]S[/itex]. So:
    1. See if you can construct a proof of [itex]C[/itex] where the first statement is [itex](A \rightarrow B) \rightarrow C[/itex] and the second statement is [itex]B[/itex]. So this original proof will have [itex]C[/itex] as its last sentence.
    2. Now, modify your proof as follows: Starting with the third statement, replace each statement [itex]S[/itex] by the modified statement [itex]B \rightarrow S[/itex]. Now, see if you can add additional steps so that you prove each modified statement without using [itex]B[/itex] as an axiom. After these modifications, you will have a proof where [itex]B \rightarrow C[/itex] is the last statement.
    3. Now, modify your proof again: Starting with the new third statement, replace each statement [itex]S[/itex] by the modified statement [itex]((A \rightarrow B) \rightarrow C) \rightarrow S[/itex]. Now, see if you can add additional steps so that you can prove each modified statement without using [itex](A \rightarrow B) \rightarrow C[/itex] as an axiom. After these modifications, you will have a proof where [itex]((A \rightarrow B) \rightarrow C) \rightarrow (B \rightarrow C)[/itex] is the last statement.
    4. Now, get rid of the first two statements, since you are no longer using them. Now you have a proof of [itex]((A \rightarrow B) \rightarrow C) \rightarrow (B \rightarrow C)[/itex]
     
  4. Oct 30, 2016 #3
    Thanks, I got it!
     
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook

Have something to add?
Draft saved Draft deleted



Similar Discussions: A proof in the Hilbert-style axiom system
  1. Hilbert Hotel (Replies: 6)

Loading...