IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Tarski_ZF imports ZF.Cardinal

begin

A small theory on the Tarski's axiom, inspired by a question on mathoverflow.org.

Two versions of the Tarski's axiom

There are two versions of the Tarski's axiom, one adapted from Tarski 1939 according to Wikipedia's page on Tarski-Grothendieck set theory:

\(\forall x.\ \exists y.\ x\in y \wedge (\forall z\in y.\ \mathcal{P}(z)\in \mathcal{P}(y) \wedge \mathcal{P}(z)\in y) \wedge (\forall z\in \mathcal{P}(y).\ z\approx y \vee z\in y))\),

and another one from Metamath, adapted from that page:

\(\forall x.\ \exists y.\ x\in y \wedge (\forall z\in y.\ \mathcal{P}(z)\in \mathcal{P}(y) \wedge (\exists w\in y.\ \mathcal{P}(z)\in \mathcal{P}(w))) \wedge (\forall z.\ z\in \mathcal{P}(y) \longrightarrow z\approx y \vee z\in y)\).

In this section we show that these two versions are equivalent.

The two versions of Tarski's axiom are equivalent.

theorem Tarski_axioms:

shows \( (\forall x.\ \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge Pow(z)\in y) \wedge (\forall z\in Pow(y).\ z\approx y \vee z\in y))\) \( \longleftrightarrow \) \( (\forall x.\ \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge (\exists w\in y.\ Pow(z)\in Pow(w))) \wedge (\forall z.\ z\in Pow(y) \longrightarrow z\approx y \vee z\in y)) \)proof

assume T1: \( \forall x.\ \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge Pow(z)\in y) \wedge (\forall z\in Pow(y).\ z\approx y \vee z\in y) \)

{

fix \( x \)

from T1 have \( \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge Pow(z)\in y) \wedge (\forall z\in Pow(y).\ z\approx y \vee z\in y) \)

then obtain \( y \) where \( x\in y \), \( \forall z\in y.\ Pow(z)\in Pow(y) \wedge Pow(z)\in y \), \( \forall z.\ z\in Pow(y) \longrightarrow z\approx y \vee z\in y \)

hence \( \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge (\exists w\in y.\ Pow(z)\in Pow(w))) \wedge (\forall z.\ z\in Pow(y) \longrightarrow z\approx y \vee z\in y) \)

}

thus \( \forall x.\ \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge (\exists w\in y.\ Pow(z)\in Pow(w))) \wedge (\forall z.\ z\in Pow(y) \longrightarrow z\approx y \vee z\in y) \)

next

assume T2: \( \forall x.\ \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge (\exists w\in y.\ Pow(z)\in Pow(w))) \wedge (\forall z.\ z\in Pow(y) \longrightarrow z\approx y \vee z\in y) \)

{

fix \( x \)

from T2 have \( \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge (\exists w\in y.\ Pow(z)\in Pow(w))) \wedge (\forall z.\ z\in Pow(y) \longrightarrow z\approx y \vee z\in y) \)

then obtain \( y \) where \( x\in y \) and I: \( \forall z\in y.\ Pow(z)\in Pow(y) \wedge (\exists w\in y.\ Pow(z)\in Pow(w)) \) and II: \( \forall z.\ z\in Pow(y) \longrightarrow z\approx y \vee z\in y \)

from II have III: \( \forall z\in Pow(y).\ z\approx y \vee z\in y \)

{

fix \( z \)

assume \( z\in y \)

with I have \( Pow(z)\in Pow(y) \) and \( \exists w\in y.\ Pow(z)\in Pow(w) \)

then obtain \( w \) where \( w\in y \) and \( Pow(z)\in Pow(w) \)

with I have \( Pow(z) \in y \)

with I, \( z\in y \) have \( Pow(z)\in Pow(y) \wedge Pow(z)\in y \)

}

hence \( \forall z\in y.\ Pow(z)\in Pow(y) \wedge Pow(z)\in y \)

with \( x\in y \), III have \( \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge Pow(z)\in y) \wedge (\forall z\in Pow(y).\ z\approx y \vee z\in y) \)

}

thus \( \forall x.\ \exists y.\ x\in y \wedge (\forall z\in y.\ Pow(z)\in Pow(y) \wedge Pow(z)\in y) \wedge (\forall z\in Pow(y).\ z\approx y \vee z\in y) \)

qed

end