Set Theory and Logic

Cantor's Theorem

Every set is strictly smaller than its power set: |X| < |2^X| for any set X.

lean4-proofset-theory-logicvisualization

Schröder–Bernstein Theorem

If there are injections A → B and B → A, then A and B have equal cardinality.

lean4-proofset-theory-logicvisualization

Zorn's Lemma

If every chain in a nonempty poset has an upper bound, the poset has a maximal element.

lean4-proofset-theory-logicvisualization

Well-Ordering Theorem

Every set can be well-ordered: given AC, every set admits a relation under which every nonempty subset has a minimum.

lean4-proofset-theory-logicvisualization

Compactness Theorem (FOL)

A first-order theory has a model if and only if every finite subset has a model.

lean4-proofset-theory-logicvisualization

Löwenheim–Skolem Theorem

A first-order theory with an infinite model has models of every infinite cardinality.

lean4-proofset-theory-logicvisualization

Gödel's Completeness Theorem

A first-order sentence is provable from a theory iff it holds in every model of that theory.

lean4-proofset-theory-logicvisualization

Halting Problem Undecidable

There is no computable function that decides whether an arbitrary program halts on a given input.

lean4-proofset-theory-logicvisualization

Gödel's Incompleteness Theorems

In any consistent, sufficiently strong formal system, there are true statements that cannot be proved — and the system cannot prove its own consistency.

lean4-proofset-theory-logicvisualization

Axiom of Choice

For any collection of nonempty sets there exists a function selecting one element from each — equivalent to Zorn's lemma and the well-ordering theorem.

lean4-proofset-theory-logicvisualization