Question

prove using the Hilbert System

{not q} ⊢ (p→q)→(not p)

Answer 1

I'm supposed to use the 3 axioms of the Hilbert System and Modus Ponens to prove this

Answer 2

Using the Hilbert Axioms.
We state our given:
\[
\neg q \vdash (p\to q)\to\neg p
\]Using the fourth (or third primary axiom):
\[
(\neg p\to \neg q)\to(q \to p)
\]We contraposition the first clause, since they are equivalent statements, by the above logical axiom:
\[
\neg q \vdash (\neg q\to \neg p)\to\neg p
\]Since\[
\neg p\to \neg p
\]By a simple reduction, then:
\[
\neg q \to \neg p
\]QED.

Answer 3

I think I need to assume (not q) and use that with the Hilbert System to come to the conclusions that (p→q)→(not p)

Answer 4

sorry if the way I wrote that made it confusing

Answer 5

Oh, all right, sorry, that's not all too difficult, let me retype the above:

Answer 6

It's essentially the same proof, just that we assume only the first given to denote the second. We assume:
\[
\neg q, (p\to q)
\]To be true, along with the three logical actions in the Hilbert system.
We begin:
\[
(p\to q)\to (\neg q \to \neg p)
\]By (3):
\[
\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)
\]So:
\[
(\neg q \to \neg p)\to \neg p\wedge \neg q\to \neg p
\]Consequentially:
\[
\neg q \vdash (p\to q) \to \neg p
\]QED.

Answer 7

are you assuming p->q at the beginning?

Answer 8

Yes, you have to, otherwise nothing follows.

Answer 9

Because we would then have no relation between instance \(p\) and \(q\).

Answer 10

well the only assumption I think I can make is not q

Answer 11

and I can only use things I can derive from the 3 axioms or modus ponens

Answer 12

for example I could use axiom 1 to write ((~q) ->(p->(~q))

Answer 13

and use that like an assumption

Answer 14

at least this is my understanding of the hilbert proof system

Answer 15

This is my first time using it

Answer 16

Yeah, I only used axioms, the third axiom states the manipulation above, and there needs to be some relation for p, q, otherwise we can only imply \(q\to q\), or some other singly-defined tautology.

Answer 17

I don't understand how you went from (p→q)→(¬q→¬p) to the end

Answer 18

I can get to this point by manipulating the axioms

Answer 19

how can you get the end to be just (not p)

Answer 20

and I've never seen an ^ in any Hilber proofs before

Answer 21

You can take the first axiom (or a conjunction/disjunction operator, I don't know if you're allowed to use these, but that's what my proof contains):
An explicit-axiom proof would look like this, for
\[
(p\to q)\to (\neg q \to \neg p)
\]Thus, MP:
\[
\frac{\neg q\to\neg p,\neg q}{\therefore \neg p}
\]

Answer 22

I don't know what a conjunction/disjunction operator is.

the only thing I have available to me are these axioms
A1 (A -> (B->A))
A2 ((A -> (B->C)) -> ((A->B)->(A->C)))
A3 (((~A) -> (~B)) -> (B->A))

and modus ponens hich states
if we have A->B and A we can infer B

Answer 23

Well, yeah, I've already proven it using only those.

Answer 24

sorry for not responding, I had to catch a bus

Answer 25

hmm maybe I'm confused about how you wrote it then

Answer 26

It's all right... but I've already shown the proof with only those 3.. I can re-write it wholly, if you wish...

Answer 27

well can you explain how you use each axiom at each step?
From the examples I've been provided it seems like you need to start with an assumption like (~q) or one of the axioms with values substituted into it

Answer 28

I'm a little confused how you begin with (p→q)→(¬q→¬p)

Answer 29

actually that is axiom 3 isn't it with A=¬p and B=¬q

Answer 30

We assume:
\[\neg q, (p\to q)
\]To be true, along with the three logical actions in the Hilbert system.
We begin:
As given by Axiom (3) which states:
\[
\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)
\]Then:
\[
(p\to q)\to (\neg q \to \neg p)
\](Since, we can replace it the logical inverses of each operator)
So, by the above:
\[
\frac{\neg q\to\neg p,\neg q}{\therefore \neg p}
\]And we're done.

Answer 31

Yes, it is.

Answer 32

The Hilbert System allows one to replace any single instance \(\phi\) with whatever other instance we wish, so long as it holds true.

Answer 33

could you please explain where this part comes from? ¬q→¬p,¬q

Answer 34

We know by our previous deduction that:
\[
\neg q\to \neg p
\]Since we have:
\[
\neg q
\]Therefore:
\[
\neg p
\](Modus Ponens)

Answer 35

can you apply modus ponens to the end of a statement like that?

Answer 36

From what I've seen they only apply modus ponens to the whole thing

Answer 37

Well, the statement I gave IS Modus Ponens (MP). We're simply taking our final logical deduction given by our previous.

Answer 38

but we are only applying it to (¬q→¬p) rather than the whole (p→q)→(¬q→¬p)
can we assume (¬q→¬p) based on (p→q)→(¬q→¬p)?

Answer 39

or are you getting the assumption that (¬q→¬p) from somewhere else?

Answer 40

No, the assumption is reached by the previous statement. I think it's easier to write it out.

We have that (p implies q) implies (not q implies not p). Therefore, by our assumption, we can therefore say that, for anything that holds in (p implies q), such will also hold in (not q implies not p). With this, we give the statement that not p is true based upon the fact that not q is true as the statement previously given follows.

Answer 41

Treat \(p \to q\) as our premise, and \(\neg q \to \neg p\) as our conclusive statement.
Because we can say that, if \(\Gamma\vdash a\to b \), then, by MP:
\[
\frac{\Gamma\vdash a}{\Gamma \vdash b}
\]

Answer 42

so you are assuming (p→q) to infer that (¬q→¬p) then

Answer 43

Yep.

Answer 44

I don't think I can use (p→q) as an assumption though. I think the only thing I can use as an assumption is (¬q) unless I can derive (p→q) from one of the axioms

Answer 45

OK so I completely understand your solution now. But I need to write an explicit proof so I can't just convert (¬¬p→¬¬q)→(¬q→¬p) to (p→q)→(¬q→¬p). I need o show I can get the (¬¬p→¬¬q) with the axioms as well. Can you help me out with that please?