Online Otter-λ
Examples
As background for this collection of examples, one should know about the use of a P-predicate to formalize various axiom systems for propositional logic. The purpose of this example is to explore the possibility of using lambda logic to extend the P-predicate method to first-order logic, and the use of Otter-λ to find formal proofs in your favorite axiom system for first-order logic.
In order to do this, we think of lambda(x,A[x]) as a propositional function, that is, a function whose value for any particular argument is a proposition. Here informally A[x] indicates an expression containing x; so A and A[x] are just two ways of mentioning the same expression, the latter emphasizing that "x" may occur in A. A proposition is usually defined as something that can be true or false. The universal quantifier "all" is a function that applies to a propositional function A and produces the proposition that we usually express as "for all x, A[x]". This can be expressed as all(lambda(x,A)).
Using this scheme, we can express in lambda logic the axioms from any of the usual formalisms for first order logic. In this example, we choose the system from Kleene's textbook, Introduction to Metamathematics. Here are the propositional axioms, using i(x,y) for "x implies y" and n(x) for "not x".
P(i(x,i(y,x))).
P(i(i(x,y),i(i(x,i(y,z)),i(x,z)))).
P(i(i(x,y),i(i(x,n(y)),n(x)))).
P(i(n(n(x)),x)).
P(i( i(n(x),n(y)), i(y,x))).
P(i( i(x,y), i(n(y),n(x)))).
From these axioms it is not difficult for Otter (or Otter-lambda) to derive
P(i(u,u)).
but we put this in as an axiom in order to focus on the treatment of quantifiers. One of the axioms for the universal quantifier is the following:
P(i(all(lambda(x,Ap(y,x))), Ap(y,z))).
This can be written down as a single axiom because we use a variable y for the propositional function. Normally in logic textbooks, this axiom is written using a "syntactic variable" or "metavariable", but it stands for an infinite set of axioms in the formal logic, one for each formula defining a propositional function. Textbooks usually call this an axiom schema. If a variable is used for a propositional function as an official part of the language, the system is called second order logic.In a sense then, what we are formulating here is a "weak second order logic". (It is "weak" because you can't quantify over propositions.) But when we use Otter-λ to generate proofs, the propositional variables will get instantiated to first order formulas, and the result will be first order proofs in Kleene's system.
The rule of inference to be used in this system for first order logic is, as in the prior work on propositional logics in Otter,
the rule of condensed detachment:
-P(x) | -P(i(x,y)) | P(y).
When this is used, x and y will get assigned to specific formulas of first-order logic. If we are using
hyperresolution as the inference rule in Otter-lambda, then this serves to derive P(y) when we have already
shown P(x) and P(i(x,y)). This corresponds to the use of condensed detachment in first-order logic. The
relationship between condensed detachment proofs and proofs using substitution and modus ponens is discussed
in detail in [1].
We put these axioms in list(usable). In first order logic, we can define the existential quantifier
"there exists" by the equivalence "there exists an x such that A[x]" if and only if "not for all x not A[x]".
One of the laws that "there exists" should obey is that if A[c] holds then "there exists x such that A[x]" should hold.
We should be able to check that in Otter-lambda, and that is the point of this example. We set this up by
representing A[x] as Ap(a,x). This example checks the rule of inference that if A[c] is provable then
"there exists x A[x]" is provable:
list(sos).
P(Ap(a,c)).
-P(n(all(lambda(x,n(Ap(a,x)))))).
end_of_list.
In work on propositional logic with Otter, it has been traditional to cause terms with double negations to be discarded by demodulating double negation to junk. The demodulators you see in the input file are for that purpose; there is nothing new in that part of the file.
When we run this file with hyperresolution as the only inference rule (which corresponds to forwards reasoning using condensed detachment, Otter-lambda does not find a proof. But when we add unit-resulting resolution (UR-resolution), it quickly finds the following proof:
2 [] -P(x)| -P(i(x,y))|P(y).
3 [] P(i(x,i(y,x))).
5 [] P(i(i(x,y),i(i(x,n(y)),n(x)))).
10 [] P(i(all(lambda(x,Ap(y,x))),Ap(y,z))).
17 [] P(Ap(a,c)).
18 [] -P(n(all(lambda(x,n(Ap(a,x)))))).
19 [hyper,17,2,3] P(i(x,Ap(a,c))).
21 [hyper,19,2,5] P(i(i(x,n(Ap(a,c))),n(x))).
43 [ur,21,2,18] -P(i(all(lambda(x,n(Ap(a,x)))),n(Ap(a,c)))).
44 [binary,43.1,10.1] $F.
Note that line 21 doesn't directly correspond to a first-order step from Kleene's axioms, because it has a variable in the place where a proposition belongs; it's a schema of a derivation. If we substitute any particular proposition x, we will get a first-order derivation. When this line is resolved with the negated goal, x does become instantiated to a particular proposition, so a derivation in Kleene's system does result. This sort of ex post facto construction of a first-order derivation is a familiar phenomenon in natural-deduction provers or provers based on Gentzen sequent calculi. It is interesting to see it here in the context of a clausal theorem prover.
This example is also of interest as an example of implicit typing. In implicit typing, each function symbol is implicitly (that means, unofficially) assigned a return type and a type for each of its arguments. In this example these types are indicated in comments in the input file. The types are:
PF (propositional function)
prop (proposition)
obj (object)
PF lambda(obj, prop)
prop all(PF)
bool P(prop)
prop i(prop,prop)
prop n(prop)
prop Ap(PF, obj)