simptcheck formal version of this item

Automated Reasoning in Higher Order Logic

Automated Reasoning in Higher Order Logic

Contact Person
Chad E Brown

Definition

Let x and y be objects. Then we define ⟨x,y⟩ to be the object given by {{x},{x,y}}.

Background

The following background is necessary to understand this definition.

(.) ∅ is an object.

(.) Let x and y be objects. Then {x}∪y is an object.

(.) We use {x1,...,xn} as shorthand notation for the finite set with elements x1, ..., xn.

Kuratowski pairs will be our primary notion of ordered pair.

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

Feedback