Thread: 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.

Which exactly step in the conversion algorithm or in the example described in your link to Wikipedia is not clear to you?

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?

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.

Originally Posted by ToaTerra

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.

Much more clear - thank you. I do have a follow up question.

Originally Posted by emakarov

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)?

(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}.)

Originally Posted by emakarov

(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.

Originally Posted by emakarov

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.

Originally Posted by emakarov

What does this have to do with (A)?

Nothing. It has to do with (B).

Originally Posted by emakarov

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?

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.

Originally Posted by emakarov

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.

Originally Posted by emakarov

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?

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.

Originally Posted by emakarov

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.

Originally Posted by emakarov

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".

Originally Posted by emakarov

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.

Originally Posted by emakarov

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").

Originally Posted by emakarov

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?

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.

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.

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