simptcheck formal version of this item

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

Scunak

Impressum
Contact Person
Chad E Brown

Definition

Let A be an object. Then we say A is a transitive set if ∀a∈A⋅a⊆A.

Background

The following background is necessary to understand this definition.

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

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Then "∀a∈A⋅φ(a)" is a proposition.

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

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 Theorem Theorem Theorem Theorem Theorem