Axiomatic Foundations - Mizar

1. ZF Axioms in Mizar
2. Soft Types Examples: Subsets

The foundations of mathematics used by Mizar is actually formalized in a couple articles in the current MML:

tarski_0 for the ZF axioms used by Mizar
tarski_a for the axiom stating the existence of a Grothendieck universe containing a given set

1. ZF Axioms in Mizar

The ZF axioms contained in Mizar:

Extensionality: for \(X,Y\) being set st
(for \(x\) being object holds (\(x\in X \iff x\in Y\)))
holds \(X = Y\)
Regularity: for \(x_{1}\) being object
for \(X\) being set st \(x_{1}\in X\) holds
exists \(Y\) being set st
(\(Y\in X\) & (for \(x_{2}\) being object holds (\(x_{2}\notin X\) or \(x_{2}\notin Y\))))
Pair: for \(X,Y\) being any object
exists \(Z\) being a set such that
for any object \(a\)
holds \(a\in Z\) if and only if \(a=X\) or \(a=Y\).
Union: for \(X\) being set
exists \(Z\) being set st
for \(x\) being object holds
(\(x\in Z\) iff exists \(Y\) being set st (\(x\in Y\) & \(Y\in X\)))
Schema of Replacement: exists \(X\) being set st
for \(x\) being object holds
(\(x\in X\) iff exists \(y\) being object st (\(y\in F_{1}()\) & \(P_{1}[y,x]\)))
provided for \(x, y, z\) being object st \(P_{1}[x,y]\) & \(P_{1}[x,z]\) holds \(y = z\)

The axiom of regularity may look a little strange, but remember: if we have \(\forall X((\exists x, P[x,X])\implies Q[X])\), then this is logically equivalent to \(\forall X\forall x(P[x,X]\implies Q[X])\).

The axiom schema of specification can be derived from the schema of replacement.

Mizar just defines the unordered pair \(\{X,Y\}\) for any \(X\), \(Y\) in TARSKI:def 2…but uses the axiom of pairing to justify its existence.

The two missing ZF axioms are the axiom of infinity, and the axiom of the power set. The power set in Mizar is bool X for \(\mathcal{P}(X)\) and is defined in ZFMISC_1:def 1, its existence follows from the Universe axiom.

Tarski Universe Axiom: for \(N\) being set
exists \(M\) being set st
(\(N\in M\) &
(for \(X\), \(Y\) being set st \(X\in M\) & \(Y\subset X\) holds \(Y\in M\)) &
(for \(X\) being set st \(X\in M\) holds
exists \(Z\) being set st
(\(Z \in M\) & (for \(Y\) being set st \(Y\subset X\) holds \(Y\in Z\)))) &
(for \(X\) being set holds (\(X\not\subset M\), or \(X\) and \(M\) are equipotent, or \(X\in M\))))

This gives us the powerset exists (it's the third condition).

The generalized axiom of infinity is derived as Ordinal_1:Th32. Of course, working our way backwards, this uses Theorem ZfMisc_1:112 which depends on the axiom of the universe.

There is also the well-ordering theorem (which Wikipedia includes in the ZF axioms, but I do not believe it's actually needed — it should be included for ZFC, though). Mizar proves this in WELLORD2:Th17.

Thus Tarski-Grothendieck set theory contains ZF set theory's axioms.

Furthermore, the axiom of choice is derived from the axiom of the universe in WELLORD2:Th18. So really, Tarski-Grothendieck set theory contains the ZFC axioms.

These formed the contents of the first article in Formalized Mathematics:

Andrzej Trybulec,
"Tarski Grothendieck Set Theory".
Formalized Mathematics 1, no.1 (1990) 9–11, PDF.

2. Soft Types Examples: Subsets

We have a predicate for \(\subseteq\) encoded in Mizar TARSKI:def 3 as:

definition
  let X, Y be set;
  pred X c= Y means :: TARSKI:def 3
  for x being object st x in X holds x in Y;
  reflexivity;
end;

The type for a Subset of \(X\) is defined in SUBSET_1 as

definition
  let X be set;
  mode Subset of X is Element of bool X;
end;

and bool of X is defined in ZFMISC_1:def 1 as:

definition
  let X be set ;
  func bool X -> set means :Def1: :: ZFMISC_1:def 1
  for Z being set holds
  (Z in it iff Z c= X);
  :: correctness conditions omitted
end;

When we include SUBSET in the requirements directive, Mizar will automatically infer from X c= Y that X is Subset of Y. If we want to establish this claim, it amounts to showing for any object x st x in X we have x in Y.

Axiomatic Foundations - Mizar

Table of Contents

1. ZF Axioms in Mizar

2. Soft Types Examples: Subsets