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

Matracas Mathematics Related Software

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. Assume φ and ¬φ. Then we know ψ.

(.) "false" is a proposition.

(.) Let φ be a proposition. Assume φ implies false. Then we know ¬φ.

(.) Let A, B and x be objects. Assume xAB. Let φ be a proposition. Assume xA implies ¬xB implies φ and ¬xA implies xB implies φ. Then we know φ.

Proof

It is enough to show xAB implies false. Assume xAB. Since xB, we know xA implies ¬xB implies false. Since xA, we have ¬xA implies xB implies false. Using this, xA implies ¬xB implies false and xAB, we conclude false.


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

Hide Background.

Test yourself on this item.