Posted on the Web June 6, 2001. Last updated on May 8, 2011 by Bob Veroff.

i(s,t) (major premise) r (minor premise) ------------------------ sigma(t), where sigma is a most general unifier for terms r and s.In particular, we focus here on proving theorems in these logical calculi using resolution-style automated reasoning programs such as Otter [4]. The questions considered include determining the equivalence of various axiom systems, finding proofs to specific theorems, and finding proofs with certain specified properties.

*CD* problems are easily represented for resolution theorem provers.
If we let

P(t)represent the assertion that

tis a theorem, then applications of condensed detachment can be implemented using hyperresolution and the following clause.

-P(i(x,y)) | -P(x) | P(y).The page currently includes the following.

- Distributivity Theorems in Many-Valued Logic
- Finding CD-Derivations of Specific Instances
- Proving the Harris / Rezus Single Axiom is a Theorem in Many-Valued Logic
- CD-Derivation of the Long Rezus Single Axiom for RI
- Whitehead and Russell Dependency
- Theorems in Intuitionistic Logic

% axioms for many-valued logic P(i(x,i(y,x))) (MV1) P(i(i(x,y),i(i(y,z),i(x,z)))) (MV2) P(i(i(i(x,y),y),i(i(y,x),x))) (MV3) P(i(i(n(x),n(y)),i(y,x))) (MV4)The problem is to find

% KA1: K distributes over A, direction 1 (KpAqr -> AKpqKpr) P(i(n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))), i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(n(x),n(z)),n(z)))),n(i(i(n(x),n(z)),n(z)))))) # label("KA1"). % KA2: K distributes over A, direction 2 (KpAqr <- AKpqKpr) P(i(i(i(n(i(i(n(x),n(y)),n(y))),n(i(i(n(x),n(z)),n(z)))),n(i(i(n(x),n(z)),n(z)))), n(i(i(n(x),n(i(i(y,z),z))),n(i(i(y,z),z)))))) # label("KA2"). % AK1: A distributes over K, direction 1 (ApKqr -> KApqApr) P(i(i(i(x,n(i(i(n(y),n(z)),n(z)))),n(i(i(n(y),n(z)),n(z)))), n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))))) # label("AK1"). % AK2: A distributes over K, direction 2 (ApKqr <- KApqApr) P(i(n(i(i(n(i(i(x,y),y)),n(i(i(x,z),z))),n(i(i(x,z),z)))), i(i(x,n(i(i(n(y),n(z)),n(z)))),n(i(i(n(y),n(z)),n(z)))))) # label("AK2").The comments refer to operators A and K, which are defined below.

Previous proofs of these theorems rely on several lemmas and on
meta-theoretical inferences such as term-level equality
substitutions ([1]). Our interest is in using an automated
reasoning program such as Otter to find proofs that rely solely on the axioms
and on applications of condensed detachment. In particular, the challenge
is to find these proofs from scratch--without relying on any knowledge of
the known meta-theoretical proofs. Our approach is to find meta-theoretical
proofs of our own, which are in turn used as proof sketches
([8]) to help Otter find the desired *CD*-only proofs.

CpCqp | (MV1) | |

CCpqCCqrCpr | (MV2) | |

CCCpqqCCqpp | (MV3) | |

CCNpNqCqp | (MV4) |

where C and N are related, respectively, to our usual notions of logical implication and negation. In addition, two operators A and K are defined as follows.

Apq = CCpqq | |

Kpq = NCCNpNqNq |

These two operators are related, respectively, to our
usual notions of logical disjunction (**or**) and conjunction (**and**).

It is known that the following distributivity properties hold for K and A.

KpAqr = AKpqKpr | (K distributes over A) | |

ApKqr = KApqApr | (A distributes over K) |

In the primitives of MV, these are stated as four implications:

- KpAqr = AKpqKpr (K distributes over A)
KpAqr -> AKpqKpr (KA1) KpAqr <- AKpqKpr (KA2) - ApKqr = KApqApr (A distributes over K)
ApKqr -> KApqApr (AK1) ApKqr <- KApqApr (AK2)

Expanding the four theorems with the definitions of A and K gives

% KA1: K distributes over A, direction 1 (KpAqr -> AKpqKpr) CNCCNpNCCqrrNCCqrrCCNCCNpNqNqNCCNpNrNrNCCNpNrNr % KA2: K distributes over A, direction 2 (KpAqr <- AKpqKpr) CCCNCCNpNqNqNCCNpNrNrNCCNpNrNrNCCNpNCCqrrNCCqrr % AK1: A distributes over K, direction 1 (ApKqr -> KApqApr) CCCpNCCNqNrNrNCCNqNrNrNCCNCCpqqNCCprrNCCprr % AK2: A distributes over K, direction 2 (ApKqr <- KApqApr) CNCCNCCpqqNCCprrNCCprrCCpNCCNqNrNrNCCNqNrNrwhich correspond directly to the clauses presented at the beginning of this section. In clause form, Cpq is represented as i(p,q); Np is represented as n(p); and the propositional variables p, q, and r are represented, respectively, with the Otter variables x, y, and z.

For more information on the Harris/Fitelson work on distributivity presented in [3], see the paper's companion Web page.

% theorem d2 P(i(i(x,x),i(n(x),n(x)))). % theorem d3 P(i(i(x,x),i(i(y,y),i(i(x,y),i(x,y))))).in many-valued logic (MV)

% axioms for many-valued logic P(i(x,i(y,x))) (MV1) P(i(i(x,y),i(i(y,z),i(x,z)))) (MV2) P(i(i(i(x,y),y),i(i(y,x),x))) (MV3) P(i(i(n(x),n(y)),i(y,x))) (MV4)and also in the intuitionistic logic (H)

% axioms for intuitionistc logic P(i(x,i(y,x))) (H1) P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) (H2) P(i(i(x,n(x)),n(x))) (H3) P(i(x,i(n(x),y))) (H4)These theorems are instances of more general theorems that are not difficult to prove. What makes these problems interesting (and challenging) is the requirement of deriving precisely the specified instances of the theorems.

These results are relevant to a larger work ([2]) concerning the elimination of occurrences of double negation in proofs.

The Harris / Rezus axiom,

P(i(i(i(x,i(y,x)),i(i(i(i(i(i(i(i(i(z,u),i(i(v,z),i(v,u))),i(i(w,i(v6,w)),v7)),v7),i(i(i(i(v8,v9),v9),i(i(v9,v8),v8)),v10)),v10),i(i(i(i(v11,v12),i(v12,v11)),i(v12,v11)),v13)),v13),i(i(v14,i(v15,v14)),v16))),v16)).is known to be a single axiom for the implicational fragment of many-valued logic, which can be described in clause form with the following four axioms.

% axioms for the implicational fragment of many-valued logic P(i(x,i(y,x))) (MV1) P(i(i(x,y),i(i(y,z),i(x,z)))) (MV2) P(i(i(i(x,y),y),i(i(y,x),x))) (MV3) P(i(i(i(x,y),i(y,x)),i(y,x))) (MV5)The problem here is to find a

As far as we know, this is the first explicitly presented *CD*-only proof.

From

P(i(i(u,v),i(i(v,w),i(u,w)))) (B) P(i(i(u,i(v,w)),i(v,i(u,w)))) (C) P(i(u,u)) (I) P(i(i(u,i(u,v)),i(u,v))) (W)derive

% A Rezus-style single axiom for RI P(i(i(i(x,i(i(i(y,y),i(i(z,z),i(i(u,u),i(i(v,v),i(x,w))))),w)),i(i(i(i(i(v6,v7),i(i(v7,v8),i(v6,v8))),i(i(i(i(i(v9,i(v9,v10)),i(v9,v10)),i(i(i(v11,v12),i(i(v12,v13),i(v11,v13))),v14)),v14),v15)),v15),i(i(v16,i(i(i(v17,v17),i(i(v18,v18),i(i(v19,v19),i(i(v20,v20),i(v16,v21))))),v21)),v22))),v22)).We include input, output, proof and xml files created as follows.

prover9 -f RI_rezus.in > RI_rezus.outprooftrans -f RI_rezus.out > RI_rezus.pf

prooftrans xml -f RI_rezus.out > RI_rezus.xml

We note that this essentially is a proof checking run, since it includes the steps from a previously found proof as hints. The original proofs were found using the method of proof sketches ([8]). In particular, our approach was to find derivations of the Rezus axiom with extra assumptions included as input; the resulting derivations in turn were used as proof sketches to help Prover9 find the desired CD-only proofs.

% Definition: x -> y = ~x v y P((x -> y) -> (~x v y)) (-> Definition, part a) P((~x v y) -> (x -> y)) (-> Definition, part b) % WR axioms WR1 .. WR4 P((x v x) -> x) (WR1) P(y -> (x v y)) (WR2) P((x v y) -> (y v x)) (WR3) P((y -> z) -> ((x v y) -> (x v z))) (WR4)derive

P((x v (y v z)) -> (y v (x v z))) (WR5)This establishes the dependency of WR5 in Whitehead and Russell's system for PC.

We include input, output, proof and xml files created as follows.

prover9 -f WandR.in > WandR.out

We note that this essentially is a proof checking run, since it includes the steps from a previously found proof as hints. The original proofs were found using the method of proof sketches ([8]). In particular, our approach was to find derivations of WR5 with extra assumptions included as input; the resulting derivations in turn were used as proof sketches to help Prover9 find the desired CD-only proofs.

From

P(i(x,i(y,x))) (A1) P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))) (A2) P(i(k(x,y),x)) (A3) P(i(k(x,y),y)) (A4) P(i(i(x,y),i(i(x,z),i(x,k(y,z))))) (A5) P(i(x,a(x,y))) (A6) P(i(x,a(y,x))) (A7) P(i(i(x,y),i(i(z,y),i(a(x,z),y)))) (A8) P(i(i(x,n(y)),i(y,n(x)))) (A9) P(i(n(x),i(x,y))) (A10)derive

P(i(i(x,y),i(a(x,z),a(y,z)))) (H334) P(k(i(a(k(x,y),z),k(a(x,z),a(y,z))),i(k(a(x,z),a(y,z)),a(k(x,y),z)))) (HIF4) P(k(i(n(a(x,y)),k(n(x),n(y))),i(k(n(x),n(y)),n(a(x,y))))) (HIF5)

We include input, output, proof and xml files created as follows.

prover9 -f IL.in > IL.out

We note that this essentially is a proof checking run, since it includes the steps from a previously found proof as hints. The original proofs were found using the method of proof sketches ([8]). In particular, our approach was to find derivations with extra assumptions included as input; the resulting derivations in turn were used as proof sketches to help Prover9 find the desired CD-only proofs.

[1] Beavers, G.,
``Distribution in Lukasiewicz logics,''
*Bulletin of the Section of Logic*, vol 21, no. 4, pp. 140-146 (1992).
(pdf)

[2] Beeson, M., Veroff, R., and Wos, L.,
``Double negation elimination in some propositional logics,''
*Studia Logica*, 80:195-234, 2005.
(pdf)

[3] Harris, K. and Fitelson, B.,
``Distributivity in L_aleph0 and other sentential logics,''
*Journal of Automated Reasoning*, Vol. 27, no. 2, pp. 141-156 (2001).
(pdf)

[4] McCune, W., OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois, 1994.

[5] Rezus, A.,
``On a theorem of Tarski,''
*Libertas Mathematica*, vol 2, pp. 63-97 (1982).

[6] Rose, A. and Rosser, J.,
``Fragments of many-valued statement calculi,''
*Trans. American Mathematical Society*, vol 87, pp. 1-53 (1958).

[7] Tarski, A.,
``Investigations into the sentential calculus,''
in *Logic, Semantics and Metamathematics*, Hackett Publishing,
Indianapolis (1983).

[8] Veroff, R.,
``Solving open questions and other challenge problems using proof sketches,''
*Journal of Automated Reasoning*, Vol. 27, no. 2, pp. 157-174 (2001).
(postscript)