Peter Smith writes in his Types of Proof System: "How do you get from: $\lnot$(P -> $\lnot$ Q) to the desired conclusion P? It can be done, but as far as I know it takes well over fifty lines (if done from first principles, without appealing to any previously-established results about the system M)."

The M-system has axiom schema:

Ax1. (A -> (B -> A))

Ax2. ((A -> (B -> C)) -> ((A -> B) -> (A -> C)))

Ax3. ((¬B -> ¬A) -> (A -> B))

The only rule of inference is formal modus ponens; from A along with (A -> C) infer C.

Some comments here imply that an upper bound for a shortest proof of $\lnot$(P -> $\lnot$ Q) $\vdash$$_M$ P is 31 steps. Can a proof in M get written in less than 30 lines?


Suppose we set up a correspondence between the definition of a well-formed formula in M and a meaningful expression in a system P in Polish notation such that each type of well-formed formula in M has a correspondent meaningful expression in P. The correspondence goes from M to P and from P to M.

The following will use a slightly different definition of a wff than many authors use. The definition will go as follows:

  1. Any letter in nopqrstuvwxyz is a propositional wff.

  2. Any letter in abcdefghijklm is a variable wff.

  3. All variable wffs are wffs.

  4. All propositional wffs are wffs.

  5. If α is wff, then so is Nα.

  6. If α is a wff, if β is a wff also, then Cαβ is a wff.

Variable wffs can get substituted by any meaningful expression (wff) in any formula (wff) in which the statement form (wff) appears. Propositional wffs can't get substituted by any meaningful expression.

Thus, we can address the above question by seeing if we can write a shorter than 30 line proof of p starting from the premiss NCpNq in a system P with the above definition of a wff with the following axiom schema:

Ax1. CaCba

Ax2. CCaCbcCCabCac

Ax3. CCNaNbCba

We have a definition:

Def. Kab is defined as NCaNb

And the only rule of inference is C-detachment; from a wff of the form C$\alpha$$\beta$ and a wff of the form $\alpha$, we may infer a wff of the form $\beta$.

Premiss                          1 Kpq
by 1 and the definition of Kab   2 NCpNq
Ax1 a/NCpNq, b/Na                3 CNCpNqCNaNCpNq
3 * C2-4                         4 CNaNCpNq
Ax3 b/CpNq                       5 CCNaNCpNqCCpNqa
5 * C4-6                         6 CCpNqa
Ax1 a/CCpNqa, b/CNNqNp           7 CCCpNqaCCNNqNpCCpNqa
7 * C6-8                         8 CCNNqNpCCpNqa
Ax2 a/CNNqNp, b/CpNq, c/a        9 CCCNNqNpCCpNqaCCCNNqNpCpNqCCNNqNpa
9 * C8-10                       10 CCCNNqNpCpNqCCNNqNpa
Ax3 a/Nq, b/p                   11 CCNNqNpCpNq
10 * C11-12                     12 CCNNqNpa
Ax1 a/CCNqNpa, b/Np             13 CCCNNqNpaCNpCCNNqNpa
13 * C12-14                     14 CNpCCNNqNpa
Ax2 a/Np, b/CNNqNp, c/a         15 CCNpCCNNqNpaCCNpCNNqNpCNpa
15 * C14-16                     16 CCNpCNNqNpCNpa
Ax 1 a/Np, b/NNq                17 CNpCNNqNp
16 * C17-18                     18 CNpa
18 a/NCNpa                      19 CNpNCNpa
Ax 3 a/p, b/CNpa                20 CCNpNCNpaCCNpap
20 * C19-21                     21 CCNpap
21 * C18-22                     22 p

Twenty-two is less than thirty. So is twenty-one if we ignore the 1st step. Can step 20 get eliminated? Can there get written a twenty-one step proof?

For accepting this answer, the above system might differ substantially from Mendelson's and thus might not work.

I got an outline for constructing a previous proof (see earlier postings here) from this first-order hyper-resolution proof of OTTER written by the late William McCune at Argonne National Laboratory:

-----> EMPTY CLAUSE at 0.17 sec ----> 2433 [hyper,2,2424] $F.

Length of proof is 10. Level of proof is 10.

---------------- PROOF ----------------

1 [] -P(C(x,y))| -P(x)|P(y).

2 [] -P(p).

3 [] P(C(x,C(y,x))).

4 [] P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).

5 [] P(C(C(N(x),N(y)),C(y,x))).

6 [] P(N(C(p,N(q)))).

8 [hyper,1,3,6] P(C(x,N(C(p,N(q))))).

12 [hyper,1,5,8] P(C(C(p,N(q)),x)).

13 [hyper,1,3,12] P(C(x,C(C(p,N(q)),y))).

24 [hyper,1,4,13] P(C(C(x,C(p,N(q))),C(x,y))).

76 [hyper,1,24,5] P(C(C(N(N(q)),N(p)),x)).

102 [hyper,1,3,76] P(C(x,C(C(N(N(q)),N(p)),y))).

116 [hyper,1,4,102] P(C(C(x,C(N(N(q)),N(p))),C(x,y))).

2404 [hyper,1,116,3] P(C(N(p),x)).

2419 [hyper,1,5,2404] P(C(x,p)).

2424 [hyper,1,2419,2419] P(p).

2433 [hyper,2,2424] $F.

------------ end of proof -------------


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.