charq is the characteristic function of the set of characteristic functions.
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. end_of_list.
Proof of a(charq,xf) = p2 | a(xf,x) = p1 | a(xf,x) = p2. | OTTER output file
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. a(charq,xf) = p1 | a(xf,noteq(a(isp1,xf),xf)) != p2. end_of_list.
Proof that if f is a characteristic function, then charq f = p1 | OTTER output file
up | previous | next | detailed contents | brief contents