Results 1 to 5 of 5

Math Help - Deduction theorem

  1. #1
    Junior Member
    Joined
    Jul 2010
    Posts
    28

    Deduction theorem

    Hi all,

    I'm struggling to see how to derive the deduction theorem from some particular axioms. Basically I've got:
    (1) A -> (B -> A)
    (2) A -> (B -> C) ->((A -> B) -> (A -> C))
    (3) (~A -> ~B) -> (B -> A)
    (4) (x)A -> A(t) where t is free for x.

    Rules of inference are:
    (1*) MP
    (2*) From A -> B, infer A -> (x)B so long as x does not occur free in A or any premise.

    Supposing we are proving the theorem for A, at the inductive step I get stuck showing that if C is derived from D by means of (2*) and we have A -> D, then we have A ->C.

    Any help would be really great.

    Regards
    Sam
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Junior Member
    Joined
    Jul 2010
    Posts
    28
    Just to say: I'd also be really interested to hear if people who think they should be able to prove the deduction theorem from these premises can't. I'm suspicious that they can, but I'd like to know either way!

    Sam
    Follow Math Help Forum on Facebook and Google+

  3. #3
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769
    Suppose that the derivation with an assumption A ends with the application of (2*); say, we infer B -> (x)C from B -> C. By IH, there exists a derivation of A -> (B -> C). Now, it is equivalent to A /\ B -> C, i.e., ~(A -> ~B) -> C. In more detail, the formulas

    (A -> (B -> C)) -> (~(A -> ~B) -> C) (*)

    and

    (~(A -> ~B) -> C) -> (A -> (B -> C)) (**)

    are derivable in propositional logic. Therefore, from (A -> (B -> C)) and (*) we can derive ~(A -> ~B) -> C by MP. Since (2*) was applied legally in the old derivation, x does not occur freely in A or B, so we can get ~(A -> ~B) -> (x)C. From here and (**), A -> (B -> (x)C) is obtained by MP.

    Of course, (*) and (**) have to be derived first. For example, completeness theorem for propositional logic can be proved before considering predicate logic.

    This method may not be optimal because one has to use the axiom (3) to derive (*) and (**), whereas, say, in Natural Deduction, the analog of (3) is not necessary.

    Do you have a proof of this fact from a textbook or a lecture? If you don't understand a particular step, we can discuss it.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Junior Member
    Joined
    Jul 2010
    Posts
    28
    Thanks ever so much for that.

    I was totally blocked on this, and couldn't see the woods for the trees.

    Thanks again.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Senior Member
    Joined
    Feb 2010
    Posts
    466
    Thanks
    4
    Too bad it's not the system exactly as the one in the original post except (2*) is replaced by axiom schema (5): B -> (x)B, where x does not occur free in B.

    Then you'd be done just by proving the four cases you've already proven: (1) the conclusion is an axiom, (2) the conclusion is a premise, (3) the conclusion is of the form P -> P, (4) the conclusion follows by modus ponens.
    Last edited by MoeBlee; October 11th 2010 at 11:35 AM.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Natural Deduction
    Posted in the Discrete Math Forum
    Replies: 9
    Last Post: June 9th 2011, 03:15 AM
  2. Deduction Theorem Help
    Posted in the Discrete Math Forum
    Replies: 6
    Last Post: August 17th 2010, 11:49 AM
  3. Deduction with Stoke's Theorem
    Posted in the Calculus Forum
    Replies: 7
    Last Post: May 16th 2010, 03:18 AM
  4. natural deduction
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: April 24th 2010, 11:47 AM
  5. Demonstration and deduction
    Posted in the Algebra Forum
    Replies: 4
    Last Post: June 22nd 2009, 10:56 AM

Search Tags


/mathhelpforum @mathhelpforum