Thread: Proofs using Hilbert Axiomatic System

I'm having trouble understanding how to go about coming up with these proofs. I understand that we have a list of axioms and a reference rule (Modus Ponens) to make use of and we have to use a combination of them to get down to what we are trying to prove.



I tried this:







But this doesn't seem right to me. It seems way too short. So what I'm confused about is how to actually go about these proofs. I'm still confused by what is meant by Modus Ponens.

That was if and A then B. Does this just mean if I have that I can replace that with just B?

I think you missed a part of the first formula. Also, can you write Axiom 3 because it is formulated in different ways? Finally, the second line of your derivation says by MP, 1, but Modus Ponens requires two premises.

Um no that is what I was given for the first formula. There isn't anything before the "turnstyle".

And Axiom 3 is given as

Originally Posted by chili5

Implication cannot be followed by the right parenthesis.

Oops. It is a

If axiom 3 were

,

then we could take its instance

,

derive (see below) and derive from the last two formulas by MP. As it is, it requires some thought.

Here is a derivation of A -> A for any A.

1. (A -> ((B -> A) -> A)) -> ((A -> (B -> A)) -> (A -> A)) Ax. 1
2. A -> ((B -> A) -> A) Ax. 2
3. (A -> (B -> A)) -> (A -> A) MP, 1, 2
4. A -> (B -> A) Ax. 2
5. A -> A MP, 3, 4

As you see, Hilbert System is pretty awkward.

Have you derived any other useful formulas, or have you proved any metatheorems, like the deduction theorem?

That was if and A then B. Does this just mean if I have that I can replace that with just B?

You don't replace anything; you just write new and new formulas. You are allowed to write B is you have A -> B and A already written.

It is easy to show ~p -> p |- p. Indeed, by axiom 3, (~p -> p) -> (~p -> ~p) -> p, so by using MP and the assumption (~p -> ~p) -> p. Next, ~p -> ~p is derivable in post #6, so p.

Deduction theorem then claims that |- (~p -> p) -> p. To get a concrete derivation, it is possible to replay the proof of the deduction theorem in this concrete case. However, it seems that it would use formulas longer than a line and would have 11 steps even not counting the ~p -> ~p lemma. I am not sure it would help understand Hilbert system better. If you still need it, let us know.

Don't know the deduction theorem yet. Still trying to figure out modus ponens.

Here:


1. (A -> ((B -> A) -> A)) -> ((A -> (B -> A)) -> (A -> A)) Ax. 1
2. A -> ((B -> A) -> A) Ax. 2
3. (A -> (B -> A)) -> (A -> A) MP, 1, 2

How can you use Modens Ponus on line 3? So on line 1 you are making A = A, B = B -> A and C = A for Ax. 1. Then on line 1 you say A -> B and on line 2 you mention just A at the very beginning of line 2 which lets you use MP, yes? Then how do you just conclude B->A. I don't see how you arrive at line 3?

Modus Ponens lets you take two formulas: D -> E and D, where D and E are arbitrary formulas, and conclude E. Here you have

1. (A -> ((B -> A) -> A)) -> ((A -> (B -> A)) -> (A -> A))
2. (A -> ((B -> A) -> A))
3. ((A -> (B -> A)) -> (A -> A)) MP 1, 2

I.e., D = (A -> ((B -> A) -> A)) and E = ((A -> (B -> A)) -> (A -> A)).

By the way, does your axiomatic system really make A -> ((B -> A) -> A) an instance of axiom 2? It's an instance of D -> (E -> D), which is usually called axiom 1. See, for example, this scan from another thread.

Thank you so much! That is VERY helpful!

Just one more thing if I write



what does the {\neg q} before the turnstyle mean? Is that some kind of assumption? Like in the above proof there was nothing before the turnstyle so does that mean there are no assumptions being made?

Then the next step is practice and to derive the deduction theorem yes?

You are welcome.

Originally Posted by chili5

what does the {\neg q} before the turnstyle mean? Is that some kind of assumption? Like in the above proof there was nothing before the turnstyle so does that mean there are no assumptions being made?

Yes, formulas left of the turnstile can be used as if they were axioms, i.e., one can insert such formula in a derivation at any time.

Originally Posted by chili5

Then the next step is practice and to derive the deduction theorem yes?

Hilbert system is somewhat tricky. It is so minimalistic because it has only two connectives, three axioms and one inference rule, which makes it easy to prove (meta)theorems about it, like the deduction theorem or the soundness theorem. However, this also makes it pretty hard to derive some simple formulas, even p -> p. So, yes, one needs practice, but don't be surprised if you can't derive some obvious tautologies because it can indeed be tricky. Be sure to read a lot of example derivations in your textbook or lecture notes.