Contents

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

Impressum
Contact Person
Chad E Brown

Theorem

Let A be an object. Then we have "A is nonempty"⊃∃a∈A⋅a∩A=∅.

Background

The following background is necessary to understand this theorem.

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

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

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

(.) ∅ is an object.

(.) 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 an object.

(.) Let x be an object. Then "x is nonempty" is a proposition.

Background for Proof

The following background is necessary for the proof.

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

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

(.) Let φ(x) be a proposition depending on an object x. Then ∀x φ(x) is a proposition.

(.) Let φ(x) be a proposition depending on an object x. Then ∃x φ(x) is a proposition.

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

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

(.) Let φ(x) be a proposition depending on an object x. Assume ∀x φ(x). Let x be an object. Then we know φ(x).

(.) We know ∀A (∃x x∈A⊃∃B (B∈A∧¬(∃x (x∈B∧x∈A)))).

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

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

(.) Let φ(x) be a proposition depending on an object x. Assume ∃x φ(x). Let ψ be a proposition. Assume for all x φ(x) implies ψ. Then we know ψ.

(.) 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∈A⋅φ(a).

(.) Let A and B be objects. Assume ¬(∃x (x∈A∧x∈B)). Then we know A∩B=∅.

(.) Let A be an object. Assume A is nonempty. Then we know ∃x x∈A.

Proof

Assume A is nonempty.

Claim: ∃B (B∈A∧¬(∃x (x∈B∧x∈A))).

Proof of Claim:

Claim: ∃x x∈A⊃∃B (B∈A∧¬(∃x (x∈B∧x∈A))).

Proof of Claim: Clearly, ∀A (∃x x∈A⊃∃B (B∈A∧¬(∃x (x∈B∧x∈A)))). Using this, we are done. This completes the proof of the claim.

Since A is nonempty, we know ∃x x∈A. Using this and ∃x x∈A⊃∃B (B∈A∧¬(∃x (x∈B∧x∈A))), we conclude ∃B (B∈A∧¬(∃x (x∈B∧x∈A))). This completes the proof of the claim.

Let B be such that B∈A∧¬(∃x (x∈B∧x∈A)). We will show B∩A=∅. Since B∈A∧¬(∃x (x∈B∧x∈A)), we have ¬(∃x (x∈B∧x∈A)). Using this, we are done.

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