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


Some basic assumptions:

For propositions A, B and C following are axioms:




The only inference rule is Modus Ponens:




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!

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

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:
is set of propositions, and A and B are propositions.


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.

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.