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.
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.
end_of_list.

Proof that if every member of x is closed under f then the intersection of x is closed under f | OTTER output file


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.
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.     %    (not used in later proofs)
end_of_list.

Proof that the intersection of a set is a subset of every member of the set | OTTER output file


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.
a(subset,pair(z,a(a(kintersection,x),y))) = p1  | a(subset,pair(z,notinint(x,notsub(z,a(a(kintersection,x),y))))) = p2.
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 | OTTER output file


up show outline