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

Definition

Let A and B be objects. Then we define AB to be the object given by {xABxA∨¬xB}.

Background

The following background is necessary to understand this definition.

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

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

(.) 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 and B be objects. Then "AB" is an object.


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

Hide Background.

Test yourself on this item.


See Also

Theorem Theorem Theorem Theorem Theorem Theorem Theorem Theorem