Theory Tarski_ZF

section‹Two versions of Tarski's Axiom›

theory Tarski_ZF imports ZF.Cardinal

begin

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

subsection‹Two versions of the Tarski's axiom›

text‹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. ›

text‹The two versions of Tarski's axiom are equivalent.›

theorem Tarski_axioms: shows 
  "(∀x. ∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ Pow(z)∈y) ∧ (∀z∈Pow(y). z≈y ∨ z∈y))
  ⟷
  (∀x. ∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ (∃w∈y. Pow(z)∈Pow(w))) ∧ (∀z. z∈Pow(y) ⟶ z≈y ∨ z∈y))"
proof
  assume T1: "∀x. ∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ Pow(z)∈y) ∧ (∀z∈Pow(y). z≈y ∨ z∈y)"
  { fix x
    from T1 have "∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ Pow(z)∈y) ∧ (∀z∈Pow(y). z≈y ∨ z∈y)"
      by simp
    then obtain y where "x∈y" "∀z∈y. Pow(z)∈Pow(y) ∧ Pow(z)∈y" "∀z. z∈Pow(y) ⟶ z≈y ∨ z∈y" 
      by auto
    hence 
      "∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ (∃w∈y. Pow(z)∈Pow(w))) ∧ (∀z. z∈Pow(y) ⟶ z≈y ∨ z∈y)"
      by auto
  } 
  thus 
    "∀x. ∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ (∃w∈y. Pow(z)∈Pow(w))) ∧ (∀z. z∈Pow(y) ⟶ z≈y ∨ z∈y)"
    by simp
next
  assume T2: 
    "∀x. ∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ (∃w∈y. Pow(z)∈Pow(w))) ∧ (∀z. z∈Pow(y) ⟶ z≈y ∨ z∈y)"
  { fix x
    from T2 have 
      "∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ (∃w∈y. Pow(z)∈Pow(w))) ∧ (∀z. z∈Pow(y) ⟶ z≈y ∨ z∈y)"
      by simp
    then obtain y where "x∈y" and I: "∀z∈y. Pow(z)∈Pow(y) ∧ (∃w∈y. Pow(z)∈Pow(w))" and
      II: "∀z. z∈Pow(y) ⟶ z≈y ∨ z∈y" by auto
    from II have III: "∀z∈Pow(y). z≈y ∨ z∈y" by blast
    { fix z assume "z∈y"
      with I have "Pow(z)∈Pow(y)" and "∃w∈y. Pow(z)∈Pow(w)" by simp_all
      then obtain w where "w∈y" and "Pow(z)∈Pow(w)" by auto
      with I have "Pow(z) ∈ y" by auto
      with I ‹z∈y› have "Pow(z)∈Pow(y) ∧ Pow(z)∈y" by simp
    } hence "∀z∈y. Pow(z)∈Pow(y) ∧ Pow(z)∈y" by simp
    with ‹x∈y› III have "∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ Pow(z)∈y) ∧ (∀z∈Pow(y). z≈y ∨ z∈y)"
      by auto
  }
  thus "∀x. ∃y. x∈y ∧ (∀z∈y. Pow(z)∈Pow(y) ∧ Pow(z)∈y) ∧ (∀z∈Pow(y). z≈y ∨ z∈y)"
    by simp
qed
       
end