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?

  • $\begingroup$ Are you looking for a formal proof, is that it? $\endgroup$ – Git Gud Apr 24 '14 at 17:04
  • $\begingroup$ Yep, I aim to write a formal proof, but approaches and strategies in this case are very accepted rather than a straight answer. I have been spending over 2 hours so far to understand what I am doing wrong by doing the substitutions in A3 $\endgroup$ – graphtheory92 Apr 24 '14 at 17:11
  • $\begingroup$ The most general strategy you can use is to use the proof of the Deduction Theorem. This is not necessarily the fastest way. $\endgroup$ – Git Gud Apr 24 '14 at 17:13

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*}

  • $\begingroup$ While for ¬¬p→(p→q), it is just about applying A1 wit MP as you did above, ¬¬p→p is the hard bit whose expansion gets too big and I can't reach an end $\endgroup$ – graphtheory92 Apr 24 '14 at 17:43
  • $\begingroup$ @graphtheory92 I hope the edit helps. $\endgroup$ – Git Gud Apr 25 '14 at 2:10

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


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

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


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.