Hilbert System with propositional logic $p \rightarrow q,\neg q \vdash \neg p$

Question

This is my set of axiom

1. $A \rightarrow (B\rightarrow A)$
2. $(A\rightarrow(B\rightarrow C))\rightarrow ((A\rightarrow B) \rightarrow (A \rightarrow C))$
3. $(\neg A \rightarrow B)\rightarrow ((\neg A \rightarrow \neg B)\rightarrow A)$

When applying it to prove $$p \rightarrow q,\neg q \vdash \neg p$$ I get inside an exponential expansion which makes me feel it is not provable. So far I have been trying a several combinations in which start from A3 by substituting $A=\neg p$, $B=q$ and even with $B=\neg q$.

Is there any substitution that I am not seeing?

Answer 1

This is a possible thought process. I don't have time to go through the details, but this seems to work.

Almost likely the formal proof of this theorem ends with an application of axiom 3 and modus ponens.

Axiom 3. with $A=\neg p$ and $B=q$ yields $$(\neg \neg p\to q)\to ((\neg \neg p\to \neg q)\to \neg p).$$

So it's enough to be able to deduce $\neg \neg p\to q$ and $\neg \neg p\to \neg q$.

Axiom 1 yields $\neg q\to(\neg \neg p\to \neg q)$, so $\neg \neg p\to \neg q$ is taken care of.

It remains to get $\neg \neg p\to q$. Since it is a conditional statement, it is likely a consequence of the second axiom.

The second axiom with $A=\neg \neg p, B=p$ and $C=q$ yields $$(\neg \neg p\to (p\to q))\to ((\neg \neg p\to p)\to (\neg \neg p\to q)).$$

So now you want to use modus ponens on the above formula. Therefore it suffices to find proofs of $\neg \neg p\to (p\to q)$ and $\neg \neg p\to p$. The first of these is easy. The other one is harder.

Proof of $\neg \neg p\to p$:

\begin{alignat*}{3} 1. \,&((\neg p\to \neg \neg p)\to p)\to (\neg \neg p\to ((\neg p \to \neg \neg p)\to p)) &&(\text A1)\\ 2. \,&(\neg p \to \neg p)\to ((\neg p\to \neg \neg p)\to p) &&(\text A3)\\ 3. \,&\neg p \to ((\neg p \to \neg p)\to \neg p) &&(\text{A} 1)\\ 4. \,&(\neg p\to ((\neg p \to \neg p)\to \neg p))\to ((\neg p \to (\neg p \to \neg p))\to (\neg p \to \neg p)) &&(\text{A} 2)\\ 5. \,&(\neg p \to (\neg p \to \neg p))\to (\neg p \to \neg p) &&(\text{MP }3,4)\\ 6. \,&\neg p \to (\neg p\to \neg p) &&(\text{A}1)\\ 7. \,&\neg p \to \neg p &&(\text{MP }5,6)\\ 8. \,&(\neg p \to \neg \neg p)\to p &&(\text{MP }7,2)\\ 9. \,&\neg \neg p\to ((\neg p \to \neg \neg p)\to p) &&(\text{MP }8,1)\\ 10. \,&(\neg \neg p\to ((\neg p \to \neg \neg p)\to p))\to ((\neg \neg p\to (\neg p \to \neg \neg p))\to (\neg \neg p \to p)) &&(\text{A}2)\\ 11. \,&(\neg \neg p\to (\neg p \to \neg \neg p))\to (\neg \neg p \to p) &&(\text{MP 9,10})\\ 12. \,&\neg \neg p \to (\neg p \to \neg \neg p) &&(\text{A}1)\\ 13. \,&\neg \neg p \to p &&(\text{MP }12, 11)\\ \end{alignat*}

Answer 2

I use Polish notation and condensed detachment.

The axioms I'll write as:

3 CpCqp
4 CCpCqrCCpqCpr   
5 CCNpqCCNpNqp

D3.3    7 CpCqCrq
D4.4    8 CCCpCqrCpqCCpCqrCpr
D3.4    9 CpCCqCrsCCqrCqs
D4.3   10 CCpqCpp
D4.5   11 CCCNpqCNpNqCCNpqp
D3.5   12 CpCCNqrCCNqNrq
D3.7   13 CpCqCrCsr
D10.12 14 Cpp
D5.14  15 CCNpNNpp
D4.14  16 CCCpqpCCpqq
D8.7   17 CCpCCqprCpr
D3.15  18 CpCCNqNNqq
D8.13  19 CCpCCqCrqsCps
D8.9   20 CCCpCqrCCCpqCprsCCpCqrs
D17.18 21 CNNpp
D17.12 22 CpCCNqNpq
D17.9  23 CCpqCCrpCrq
D3.21  24 CpCNNqq
D16.24 25 CCCNNppqq
D11.24 26 CCNNNppNNp
D4.22  27 CCpCNqNpCpq
D19.23 28 CCCpqrCqr
D3.28  29 CpCCCqrsCrs
D28.26 30 CpNNp
D28.16 31 CpCCpqq
D23.30 32 CCpqCpNNq

Break...

D23.31 33 CCpqCpCCqrr
D28.27 34 CCNpNqCqp
D23.34 35 CCpCNqNrCpCrq
D20.29 36 CCpCqrCqCpr
D25.33 37 CNNpCCpqq
D36.37 38 CCpqCNNpq
D36.32 39 CpCCpqNNq
D38.39 40 CNNpCCpqNNq
D36.40 41 CCpqCNNpNNq
D35.41 42 CCpqCNqNp

When using the proof of the deduction theorem to convert a demonstration with an assumption to a formal proof the theorems in the following sequence can prove especially useful:

     1 CpCqp
     2 CCpCqrCCpqCpr
D1.2 3 CpCCqCrsCCqrCqs
D2.3 4 CCpCqCrsCpCCqrCqs
D1.4 5 CpCCqCrCstCqCCrsCst
D2.5 6 CCpCqCrCstCpCqCCrsCst
D1.6 7 CpCCqCrCsCtuCqCrCCstCtu
D2.7 8 CCpCqCrCsCtuCpCqCrCCstCtu

Answer 3

This answer is distinct from the last.

Axiom three tells us that if we have a negation implying a proposition, and also implying that proposition's negation, we can obtain the proposition. So, since we want Np from {Cpq, Nq}, we might assume NNp. We know that we should be able to get CNNpp in this system, since it's a tautology. So, then we can get p, then q, and Nq. Since we have NNp as our assumption, using the deduction theorem will yield CNNpq and CNNpNq. With less work though, since we already have Nq as an assumption, we can get CNNpNq from CaCba and Nq. Then having CCNabCCNaNba, CNNpq, and CNNpNq we can obtain Np after two detachments.

How do we get CNNpp? Well, much in the same way that we can get to Np above. We assume the negation of the consequent "p". Since we already have NNp as a hypothesis we can then derive CNpNNp. Since Caa is a theorem, we can derive CNpNp. Along with axiom 3 we can then obtain p.

Thus, we can write...

1 CCaCbaCCabCaa from axiom 2
2 CaCba axiom 1
3 CCabCaa detachment 1, 2
4 CCaCbaCaa from 3
5 Caa detachment 4, 2
6  | NNa hypothesis
7  | CNNaCNaNNa axiom 1
8  | CNaNNa detachment 7, 6
9  | CNaNa from 5
10 | CCNaNaCCNaNNaa axiom 3
11 | CCNaNNaa detachment 10, 9
12 | a  detachment 11, 8
13 CNNaa conditional introduction 6-12
14 | Cpq assumption
15 | Nq  assumption
16 || NNp hypothesis
17 || CNNpp by 13
18 || p  detachment 17, 16
19 || q  detachment 14, 18
20 | CNNpq conditional introduction 16-19
21 | CNqCNNpNq by axiom 1
22 | CNNpNq detachment 21, 15
23 | CCNNpqCCNNpNqNp by axiom 3
24 | CCNNpNqNp detachment 23, 20
25 | Np 24, 22 detachment

Note that this has 7 lines in the first part which need discharged and 4 lines in the second part which need discharged. So, we have {[3(7)+2]+[3(4)+2]}=37 lines to write if we use the strictest proof of the deduction metatheorem. With some pre-processing, and maybe also using condensed detachment, this can get considerably shortened. In fact, I found that you can write a proof of CCpqCNqNp in this system using just 27 condensed detachments (which makes for a 30 line proof if you list the axioms also).

Answer 4

Combining the subformula strategy, weighting of the axioms, the assumptions, and the goal, and a (partial) level saturation search, I've found a 20 step (excluding the axioms and assumptions), level 6 proof using OTTER [1] (OTTER treats "p" and "q" here as nullary functions or in other words, constants).

axiom             4 CxCyx.                  level 0
axiom             5 CCxCyzCCxyCxz.          0
axiom             6 CCNxyCCNxNyx.           0
assumption        7 Cpq                     0
assumption        8 Nq                      0
D4.4              9 CxCyCzy                 1
D5.5             10 CCCxCyzCxyCCxCyzCxz     1
D4.5             11 CxCCyCzuCCyzCyu         1
D5.4             12 CCxyCxx                 1
D5.6             13 CCCNxyCNxNyCCNxyx       1
D4.7             15 CxCpq                   1
D4.8             16 CxNq                    1
D4.9             19 CxCyCzCuz               2
DD5.5.9          20 CCxCCyxzCxz             2
DD5.4.4          27 Cxx                     2
D5.15            33 CCxpCxq                 2
D4.16            36 CxCyNq                  2
DD5.5.19         47 CCxCCyCzyuCxu           3
D20.11           50 CCxyCCzxCzy             3
D6.27            66 CCNxNNxx                3
DD5.6.36         95 CCNxqx                  3
D47.50          163 CCCxyzCyz               4
DD5.15.66       211 CCNpNNpq                4
D163.211        910 CNNpq                   5
D95.910        6213 Np                      6

[1]- W. McCune, "OTTER and Mace2", http://www.mcs.anl.gov/research/projects/AR/otter/, 1988-2014.