A simple example

[Amir]

Here a simple proof in Hilbert system by using the Axioms in the
textbook. I believe Prof. Buss has done this in his lectures.

Cheers,
Amir.
-----------------------

Suppose, we want to prove "|- (~A -> ~B) -> (B -> A)". By Applying the
Deduction Theorem twice, we get that proving "B, ~A -> ~B |- A" is
equivalent to showing that "|- (~A -> ~B) -> (B -> A)" holds. Now, we
start proving "B, ~A -> ~B |- A" where "B" and "~A -> ~B" are the
assumptions:

1) B Assumption,

2) ~A -> ~B Assumption,

3) B -> (~A -> B) Axiom 1,

4) ~A -> B MP(1,3),

5) (~A -> ~B) -> ((~A -> B) -> A) Axiom 3,

6) (~A -> B) -> A MP(2,5),

7) A MP(4,6).

Therefore, we proved that "B, ~A -> ~B |- A" holds, and as a result of
the Deduction Theorem, "|- (~A -> ~B) -> (B -> A)" holds as well.

A NOTE ON AXIOM 3:

The intuition behind axiom 3 is that if a formula ("~A") implies another
formula ("~B") and its negation ("B"), then the negation of the original
formula holds ("A"). This is basically proof by contradiction.

"|- (~A -> ~B) -> ((~A -> B) -> A)"

Hope this is helpful.

[Henry S]

Post by Amir
Here a simple proof in Hilbert system by using the Axioms in the
textbook. I believe Prof. Buss has done this in his lectures.
Cheers,
Amir.
-----------------------
Suppose, we want to prove "|- (~A -> ~B) -> (B -> A)". By Applying the
Deduction Theorem twice, we get that proving "B, ~A -> ~B |- A" is
equivalent to showing that "|- (~A -> ~B) -> (B -> A)" holds. Now, we
start proving "B, ~A -> ~B |- A" where "B" and "~A -> ~B" are the
1) B Assumption,
2) ~A -> ~B Assumption,
3) B -> (~A -> B) Axiom 1,
4) ~A -> B MP(1,3),
5) (~A -> ~B) -> ((~A -> B) -> A) Axiom 3,
6) (~A -> B) -> A MP(2,5),
7) A MP(4,6).
Therefore, we proved that "B, ~A -> ~B |- A" holds, and as a result of
the Deduction Theorem, "|- (~A -> ~B) -> (B -> A)" holds as well.
The intuition behind axiom 3 is that if a formula ("~A") implies another
formula ("~B") and its negation ("B"), then the negation of the original
formula holds ("A"). This is basically proof by contradiction.
"|- (~A -> ~B) -> ((~A -> B) -> A)"
Hope this is helpful.

Thanks for your example.

I noticed that in the above proof, you used the deduction theorem that
A,B |- C is equivalent to A |- B -> C

Can we use this type of deduction theorem for Question 2 (full formal
proof)?

I'm hearing different responses from the professors and the TA's.

Thanks,
Henry

[Amir]

Well... The head TA (Omer) told us in the TA meeting that you can use
deduction theorem for question 2.

Post by Henry S

Post by Amir
Here a simple proof in Hilbert system by using the Axioms in the
textbook. I believe Prof. Buss has done this in his lectures.
Cheers,
Amir.
-----------------------
Suppose, we want to prove "|- (~A -> ~B) -> (B -> A)". By Applying the
Deduction Theorem twice, we get that proving "B, ~A -> ~B |- A" is
equivalent to showing that "|- (~A -> ~B) -> (B -> A)" holds. Now, we
start proving "B, ~A -> ~B |- A" where "B" and "~A -> ~B" are the
1) B Assumption,
2) ~A -> ~B Assumption,
3) B -> (~A -> B) Axiom 1,
4) ~A -> B MP(1,3),
5) (~A -> ~B) -> ((~A -> B) -> A) Axiom 3,
6) (~A -> B) -> A MP(2,5),
7) A MP(4,6).
Therefore, we proved that "B, ~A -> ~B |- A" holds, and as a result of
the Deduction Theorem, "|- (~A -> ~B) -> (B -> A)" holds as well.
The intuition behind axiom 3 is that if a formula ("~A") implies another
formula ("~B") and its negation ("B"), then the negation of the original
formula holds ("A"). This is basically proof by contradiction.
"|- (~A -> ~B) -> ((~A -> B) -> A)"
Hope this is helpful.

Thanks for your example.
I noticed that in the above proof, you used the deduction theorem that
A,B |- C is equivalent to A |- B -> C
Can we use this type of deduction theorem for Question 2 (full formal
proof)?
I'm hearing different responses from the professors and the TA's.
Thanks,
Henry

[Amir]

The head TA (Omer) told us in the TA meeting that you can use deduction
theorem for question 2.

Post by Henry S

Post by Amir
Here a simple proof in Hilbert system by using the Axioms in the
textbook. I believe Prof. Buss has done this in his lectures.
Cheers,
Amir.
-----------------------
Suppose, we want to prove "|- (~A -> ~B) -> (B -> A)". By Applying the
Deduction Theorem twice, we get that proving "B, ~A -> ~B |- A" is
equivalent to showing that "|- (~A -> ~B) -> (B -> A)" holds. Now, we
start proving "B, ~A -> ~B |- A" where "B" and "~A -> ~B" are the
1) B Assumption,
2) ~A -> ~B Assumption,
3) B -> (~A -> B) Axiom 1,
4) ~A -> B MP(1,3),
5) (~A -> ~B) -> ((~A -> B) -> A) Axiom 3,
6) (~A -> B) -> A MP(2,5),
7) A MP(4,6).
Therefore, we proved that "B, ~A -> ~B |- A" holds, and as a result of
the Deduction Theorem, "|- (~A -> ~B) -> (B -> A)" holds as well.
The intuition behind axiom 3 is that if a formula ("~A") implies another
formula ("~B") and its negation ("B"), then the negation of the original
formula holds ("A"). This is basically proof by contradiction.
"|- (~A -> ~B) -> ((~A -> B) -> A)"
Hope this is helpful.

Thanks for your example.
I noticed that in the above proof, you used the deduction theorem that
A,B |- C is equivalent to A |- B -> C
Can we use this type of deduction theorem for Question 2 (full formal
proof)?
I'm hearing different responses from the professors and the TA's.
Thanks,
Henry

[Roman]

Post by Amir
The head TA (Omer) told us in the TA meeting that you can use deduction
theorem for question 2.

Post by Henry S

Post by Amir
Here a simple proof in Hilbert system by using the Axioms in the
textbook. I believe Prof. Buss has done this in his lectures.
Cheers,
Amir.
-----------------------
Suppose, we want to prove "|- (~A -> ~B) -> (B -> A)". By Applying the
Deduction Theorem twice, we get that proving "B, ~A -> ~B |- A" is
equivalent to showing that "|- (~A -> ~B) -> (B -> A)" holds. Now, we
start proving "B, ~A -> ~B |- A" where "B" and "~A -> ~B" are the
1) B Assumption,
2) ~A -> ~B Assumption,
3) B -> (~A -> B) Axiom 1,
4) ~A -> B MP(1,3),
5) (~A -> ~B) -> ((~A -> B) -> A) Axiom 3,
6) (~A -> B) -> A MP(2,5),
7) A MP(4,6).
Therefore, we proved that "B, ~A -> ~B |- A" holds, and as a result of
the Deduction Theorem, "|- (~A -> ~B) -> (B -> A)" holds as well.
The intuition behind axiom 3 is that if a formula ("~A") implies another
formula ("~B") and its negation ("B"), then the negation of the original
formula holds ("A"). This is basically proof by contradiction.
"|- (~A -> ~B) -> ((~A -> B) -> A)"
Hope this is helpful.

Thanks for your example.
I noticed that in the above proof, you used the deduction theorem that
A,B |- C is equivalent to A |- B -> C
Can we use this type of deduction theorem for Question 2 (full formal
proof)?
I'm hearing different responses from the professors and the TA's.
Thanks,
Henry

Thanks for this answer and for the example.

[hamir]

Hey guys,

Based on the note that Prof Buss just provided (see next thread), we may
not "use" the deduction theorem in our proof.

Hashim