Results 1 to 14 of 14

Math Help - Procedure for deductive theorem proof done in axiomatic logic

  1. #1
    Newbie
    Joined
    Apr 2011
    Posts
    7

    Procedure for deductive theorem proof done in axiomatic logic

    In the wikipedia article Deduction theorem - Wikipedia, the free encyclopedia under the section titled "Conversion from proof using the deduction meta-theorem to axiomatic proof", it explains there is a procedure for converting a Deduction Theorem proof to a proof in axiomatic logic. I tried to follow the description but was unable to generate the axiomatic proof. I am looking for someone who can help me understand this procedure.

    Given some conditional A -> B, which can be proven by A |- B => |- A -> B (via Deduction Theorem), what is the procedure/process for generating an equivalent proof of A -> B in only axiomatic logic (without the Deduction Theorem).

    Thanks.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780
    Which exactly step in the conversion algorithm or in the example described in your link to Wikipedia is not clear to you?
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Apr 2011
    Posts
    7
    The first step is:
    1. Suppose that we have that Γ and H prove C, and we wish to show that Γ proves H→C.

    To simply things, lets define T as the first-order theory (or propositional logic) and A and can show T+A |- B. I want to show T |- A -> B.

    2. For each step S in the deduction which is a premise in Γ (a reiteration step) or an axiom, we can apply modus ponens to the axiom 1, S→(H→S), to get H→S.

    This step seems informative. Since A is not a theorem of T it doesn't seem to apply. But suppose there was some formula S such that T |- S, then we would have S -> ((A -> B) -> S) => ((A -> B) -> S)

    3. If the step is H itself (a hypothesis step), we apply the theorem schema to get H→H.

    Okay, now I'm lost already. "If the step is H itself..." How did we get here?

    There rest of the items appear to be guidelines for what to do at each step, but I don't see the general algorithm for what to do.

    I also understand the preceding proof to show P -> P, but how does that help show T |- A -> B?
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780
    Let's remind the definition of a derivable formula in Hilbert calculus. A formula A is derivable from T if

    (1) A is an axiom or
    (2) A is an element of T or
    (3) B -> A and B are derivable from T for some formula B.

    The proof of the Deduction theorem proceeds by induction on this definition.

    Quote Originally Posted by ToaTerra View Post
    To simply things, lets define T as the first-order theory (or propositional logic) and A and can show T+A |- B. I want to show T |- A -> B.

    2. For each step S in the deduction which is a premise in Γ (a reiteration step) or an axiom, we can apply modus ponens to the axiom 1, S→(H→S), to get H→S.

    This step seems informative. Since A is not a theorem of T it doesn't seem to apply. But suppose there was some formula S such that T |- S, then we would have S -> ((A -> B) -> S) => ((A -> B) -> S)
    I am not sure I understand. First, yes, typically A is not a theorem of T: otherwise, there is no sense in adding it to T. However, whether T |- A is irrelevant and is not used anywhere.

    Second, "suppose there was some formula S such that T |- S." Of course there is such a formula: take S to be any axiom. What is the purpose of deriving ((A -> B) -> S)? I thought the goal is to derive A -> B.

    Here is how the proof goes. Suppose T, A |- B by (1) or (2) above (in the case of (2), at this point we consider only the case where B is in T, not when B is the same as A). Then T |- B -> (A -> B) by (1) and T |- B by (1) or (2). Therefore, A -> B is derivable by (3), as required.

    3. If the step is H itself (a hypothesis step), we apply the theorem schema to get H→H.

    Okay, now I'm lost already. "If the step is H itself..." How did we get here?
    Here we consider the case where B is the same as A and T, A |- B, i.e., T, A |- A, by (2). Then we need to derive T |- A -> A, and the Wiki page shows how to do this.

    Finally, suppose B is obtained by Modus Ponens from C -> B and C for some formula C, both of which are derivable from T and A (rule (3) above), i.e.,

    T, A |- C -> B

    and

    T, A |- C.

    By induction hypothesis, T |- A -> (C -> B) and T |- A -> C. We take the axiom

    (A -> (C -> B)) -> ((A -> C) -> (A -> B))

    and apply Modus Ponens twice to get T |- A -> B.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Newbie
    Joined
    Apr 2011
    Posts
    7
    Much more clear - thank you. I do have a follow up question.

    Quote Originally Posted by emakarov View Post
    Here is how the proof goes. Suppose T, A |- B by (1) or (2) above (in the case of (2), at this point we consider only the case where B is in T, not when B is the same as A). Then T |- B -> (A -> B) by (1) and T |- B by (1) or (2). Therefore, A -> B is derivable by (3), as required.
    1. Can you dwelve a little deeper about how you got this Modus Ponens to work for all cases? We have:

    (A) ~(B=A) and B in T
    (B) ~(B=A) and B not in T
    (C) B=A regardless of whether B in or not in T.

    You have presented cases (A) and (C). What about (B)? Given the conditional T |- (A -> B), which is equivalent to T |- ~A or B, all of the following could be valid: T |- A and B (which makes it case (A)); T |- ~A and B (which makes it case (A)); or T |- ~A and ~B. So for the case T |- ~A and ~B how do we complete the conditional T |- B -> (A -> B)?
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780
    (A) ~(B=A) and B in T
    (B) ~(B=A) and B not in T
    (C) B=A regardless of whether B in or not in T.

    You have presented cases (A) and (C). What about (B)?
    (B) splits into (B1): B is an axiom and (B2): B is obtained by MP from two derivable formulas. I explained both subcases. In particular, (B1) is treated in the same way as (A).

    I don't understand the rest of your question.

    Given the conditional T |- (A -> B)
    Why is it given?

    which is equivalent to T |- ~A or B, all of the following could be valid: T |- A and B (which makes it case (A))
    What does this have to do with (A)? Also, T |- ~A \/ B is not equivalent to (T |- ~A) or (T |- B). (Consider T = {~A \/ B}.)
    Follow Math Help Forum on Facebook and Google+

  7. #7
    Newbie
    Joined
    Apr 2011
    Posts
    7
    Quote Originally Posted by emakarov View Post
    (B) splits into (B1): B is an axiom and (B2): B is obtained by MP from two derivable formulas. I explained both subcases. In particular, (B1) is treated in the same way as (A).
    No, (B) does not split into (B1) and (B2). (B) is the case where B is not derivable in T. What you call (B1) is, as you observed, already covered in (A). And what you call (B2) is already covered in later in your post.

    Quote Originally Posted by emakarov View Post
    I don't understand the rest of your question.
    I was asking about the case where ~( T |- B); ie, where B cannot be derived in T.

    Quote Originally Posted by emakarov View Post
    What does this have to do with (A)?
    Nothing. It has to do with (B).

    Quote Originally Posted by emakarov View Post
    Also, T |- ~A \/ B is not equivalent to (T |- ~A) or (T |- B). (Consider T = {~A \/ B}.)
    I apologize for not being clear. What I was trying to say is: Suppose T |- ~A & ~B, then T|- ~A, then T |- ~A v B, then T |- A -> B. In this case, you cannot use the schema B -> (A -> B) because B cannot be derived. This was the case I didn't see you address. How is this case derived using the axioms schema specified in the wikipedia article?
    Follow Math Help Forum on Facebook and Google+

  8. #8
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780
    No, (B) does not split into (B1) and (B2). (B) is the case where B is not derivable in T.
    I disagree. T is a set of formulas (in this theorem, it is usually not considered to be deductively closed, i.e., not something like a deductive theory), and "B is in T" means that B is an element of T. Thus, the case (B), i.e., "~(B=A) and B not in T," implies that B is not an element of T, not that B is not derivable from T. The proof proceeds by cases on whether B is an element of T, not on whether it is derivable from T.

    The case (B) does split into

    (B1): B is an axiom

    and

    (B2): B is obtained by MP from two derivable formulas.

    Indeed, if B is not an element of T and is not A and yet it is derivable, it must be derived by rule (1) or (3) above. Therefore, either B is an axiom or it is derived by MP.

    What you call (B1) is, as you observed, already covered in (A).
    No. The case (B1) says "B is an axiom" (one of the 10 or however many standard axiom of classical logic), while (A) says that B is an element of T, which are user-specific assumptions, so to speak, and which don't have to include any axioms.

    Suppose T |- ~A & ~B, then T|- ~A, then T |- ~A v B, then T |- A -> B. In this case, you cannot use the schema B -> (A -> B) because B cannot be derived. This was the case I didn't see you address. How is this case derived using the axioms schema specified in the wikipedia article?
    This is irrelevant to the proof. There are just four cases:

    (A) B is in T
    (B1) B is an axiom
    (B2) B is obtained by MP from two derivable formulas
    (C) B is A.

    The proof shows how to derive T |- A -> B in each of them. Whether T |- ~A /\ ~B does not matter. However, as you pointed out, T |- ~A already implies T |- A -> B.
    Follow Math Help Forum on Facebook and Google+

  9. #9
    Newbie
    Joined
    Apr 2011
    Posts
    7
    Quote Originally Posted by emakarov View Post
    Indeed, if B is not an element of T and is not A and yet it is derivable,...
    I am not saying B is not an element of T and is not A and yet is derivable. I am saying B is not an element of T and is not A and is not derivable.

    Quote Originally Posted by emakarov View Post
    The proof proceeds by cases on whether B is an element of T, not on whether it is derivable from T.
    A proof by cases must cover all cases:

    Case 1: B is a theorem of T and B = A (Covered by P -> P).
    Case 2: B is a theorem of T and B != A (Covered by P -> (Q -> P)).
    Case 3: B is not a theorem of T and B = A (Covered by P -> P).
    Case 4: B is not a theorem of T and B != A (Not Covered as neither P -> P nor P -> (Q -> P) apply; or if covered by ?? I don't recognize it as covered).

    [QUOTE=emakarov;646696]
    This is irrelevant to the proof. There are just four cases:

    (A) B is in T
    (B1) B is an axiom
    (B2) B is obtained by MP from two derivable formulas
    (C) B is A.
    QUOTE]

    Let me restate them as:

    (A) B is a theorem of T.
    (B1) B is an axiom of T.
    (B2) B is obtained by MP from two theorems of T (not T+A)
    (C) B = A and B is a theorem of T.

    I see a fourth case:

    (D) B != A and B is not a theorem of T.

    Is there an example of Case-4/(D)? Or is there an explanation of why Case-4/(D) is not valid?
    Follow Math Help Forum on Facebook and Google+

  10. #10
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780
    Let me restate them as:

    (A) B is a theorem of T.
    (B1) B is an axiom of T.
    (B2) B is obtained by MP from two theorems of T (not T+A)
    (C) B = A and B is a theorem of T.
    This is not the same thing. Let's agree on whether you are asking questions about the proof from Wikipedia or if you are offering another proof. The proof from Wikipedia never proceeds by cases on whether something is derivable. The only choices are about membership, as I wrote above. Also, "B is an axiom of T" does not make sense because only logics have axioms; T is not a logic but a set of formulas. Finally, (B2) is precisely about two theorems of T + A, not just T. The idea is that B is derived from T + A, and so two formulas from which B is obtained by MP also may use T as well as A.

    I see a fourth case:

    (D) B != A and B is not a theorem of T.
    This case is possible, but it is irrelevant to the proof.
    Follow Math Help Forum on Facebook and Google+

  11. #11
    Newbie
    Joined
    Apr 2011
    Posts
    7
    Quote Originally Posted by emakarov View Post
    This is not the same thing. ... The proof from Wikipedia never proceeds by cases on whether something is derivable. The only choices are about membership, as I wrote above.
    The restatement is about membership and not derivability. I did not state:

    (A) B is a conclusion of a proof on T....

    I'm not sure what you are objecting too. The phrase "x is a theorem of y" means x is a wff and a member of the set y.

    Quote Originally Posted by emakarov View Post
    Also, "B is an axiom of T" does not make sense because only logics have axioms; T is not a logic but a set of formulas.
    Again, I'm not sure what you are objecting too. The phrase "x is an axiom of y" means x is a wff and is a member of the set y and x does not have to be the conclusion of some proof. Are you confusing "axiom" with the "logical axiom" of a logic? To me, "axiom" is a synonym for "non-logical axiom".

    Quote Originally Posted by emakarov View Post
    Let's agree on whether you are asking questions about the proof from Wikipedia or if you are offering another proof.
    Yes, I was asking about the fourth paragraph in wikipedia.

    Quote Originally Posted by emakarov View Post
    Finally, (B2) is precisely about two theorems of T + A, not just T. The idea is that B is derived from T + A, and so two formulas from which B is obtained by MP also may use T as well as A.
    Ah, the section I referenced deals only in T and not T+A. If we have T+A, we can just use the Deduction Theorem. The point of the section was the consequence of the Deduction Theorem can be done entirely in T. Perhaps this is where we are mis-communicating. Are you thinking the section allows T+A? We don't; we only have T and A proves B available to us ("Suppose that we have that Γ and H prove C").

    Quote Originally Posted by emakarov View Post
    This case is possible, but it is irrelevant to the proof.
    This is the point I'm not following/understanding yet. Why is it irrelevant to showing an equivalent proof to the Deduction Theorem in T?
    Follow Math Help Forum on Facebook and Google+

  12. #12
    Newbie
    Joined
    Apr 2011
    Posts
    7
    Ah, re-reading my post, I see the phrase "Γ and H prove C" is English for T & H |- C. So that particular section doesn't really show a conversion from the Deductive Theorem to an axiomatic proof. Instead it simply shows the proof of C -> (H -> C) in T+H.

    Thanks for your help and sorry it took so long to understand what you were saying.

    Regards.
    Follow Math Help Forum on Facebook and Google+

  13. #13
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780
    The phrase "x is a theorem of y" means x is a wff and a member of the set y.
    No, "x is a theorem of y" means that there exists a derivation from assumptions in y that ends with x. As I stated above, the Deduction theorem does not assume that y is a deductive theory, i.e., contains all its corollaries. Here y is just an arbitrary set of formulas.

    The phrase "x is an axiom of y" means x is a wff and is a member of the set y and x does not have to be the conclusion of some proof. Are you confusing "axiom" with the "logical axiom" of a logic? To me, "axiom" is a synonym for "non-logical axiom".
    Yes, I used "axiom" to mean "logical axiom." I think Mendelson's book makes a distinction between logical and non-logical axioms. I prefer to refer to non-logical axioms as assumptions or hypotheses. The difference between axioms and assumptions is somewhat subjective: there are axioms in standard theories like partial order, but one uses the word "assumptions" for formulas that are temporarily used as axioms but will be eventually closed (e.g., using Deduction theorem). In any case, the phrase "x is an axiom of y" is not often used when y is just a set of formulas.

    Are you thinking the section allows T+A? We don't; we only have T and A proves B available to us
    It is becoming difficult to see which section you are referring to. I don't see the distinction between T and A proving B and T + A proving B (formally, it should be "T union {A}" instead of T + A). The proof of the Deduction theorem starts with the assumption that T and A proves B, so all formulas in the derivation of B are derived from T and A. The goal is to eliminate A from the assumptions.

    Ah, re-reading my post, I see the phrase "Γ and H prove C" is English for T & H |- C. So that particular section doesn't really show a conversion from the Deductive Theorem to an axiomatic proof. Instead it simply shows the proof of C -> (H -> C) in T+H.
    Again, I am not sure what sections you mean, but I am glad it is clearer now. I hope you can agree now that when B is derived from T and A, there are four cases described in post #8.
    Follow Math Help Forum on Facebook and Google+

  14. #14
    Senior Member
    Joined
    Feb 2010
    Posts
    466
    Thanks
    4
    There should not be terminological confusion in this matter.

    Let A, B, C, P, Q, and R be any formulas.
    Let G and T be any sets of formulas.
    Let the logical axioms at least include all formulas:

    P -> (Q -> P)
    and
    (P -> (Q -> R)) -> ((P -> Q) -> (P -> R))

    "There is a derivation of B from G."
    means:
    There is a finite sequence of formulas ending with the formula B and such that every line of the sequence is either (1) a logical axiom, or (2) a member of G, or (3) derived from previous lines by modus ponens.

    G |- B
    stands for
    "There is a derivation of B from G."

    |- B
    stands for
    "There is a derivation of B from the empty set." I.e., there is derivation of B such that that every line of the derivation is either a logical axiom or is derived from previous lines by modus ponens.

    And, as already agreed, we can show:

    |- B -> B

    We claim: If Tu{A} |- B then T |- A -> B.
    We show this by strong induction on the length of any given derivation of B from Tu{A}:

    Case 1: B in T. So T |- B. And B -> (A -> B). So T |- A -> B.

    Case 2: B is A. So A -> B.

    Case 3: B is a logical axiom. So |- B. And B -> (A -> B). So |- A -> B. So, perforce, T |- A -> B.

    Case 4. B was derived, from previous lines, C and C ->B, by modus ponens.
    By the induction hypothesis, T |- A -> C and T |- A -> (C -> B).
    And (A -> (C -> B)) -> ((A -> C) -> (A -> B)) is an axiom.
    So T |- (A -> C) -> (A -> B).
    So T | - A -> B.

    /

    Given a proof, using the deduction theorem and Tu{A} |- B, of T |- A -> B, convert to a derivation showing T |- A -> B with this routine:

    (1) Is B in T?

    If yes, then write the derivation:
    1. B
    2. B -> (A -> B)
    3. A -> B

    If no, then (2) Is B the formula A?

    If yes, then write the derivation of B -> B using only the logical axioms.

    If no, then (3) Is B a logical axiom?

    If yes, then write the derivation:
    1. B
    2. B -> (A -> B)
    3. (A -> B)

    (4) If no, then for some C, we have that B was derived, from C and C -> B, by modus ponens.
    Recursively call this (1)-(4) routine itself, mutatis mutandis, and looping back and concatenating derivations as required, to get an n+1 length derivation with line n being A -> C and line n+1 being A -> (C -> B). Then write the derivation that ends:
    n. A -> C
    n+1. A -> (C -> B)
    n+2. (A -> (C -> B)) -> ((A -> C) -> (A -> B))
    n+3. ((A -> C) -> (A -> B))
    n+4. A -> B
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Proving a Theorem (Predicate Logic)
    Posted in the Discrete Math Forum
    Replies: 2
    Last Post: October 13th 2011, 03:57 AM
  2. Proof in axiomatic system (Prop. logic)
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: October 3rd 2010, 11:12 AM
  3. logic proof
    Posted in the Discrete Math Forum
    Replies: 4
    Last Post: February 12th 2010, 08:23 AM
  4. Replies: 5
    Last Post: December 13th 2009, 10:47 AM
  5. Oh man deductive proof...Please help?!
    Posted in the Geometry Forum
    Replies: 1
    Last Post: July 3rd 2007, 11:02 PM

Search Tags


/mathhelpforum @mathhelpforum