Type Theory

Type Theory from a Set-Theoretic Perspective

In early type theory and logic, expressions like

$\{x \mid x \neq x\}$

describe a collection of objects satisfying a property.

Read it as:

“the collection of all $x$ such that $x$ is not equal to $x$.”

Here:

• x is a variable
• | means “such that”
• x \neq x is the predicate (a logical condition)

But equality is reflexive:

$x = x$

for every $x$.

So the predicate is always false.

That means no object inhabits this set:

$\{x \mid x \neq x\} = \emptyset$