Online Otter-λ

Examples

Distributivity of union over intersection in set theory

This is the example suggested by Sutcliffe for a workshop in summer 2008.

The problem takes sets to be defined by their characteristic functions. That is,

"x is a member of y" should be represented by Ap(x,y).

Accordingly, the input file contains the demodulator in(x,y) = Ap(x,y).

To represent sets in this way, and have a consistent theory, one needs a notion of "Proposition". Propositions can be combined with operators "or", "and", "implies", and "not" to yield other propositions. We say "x is a set", represented as Set(x), if for every y, Ap(x,y) is a proposition.

In this problem, union and intersection are themselves given by constants; our input file uses i and j for those constants, so that the union of sets p and q is given by

Ap(Ap(i,p),q)

The double application results from the convention of "Currying".

The principles set out so far are not sufficient for the distributive property, because nothing forces the (internal) logic of propositions to be classical logic. The principles set out so far are enough to reduce the distributive law of set theory to the corresponding distributive law of propositional logic, namely and(x,or(y,z)) = or(and(x,y),and(x,z)). Since the spirit of this problem is the set-theoretical aspect, we simply threw this propositional principle in as an axiom. Of course, we could have put in some axioms for propositional logic and tried to have the prover derive this principle, but that is another type of problem, not a set theory problem.

As is usual for a resolution prover, the goal is negated, and the variables in the goal become constants p,q,r. The hypotheses Set(p), Set(q), Set(r) are placed in list(usable), and the negated distributivity law is placed in list(sos). The proof is found instantly and is quite short. It only uses demodulation and beta-reduction to unwind the definitions, reducing the set theory problem to the logical distributive law.

Comment: This example does not require even one lambda unification. Hence, it could even be done in the first-order prover Otter, if one first defines lambda terms using combinators. That can be done in an input file to Otter (or its successor Prover9). Hence there is really nothing at all "higher-order" about this example. Beta-reduction is the only thing needed, and that can be done first-order using combinatory logic.

Comment: Some readers may complain that the axiom of logical distributivity should only apply to propositions, i.e. we should have extra hypotheses Prop(x), etc., where the law "and(x,or(y,z)) = or(and(x,y),and(x,z))" is stated. Such hypotheses are not required, because of the theorems on implicit typing given in the following places:

implicit typing in first order logic
implicit typing in lambda logic

Essentially, the point is Prop is a sort, and the functors "or" and "and" appearing in the input file are used consistently with respect to that sort, so resolution theorem-proving will only be able to derive theorems in which "or" and "and" are used correctly. Another way to look at the matter is just that it does not matter what "or" and "and" do on non-propositions. It is like saying that the square root of a negative number is something, but it doesn't matter what, because all the axioms about square roots apply only to nonnegative numbers.