Satallax
Satallax is a higher-order
automated theorem prover.
Satallax won the THF division
of CASC-23 in 2011.

Automated Reasoning in Higher Order Logic

Automated Reasoning in Higher Order Logic

Impressum
Contact Person
Chad E Brown

Theorem

Let A, B and x be objects. Assume ¬xA and xB. Then we have xAB.

Background

The following background is necessary to understand this theorem.

(.) Let A and x be objects. Then xA is a proposition.

(.) Let φ be a proposition. Then ¬φ is a proposition.

(.) Let x and y be objects. Then "xy" is an object.

Background for Proof

The following background is necessary for the proof.

(.) Let φ and ψ be propositions. Then φψ is a proposition.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Then {aA|φ(a)} is an object.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Let a be a member of A. Assume φ(a). Then we know a∈{aA|φ(a)}.

(.) Let φ and ψ be propositions. Assume φ. Then we know φψ.

(.) Let A and B be objects. Then "AB" is an object.

(.) Let A, B and x be objects. Assume xB. Then we know xAB.

(.) Let A and B be objects. Then AB is the object given by {xABxA∨¬xB}.

Proof

We will show x∈{xABxA∨¬xB}. Since ¬xA, we have ¬xA∨¬xB. Using this, we are done.


Click here to modify variable names (JavaScript Must Be Enabled).

Hide Background.

Test yourself on this item.