Results 1 to 4 of 4

Math Help - Proof in axiomatic system (Prop. logic)

  1. #1
    Junior Member Greg98's Avatar
    Joined
    Oct 2009
    From
    Brugge, BEL
    Posts
    39

    Proof in axiomatic system (Prop. logic)

    Hello,
    the task is to prove following theorem in propositional logic's axiomatic system (http://ww2.cs.mu.oz.au/255/lec/subject-prop_axiom.pdf):
     \vdash_{ax} A \rightarrow ((A \rightarrow B) \rightarrow B)

    Some basic assumptions:

    For propositions A, B and C following are axioms:
    A \rightarrow (B \rightarrow A)
    (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))
    (\neg A \rightarrow \neg B) \rightarrow (B \rightarrow A)

    The only inference rule is Modus Ponens:
    \vdash_{ax} A
    \vdash_{ax} A \rightarrow B
    \Rightarrow \ \vdash_{ax} B

    I tried to use the axioms in many ways, but somehow I couldn't get the right combination. At first, the problem seems quite mechanical, but atleast I didn't know how to achieve the goal. Any help is appreciated. Thanks very much!
    Last edited by Greg98; October 1st 2010 at 10:56 AM.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780
    First, thank you indeed for giving the context of your problem, i.e., describing the deduction system you are using. Too many posts in this forum ask for help in deriving something but don't give the inference rules.

    Yours is called Hilbert system. Because it is simple, it is easy to prove facts about it, but it us awful for constructing actual derivations. There are other systems (Natural Deduction and Sequent Calculus) that are much easier to use in practice and that are, in fact, used in a number of theorem provers.

    So don't be surprised how awful this looks. I found the derivation using some general method; feel free to ask about it. Obviously, it is much easier to prove that A \rightarrow ((A \rightarrow B) \rightarrow B) is derivable using the Deduction Theorem twice. The easiest way to construct a complete derivation may be to carefully replay the proof of the Deduction Theorem in this particular case.

    So, let's start. I assume that -> is associated to the right, i.e., A -> B -> C is A -> (B -> C). I will refer to the first two axioms as A1 and A2.

    Lemma 1. For any formula A, |- A -> A.
    Proof.
    Consider the following instance of A2.

    [A -> (B -> A) -> A] -> [A -> (B -> A)] -> [A -> A]

    The two premises are instances of A1.
    End proof.

    Lemma 2. For any formulas A, B, if |- A, then |- B -> A.
    Proof.
    Apply A1: A -> (B -> A) to A.
    End proof.

    Lemma 3. For any formulas A, B,
    |- A -> ((A -> B) -> A) -> ((A -> B) -> B).
    Proof.
    Consider the following instance of A2.

    [(A -> B) -> (A -> B)] -> [(A -> B) -> A] -> [(A -> B) -> B)]

    The first premise can be taken away by Lemma 1. Then add a vacuous premise A by Lemma 2.
    End proof.

    Theorem. For any formulas A, B, |- A -> (A -> B) -> B.
    Proof.
    Consider the following instance of A2.

    [A -> ((A -> B) -> A) -> ((A -> B) -> B)] -> [A -> ((A -> B) -> A)] -> [A -> ((A -> B) -> B)]

    The first premise can be removed by Lemma 3, the second one is an instance of A1.
    End proof.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Junior Member Greg98's Avatar
    Joined
    Oct 2009
    From
    Brugge, BEL
    Posts
    39
    Thousand thanks for your time and helpful answer - I studied it extensively. But one thing puzzles me. You said, that derivation is easier, with using deduction theorem twice. Deduction theorem goes like this:
     \Gamma is set of propositions, and A and B are propositions.
     \Gamma \cup\ \{ A \} \vdash_{ax} B \Longleftrightarrow \Gamma \vdash_{ax} A \rightarrow B

    I tried couple a hours to mess with that, but I couldn't come with the derivation. So, can you show me, how to do that, please. It would be very useful to know, because I believe, that inventing couple of lemmas and proving them, would be beyond of my abilities, if I had to make that kind of derivations in the future. I tried alternative proofing method called semantic trees, and it seemed much handier than Hilbert's system, for those derivations. Somehow, Hilbert's system seems to be like a nightmarish game, where you know the goal, but there's thousands of different paths, and there's no hints which one is leading to the goal. Thanks, once more.
    Last edited by Greg98; October 3rd 2010 at 10:52 AM.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780
    With the Deduction theorem, this is trivial. Indeed, the sequence A, A -> B, B is a derivation where the first two formulas are assumptions and B is obtained from them by MP. That is, A, A -> B |- B. By Deduction Theorem, A |- (A -> B) -> B. Applying it a second time, we get |- A -> (A -> B) -> B.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 13
    Last Post: May 6th 2011, 09:16 AM
  2. Proof System questions (Logic)
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: October 21st 2009, 07:50 PM
  3. Prop. Logic help
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: September 20th 2009, 10:00 PM
  4. Axiomatic system...
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: September 9th 2009, 06:29 AM
  5. Prop Logic shenanigans
    Posted in the Discrete Math Forum
    Replies: 4
    Last Post: December 20th 2008, 10:02 PM

Search Tags


/mathhelpforum @mathhelpforum