In the present thesis I show how to use the automated theorem prover OTTER [1] to create an ultra-formal verification of a recent result in combinatory logic. This result is a main technical lemma of M. R. Holmes [2], who found a system of combinatory logic, which he calls TRC, equivalent to Quine's set theory New Foundations [3]. The automated reasoning techniques build on those of Art Quaife [4], who showed how to use the automated theorem prover OTTER as a proof finder/verifier in set theory. I believe that this thesis provides evidence that a combinatory logic formulation of set theory is more amenable to automated theorem proving than the usual formulation in the language of set theory.

In this work I have heavily used not only OTTER, but also custom programs that I have written in a variety of languages, including Scheme, Emacs Lisp, and Java. Perhaps the most valuable aspect of my work is that it gives a very preliminary glimpse---a prototype for a prototype---of how a powerful proof-finding engine like OTTER could be combined with software for preparing, managing and organizing input and output files to provide a powerful and user-friendly environment for painlessly writing, storing, retrieving, and creating proofs that are verified on an ultra-formal level. A desirable continuation of the present work would be to design and build a mathematical integrated development environment that would do all of these things.

The result that I verify is that, in TRC, a particular term push defines a bijection from the universe to the characteristic functions (in the sense of Holmes[2]; details follow in later sections). I do this by verifying three separate statements:

First: The function defined by push is one-to-one, or more formally, TRC proves that if push x = push y then x = y.
Second: The function defined by push x is always a characteristic function.
Third: For every characteristic function y there is some x such that push x = y.

The development consists of ten definitions of terms, and sixty-five proofs. I made hundreds or thousands of OTTER runs over a period of years, sometimes letting OTTER run continuously for weeks at a time, trying different ways of building up the definition of push, exploring different branches and collecting those definitions and proofs that seemed to be leading in the right direction. Desirable continuations of this work would be to further systematize and automate this work, and perhaps to somehow collect and analyze some sort of statistics on which approaches do and do not work. It would also be desirable to produce a novel proof of a more challenging result such as Specker's theorem.

General procedure used

In this document I used OTTER [1] to produce a semi-automated ultra-formal verification of a main technical lemma in Holmes [2]. To keep track of the main line of reasoning, I started all OTTER runs from a single, growing input file. This file started out with only the axioms of TRC from Holmes and grew according to the process (executed by hand) whose main loop is shown here:

A new definition is introduced as a demodulator of the form newName = term where newName is a new constant (an atomic term not beginning with u, v, w, x, y, or z), and term is a term of TRC built from the constants p1, p2, abst, eq and any constants that were introduced by definitions in earlier iterations of this loop. The term term was produced from a lambda-expression using a program I wrote to implement the abstraction algorithm given in Holmes [2]. In the present document, whenever such a definition is introduced, the actual demodulator input to OTTER is listed first, then an explanation of the rationale for the definition is given. I then repeat the following sub-loop to prove various properties of term:
1. Negate the property and add one or more clauses from the negation to the set of support, adding all other clauses from the negation to the usable list.
2. When a refutation has been found, add the positive statement of the property to the usable list for use in all future runs.
3. Immediately after the new usable item(s), insert a copy of OTTER's proof as well as an HTML link to the OTTER output file.

When the entire argument was complete, I added explanatory text to the input file and wrote a Java program to convert the input file into a collection of HTML files, automatically inserting links from each input clause in each proof to the place earlier in the file where the clause was first introduced, where either a proof is given or the clause is clearly identified as a definition or an axiom of TRC. This relieves human readers from part of the tedium of checking the generated proof. The end result is the present document, which is generated in both printable and web-browsable form.

Notations and Definitions

For technical reasons, three different notations are used for terms of TRC in this document. The reader will quickly get used to switching between them.

OTTER's default input notation, in which the basic operations of pairing, application and constant-function formation are written in the usual mathematical notation for functions. An example is a(a(a(abst,x),y),z) = a(a(x,k(z)),a(y,z)). This notation is used only in the direct listings of the OTTER input.
OTTER's bird_print output notation (so named presumably because combinators are described as "birds" in Ramond Smullyan's book To Mock a Mockingbird [7]). The bird_print notation is just the standard notation for combinatory logic, where the application operation is written simply as a blank space, and parentheses are dropped when possible using the convention of association to the left. An example is abst x y z = x k(z) (y z).
A LISP-like notation which uses the language of TRC together with syntax for two forms of lambda-expression. An example is (a (a (a abst x) y) z) = (a (a x (k z)) (a y z)). I format this notation using the LISP pretty-printing convention of aligning all the operands of a given operation at the same column. I use this notation for readability in long, complex terms and as input to my programs which use Holmes's abstraction-algorithm to eliminate the lambda syntax. This lambda-syntax is not part of the formal language I use in this document. It is always systematically eliminated using my implementation of Holmes's abstraction algorithm before an OTTER input file is generated.

An example of the third notation with the lambda syntax follows:

(lambda x
  (lambda y
    (lambda z
      (a (a x (k z))
	 (a y z)))))

Note that the two operands of the top-level a operator are aligned at the same column, making it easier to discern the structure of the term. The above lambda-term would be converted by my program to the atomic term abst.

We can think of abst as a function of three arguments x, y, and z at three different levels, level 2, level 1, and level 0 respectively. A level-2 object is thought of as a function from level-1 objects to level-1 objects, and a level-1 object is thought of as a function from level-0 objects to level-0 objects.

More formally, if x is a variable and S and T are terms, then

x occurs at level 0 in the atomic term x
if x occurs at level n in S then x occurs at level n + 1 in S T.
if x occurs at level n in T then x occurs at level n in S T.
if x occurs at level n in S then x occurs at level n - 1 in k(S).
if x occurs at level n in S or in T then x occurs at level n in pair(S,T).

Note that a variable may occur at more than one level in a term. In this case we say that the term is unstratified. The basic abstraction property [2] of TRC is that if x does not occur in T at any level other than zero, then there is a term (lambda x T) which when applied to S yields a term provably equal to the term T' obtained from T by substituting S for all occurrences of x.

We can use TRC's pairing facility to represent functions of multiple arguments where all arguments are at the same level. My programs allow a special lambda-notation for a function of two level-0 arguments. An example follows:

(lambda f
  (lambda (x y)
    (a eq (pair (a f x)
		(a f y)))))

Note that a single argument (like f in the above term) is not enclosed in parentheses, but a pair of arguments at the same level (like (x y) in the above term) is enclosed in parentheses. Every object in TRC can also be regarded as a pair of objects. The above lambda-term is actually just a shorthand for the one below, where the argument pair (x y) is replaced by u, while x is replaced by (a p1 u), and y is replaced by (a p2 u).

(lambda f
  (lambda u
    (a eq (pair (a f (a p1 u))
		(a f (a p2 u))))))

My program will eliminate the bound variables f, x, y, and u in the above terms, and both terms will be transformed into the following term built using only the four constants mentioned in the axioms of TRC:

(a (a abst (k (a abst (k eq))))
   (pair (a (a abst abst) 
	    (k p1)) 
	 (a (a abst abst) 
	    (k p2))))

In the online version of this thesis, you can click the button above to bring up an applet that I wrote in Java. The applet translates between the three notations described above. Any change you make in the input term is immediately reflected in the output. The applet follows the OTTER convention of treating atomic terms as variables if their names begin with u, v, w, x, y, or z. The text box on the right-hand side of the applet window lists the free variables beginning with u, v, w, x, y, or z and the levels at which they occur. Check both the reduce and factor checkboxes to simplify the answers using axioms of TRC. The pop-up menu and command button let you insert the definition of push, or of other terms used in the definition of push, into the input.

Try pasting the following examples into the applet, then try your own variations. Notice the levels of the variables, listed on the right-hand side of the applet window.

In LISP input mode:
- (k (a x y))
- (lambda x (k (a x y)))
- (lambda y (k (a x y)))
- (lambda x z)
- (lambda (f g) (lambda x (a eq (pair (a f x) (a g x)))))
- (lambda x (lambda y (lambda z (a (a x (k z)) (a y z)))))
- (lambda (x y) (pair (pair y x) (pair y x)))
- (lambda (x y) (a eq (pair x y)))
In Bird input mode:
- abst abst x y z (check the "Reduce" checkbox)
- x y z (x y z)
- eq (pair(p1,p2) x)

OTTER settings

include(quiet).

set(unit_deletion).           %
set(ur_res).                  % 
set(para_into).               %   
set(para_from).               %  cancelled at one point
set(back_demod).              %
assign(pick_given_ratio,3).
assign(max_weight,1000).
assign(max_proofs,1).

set(interactive_given).

set(control_memory).

In a first attempt at a proof I generally used the above options as my default settings for OTTER. I always turned off the interactive selection of given clauses by entering 0 immediately. If the search failed, I used interactive_given to help me debug the input file and the search options. All of the final proofs in this document were obtained with no human intervention in the selection of given clauses.

The included file quiet contains the following commands:

clear(print_kept).
clear(print_new_demod).
clear(print_back_sub).
clear(print_back_demod).
assign(max_mem,24000).
set(bird_print).

These prevent the output file from being too big, limit the main memory usage, and cause the output to be printed in an easier-to-read standard notation for combinatory logic.

Various combinations of the following "emergency measures" were tried whenever the first attempt at proof failed.

Emergency measures

When attempting a proof, at first I kept all of the following lines commented out. If the initial search failed, I uncommented various combinations of these.

set(para_ones_rule).
set(para_into_units_only).    % has been quite useful
set(para_from_units_only).   
set(interactive_given).
set(knuth_bendix).           
assign(max_literals,2).
set(hyper_res).
set(neg_hyper_res).

include(demodulators).
include(equadulators).

The file demodulators was usually included when proving the basic properties of a new definition. It consists of all axioms of TRC that would be considered as reduction rules in combinatory logic. They are as follows. All of them are placed in the demodulators list. The inclusion of these demodulators causes OTTER to perform long chains of reductions in a single proof step, but the proof steps remain easy to verify with the help of a pencil and paper.

a(k(x),y) = x.
a(p1,pair(x,y)) = x.
a(p2,pair(x,y)) = y.
a(pair(x,y),z) = pair(a(x,z),a(y,z)).
pair(a(p1,x),a(p2,x)) = x.
a(a(a(abst,x),y),z) = a(a(x,k(z)),a(y,z)).
a(eq,pair(x,x)) = p1.

The file equadulators came in to play only once. In OTTER, not only terms but also literals (atomic clauses) can be rewritten using demodulators. I called the following equadulators, for equality demodulators. Its contents, in the demodulators list, are as follows:

(k(x) = k(y)) = (x = y).
(pair(x,y) = pair(x,z)) = (y = z).
(pair(x,z) = pair(y,z)) = (x = y).
(a(eq,pair(x,y)) = p1) = (x = y).

Only the last one of these "equadulators" ever came into play.

Reflexive property of equality

The reflexive axiom for equality must be present in order to get refutations using paramodulation.

list(usable).
x=x.  (reference number 1)
end_of_list.

TRC Basic Axioms

Below are the basic axioms of TRC [2].

list(usable).

a(k(x),y) = x.  (reference number 2)

a(p1,pair(x,y)) = x.  (reference number 3)
a(p2,pair(x,y)) = y.  (reference number 4)

a(pair(x,y),z) = pair(a(x,z),a(y,z)).  (reference number 5)

pair(a(p1,x),a(p2,x)) = x.  (reference number 6)

a(a(a(abst,x),y),z) = a(a(x,k(z)),a(y,z)).  (reference number 7)

x != y | a(eq,pair(x,y)) = p1.  (reference number 8)
x  = y | a(eq,pair(x,y)) = p2.  (reference number 9)

x = y | a(x,noteq(x,y)) != a(y,noteq(x,y)).  (reference number 10)

p1 != p2.  (reference number 11)

end_of_list.

The first clause says that for every object, there is a corresponding constant function. The next two assert the existence of a pairing function (which is not a combinator) and projections (which are combinators). The fourth clause describes how a pair behaves as a function. The fifth clause says that everything is a pair, and together with the fourth implies that pair(p1, p2) is an identity combinator, in fact the identity combinator if we also consider the axiom of extensionality below. The sixth clause defines the action of the combinator abst which provides stratified combinatory completeness. The seventh and eighth clauses postulate the existence of eq, the characteristic function of equality. The ninth clause uses a skolem function noteq to express the axiom of extensionality, which says that if two combinators represent the same function, that is, given identical inputs they always produce identical outputs, then they are equal. The last clause precludes a trivial universe consisting of a single combinator.

At the outset I added some redundant versions of some of the above axioms in the hope that they would help OTTER to find proofs. The following two clauses follow so immediately from the above that we do not bother including the one-line OTTER proofs.

list(usable).
p2 != p1.  (reference number 12)
a(eq,pair(x,x)) = p1.  (reference number 13)
end_of_list.

Because the pairing function is surjective, anything that can be said about pairs can be recast into an equivalent statement about the projections, and vice-versa. In the following two clauses, I restate the definition of eq in terms of projections.

list(usable).
a(p1,x) != a(p2,x) | a(eq,x) = p1.  (reference number 14)
end_of_list.

Proof of `a(p1,x) != a(p2,x) | a(eq,x) = p1.`

Since this is the first OTTER proof presented in this document, I'll explain the procedure I use to get proofs. In OTTER any atomic term beginning with u, v, w, x, y, z is by default treated as a (universally quantified) variable, while any atomic term beginning with any other letter is treated as a constant. Most of the assertions we need to prove are universal, like the present one, which is asserted for all x. We need to refute the negation of this universal assertion. The negation asserts the existence of some constant for which the universal assertion fails. Thus in the set-of-support clauses below, I change x to bad, which, beginning with b, is treated as a constant. The same convention is followed throughout this document: if a clause has only one universally quantified variable, I replace this variable with bad in the clauses to be refuted. If a clause has more than one universally quantified variable, I generally prefix the names of the variables with bad, so x and y become badx and bady.

list(sos).
a(p1,bad) = a(p2,bad).
a(eq,bad) != p1.
end_of_list.

As Art Quaife [4] points out, when the statement to be refuted contains no variables, one can restrict the search tremendously by using a weight template to immediately discard all clauses with variables.

weight_list(pick_and_purge).
weight(x,100).
end_of_list.

The proofs in this document are automatically processed by my Java application which adds a hypertext link from each input clause in a proof (OTTER marks input clauses with the empty justification [ ]) to the place where it was introduced earlier in the input file. This makes it easy to find the proof of each input clause. In the present proof the input clauses are axioms, so the link refers to the section where the axioms of TRC were introduced. Input clauses containing the string "bad" are automatically marked "assumption to refute".

----> UNIT CONFLICT at   0.10 sec ----> 46 [binary,44.1,20.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof



5 [reference 6] pair(p1 x,p2 x)=x.
15 [reference 8] x!=y|eq pair(x,y) =p1.
19 [assumption to refute] p1 bad=p2 bad.
20 [assumption to refute] eq bad!=p1.
44 [ur,19,15,demod,5] eq bad=p1.
46 [binary,44.1,20.1] $F.

list(usable).
a(p1,x) = a(p2,x) | a(eq,x) = p2.  (reference number 15)
end_of_list.

Proof of `a(p1,x) = a(p2,x) | a(eq,x) = p2.`

----> UNIT CONFLICT at   0.12 sec ----> 51 [binary,49.1,21.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof



5 [reference 6] pair(p1 x,p2 x)=x.
16 [reference 9] x=y|eq pair(x,y) =p2.
20 [assumption to refute] p1 bad!=p2 bad.
21 [assumption to refute] eq bad!=p2.
49 [ur,20,16,demod,5] eq bad=p2.
51 [binary,49.1,21.1] $F.

The term `isp1` is a projection from functions to characteristic functions.

OTTER has no trouble at all verifying the basic properties of this term. Of course, we would like OTTER to actually find the term isp1 using an answer literal, but it seems to have trouble finding terms of even this modest complexity, at least with every approach that I have tried.

Definition of `isp1`


list(demodulators).
isp1 = a(a(abst,k(a(abst,k(eq)))),pair(k(k(p1)),pair(p1,p2))).  (reference number 16)
end_of_list.





 Click button to load the definition of isp1 into TRC applet.

The combinator isp1 is defined as follows: isp1 x y = p1 if x y = p1, and isp1 x y = p2 if x y != p1.

The combinator isp1 is a natural projection from all the functions to just the characteristic functions. It is defined by the stratified lambda-term

(lambda x
  (lambda y
    (a eq (pair p1 
                (a x y)))))

Basic defining properties of `isp1`

The following clause says that if x y = p1 then isp1 x y = p1.

list(usable).
a(x,y) != p1 | a(a(isp1,x),y) = p1.  (reference number 17)
end_of_list.

Proof of `a(x,y) != p1 | a(a(isp1,x),y) = p1.`

Note the use of the literal p in lines 13 and 15 of the proof below. This is a trick (or "kludge") due to Hart and Kunen [8]. Since p occurs only in these two lines, the two lines are for the purposes of this proof equivalent to the equation isp1 bad1 bad2 != p1. The purpose of this trick is to force immediate demodulation of this equation without forcing demodulation of the other input clauses. Thus isp1 will immediately be replaced with its definition, and isp1 bad1 bad2 will be reduced as much as possible.

Also, a program was used to generate weights, giving every subterm of isp1 a weight of 1. This and related automatically generated weights are used throughout the development. The related weighting methods, not used for isp1, are to apply a lambda-term to a variable x, reduce it, and weight all subterms with weight 1. If a lambda term has the form (lambda (x y) ...) then it is additionally applied to pair(x,x). This process is carried out for all subterms of the original definition of the form (lambda ...). The resulting weights are duplicated with x replaced by the template $(1) which matches any term substituted for x.

----> UNIT CONFLICT at   1.39 sec ----> 299 [binary,298.1,14.1] $F.

Length of proof is 12.  Level of proof is 12.

Proof



2 [reference 2] k(x) y=x.
5 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 6] pair(p1 x,p2 x)=x.
7 [reference 7] abst x y z=x k(z) (y z).
8 [reference 8] x!=y|eq pair(x,y) =p1.
12 [reference 16] isp1=abst k(abst k(eq)) pair(k(k(p1)),pair(p1,p2)).
13 [assumption to refute] p.
14 [assumption to refute] bad1 bad2=p1.
15 [assumption to refute] -p|isp1 bad1 bad2 !=p1.
26 [ur,15,13,demod,12] abst k(abst k(eq)) pair(k(k(p1)),pair(p1,p2)) bad1 bad2!=p1.
37 [para_into,26.1.1.1,7.1.1] k(abst k(eq)) k(bad1) (pair(k(k(p1)),pair(p1,p2)) bad1) bad2!=p1.
88 [para_into,37.1.1.1.1,2.1.1] abst k(eq) (pair(k(k(p1)),pair(p1,p2)) bad1) bad2!=p1.
98 [para_into,88.1.1,7.1.1] k(eq) k(bad2) (pair(k(k(p1)),pair(p1,p2)) bad1 bad2)!=p1.
112 [para_into,98.1.1.1,2.1.1] eq (pair(k(k(p1)),pair(p1,p2)) bad1 bad2)!=p1.
121 [para_into,112.1.1.2.1,5.1.1] eq (pair(k(k(p1)) bad1,pair(p1,p2) bad1) bad2)!=p1.
207 [para_into,121.1.1.2.1.1,2.1.1] eq (pair(k(p1),pair(p1,p2) bad1) bad2)!=p1.
217 [para_into,207.1.1.2,5.1.1] eq pair(k(p1) bad2,pair(p1,p2) bad1 bad2)!=p1.
242 [ur,217,8,flip.1] pair(p1,p2) bad1 bad2!=k(p1) bad2.
254 [para_into,242.1.2,2.1.1] pair(p1,p2) bad1 bad2!=p1.
259 [para_into,254.1.1.1,5.1.1] pair(p1 bad1,p2 bad1) bad2!=p1.
298 [para_into,259.1.1.1,6.1.1] bad1 bad2!=p1.
299 [binary,298.1,14.1] $F.

The following clause says that if x y != p1 then isp1 x y = p2.

list(usable).
a(x,y) = p1 | a(a(isp1,x),y) = p2.  (reference number 18)
end_of_list.

Proof of `a(x,y) = p1 | a(a(isp1,x),y) = p2.`

----> UNIT CONFLICT at   0.11 sec ----> 56 [binary,54.1,22.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof



1 [reference 2] k(x) y=x.
4 [reference 5] pair(x,y) z=pair(x z,y z).
5 [reference 6] pair(p1 x,p2 x)=x.
6 [reference 7] abst x y z=x k(z) (y z).
16 [reference 9] x=y|eq pair(x,y) =p2.
19 [reference 16] isp1=abst k(abst k(eq)) pair(k(k(p1)),pair(p1,p2)).
21 [assumption to refute] p.
22 [assumption to refute] bad1 bad2!=p1.
23 [assumption to refute] -p|isp1 bad1 bad2 !=p2.
29 [ur,23,21,demod,19,6,1,4,1,4,5,6,1,4,1] eq pair(p1,bad1 bad2)!=p2.
54 [ur,29,16,flip.1] bad1 bad2=p1.
56 [binary,54.1,22.1] $F.

The combinator `isp1` is a projection from functions to characteristic functions.

Whenever I introduced a new combinator leading toward push, I started by proving a set of clauses that define its basic behavior. In most cases, by extensionality, these clauses uniquely determine the combinator. That is, in most cases, the first set of clauses that I proved completely specifies the behavior of the combinator.

After proving the basic defining clauses, I tried to think of other natural, simple facts about the term, in the hope that these would come in handy for later proofs. One such clause follows. This particular clause did not prove to be crucial to the subsequent argument.

Once the basic defining clauses have been proved, I remove the demodulator that eliminates the name of the new combinator in favor of its definition. Further properties are then proved from the basic defining clauses.

list(usable).
a(isp1,a(isp1,x)) = a(isp1,x).  (reference number 19)
end_of_list.

list(demodulators).
a(isp1,a(isp1,x)) = a(isp1,x).  (reference number 20)
end_of_list.

First proof of `a(isp1,a(isp1,x)) = a(isp1,x).`

-----> EMPTY CLAUSE at  28.66 sec ----> 3055 [back_demod,2051,demod,3047,7,unit_del,33,3048] $F.

Length of proof is 8.  Level of proof is 3.

Proof



7 [reference 13] eq pair(x,x)=p1.
16 [reference 9] x=y|eq pair(x,y) =p2.
17 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
18 [reference 11] p1!=p2.
19 [reference 17] x y!=p1|isp1 x y =p1.
20 [reference 18] x y=p1|isp1 x y =p2.
21 [assumption to refute] isp1 (isp1 bad)!=isp1 bad.
22 [ur,21,17] isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad)!=isp1 bad noteq(isp1 (isp1 bad),isp1 bad).
24,23 [ur,21,16] eq pair(isp1 (isp1 bad),isp1 bad)=p2.
33 [para_from,23.1.2,18.1.2,demod,24,flip.1] p2!=p1.
50 [ur,22,16] eq pair(isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad),isp1 bad noteq(isp1 (isp1 bad),isp1 bad))=p2.
59 [para_into,22.1.1,19.2.1,flip.1] isp1 bad noteq(isp1 (isp1 bad),isp1 bad)!=p1.
2051 [para_into,50.1.1.2.2,20.2.1] eq pair(isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad),p2)=p2|bad noteq(isp1 (isp1 bad),isp1
 bad) =p1.
3047,3046 [ur,59,20] isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad)=p2.
3048 [ur,59,19] bad noteq(isp1 (isp1 bad),isp1 bad)!=p1.
3055 [back_demod,2051,demod,3047,7,unit_del,33,3048] $F.

I noticed that the first proof was a bit long and that the use of the term eq in the proof seemed unecessary. I removed the axioms defining eq and ran OTTER. This time it took OTTER longer to find a proof, but when it did find the proof, it was shorter.

Second proof of `a(isp1,a(isp1,x)) = a(isp1,x).`

----> UNIT CONFLICT at 178.00 sec ----> 6295 [binary,6294.1,8.1] $F.

Length of proof is 5.  Level of proof is 4.

Proof



8 [reference 1] x=x.
15 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
17 [reference 17] x y!=p1|isp1 x y =p1.
18 [reference 18] x y=p1|isp1 x y =p2.
19 [assumption to refute] isp1 (isp1 bad)!=isp1 bad.
20 [ur,19,15] isp1 (isp1 bad) noteq(isp1 (isp1 bad),isp1 bad)!=isp1 bad noteq(isp1 (isp1 bad),isp1 bad).
74 [para_into,20.1.1,18.2.1,flip.1] isp1 bad noteq(isp1 (isp1 bad),isp1 bad)!=p2|isp1 bad noteq(isp1 (isp1 bad),isp1 bad) =p1.
76 [para_into,20.1.1,17.2.1,flip.1] isp1 bad noteq(isp1 (isp1 bad),isp1 bad)!=p1.
6168,6167 [para_into,74.1.1,18.2.1,unit_del,8,76] bad noteq(isp1 (isp1 bad),isp1 bad)=p1.
6294 [ur,76,17,demod,6168] p1!=p1.
6295 [binary,6294.1,8.1] $F.

The term `notp1` finds complements of characteristic functions.

Definition of `notp1`


list(demodulators).
notp1 = a(a(abst,k(a(abst,k(eq)))),pair(k(k(p2)),isp1)).  (reference number 21)
end_of_list.





 Click button to load the definition of notp1 into TRC applet.

The combinator notp1 is defined as follows: notp1 x y = p1 if x y != p1, and notp1 x y = p2 if x y = p1.

The combinator notp1 sends the characteristic function of a set to the characteristic function of the complement of that set. It is derived from the following lambda-term:

(lambda x
  (lambda y
    (a eq (pair p2
                (a (a isp1 x) y)))))

Basic defining clauses

list(usable).
a(x,y) = p1 | a(a(notp1,x),y) = p1.  (reference number 22)
end_of_list.

Proof of `a(x,y) = p1 | a(a(notp1,x),y) = p1.`

----> UNIT CONFLICT at   0.07 sec ----> 40 [binary,39.1,8.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof



1 [reference 2] k(x) y=x.
4 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 7] abst x y z=x k(z) (y z).
7 [reference 13] eq pair(x,x)=p1.
8 [reference 1] x=x.
20 [reference 18] x y=p1|isp1 x y =p2.
23 [reference 21] notp1=abst k(abst k(eq)) pair(k(k(p2)),isp1).
24 [assumption to refute] bad1 bad2!=p1.
25 [assumption to refute] notp1 bad1 bad2!=p1.
27,26 [ur,24,20] isp1 bad1 bad2=p2.
39 [para_into,25.1.1.1.1,23.1.1,demod,6,1,4,1,6,1,4,1,27,7] p1!=p1.
40 [binary,39.1,8.1] $F.

list(usable).
a(x,y) != p1 | a(a(notp1,x),y) = p2.  (reference number 23)
end_of_list.

Proof of `a(x,y) != p1 | a(a(notp1,x),y) = p2.`

----> UNIT CONFLICT at   0.10 sec ----> 67 [binary,66.1,8.1] $F.

Length of proof is 5.  Level of proof is 4.

Proof



1 [reference 2] k(x) y=x.
4 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 7] abst x y z=x k(z) (y z).
8 [reference 1] x=x.
16 [reference 9] x=y|eq pair(x,y) =p2.
18 [reference 11] p1!=p2.
19 [reference 17] x y!=p1|isp1 x y =p1.
23 [reference 21] notp1=abst k(abst k(eq)) pair(k(k(p2)),isp1).
25 [assumption to refute] bad1 bad2=p1.
26 [assumption to refute] notp1 bad1 bad2!=p2.
28,27 [ur,25,19] isp1 bad1 bad2=p1.
42 [para_from,25.1.2,18.1.1] bad1 bad2!=p2.
50 [para_into,42.1.1,25.1.1,flip.1] p2!=p1.
55,54 [ur,50,16] eq pair(p2,p1)=p2.
66 [para_into,26.1.1.1.1,23.1.1,demod,6,1,4,1,6,1,4,1,28,55] p2!=p2.
67 [binary,66.1,8.1] $F.

Two simple properties

The combinator notp1 has no fixed point.

list(usable).
a(notp1,x) != x.  (reference number 24)     %    (not used in later proofs)
end_of_list.

Proof of `a(notp1,x) != x.`

----> UNIT CONFLICT at   0.06 sec ----> 47 [binary,46.1,8.1] $F.

Length of proof is 4.  Level of proof is 3.

Proof



8 [reference 1] x=x.
18 [reference 11] p1!=p2.
23 [reference 22] x y=p1|notp1 x y =p1.
24 [reference 23] x y!=p1|notp1 x y =p2.
25 [assumption to refute] notp1 bad=bad.
32 [para_from,25.1.1,24.2.1.1] bad x!=p1|bad x =p2.
34,33 [para_from,25.1.1,23.2.1.1] bad x=p1.
41,40 [back_demod,32,demod,34,34,unit_del,8,flip.1] p2=p1.
46 [back_demod,18,demod,41] p1!=p1.
47 [binary,46.1,8.1] $F.

Applying notp1 to any combinator yields a characteristic function.

list(usable).
a(a(notp1,x),y) = p1 | a(a(notp1,x),y) = p2.  (reference number 25)
end_of_list.

Proof of `a(a(notp1,x),y) = p1 | a(a(notp1,x),y) = p2.`

----> UNIT CONFLICT at   0.07 sec ----> 58 [binary,56.1,27.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof



23 [reference 22] x y=p1|notp1 x y =p1.
24 [reference 23] x y!=p1|notp1 x y =p2.
26 [assumption to refute] notp1 bad1 bad2!=p1.
27 [assumption to refute] notp1 bad1 bad2!=p2.
28 [ur,26,23] bad1 bad2=p1.
56 [ur,28,24] notp1 bad1 bad2=p2.
58 [binary,56.1,27.1] $F.

Algebra of notp1 and isp1 under composition

list(usable).
a(notp1,a(notp1,x)) = a(isp1,x).  (reference number 26)
end_of_list.

list(demodulators).
a(notp1,a(notp1,x)) = a(isp1,x).  (reference number 27)
end_of_list.

Proof of `a(notp1,a(notp1,x)) = a(isp1,x).`

-----> EMPTY CLAUSE at  77.70 sec ----> 5386 [back_demod,2319,demod,4557,4563,unit_del,94,94] $F.

Length of proof is 15.  Level of proof is 5.

Proof



8 [reference 1] x=x.
16 [reference 9] x=y|eq pair(x,y) =p2.
17 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
18 [reference 11] p1!=p2.
19 [reference 17] x y!=p1|isp1 x y =p1.
20 [reference 18] x y=p1|isp1 x y =p2.
23 [reference 22] x y=p1|notp1 x y =p1.
24 [reference 23] x y!=p1|notp1 x y =p2.
26 [reference 25] notp1 x y=p1|notp1 x y =p2.
27 [assumption to refute] notp1 (notp1 bad)!=isp1 bad.
28 [ur,27,17] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)!=isp1 bad noteq(notp1 (notp1 bad),isp1 bad).
30,29 [ur,27,16] eq pair(notp1 (notp1 bad),isp1 bad)=p2.
64 [para_into,28.1.1,26.2.1,flip.1] isp1 bad noteq(notp1 (notp1 bad),isp1 bad)!=p2|notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad) =p1.
65 [para_into,28.1.1,26.1.1,flip.1] isp1 bad noteq(notp1 (notp1 bad),isp1 bad)!=p1|notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad) =p2.
66 [para_into,28.1.1,24.2.1,flip.1] isp1 bad noteq(notp1 (notp1 bad),isp1 bad)!=p2|notp1 bad noteq(notp1 (notp1 bad),isp1 bad) !=p1.
83 [para_into,28.1.2,19.2.1] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)!=p1|bad noteq(notp1 (notp1 bad),isp1 bad) !=p1.
94 [para_from,29.1.2,18.1.2,demod,30,flip.1] p2!=p1.
628 [para_into,64.1.1,20.2.1,unit_del,8] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)=p1|bad noteq(notp1 (notp1 bad),isp1 bad) =p1.
752 [para_into,65.1.1,19.2.1,unit_del,8] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)=p2|bad noteq(notp1 (notp1 bad),isp1 bad) !=p1.
867 [para_into,83.1.1,23.2.1,unit_del,8] bad noteq(notp1 (notp1 bad),isp1 bad)!=p1|notp1 bad noteq(notp1 (notp1 bad),isp1 bad) =p1.
2319 [para_from,628.2.1,24.1.1,unit_del,8] notp1 bad noteq(notp1 (notp1 bad),isp1 bad)=p2|notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad) =p1.
4375 [para_into,66.2.1,23.2.1,unit_del,8] isp1 bad noteq(notp1 (notp1 bad),isp1 bad)!=p2|bad noteq(notp1 (notp1 bad),isp1 bad) =p1.
4432,4431 [para_into,4375.1.1,20.2.1,unit_del,8] bad noteq(notp1 (notp1 bad),isp1 bad)=p1.
4557,4556 [back_demod,867,demod,4432,unit_del,8] notp1 bad noteq(notp1 (notp1 bad),isp1 bad)=p1.
4563,4562 [back_demod,752,demod,4432,unit_del,8] notp1 (notp1 bad) noteq(notp1 (notp1 bad),isp1 bad)=p2.
5386 [back_demod,2319,demod,4557,4563,unit_del,94,94] $F.

list(usable).
a(notp1,a(isp1,x)) = a(notp1,x).  (reference number 28)
end_of_list.

list(demodulators).
a(notp1,a(isp1,x)) = a(notp1,x).  (reference number 29)
end_of_list.

Proof of `a(notp1,a(isp1,x)) = a(notp1,x).`

----> UNIT CONFLICT at   1.93 sec ----> 820 [binary,818.1,806.1] $F.

Length of proof is 6.  Level of proof is 5.

Proof



14 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
16 [reference 17] x y!=p1|isp1 x y =p1.
17 [reference 18] x y=p1|isp1 x y =p2.
23 [reference 25] notp1 x y=p1|notp1 x y =p2.
24 [reference 26] notp1 (notp1 x)=isp1 x.
25 [assumption to refute] notp1 (isp1 bad)!=notp1 bad.
26 [ur,25,14] notp1 (isp1 bad) noteq(notp1 (isp1 bad),notp1 bad)!=notp1 bad noteq(notp1 (isp1 bad),notp1 bad).
36 [para_into,26.1.1.1.2,24.1.2] notp1 (notp1 (notp1 bad)) noteq(notp1 (isp1 bad),notp1 bad)!=notp1 bad noteq(notp1 (isp1 bad),n
otp1 bad).
746 [para_into,36.1.1.1,24.1.1] isp1 (notp1 bad) noteq(notp1 (isp1 bad),notp1 bad)!=notp1 bad noteq(notp1 (isp1 bad),notp1 bad).
794 [para_into,746.1.1,16.2.1,flip.1] notp1 bad noteq(notp1 (isp1 bad),notp1 bad)!=p1.
806 [para_into,746.1.2,23.2.1,unit_del,794] isp1 (notp1 bad) noteq(notp1 (isp1 bad),notp1 bad)!=p2.
818 [ur,794,17] isp1 (notp1 bad) noteq(notp1 (isp1 bad),notp1 bad)=p2.
820 [binary,818.1,806.1] $F.

list(usable).
a(isp1,a(notp1,x)) = a(notp1,x).  (reference number 30)     %    (not used in later proofs)
end_of_list.

list(demodulators).
a(isp1,a(notp1,x)) = a(notp1,x).  (reference number 31)     %    (not used in later proofs)
end_of_list.

Proof of `a(isp1,a(notp1,x)) = a(notp1,x).`

----> UNIT CONFLICT at   0.10 sec ----> 57 [binary,56.1,25.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof



24 [reference 26] notp1 (notp1 x)=isp1 x.
25 [reference 28] notp1 (isp1 x)=notp1 x.
26 [assumption to refute] isp1 (notp1 bad)!=notp1 bad.
31 [para_into,26.1.1,24.1.2] notp1 (notp1 (notp1 bad))!=notp1 bad.
56 [para_into,31.1.1.2,24.1.1] notp1 (isp1 bad)!=notp1 bad.
57 [binary,56.1,25.1] $F.

The term `charq` is the characteristic function of the set of characteristic functions.

Definition of `charq`

list(demodulators).
charq = a(a(abst,k(eq)),pair(pair(p1,p2),isp1)).  (reference number 32)
end_of_list.





 Click button to load the definition of charq into TRC applet.

By definition, f is a characterstic function if for all x, either f x = p1 or f x = p2. One can write a very simple predicate for the set of all characteristic functions by noting that f is a characteristic function iff it is a fixed point for isp1, i. e. if isp1 f = f. This definition is expressed by the following stratified lambda-term:

(lambda f
  (a eq (pair f
              (a isp1 f))))

I prove here only the basic defining properties of charq. The following clause says that charq f = p2 unless f is a characteristic function, i. e. if f is not a characteristic function then charq f = p2.

list(usable).
a(charq,xf) = p2 | a(xf,x) = p1 | a(xf,x) = p2.  (reference number 33)
end_of_list.

Proof of `a(charq,xf) = p2 | a(xf,x) = p1 | a(xf,x) = p2.`

----> UNIT CONFLICT at   0.12 sec ----> 79 [binary,77.1,34.1] $F.

Length of proof is 4.  Level of proof is 3.

Proof



1 [reference 2] k(x) y=x.
4 [reference 5] pair(x,y) z=pair(x z,y z).
5 [reference 6] pair(p1 x,p2 x)=x.
6 [reference 7] abst x y z=x k(z) (y z).
16 [reference 9] x=y|eq pair(x,y) =p2.
20 [reference 18] x y=p1|isp1 x y =p2.
30 [reference 32] charq=abst k(eq) pair(pair(p1,p2),isp1).
31 [assumption to refute] -p.
32 [assumption to refute] p|charq badf !=p2.
33 [assumption to refute] badf badx!=p1.
34 [assumption to refute] badf badx!=p2.
35 [ur,32,31,demod,30,6,1,4,4,5] eq pair(badf,isp1 badf)!=p2.
44 [ur,33,20] isp1 badf badx=p2.
73,72 [ur,35,16,flip.1] isp1 badf=badf.
77 [back_demod,44,demod,73] badf badx=p2.
79 [binary,77.1,34.1] $F.

The following pair of clauses express the converse: charq f = p1 unless f fails to be a characteristic function. To avoid introducing a new Skolem function for the witness x for f's failure to be a characteristic function, I let OTTER find a witness in terms of the already-present Skolem function noteq. I did that by using OTTER's answer literal feature.

The direct reading of the clauses, "charq f = p1 unless f fails to be a characteristic function," can be rephrased as "If f is a characteristic function, then charq f = p1

list(usable).
a(charq,xf) = p1 | a(xf,noteq(a(isp1,xf),xf)) != p1.  (reference number 34)
a(charq,xf) = p1 | a(xf,noteq(a(isp1,xf),xf)) != p2.  (reference number 35)
end_of_list.

Proof that if `f` is a characteristic function, then `charq f = p1`

----> UNIT CONFLICT at  66.78 sec ----> 5520 [binary,5519.1,4556.1] $ans(noteq(isp1 badf,badf)).

Length of proof is 8.  Level of proof is 6.

Proof



1 [reference 2] k(x) y=x.
4 [reference 5] pair(x,y) z=pair(x z,y z).
5 [reference 6] pair(p1 x,p2 x)=x.
6 [reference 7] abst x y z=x k(z) (y z).
15 [reference 8] x!=y|eq pair(x,y) =p1.
16 [reference 9] x=y|eq pair(x,y) =p2.
17 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
19 [reference 17] x y!=p1|isp1 x y =p1.
20 [reference 18] x y=p1|isp1 x y =p2.
30 [reference 32] charq=abst k(eq) pair(pair(p1,p2),isp1).
32 [assumption to refute] p.
33 [assumption to refute] -p|charq badf !=p1.
34 [assumption to refute] badf x=p1|badf x =p2|$ans(x).
35 [ur,33,32,demod,30,6,1,4,4,5] eq pair(badf,isp1 badf)!=p1.
56 [ur,35,15,flip.1] isp1 badf!=badf.
65 [para_into,35.1.1,16.2.1,unit_del,56] p2!=p1.
75 [para_into,65.1.2,20.1.2,flip.1] x y!=p2|isp1 x y =p2.
78 [ur,56,17] isp1 badf noteq(isp1 badf,badf)!=badf noteq(isp1 badf,badf).
4548 [para_into,78.1.1,75.2.1,flip.1] badf noteq(isp1 badf,badf)!=p2.
4556 [para_into,78.1.1,19.2.1,flip.1] badf noteq(isp1 badf,badf)!=p1.
5519 [ur,4548,34] badf noteq(isp1 badf,badf)=p1|$ans(noteq(isp1 badf,badf)).
5520 [binary,5519.1,4556.1] $ans(noteq(isp1 badf,badf)).

The term `setof` finds the characteristic function of a given function.

Definition of `setof`

list(demodulators).
setof = a(a(abst,k(a(abst,k(eq)))),pair(k(p2),a(a(abst,abst),k(p1)))).  (reference number 36)
end_of_list.





 Click button to load the definition of setof into TRC applet.

The combinator setof sends each function to the characteristic function of its graph, i. e. setof f pair(x, y) = p1 if f x = y, and otherwise setof f pair(x, y) = p2. This definition is expressed by the following stratified lambda-term:

(lambda f
  (lambda (x y)
    (a eq (pair y
                (a f x)))))

Basic defining clauses (2 versions)

The basic defining conditions for setof can be expressed in two alternate, equivalent ways:

setof f pair(x,y) = p1 iff f x = y, otherwise setof f pair(x,y) = p2.
setof f z = p1 iff p2 z = f (p1 z), otherwise setof f z = p2.

As one would expect, once the first pair of clauses is proved, the second pair, being a simple reformulation of the first, have very short proofs.

Defining clauses for `setof` using `pair`

list(usable).
a(a(setof,xf),pair(x,a(xf,x))) = p1.  (reference number 37)
end_of_list.

Proof of `a(a(setof,xf),pair(x,a(xf,x))) = p1.`

----> UNIT CONFLICT at   0.08 sec ----> 37 [binary,36.1,8.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 7] abst x y z=x k(z) (y z).
7 [reference 13] eq pair(x,x)=p1.
8 [reference 1] x=x.
33 [reference 36] setof=abst k(abst k(eq)) pair(k(p2),abst abst k(p1)).
34 [assumption to refute] p.
35 [assumption to refute] -p|setof badf pair(badx,badf badx) !=p1.
36 [ur,35,34,demod,33,6,1,4,1,6,1,6,1,4,3,6,1,2,7] p1!=p1.
37 [binary,36.1,8.1] $F.

list(usable).
a(a(setof,xf),pair(x,y)) = p2 | a(xf,x) = y.  (reference number 38)
end_of_list.

Proof of `a(a(setof,xf),pair(x,y)) = p2 | a(xf,x) = y.`

----> UNIT CONFLICT at   0.13 sec ----> 60 [binary,58.1,36.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 7] abst x y z=x k(z) (y z).
16 [reference 9] x=y|eq pair(x,y) =p2.
32 [reference 36] setof=abst k(abst k(eq)) pair(k(p2),abst abst k(p1)).
34 [assumption to refute] p.
35 [assumption to refute] -p|setof badf pair(badx,bady) !=p2.
36 [assumption to refute] badf badx!=bady.
37 [ur,35,34,demod,32,6,1,4,1,6,1,6,1,4,3,6,1,2] eq pair(bady,badf badx)!=p2.
58 [ur,37,16,flip.1] badf badx=bady.
60 [binary,58.1,36.1] $F.

Defining clauses for `setof` using `p1` and `p2`.

list(usable).
a(p2,xy) != a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p1.  (reference number 39)
end_of_list.

Proof of `a(p2,xy) != a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p1.`

----> UNIT CONFLICT at   0.16 sec ----> 107 [binary,105.1,34.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof



5 [reference 6] pair(p1 x,p2 x)=x.
32 [reference 37] setof xf pair(x,xf x)=p1.
34 [assumption to refute] setof badf badp!=p1.
35 [assumption to refute] p2 badp=badf (p1 badp).
105 [para_from,35.1.2,32.1.1.2.2,demod,5] setof badf badp=p1.
107 [binary,105.1,34.1] $F.

list(usable).
a(p2,xy) = a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p2.  (reference number 40)
end_of_list.

Proof of `a(p2,xy) = a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p2.`

----> UNIT CONFLICT at   0.34 sec ----> 226 [binary,224.1,35.1] $F.

Length of proof is 3.  Level of proof is 3.

Proof



5 [reference 6] pair(p1 x,p2 x)=x.
33 [reference 38] setof xf pair(x,y)=p2|xf x =y.
35 [assumption to refute] setof badf badp!=p2.
36 [assumption to refute] p2 badp!=badf (p1 badp).
38,37 [ur,35,33] setof (setof badf) pair(badp,p2)=p2.
181 [para_from,37.1.2,36.1.1.1,demod,38,flip.1] badf (p1 badp)!=p2 badp.
224 [ur,181,33,demod,5] setof badf badp=p2.
226 [binary,224.1,35.1] $F.

Important properties of `setof`

Holmes uses a Schroeder-Bernstein construction to get a bijection from the universe onto the set of characteristic functions. The starting point of such a construction is an injection from the universe into the set of all characteristic functions. The next two clauses say that setof is such a one-to-one function into the set of all characteristic functions.

list(usable).
a(charq,a(setof,x)) = p1.  (reference number 41)
end_of_list.

Proof that `setof x` is a characteristic function

In order to prove that setof is one-to-one, we use Art Quaife's technique of weighting variables so that clauses containing variables will be discarded immediately. Quaife used this method [4] in his development of Goedel-Bernays set theory. He used it, as we do here, to prove universally quantified sentences, i. e. to refute existentially quantified sentences, i. e. to show that some "bad" constant does not exist. In TRC, this technique is even more widely applicable, since any stratified sentence can be rewritten as an equivalent equation or inequation between constant terms. ***JUSTIFY

weight_list(pick_and_purge).
weight(x,1000).
end_of_list.


----> UNIT CONFLICT at   0.35 sec ----> 166 [binary,165.1,108.1] $F.

Length of proof is 4.  Level of proof is 2.

Proof



30 [reference 34] charq xf=p1|xf noteq(isp1 xf,xf) !=p1.
31 [reference 35] charq xf=p1|xf noteq(isp1 xf,xf) !=p2.
34 [reference 39] p2 xy!=xf (p1 xy) |setof xf xy =p1.
35 [reference 40] p2 xy=xf (p1 xy) |setof xf xy =p2.
36 [assumption to refute] charq (setof bad)!=p1.
39 [ur,36,31] setof bad noteq(isp1 (setof bad),setof bad)!=p2.
40 [ur,36,30] setof bad noteq(isp1 (setof bad),setof bad)!=p1.
108 [ur,39,35,flip.1] bad (p1 noteq(isp1 (setof bad),setof bad))=p2 noteq(isp1 (setof bad),setof bad).
165 [ur,40,34,flip.1] bad (p1 noteq(isp1 (setof bad),setof bad))!=p2 noteq(isp1 (setof bad),setof bad).
166 [binary,165.1,108.1] $F.

list(usable).
a(setof,x) != a(setof,y) | x = y.  (reference number 42)
end_of_list.

Proof that `setof` is one-to-one

weight_list(pick_and_purge).
weight(x,1000).
weight(noteq(bad1,bad2),1).
weight(a(setof,bad1),1).
weight(a(setof,bad2),1).
end_of_list.

-----> EMPTY CLAUSE at  49.38 sec ----> 4119 [para_into,785.1.1,35.2.1,demod,3,2,unit_del,74,8] $F.

Length of proof is 7.  Level of proof is 4.

Proof



2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
8 [reference 1] x=x.
15 [reference 8] x!=y|eq pair(x,y) =p1.
16 [reference 9] x=y|eq pair(x,y) =p2.
17 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
18 [reference 11] p1!=p2.
34 [reference 38] setof xf pair(x,y)=p2|xf x =y.
35 [reference 39] p2 xy!=xf (p1 xy) |setof xf xy =p1.
38 [assumption to refute] setof bad1=setof bad2.
39 [assumption to refute] bad1!=bad2.
41,40 [ur,38,15] eq pair(setof bad1,setof bad2)=p1.
56 [ur,39,17,flip.1] bad2 noteq(bad1,bad2)!=bad1 noteq(bad1,bad2).
71 [para_into,40.1.1,16.2.1,flip.2] p2=p1|setof bad2 =setof bad1.
74 [para_from,40.1.2,18.1.1,demod,41,flip.1] p2!=p1.
94 [ur,71,74] setof bad2=setof bad1.
97 [ur,56,34] setof bad2 pair(noteq(bad1,bad2),bad1 noteq(bad1,bad2))=p2.
785 [para_into,97.1.1.1,94.1.1] setof bad1 pair(noteq(bad1,bad2),bad1 noteq(bad1,bad2))=p2.
4119 [para_into,785.1.1,35.2.1,demod,3,2,unit_del,74,8] $F.

The term `closedunder` tests whether a set is closed under a function.

Definition of `closedunder`

list(demodulators).
closedunder = a(a(abst,k(eq)),pair(k(k(p2)),a(a(abst,k(a(abst,k(eq)))),pair(pair(p1,a(a(abst,a(a(abst,k(abst)),a(a(abst,k(a(abst,k(isp1)))),a(abst,k(p1))))),p2)),k(k(pair(p1,p2))))))).  (reference number 43)
end_of_list.





 Click button to load the definition of closedunder into TRC applet.

The term closedunder pair(s, f) can be interpreted as saying that the set represented by s is closed under the function represented by f. The combinator closedunder has the following defining properties:

closedunder pair(f, s) = p1 if for every z, if s z = p1 then s (f z) = p1.
closedunder pair(f, s) = p2 if for some z, both s z = p1 and s (f z) != p1.

To translate this into a stratified lambda-term, let z be a counterexample to the statement that s is closed under f. Then s z = p1 and isp1 s (f z) = p2. That is, pair(s z, isp1 s (f z)) = pair(p1, p2). Equivalently, the term

(a eq (pair (pair (a s z)
                  (a (a isp1 s) (a f z)))
            (pair p1
                  p2)))

is equal to p1. Now we want to say that there is no such counterexample z. Since the above lambda-term is an application of eq, it must be equal to p1 or p2. If there is no value for z which makes the above term equal to p1 then when we abstract z from the above term, we must get k(p2). These observations lead us to the following lambda-term which we take as the definition of closedunder:

(lambda (s f)
  (a eq (pair (k p2)
              (lambda z
                (a eq (pair (pair (a s z)
                                  (a (a isp1 s) (a f z)))
                            (pair p1
                                  p2)))))))

Note how this definition takes advantage of TRC's ability to rewrite any sentence with stratified quantifiers as a simple equation between two terms: we can translate `there is no z such that blah1 = blah2' as (lambda z (a eq (pair blah1 blah2))) = (k p2).

As usual, our first order of business will be to prove the basic defining properties listed above.
At this point I proved only the basic defining properties of closedunder.

Basic defining properties of `closedunder`

The following clause says that if closedunder pair(xs,xf) != p2, then xs (regarded as a set {x : (xs x = p1)}) is closed under xf (regarded as a function).

list(usable).
a(closedunder,pair(xs,xf)) = p2 | a(xs,x) != p1 | a(xs,a(xf,x)) = p1.  (reference number 44)
end_of_list.

Proof of defining property of `closedunder`

----> UNIT CONFLICT at 595.27 sec ----> 8418 [binary,8414.1,8383.1] $F.

Length of proof is 16.  Level of proof is 6.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 7] abst x y z=x k(z) (y z).
7 [reference 13] eq pair(x,x)=p1.
10 [reference 3] p1 pair(x,y)=x.
14 [reference 7] abst x y z=x k(z) (y z).
16 [reference 9] x=y|eq pair(x,y) =p2.
18 [reference 11] p1!=p2.
20 [reference 18] x y=p1|isp1 x y =p2.
21 [reference 19] isp1 (isp1 x)=isp1 x.
23 [reference 22] x y=p1|notp1 x y =p1.
24 [reference 23] x y!=p1|notp1 x y =p2.
39 [reference 43] closedunder=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(pair(p1,abst (abst k(abst) (abst k(abst k(isp1)) (abst k(p1)))) p2),k(k(pair(p1,p2))))).
40 [assumption to refute] p.
41 [assumption to refute] -p|closedunder pair(bads,badf) !=p2.
42 [assumption to refute] bads badx=p1.
43 [assumption to refute] bads (badf badx)!=p1.
44 [ur,41,40,demod,39,6,1,4,1,6,1,4,4,2,6,6,1,6,1,3,1] eq pair(k(p2),abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))))!=p2.
73 [para_into,42.1.2,23.1.2] bads badx=x y |notp1 x y =p1.
91 [para_from,42.1.2,18.1.1] bads badx!=p2.
93,92 [para_from,42.1.2,10.1.1.1] bads badx pair(x,y)=x.
102,101 [ur,43,20] isp1 bads (badf badx)=p2.
133 [para_into,91.1.1,42.1.1,flip.1] p2!=p1.
147 [ur,44,16,flip.1] abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2)))=k(p2).
483 [para_into,101.1.1.1,21.1.2] isp1 (isp1 bads) (badf badx)=p2.
3327 [para_from,147.1.1,14.1.1.1,demod,1,1,4,4,6,6,1,6,1,1,2,1,flip.1] eq pair(pair(bads x,isp1 bads (badf x)),pair(p1,p2))=p2.
6927 [para_into,73.2.1,24.2.1,unit_del,133] bads badx=x y |x y !=p1.
7433 [para_into,6927.1.2,92.1.1,demod,93] bads badx=x|x!=p1.
7501 [para_from,7433.1.1,91.1.1] x!=p2|x!=p1.
7778 [para_into,483.1.1.1.2,21.1.2] isp1 (isp1 (isp1 bads)) (badf badx)=p2.
8230,8229 [para_into,3327.1.1.2.1.1,42.1.1,demod,102,7,flip.1] p2=p1.
8383 [back_demod,7778,demod,8230] isp1 (isp1 (isp1 bads)) (badf badx)=p1.
8414 [back_demod,7501,demod,8230] x!=p1.
8418 [binary,8414.1,8383.1] $F.

The above proof, obtained without human intervention, is a bit long, so I include the proof below, which used the interactive_given option of OTTER to let me select given clauses manually.

Manual Proof

----> UNIT CONFLICT at   2.77 sec ----> 411 [binary,409.1,149.1] $F.

Length of proof is 7.  Level of proof is 5.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 7] abst x y z=x k(z) (y z).
7 [reference 13] eq pair(x,x)=p1.
14 [reference 7] abst x y z=x k(z) (y z).
15 [reference 8] x!=y|eq pair(x,y) =p1.
16 [reference 9] x=y|eq pair(x,y) =p2.
20 [reference 18] x y=p1|isp1 x y =p2.
39 [reference 43] closedunder=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(pair(p1,abst (abst k(abst) (abst k(abst k(isp1)) (abst k(p1)))) p2),k(k(pair(p1,p2))))).
40 [assumption to refute] p.
41 [assumption to refute] -p|closedunder pair(bads,badf) !=p2.
42 [assumption to refute] bads badx=p1.
43 [assumption to refute] bads (badf badx)!=p1.
44 [ur,41,40,demod,39,6,1,4,1,6,1,4,4,2,6,6,1,6,1,3,1] eq pair(k(p2),abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(
pair(bads,badf)))) badf),k(pair(p1,p2))))!=p2.
61 [ur,44,16,flip.1] abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2)))=k(p2).
149 [para_into,44.1.1,15.2.1,unit_del,61,flip.1] p2!=p1.
236 [para_from,61.1.1,14.1.1.1,demod,1,1,4,4,6,6,1,6,1,1,2,1,flip.1] eq pair(pair(bads x,isp1 bads (badf x)),pair(p1,p2))=p2.
371 [para_from,42.1.1,236.1.1.2.1.1] eq pair(pair(p1,isp1 bads (badf badx)),pair(p1,p2))=p2.
405,404 [ur,43,20] isp1 bads (badf badx)=p2.
409 [back_demod,371,demod,405,7,flip.1] p2=p1.
411 [binary,409.1,149.1] $F.

The following clause says that if closedunder pair(xs,xf) != p1, then xs (regarded as a set {x : (xs x = p1)}) fails to be closed under xf (regarded as a function).

list(usable).
a(closedunder,pair(xs,xf)) = p1 | a(xs,notclosed(xs,xf)) = p1.  (reference number 45)
a(closedunder,pair(xs,xf)) = p1 | a(xs,a(xf,notclosed(xs,xf))) != p1.  (reference number 46)
end_of_list.

Note that instead of introducing the new Skolem term notclosed(xs,xf), I could take the answer literal returned in the following proof and replace bad with x throughout. However, the resulting term seemed a bit long, so I opted for using a new Skolem function in stating the result.

Proof of converse defining property of `closedunder`

----> UNIT CONFLICT at  46.42 sec ----> 784 [binary,783.1,68.1] $ans(noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))).

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

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 7] abst x y z=x k(z) (y z).
10 [reference 3] p1 pair(x,y)=x.
11 [reference 4] p2 pair(x,y)=y.
15 [reference 8] x!=y|eq pair(x,y) =p1.
16 [reference 9] x=y|eq pair(x,y) =p2.
17 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
18 [reference 11] p1!=p2.
19 [reference 17] x y!=p1|isp1 x y =p1.
20 [reference 18] x y=p1|isp1 x y =p2.
39 [reference 43] closedunder=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(pair(p1,abst (abst k(abst) (abst k(abst k(isp1)) (abst k(p1)))) p2),k(k(pair(p1,p2))))).
41 [assumption to refute] p.
42 [assumption to refute] bads x!=p1|bads (badf x) =p1|$ans(x).
43 [assumption to refute] -p|closedunder pair(bads,badf) !=p1.
44 [ur,43,41,demod,39,6,1,4,1,6,1,4,4,2,6,6,1,6,1,3,1] eq pair(k(p2),abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))))!=p1.
51,50 [ur,44,20] isp1 eq pair(k(p2),abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))))=p2.
55 [ur,44,15,flip.1] abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2)))!=k(p2).
59 [ur,55,17,demod,6,1,4,4,6,6,1,6,1,1,2,1,1] eq pair(pair(bads noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)),isp1 bads (badf noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)))),pair(p1,p2))!=p2.
68 [para_from,50.1.2,18.1.2,demod,51,flip.1] p2!=p1.
141 [ur,59,16] pair(bads noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)),isp1 bads (badf noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))))=pair(p1,p2).
698,697 [para_from,141.1.1,11.1.1.2,demod,3,flip.1] isp1 bads (badf noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)))=p2.
699 [para_from,141.1.1,10.1.1.2,demod,2,flip.1] bads noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))=p1.
732 [ur,699,42] bads (badf noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)))=p1|$ans(noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))).
783 [ur,732,19,demod,698] $ans(noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2)))|p2=p1.
784 [binary,783.1,68.1] $ans(noteq(abst k(eq) pair(pair(bads,abst (abst k(isp1) (abst k(p1) k(pair(bads,badf)))) badf),k(pair(p1,p2))),k(p2))).

Interlude 1: Some lemmas needed for intersections

After initial troubles proving the basic properties of kintersection defined in the next major section, I thought a series of simple lemmas might help. One of them was never used in later proofs.

list(usable).
a(charq,eq) = p1.  (reference number 47)
end_of_list.

Proof of `a(charq,eq) = p1.`

----> UNIT CONFLICT at   0.16 sec ----> 99 [binary,98.1,85.1] $F.

Length of proof is 4.  Level of proof is 2.

Proof



19 [reference 14] p1 x!=p2 x |eq x =p1.
20 [reference 15] p1 x=p2 x |eq x =p2.
33 [reference 34] charq xf=p1|xf noteq(isp1 xf,xf) !=p1.
34 [reference 35] charq xf=p1|xf noteq(isp1 xf,xf) !=p2.
44 [assumption to refute] charq eq!=p1.
48 [ur,44,34] eq noteq(isp1 eq,eq)!=p2.
49 [ur,44,33] eq noteq(isp1 eq,eq)!=p1.
85 [ur,48,20,flip.1] p2 noteq(isp1 eq,eq)=p1 noteq(isp1 eq,eq).
98 [ur,49,19,flip.1] p2 noteq(isp1 eq,eq)!=p1 noteq(isp1 eq,eq).
99 [binary,98.1,85.1] $F.

list(usable).
a(charq,xf) = p2 | a(a(xf,x),pair(p1,p2)) = a(xf,x).  (reference number 48)     %    (not used in later proofs)
end_of_list.

Proof of `a(charq,xf) = p2 | a(a(xf,x),pair(p1,p2)) = a(xf,x).`

-----> EMPTY CLAUSE at   1.56 sec ----> 606 [back_demod,556,demod,595,2,7,595,unit_del,65,65] $F.

Length of proof is 7.  Level of proof is 3.

Proof



2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
7 [reference 13] eq pair(x,x)=p1.
8 [reference 1] x=x.
16 [reference 9] x=y|eq pair(x,y) =p2.
18 [reference 11] p1!=p2.
32 [reference 33] charq xf=p2|xf x =p1|xf x =p2.
45 [assumption to refute] charq badf!=p2.
46 [assumption to refute] badf badx pair(p1,p2)!=badf badx.
56 [para_into,45.1.1,32.2.1,unit_del,45,flip.1] p2!=p1|charq charq =p2.
64 [para_from,56.2.2,18.1.2,flip.1] charq charq!=p1|p2!=p1.
65 [para_into,64.1.1,56.2.1] p2!=p1.
76 [ur,46,16] eq pair(badf badx pair(p1,p2),badf badx)=p2.
78 [para_into,46.1.1.1,32.3.1,demod,3,unit_del,45,flip.1] badf badx!=p2|badf badx =p1.
556 [para_into,76.1.1.2.2,32.2.1,unit_del,45] eq pair(badf badx pair(p1,p2),p1)=p2|badf badx =p2.
595,594 [para_into,78.1.1,32.3.1,unit_del,8,45] badf badx=p1.
606 [back_demod,556,demod,595,2,7,595,unit_del,65,65] $F.

list(usable).
a(a(abst,k(x)),k(y)) = k(a(x,y)).  (reference number 49)
end_of_list.

list(demodulators).
a(a(abst,k(x)),k(y)) = k(a(x,y)).  (reference number 50)
end_of_list.

Proof of `a(a(abst,k(x)),k(y)) = k(a(x,y)).`

----> UNIT CONFLICT at   0.17 sec ----> 55 [binary,54.1,8.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof



1 [reference 2] k(x) y=x.
6 [reference 7] abst x y z=x k(z) (y z).
8 [reference 1] x=x.
17 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
50 [assumption to refute] abst k(badx) k(bady)!=k(badx bady).
54 [ur,50,17,demod,6,1,1,1] badx bady!=badx bady.
55 [binary,54.1,8.1] $F.

list(usable).
pair(x1,y1) != pair(x2,y2) | x1 = x2.  (reference number 51)
end_of_list.

Proof of `pair(x1,y1) != pair(x2,y2) | x1 = x2.`

----> UNIT CONFLICT at   0.98 sec ----> 63 [binary,62.1,8.1] $F.

Length of proof is 3.  Level of proof is 3.

Proof



2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
8 [reference 1] x=x.
10 [reference 3] p1 pair(x,y)=x.
11 [reference 4] p2 pair(x,y)=y.
52 [assumption to refute] pair(bad1,bad2)=pair(bad3,bad4).
53 [assumption to refute] bad1!=bad3.
59,58 [para_from,52.1.1,11.1.1.2,demod,3] bad4=bad2.
61,60 [para_from,52.1.1,10.1.1.2,demod,59,2] bad3=bad1.
62 [back_demod,53,demod,61] bad1!=bad1.
63 [binary,62.1,8.1] $F.

list(usable).
pair(x1,y1) != pair(x2,y2) | y1 = y2.  (reference number 52)
end_of_list.

Proof of `pair(x1,y1) != pair(x2,y2) | y1 = y2.`

----> UNIT CONFLICT at   0.94 sec ----> 63 [binary,62.1,8.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof



3 [reference 4] p2 pair(x,y)=y.
8 [reference 1] x=x.
11 [reference 4] p2 pair(x,y)=y.
52 [assumption to refute] pair(bad1,bad2)=pair(bad3,bad4).
53 [assumption to refute] bad2!=bad4.
59,58 [para_from,52.1.1,11.1.1.2,demod,3] bad4=bad2.
62 [back_demod,53,demod,59] bad2!=bad2.
63 [binary,62.1,8.1] $F.

The combinator `kintersection` takes a set of sets, and returns a constant function whose value is the intersection.

Definition of `kintersection`

list(demodulators).
kintersection = a(a(abst,a(a(abst,k(abst)),a(a(abst,k(a(abst,k(abst)))),a(a(abst,a(a(abst,k(abst)),a(a(abst,k(a(abst,k(abst)))),a(a(abst,k(a(abst,k(a(abst,k(eq)))))),pair(k(k(k(k(p2)))),a(a(abst,k(a(abst,k(a(abst,k(a(abst,k(eq)))))))),pair(k(k(k(k(pair(p1,k(p2)))))),pair(pair(p1,p2),k(k(a(abst,a(a(abst,k(abst)),a(abst,k(isp1)))))))))))))),k(k(k(pair(p1,p2)))))))),k(k(k(pair(p1,p2))))).  (reference number 53)
end_of_list.





 Click button to load the definition of kintersection into TRC applet.

Any combinator f can be thought of as representing a set, whose characteristic function is isp1 f. (Of course, many combinators could represent the same set in this way.) Since every combinator represents a set, it follows that every combinator represents a set of sets. It is natural to ask for a combinator intersection such that intersection f x = p1 if and only if for every z, if f z = p1 then z x = p1. In fact intersection cannot exist in TRC. ***JUSTIFY We can still talk about intersections using the combinator kintersection. Instead of outputting the intersection of a collection, kintersection outputs the constant function that sends everything to the intersection of that collection. We need to perform special manipulations of types at two points in the definition.

Let us see how to express kintersection as a stratified lambda-term. Given f and x, we want to know whether or not x is in the intersection of f. This will be true if there is no z such that f z = p1 and z x != p1, that is, there is no z such that pair(f z, isp1 z x) = pair(p1, p2). In order to say that there is no such z, we would like to abstract out the z, but z occurs at level zero and at level one in this statement. We can fix this using the fact that the operation of forming constant functions is one-to-one. Thus x belongs to the intersection of f if there is no z such that pair(f z, k(isp1 z x)) = pair(p1, k(p2)). Now z occurs only at level zero and we can say that x is in the intersection of f if the following term is equal to k(p2), i. e. if the equality expressed by its eq is always false:

(lambda z
  (a eq (pair (pair p1
                    (k p2))
              (pair (a f z)
                    (k (a (a isp1 z) x))))))))

It is easy to say in the language of TRC that the above term is equal to k(p2).

(a eq (pair (k p2)
            (lambda z
              (a eq (pair (pair p1
                                (k p2))
                          (pair (a f z)
                                (k (a (a isp1 z) x))))))))

The above term now expresses the statement that x is in the intersection of f. If we could abstract out the x and the f, then we would have the sought-after combinator intersection, but x is at level -2. (It is at level 0 in the expression (a (a isp1 z) x). It is inside one constant-function expression and one lambda-expression, each of which reduces its type by 1.) Since the entire term is always equal either to p1 or to p2, we can get an equivalent term by applying the whole thing to pair(p1, p2). If we do this twice, we bring x up to level zero and can then abstract it out:

(lambda x
  (a (a (a eq (pair (k p2)
                    (lambda z
                      (a eq (pair (pair p1
                                        (k p2))
                                  (pair (a f z)
                                        (k (a (a isp1 z) x))))))))
        (pair p1 p2))
     (pair p1 p2)))

The above term exactly represents the intersection of f. But we can't abstract out the f now, because it is at level one. At this point we wrap the whole thing in a constant function and settle for the term kintersection, defined below, instead of intersection, which can't exist in TRC. ***JUSTIFY

(lambda f
  (k (lambda x
       (a (a (a eq (pair (k p2)
                         (lambda z
                           (a eq (pair (pair p1
                                             (k p2))
                                       (pair (a f z)
                                             (k (a (a isp1 z) x))))))))
             (pair p1 p2))
          (pair p1 p2)))))

The following clause says that if kintersection f y x != p2 then for every z such that f z = p1, we have z x = p1. The variable y is present only for purposes of stratification, so that f is two levels higher than x.

list(usable).
a(a(a(kintersection,xf),y),x) = p2 | a(xf,z) != p1 | a(z,x) = p1.  (reference number 54)
end_of_list.

list(usable).           % trivial corollary.  choice of eq is arbitrary
a(a(a(kintersection,xf),eq),x) = p2 | a(xf,z) != p1 | a(z,x) = p1.  (reference number 55)     %    (not used in later proofs)
end_of_list.

I proved the first statement above using OTTER. The second is obtained from the first by instantiating the variable y with the value eq. The choice of eq is totally arbitrary. The proof of the second statement is not included here, but if you code its negation, OTTER will of course detect the contradiction with the first statement immediately. I added the second version because when OTTER'S weights are set to discard all variables, OTTER will never use the first clause in the right-to-left direction.

Proof of defining property for `kintersecton`

-----> EMPTY CLAUSE at  17.48 sec ----> 923 [para_into,837.1.1.2.1,23.2.1,unit_del,8,53] $F.

Length of proof is 5.  Level of proof is 5.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
5 [reference 6] pair(p1 x,p2 x)=x.
6 [reference 7] abst x y z=x k(z) (y z).
8 [reference 1] x=x.
14 [reference 7] abst x y z=x k(z) (y z).
19 [reference 12] p2!=p1.
20 [reference 14] p1 x!=p2 x |eq x =p1.
21 [reference 15] p1 x=p2 x |eq x =p2.
23 [reference 18] x y=p1|isp1 x y =p2.
49 [reference 49] abst k(x) k(y)=k(x y).
50 [reference 53] kintersection=abst (abst k(abst) (abst k(abst k(abst)) (abst (abst k(abst) (abst k(abst k(abst)) (abst k(abst k(abst k(eq))) pair(k(k(k(k(p2)))),abst k(abst k(abst k(abst k(eq)))) pair(k(k(k(k(pair(p1,k(p2)))))),pair(pair(p1,p2),k(k(abst (abst k(abst) (abst k(isp1))))))))))) k(k(k(pair(p1,p2))))))) k(k(k(pair(p1,p2)))).
51 [assumption to refute] p.
52 [assumption to refute] badf badz=p1.
53 [assumption to refute] badz badx!=p1.
54 [assumption to refute] -p|kintersection badf bad badx !=p2.
55 [ur,54,51,demod,50,6,6,1,6,1,6,6,1,6,1,6,1,4,1,6,1,4,1,4,4,5,1,1,1,6,6,1,6,6,1,6,1,4,1,6,1,4,1,4,1,1,1,1,6,6,6,1,4,1,6,1,4,1,
4,1,1,1] eq pair(k(p2),abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx))))) pair(p1,p2) 
pair(p1,p2)!=p2.
161 [para_into,55.1.1.1.1,21.2.1,demod,3,3,2,3,unit_del,8,flip.1] abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst)
 (abst k(isp1))) k(k(badx))))=k(p2).
307 [para_from,161.1.1,14.1.1.1,demod,1,1,4,1,4,6,6,1,49,1,49,flip.1] eq pair(pair(p1,k(p2)),pair(badf x,k(isp1 x badx)))=p2.
824 [para_into,307.1.1,20.2.1,demod,2,3,unit_del,19,flip.1] pair(badf x,k(isp1 x badx))!=pair(p1,k(p2)).
837 [para_into,824.1.1.1,52.1.1] pair(p1,k(isp1 badz badx))!=pair(p1,k(p2)).
923 [para_into,837.1.1.2.1,23.2.1,unit_del,8,53] $F.

list(usable).
a(a(a(kintersection,xf),y),x) = p1 | a(xf,notinint(xf,x)) = p1.  (reference number 56)
a(a(a(kintersection,xf),y),x) = p1 | a(notinint(xf,x),x) != p1.  (reference number 57)
end_of_list.

list(usable).
a(a(a(kintersection,xf),eq),x) = p1 | a(xf,notinint(xf,x)) = p1.  (reference number 58)     %    (not used in later proofs)
a(a(a(kintersection,xf),eq),x) = p1 | a(notinint(xf,x),x) != p1.  (reference number 59)     %    (not used in later proofs)
end_of_list.

The following proof was obtained only after turning on the OTTER option para_ones_rule, specialized for the study of combinatory logic. Again, I proved the first pair of clauses above using OTTER. The second pair are obtained from the first by instantiating y with the (arbitrarily chosen) constant eq.

Proof of converse defining property for `kintersecton`

-----> EMPTY CLAUSE at  77.87 sec ----> 5815 [para_into,5716.1.1,22.2.1,unit_del,19,5750] $ans(noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))).

Length of proof is 8.  Level of proof is 6.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
5 [reference 6] pair(p1 x,p2 x)=x.
6 [reference 7] abst x y z=x k(z) (y z).
8 [reference 1] x=x.
9 [reference 2] k(x) y=x.
17 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
19 [reference 12] p2!=p1.
20 [reference 14] p1 x!=p2 x |eq x =p1.
21 [reference 15] p1 x=p2 x |eq x =p2.
22 [reference 17] x y!=p1|isp1 x y =p1.
51 [reference 49] abst k(x) k(y)=k(x y).
52 [reference 51] pair(x1,y1)!=pair(x2,y2)|x1=x2.
53 [reference 52] pair(x1,y1)!=pair(x2,y2)|y1=y2.
54 [reference 53] kintersection=abst (abst k(abst) (abst k(abst k(abst)) (abst (abst k(abst) (abst k(abst k(abst)) (abst k(abst k(abst k(eq))) pair(k(k(k(k(p2)))),abst k(abst k(abst k(abst k(eq)))) pair(k(k(k(k(pair(p1,k(p2)))))),pair(pair(p1,p2),k(k(abst (abst k(abst) (abst k(isp1))))))))))) k(k(k(pair(p1,p2))))))) k(k(k(pair(p1,p2)))).
56 [assumption to refute] p.
57 [assumption to refute] badf z!=p1|z badx =p1|$ans(z).
58 [assumption to refute] -p|kintersection badf bady badx !=p1.
59 [ur,58,56,demod,54,6,6,1,6,1,6,6,1,6,1,6,1,4,1,6,1,4,1,4,4,5,1,1,1,6,6,1,6,6,1,6,1,4,1,6,1,4,1,4,1,1,1,1,6,6,6,1,4,1,6,1,4,1,4,1,1,1] eq pair(k(p2),abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx))))) pair(p1,p2) pair(p1,p2)!=p1.
78 [para_into,59.1.1.1.1,20.2.1,demod,2,2,2,3,unit_del,8,flip.1] abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx))))!=k(p2).
109 [ur,78,17,demod,6,1,4,1,4,6,6,1,51,1,51,1] eq pair(pair(p1,k(p2)),pair(badf noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)),k(isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx)))!=p2.
376 [ur,109,21,demod,2,3,flip.1] pair(badf noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)),k(isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx))=pair(p1,k(p2)).
5612 [ur,376,53] k(isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx)=k(p2).
5613 [ur,376,52] badf noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))=p1.
5716 [para_from,5612.1.1,9.1.1.1,demod,1,flip.1] isp1 noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx=p2.
5750 [ur,5613,57] noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2)) badx=p1|$ans(noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))).
5815 [para_into,5716.1.1,22.2.1,unit_del,19,5750] $ans(noteq(abst k(eq) pair(k(pair(p1,k(p2))),pair(badf,abst (abst k(abst) (abst k(isp1))) k(k(badx)))),k(p2))).

The term `subset` tests the subset relationship between a given pair of characteristic functions.

Definition of `subset`

list(demodulators).
subset = a(a(abst,k(eq)),pair(k(k(p2)),a(a(abst,k(a(abst,k(eq)))),pair(k(k(pair(p1,p2))),pair(p1,a(a(abst,k(isp1)),p2)))))).  (reference number 60)
end_of_list.





 Click button to load the definition of subset into TRC applet.

I define subset pair(x, y) = p1 if there is no z such that x z = p1 but y z != p1. The idioms used in the lambda-term below should by now be quite familiar, so I let it speak for itself.

(lambda (x y)
  (a eq (pair (k p2)
              (lambda z
                (a eq (pair (pair p1
                                  p2)
                            (pair (a x z)
                                  (a (a isp1 y) z))))))))

Basic defining properties of `subset`

Either subset pair(x1,x2) = p2 or if x1 y = p1 then x2 y = p1.

list(usable).
a(subset,pair(x1,x2)) = p2 | a(x1,xc) != p1 | a(x2,xc) = p1.  (reference number 61)
end_of_list.

Proof of defining property for `subset`

----> UNIT CONFLICT at  39.84 sec ----> 2933 [binary,2931.1,19.1] $F.

Length of proof is 5.  Level of proof is 4.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 7] abst x y z=x k(z) (y z).
7 [reference 13] eq pair(x,x)=p1.
14 [reference 7] abst x y z=x k(z) (y z).
19 [reference 12] p2!=p1.
21 [reference 15] p1 x=p2 x |eq x =p2.
23 [reference 18] x y=p1|isp1 x y =p2.
57 [reference 60] subset=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(k(k(pair(p1,p2))),pair(p1,abst k(isp1) p2))).
58 [assumption to refute] p.
59 [assumption to refute] -p|subset pair(bad1,bad2) !=p2.
60 [assumption to refute] bad1 badc=p1.
61 [assumption to refute] bad2 badc!=p1.
62 [ur,59,58,demod,57,6,1,4,1,6,1,4,1,4,2,6,1,3] eq pair(k(p2),abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)))!=p2.
149,148 [ur,61,23] isp1 bad2 badc=p2.
185 [ur,62,21,demod,2,3,flip.1] abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2))=k(p2).
896 [para_from,185.1.1,14.1.1.1,demod,1,1,4,1,4,flip.1] eq pair(pair(p1,p2),pair(bad1 x,isp1 bad2 x))=p2.
2931 [para_into,896.1.1.2.2.1,60.1.1,demod,149,7,flip.1] p2=p1.
2933 [binary,2931.1,19.1] $F.

If subset pair(x1, x2) != p1 then there is a witness c = notsub(x1, x2) such that x1 c = p1 and x2 c != p1.

list(usable).
a(subset,pair(x1,x2)) = p1 | a(x1,notsub(x1,x2)) = p1.  (reference number 62)
a(subset,pair(x1,x2)) = p1 | a(x2,notsub(x1,x2)) != p1.  (reference number 63)
end_of_list.

Proof of converse defining property for `subset`

To obtain this proof I used OTTER's para_into_units_only and para_from_units_only options.

----> UNIT CONFLICT at   4.36 sec ----> 356 [binary,355.1,19.1] $ans(noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))).

Length of proof is 8.  Level of proof is 7.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
6 [reference 7] abst x y z=x k(z) (y z).
17 [reference 10] x=y|x noteq(x,y) !=y noteq(x,y).
19 [reference 12] p2!=p1.
20 [reference 14] p1 x!=p2 x |eq x =p1.
21 [reference 15] p1 x=p2 x |eq x =p2.
22 [reference 17] x y!=p1|isp1 x y =p1.
52 [reference 51] pair(x1,y1)!=pair(x2,y2)|x1=x2.
53 [reference 52] pair(x1,y1)!=pair(x2,y2)|y1=y2.
57 [reference 60] subset=abst k(eq) pair(k(k(p2)),abst k(abst k(eq)) pair(k(k(pair(p1,p2))),pair(p1,abst k(isp1) p2))).
59 [assumption to refute] -p|subset pair(bad1,bad2) !=p1.
60 [assumption to refute] bad1 x!=p1|bad2 x =p1|$ans(x).
61 [assumption to refute] p.
62 [ur,59,61,demod,57,6,1,4,1,6,1,4,1,4,2,6,1,3] eq pair(k(p2),abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)))!=p1.
72 [ur,62,20,demod,2,3,flip.1] abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2))!=k(p2).
87 [ur,72,17,demod,6,1,4,1,4,1] eq pair(pair(p1,p2),pair(bad1 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)),
isp1 bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))))!=p2.
199 [ur,87,21,demod,2,3,flip.1] pair(bad1 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)),isp1 bad2 noteq(abst
 k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)))=pair(p1,p2).
295,294 [ur,199,53] isp1 bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))=p2.
296 [ur,199,52] bad1 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))=p1.
344 [ur,296,60] bad2 noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))=p1|$ans(noteq(abst k(eq) pair(k(pair(p1,p
2)),pair(bad1,isp1 bad2)),k(p2))).
355 [ur,344,22,demod,295] $ans(noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2)))|p2=p1.
356 [binary,355.1,19.1] $ans(noteq(abst k(eq) pair(k(pair(p1,p2)),pair(bad1,isp1 bad2)),k(p2))).

Alternate version of defining properties for `subset`, using projections instead of pairs

list(usable).
a(subset,x) = p2 | a(a(p1,x),y) != p1 | a(a(p2,x),y) = p1.  (reference number 64)     %    (not used in later proofs)
end_of_list.

Proof of alternate defining property for `subset`

----> UNIT CONFLICT at   0.20 sec ----> 101 [binary,99.1,60.1] $F.

Length of proof is 1.  Level of proof is 1.

Proof



5 [reference 6] pair(p1 x,p2 x)=x.
57 [reference 61] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1.
60 [assumption to refute] subset bad!=p2.
61 [assumption to refute] p1 bad badc=p1.
62 [assumption to refute] p2 bad badc!=p1.
99 [ur,62,57,61,demod,5] subset bad=p2.
101 [binary,99.1,60.1] $F.

list(usable).
a(subset,x) = p1 | a(a(p1,x),notsub(a(p1,x),a(p2,x))) = p1.  (reference number 65)
a(subset,x) = p1 | a(a(p2,x),notsub(a(p1,x),a(p2,x))) != p1.  (reference number 66)
end_of_list.

Proof of converse alternate defining property for `subset`

----> UNIT CONFLICT at  27.39 sec ----> 4732 [binary,4730.1,61.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof



5 [reference 6] pair(p1 x,p2 x)=x.
58 [reference 62] subset pair(x1,x2)=p1|x1 notsub(x1,x2) =p1.
59 [reference 63] subset pair(x1,x2)=p1|x2 notsub(x1,x2) !=p1.
61 [assumption to refute] subset bad!=p1.
62 [assumption to refute] p1 bad notsub(p1 bad,p2 bad)!=p1|p2 bad notsub(p1 bad,p2 bad) =p1.
103 [hyper,62,58,demod,5,unit_del,61] p2 bad notsub(p1 bad,p2 bad)=p1.
4730 [hyper,103,59,demod,5] subset bad=p1.
4732 [binary,4730.1,61.1] $F.

Interlude 2: some lemmas about `kintersection`, `closedunder`, and `subset`.

If every member of a collection x is closed under a function z, then the intersection of x is closed under z. Equivalently, either closedunder pair(kintersection x y, z) = p1 or there is some c such that x c = p1 and closedunder pair(c,z) = p2. The witness c depends on x and z, and instead of introducing a new skolem function producing this witness, I chose to use the answer literal found by OTTER, which expresses the witness in terms of the existing Skolem functions notinint and notclosed.

list(usable).  
a(closedunder,pair(a(a(kintersection,x),y),z)) = p1 | a(x,notinint(x,a(z,notclosed(a(a(kintersection,x),y),z)))) = p1.  (reference number 67)
a(closedunder,pair(a(a(kintersection,x),y),z)) = p1 | a(closedunder,pair(notinint(x,a(z,notclosed(a(a(kintersection,x),y),z))),z)) = p2.  (reference number 68)
end_of_list.

Proof that if every member of `x` is closed under `f` then the intersection of `x` is closed under `f`

Note how the clause with variable x is placed in the usable list and the clause with no variables in the set of support: The clause bads x != p1 | closedunder pair(x,badf) != p2 | $ans(x) is in the usable list, while the clause closedunder pair(kintersection bads bad,badf) != p1 is in the set of support. This allows the use of the standard technique of assigning a high wait to variables, purging all clauses with variables from the set of support, keeping the search focused on the "bad" constants whose existence is to be refuted.

----> UNIT CONFLICT at  23.89 sec ----> 7510 [binary,7509.1,19.1] $ans(notinint(bads,badf notclosed(kintersection bads bad,badf))).

Length of proof is 8.  Level of proof is 5.

Proof



19 [reference 12] p2!=p1.
45 [reference 44] closedunder pair(xs,xf)=p2|xs x !=p1|xs (xf x) =p1.
46 [reference 45] closedunder pair(xs,xf)=p1|xs notclosed(xs,xf) =p1.
47 [reference 46] closedunder pair(xs,xf)=p1|xs (xf notclosed(xs,xf)) !=p1.
54 [reference 54] kintersection xf y x=p2|xf z !=p1|z x =p1.
55 [reference 56] kintersection xf y x=p1|xf notinint(xf,x) =p1.
56 [reference 57] kintersection xf y x=p1|notinint(xf,x) x !=p1.
63 [assumption to refute] bads x!=p1|closedunder pair(x,badf) !=p2|$ans(x).
64 [assumption to refute] closedunder pair(kintersection bads bad,badf)!=p1.
65 [hyper,64,46] kintersection bads bad notclosed(kintersection bads bad,badf)=p1.
78 [neg_hyper,64,47] kintersection bads bad (badf notclosed(kintersection bads bad,badf))!=p1.
148 [hyper,78,55] bads notinint(bads,badf notclosed(kintersection bads bad,badf))=p1.
159 [neg_hyper,78,56] notinint(bads,badf notclosed(kintersection bads bad,badf)) (badf notclosed(kintersection bads bad,badf))!=
p1.
160 [neg_hyper,78,55,63] closedunder pair(notinint(bads,badf notclosed(kintersection bads bad,badf)),badf)!=p2|$ans(notinint(bad
s,badf notclosed(kintersection bads bad,badf))).
695 [neg_hyper,159,45,160] notinint(bads,badf notclosed(kintersection bads bad,badf)) notclosed(kintersection bads bad,badf)!=p1
|$ans(notinint(bads,badf notclosed(kintersection bads bad,badf))).
7482 [ur,695,54,148] $ans(notinint(bads,badf notclosed(kintersection bads bad,badf)))|kintersection bads x notclosed(kintersecti
on bads bad,badf) =p2.
7509 [para_into,7482.2.1,65.1.1,flip.2] $ans(notinint(bads,badf notclosed(kintersection bads bad,badf)))|p2=p1.
7510 [binary,7509.1,19.1] $ans(notinint(bads,badf notclosed(kintersection bads bad,badf))).

The intersection of a collection x of sets is a subset of every member of x.

list(usable).
a(subset,pair(a(a(kintersection,x),y),z)) = p1 | a(x,z) != p1.  (reference number 69)
end_of_list.

The following clause is the same as the above, but with y instantiated as eq.

list(usable).          
a(subset,pair(a(a(kintersection,x),eq),z)) = p1 | a(x,z) != p1.  (reference number 70)     %    (not used in later proofs)
end_of_list.

Proof that the intersection of a set is a subset of every member of the set

----> UNIT CONFLICT at   0.25 sec ----> 146 [binary,144.1,19.1] $F.

Length of proof is 4.  Level of proof is 3.

Proof



2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
19 [reference 12] p2!=p1.
54 [reference 54] kintersection xf y x=p2|xf z !=p1|z x =p1.
61 [reference 65] subset x=p1|p1 x notsub(p1 x,p2 x) =p1.
62 [reference 66] subset x=p1|p2 x notsub(p1 x,p2 x) !=p1.
65 [assumption to refute] subset pair(kintersection bad1 bad2,bad3)!=p1.
66 [assumption to refute] bad1 bad3=p1.
67 [ur,65,62,demod,3,2,3] bad3 notsub(kintersection bad1 bad2,bad3)!=p1.
68 [ur,65,61,demod,2,2,3] kintersection bad1 bad2 notsub(kintersection bad1 bad2,bad3)=p1.
129,128 [ur,67,54,66] kintersection bad1 x notsub(kintersection bad1 bad2,bad3)=p2.
144 [back_demod,68,demod,129] p2=p1.
146 [binary,144.1,19.1] $F.

If z is a subset of every element of x, then z is a subset of the intersection of x.

list(usable).  
a(subset,pair(z,a(a(kintersection,x),y))) = p1  | a(x,notinint(x,notsub(z,a(a(kintersection,x),y)))) = p1.  (reference number 71)
a(subset,pair(z,a(a(kintersection,x),y))) = p1  | a(subset,pair(z,notinint(x,notsub(z,a(a(kintersection,x),y))))) = p2.  (reference number 72)
end_of_list.

Proof that if `z` is a subset of every element of `x`, then `z` is a subset of the intersection of `x`

----> UNIT CONFLICT at   0.63 sec ----> 355 [binary,353.1,313.1] $ans(notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad))).

Length of proof is 6.  Level of proof is 3.

Proof



2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
56 [reference 56] kintersection xf y x=p1|xf notinint(xf,x) =p1.
57 [reference 57] kintersection xf y x=p1|notinint(xf,x) x !=p1.
60 [reference 61] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1.
64 [reference 65] subset x=p1|p1 x notsub(p1 x,p2 x) =p1.
65 [reference 66] subset x=p1|p2 x notsub(p1 x,p2 x) !=p1.
70 [assumption to refute] bad_collection x!=p1|subset pair(bad_set,x) !=p2|$ans(x).
71 [assumption to refute] subset pair(bad_set,kintersection bad_collection bad)!=p1.
72 [ur,71,65,demod,3,2,3] kintersection bad_collection bad notsub(bad_set,kintersection bad_collection bad)!=p1.
73 [ur,71,64,demod,2,2,3] bad_set notsub(bad_set,kintersection bad_collection bad)=p1.
106 [ur,72,57] notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad)) notsub(bad_set,kintersection bad_collec
tion bad)!=p1.
107 [ur,72,56] bad_collection notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad))=p1.
313 [ur,107,70] subset pair(bad_set,notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad)))!=p2|$ans(notinint
(bad_collection,notsub(bad_set,kintersection bad_collection bad))).
353 [ur,106,60,73] subset pair(bad_set,notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad)))=p2.
355 [binary,353.1,313.1] $ans(notinint(bad_collection,notsub(bad_set,kintersection bad_collection bad))).

The term `closure` finds the closure of a set under a function.

Definition of `closure`

list(demodulators).
closure = a(a(abst,a(a(abst,k(kintersection)),a(a(abst,k(a(abst,k(eq)))),pair(k(k(pair(p1,p1))),pair(a(a(abst,k(a(abst,k(subset)))),pair(a(abst,k(p1)),k(pair(p1,p2)))),a(a(abst,k(a(abst,k(closedunder)))),pair(k(pair(p1,p2)),a(abst,k(p2))))))))),pair(p1,p2)).  (reference number 73)
end_of_list.





 Click button to load the definition of closure into TRC applet.

Define the closure of the set s under the function f as the intersection of all sets x that contain s and are closed under f. Thus

(a kintersection
   (lambda x
     (a eq (pair (pair p1
                       p1)
                 (pair (a subset (pair s x))
                       (a closedunder (pair x f)))))))

is the constant function whose value is the closure of s under f. Note also that s and f are at level -1 in the above term. I can recover the closure itself from this constant function by applying it to any arbitrary term. By doing so, I also bring s and f up to level zero so that they can be abstracted out. I chose the term pair(s, f) as the term to which I applied the above term. So, applying the above term to pair(s, f) and then abstracting out pair(s, f), we get the definition of closure, below.

(lambda (s f)
  (a (a kintersection
        (lambda x
          (a eq (pair (pair p1
                            p1)
                      (pair (a subset (pair s x))
                            (a closedunder (pair x f)))))))
     (pair s f)))

Standard characterization of `closure pair(s, f)`

The standard characterization of the closure of a set s under a function f is that it is the smallest set containing s and closed under f. The following three propositions embody this characterization. The first says that it contains s, the second that it is closed under f, and the third that it is the smallest such set.

The set `s` is a subset of `closure pair(s, f)`.

list(usable).
a(subset,pair(xs,a(closure,pair(xs,xf)))) = p1.  (reference number 74)
end_of_list.

Proof that `s` is a subset of `closure pair(s, f)`

----> UNIT CONFLICT at   4.22 sec ----> 629 [binary,627.1,19.1] $F.

Length of proof is 12.  Level of proof is 6.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
5 [reference 6] pair(p1 x,p2 x)=x.
6 [reference 7] abst x y z=x k(z) (y z).
16 [reference 9] x=y|eq pair(x,y) =p2.
19 [reference 12] p2!=p1.
48 [reference 47] charq eq=p1.
51 [reference 49] abst k(x) k(y)=k(x y).
52 [reference 51] pair(x1,y1)!=pair(x2,y2)|x1=x2.
60 [reference 61] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1.
64 [reference 65] subset x=p1|p1 x notsub(p1 x,p2 x) =p1.
65 [reference 66] subset x=p1|p2 x notsub(p1 x,p2 x) !=p1.
70 [reference 71] subset pair(z,kintersection x y)=p1|x notinint(x,notsub(z,kintersection x y)) =p1.
71 [reference 72] subset pair(z,kintersection x y)=p1|subset pair(z,notinint(x,notsub(z,kintersection x y))) =p2.
72 [reference 73] closure=abst (abst k(kintersection) (abst k(abst k(eq)) pair(k(k(pair(p1,p1))),pair(abst k(abst k(subset)) pair(abst k(p1),k(pair(p1,p2))),abst k(abst k(closedunder)) pair(k(pair(p1,p2)),abst k(p2)))))) pair(p1,p2).
73 [assumption to refute] p.
74 [assumption to refute] -p|subset pair(bads,closure pair(bads,badf)) !=p1.
75 [ur,74,73,demod,72,6,6,1,6,1,4,1,4,6,1,4,51,2,1,6,1,4,1,51,3,4,2,3] subset pair(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))!=p1.
77,76 [ur,75,71] subset pair(bads,notinint(abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf)))),notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))))=p2.
78 [ur,75,70,demod,6,1,4,1,4,6,1,4,1,4,5,77,6,1,4,4,5,1] eq pair(pair(p1,p1),pair(p2,closedunder pair(notinint(abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf)))),notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))),badf)))=p1.
80 [ur,75,65,demod,3,2,3] kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf) notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))!=p1.
81 [ur,75,64,demod,2,2,3] bads notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))=p1.
113 [para_into,75.1.2,48.1.2] subset pair(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))!=charq eq.
213 [ur,113,52] pair(subset pair(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf)),x)!=pair(charq eq,y).
240 [para_into,78.1.1.2.1.1,48.1.2] eq pair(pair(charq eq,p1),pair(p2,closedunder pair(notinint(abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf)))),notsub(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))),badf)))=p1.
355,354 [ur,80,60,81] subset pair(bads,kintersection (abst k(eq) pair(k(pair(p1,p1)),pair(abst k(subset) pair(k(bads),pair(p1,p2)),abst k(closedunder) pair(pair(p1,p2),k(badf))))) pair(bads,badf))=p2.
395 [back_demod,213,demod,355,flip.1] pair(charq eq,x)!=pair(p2,y).
626,625 [ur,395,16] eq pair(pair(charq eq,x),pair(p2,y))=p2.
627 [back_demod,240,demod,626] p2=p1.
629 [binary,627.1,19.1] $F.

The set `closure pair(s, f)` is closed under `f`.

list(usable).
a(closedunder,pair(a(closure,pair(xs,xf)),xf)) = p1.  (reference number 75)
end_of_list.

Proof that `closure pair(s, f)` is closed under `f`

----> UNIT CONFLICT at   7.47 sec ----> 919 [binary,917.1,19.1] $F.

Length of proof is 12.  Level of proof is 6.

Proof



1 [reference 2] k(x) y=x.
2 [reference 3] p1 pair(x,y)=x.
3 [reference 4] p2 pair(x,y)=y.
4 [reference 5] pair(x,y) z=pair(x z,y z).
5 [reference 6] pair(p1 x,p2 x)=x.
6 [reference 7] abst x y z=x k(z) (y z).
16 [reference 9] x=y|eq pair(x,y) =p2.
19 [reference 12] p2!=p1.
45 [reference 44] closedunder pair(xs,xf)=p2|xs x !=p1|xs (xf x) =p1.
46 [reference 45] closedunder pair(xs,xf)=p1|xs notclosed(xs,xf) =p1.
47 [reference 46] closedunder pair(xs,xf)=p1|xs (xf notclosed(xs,xf)) !=p1.
48 [reference 47] charq eq=p1.
51 [reference 49] abst k(x) k(y)=k(x y).
53 [reference 52] pair(x1,y1)!=pair(x2,y2)|y1=y2.
66 [reference 67] closedunder pair(kintersection x y,z)=p1|x notinint(x,z notclosed(kintersection x y,z)) =p1.
67 [reference 68] closedunder pair(kintersection x y,z)=p1|closedunder pair(notinint(x,z notclosed(kintersection x y,z)),z) =p2.
72 [reference 73] closure=abst (abst k(kintersection) (abst k(abst k(eq)) pair(k(k(pair(p1,p1))),pair(abst k(abst k(subset)) pair(abst k(p1),k(pair(p1,p2))),abst k(abst k(closedunder)) pair(k(pair(p1,p2)),abst k(p2)))))) pair(p1,p2).
74 [assumption to refute] p.
75 [assumption to refute] -p|closedunder pair(closure pair(bads,badf),badf) !=p1.
76 [ur,75,74,demod,72,6,6,1,6,1,4,1,4,6,1,4,51,2,1,6,1,4,1,51,

Outline

Ultra-Formal Verification of a Result in a System of Combinatory Logic

Table of Contents

Ultra-Formal Verification of a Result in a System of Combinatory Logic

General procedure used

Notations and Definitions

OTTER settings

Emergency measures

Reflexive property of equality

TRC Basic Axioms

Proof of a(p1,x) != a(p2,x) | a(eq,x) = p1.

Proof

Proof of a(p1,x) = a(p2,x) | a(eq,x) = p2.

Proof

The term isp1 is a projection from functions to characteristic functions.

Definition of isp1

Basic defining properties of isp1

Proof of a(x,y) != p1 | a(a(isp1,x),y) = p1.

Proof

Proof of a(x,y) = p1 | a(a(isp1,x),y) = p2.

Proof

The combinator isp1 is a projection from functions to characteristic functions.

First proof of a(isp1,a(isp1,x)) = a(isp1,x).

Proof

Second proof of a(isp1,a(isp1,x)) = a(isp1,x).

Proof

The term notp1 finds complements of characteristic functions.

Definition of notp1

Basic defining clauses

Proof of a(x,y) = p1 | a(a(notp1,x),y) = p1.

Proof

Proof of a(x,y) != p1 | a(a(notp1,x),y) = p2.

Proof

Two simple properties

Proof of a(notp1,x) != x.

Proof

Proof of a(a(notp1,x),y) = p1 | a(a(notp1,x),y) = p2.

Proof

Algebra of notp1 and isp1 under composition

Proof of a(notp1,a(notp1,x)) = a(isp1,x).

Proof

Proof of a(notp1,a(isp1,x)) = a(notp1,x).

Proof

Proof of a(isp1,a(notp1,x)) = a(notp1,x).

Proof

The term charq is the characteristic function of the set of characteristic functions.

Definition of charq

Proof of a(charq,xf) = p2 | a(xf,x) = p1 | a(xf,x) = p2.

Proof

Proof that if f is a characteristic function, then charq f = p1

Proof

The term setof finds the characteristic function of a given function.

Definition of setof

Basic defining clauses (2 versions)

Defining clauses for setof using pair

Proof of a(a(setof,xf),pair(x,a(xf,x))) = p1.

Proof

Proof of a(a(setof,xf),pair(x,y)) = p2 | a(xf,x) = y.

Proof

Defining clauses for setof using p1 and p2.

Proof of a(p2,xy) != a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p1.

Proof

Proof of a(p2,xy) = a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p2.

Proof

Important properties of setof

Proof that setof x is a characteristic function

Proof

Proof that setof is one-to-one

Proof

The term closedunder tests whether a set is closed under a function.

Definition of closedunder

Basic defining properties of closedunder

Proof of defining property of closedunder

Proof

Manual Proof

Proof

Proof of converse defining property of closedunder

Proof

Interlude 1: Some lemmas needed for intersections

Proof of a(charq,eq) = p1.

Proof of `a(p1,x) != a(p2,x) | a(eq,x) = p1.`

Proof of `a(p1,x) = a(p2,x) | a(eq,x) = p2.`

The term `isp1` is a projection from functions to characteristic functions.

Definition of `isp1`

Basic defining properties of `isp1`

Proof of `a(x,y) != p1 | a(a(isp1,x),y) = p1.`

Proof of `a(x,y) = p1 | a(a(isp1,x),y) = p2.`

The combinator `isp1` is a projection from functions to characteristic functions.

First proof of `a(isp1,a(isp1,x)) = a(isp1,x).`

Second proof of `a(isp1,a(isp1,x)) = a(isp1,x).`

The term `notp1` finds complements of characteristic functions.

Definition of `notp1`

Proof of `a(x,y) = p1 | a(a(notp1,x),y) = p1.`

Proof of `a(x,y) != p1 | a(a(notp1,x),y) = p2.`

Proof of `a(notp1,x) != x.`

Proof of `a(a(notp1,x),y) = p1 | a(a(notp1,x),y) = p2.`

Proof of `a(notp1,a(notp1,x)) = a(isp1,x).`

Proof of `a(notp1,a(isp1,x)) = a(notp1,x).`

Proof of `a(isp1,a(notp1,x)) = a(notp1,x).`

The term `charq` is the characteristic function of the set of characteristic functions.

Definition of `charq`

Proof of `a(charq,xf) = p2 | a(xf,x) = p1 | a(xf,x) = p2.`

Proof that if `f` is a characteristic function, then `charq f = p1`

The term `setof` finds the characteristic function of a given function.

Definition of `setof`

Defining clauses for `setof` using `pair`

Proof of `a(a(setof,xf),pair(x,a(xf,x))) = p1.`

Proof of `a(a(setof,xf),pair(x,y)) = p2 | a(xf,x) = y.`

Defining clauses for `setof` using `p1` and `p2`.

Proof of `a(p2,xy) != a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p1.`

Proof of `a(p2,xy) = a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p2.`

Important properties of `setof`

Proof that `setof x` is a characteristic function

Proof that `setof` is one-to-one

The term `closedunder` tests whether a set is closed under a function.

Definition of `closedunder`

Basic defining properties of `closedunder`

Proof of defining property of `closedunder`

Proof of converse defining property of `closedunder`

Proof of `a(charq,eq) = p1.`

Proof of `a(charq,xf) = p2 | a(a(xf,x),pair(p1,p2)) = a(xf,x).`

Proof of `a(a(abst,k(x)),k(y)) = k(a(x,y)).`

Proof of `pair(x1,y1) != pair(x2,y2) | x1 = x2.`

Proof of `pair(x1,y1) != pair(x2,y2) | y1 = y2.`

The combinator `kintersection` takes a set of sets, and returns a constant function whose value is the intersection.

Definition of `kintersection`

Proof of defining property for `kintersecton`

Proof of converse defining property for `kintersecton`

The term `subset` tests the subset relationship between a given pair of characteristic functions.

Definition of `subset`

Basic defining properties of `subset`

Proof of defining property for `subset`

Proof of converse defining property for `subset`

Alternate version of defining properties for `subset`, using projections instead of pairs

Proof of alternate defining property for `subset`

Proof of converse alternate defining property for `subset`

Interlude 2: some lemmas about `kintersection`, `closedunder`, and `subset`.

Proof that if every member of `x` is closed under `f` then the intersection of `x` is closed under `f`

Proof that if `z` is a subset of every element of `x`, then `z` is a subset of the intersection of `x`

The term `closure` finds the closure of a set under a function.

Definition of `closure`

Standard characterization of `closure pair(s, f)`

The set `s` is a subset of `closure pair(s, f)`.

Proof that `s` is a subset of `closure pair(s, f)`

The set `closure pair(s, f)` is closed under `f`.

Proof that `closure pair(s, f)` is closed under `f`