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 and B be objects. Assume AB. Then we have A \ B=∅.

Background

The following background is necessary to understand this theorem.

(.) Let x and y be objects. Then x=y is a proposition.

(.) ∅ is an object.

(.) Let A and B be objects. Then "AB" is a proposition.

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

Background for Proof

The following background is necessary for the proof.

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

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

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

(.) Let A and B be objects. Assume for all x xA implies xB. Then we know AB.

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

(.) Let A, B and x be objects. Assume xA \ B. Then we know xA.

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

(.) Let A be an object. Assume A⊆∅. Then we know A=∅.

Proof

We will show A \ B⊆∅. It is enough to show for all x xA \ B implies x∈∅. Let x be an object. Assume xA \ B.

Claim: xB.

Proof of Claim: Since xA \ B, we know xA. Using this and AB, we are done. This completes the proof of the claim.

Since xA \ B, we have ¬xB. Using this and xB, we conclude x∈∅.


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

Hide Background.

Test yourself on this item.