The Basics of First Order Language of ZFC set theory

Main Definitions

• A FirstOrder.Language.LZFC defines the language of ZFC set theory. It consists only of the binary relation ∈'.
• A FirstOrder.ZFC.fv' defines the free variable with index k. The first argument is implicitly determined.
• A FirstOrder.ZFC.bv' defines the bounded variable with index (k : Fin n). The first argument is implicitly determined.
• A FirstOrder.ZFC.bv'' defines the bounded variable with index (k : ℕ). The first argument is implicitly determined.
• A FirsOrder.ZFC.ModelSets is a class of models of set theory.

Notations

• ∈' is the symbol to mean "is an element of".
• ∉' is the symbol to mean "is not an element of".
• ≠' is the symbol to mean "is not equal to". Recall that =' is defined as FirstOrder.Language.Term.bdEqual.
• ∈ is the actual relation to mean "is an element of".
• ∉ is the actual relation to mean "is not an element of".

Implimentation notes

• Most of the relations have the theorems named "realize_*". They prove the relationship between the internal and external expressions.

inductive FirstOrder.LSetRel : ℕ → Type

Relation symbols for LSet.

• isEltOf : LSetRel 2

@[implicit_reducible]

instance FirstOrder.instDecidableEqLSetRel {a✝ : ℕ} : DecidableEq (LSetRel a✝)

Equations

• FirstOrder.instDecidableEqLSetRel = FirstOrder.instDecidableEqLSetRel.decEq

def FirstOrder.instDecidableEqLSetRel.decEq {a✝ : ℕ} (x✝ x✝¹ : LSetRel a✝) : Decidable (x✝ = x✝¹)

Equations

• FirstOrder.instDecidableEqLSetRel.decEq FirstOrder.LSetRel.isEltOf FirstOrder.LSetRel.isEltOf = isTrue FirstOrder.instDecidableEqLSetRel.decEq._proof_1

def FirstOrder.Language.LZFC : Language

Language of Set Theory.

Equations

• FirstOrder.Language.LZFC = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.LSetRel }

def FirstOrder.ZFC.isEltOfTwo : Language.LZFC.Relations 2

The version of isEltOf with the type LSet.Relations 2.

Equations

• FirstOrder.ZFC.isEltOfTwo = FirstOrder.LSetRel.isEltOf

def FirstOrder.ZFC.ϕbot : Language.LZFC.Formula ℕ

The formula ⊥

Equations

• FirstOrder.ZFC.ϕbot = FirstOrder.Language.BoundedFormula.falsum

def FirstOrder.ZFC.ϕelt {n : ℕ} (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Make an atomic formula t1 ∈ t2.

Equations

• FirstOrder.ZFC.ϕelt t₁ t₂ = FirstOrder.ZFC.isEltOfTwo.boundedFormula₂ t₁ t₂

def FirstOrder.«term_∈'_» : Lean.TrailingParserDescr

Make an atomic formula t1 ∈ t2.

Equations

• FirstOrder.«term_∈'_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_∈'_» 120 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈' ") (Lean.ParserDescr.cat `term 121))

def FirstOrder.ZFC.ϕnotElt {n : ℕ} (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

Make an atomic formula t1 ∉ t2.

Equations

• FirstOrder.ZFC.ϕnotElt t₁ t₂ = (FirstOrder.ZFC.isEltOfTwo.boundedFormula₂ t₁ t₂).not

def FirstOrder.«term_∉'_» : Lean.TrailingParserDescr

Make an atomic formula t1 ∉ t2.

Equations

• FirstOrder.«term_∉'_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_∉'_» 120 120 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∉' ") (Lean.ParserDescr.cat `term 121))

def FirstOrder.ZFC.intNotEqual {n : ℕ} (t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)) : Language.LZFC.BoundedFormula ℕ n

The negation of the equality of two terms as a bounded formula.

Equations

• FirstOrder.ZFC.intNotEqual t₁ t₂ = (t₁.bdEqual t₂).not

def FirstOrder.«term_≠'_» : Lean.TrailingParserDescr

The negation of the equality of two terms as a bounded formula.

Equations

• FirstOrder.«term_≠'_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_≠'_» 88 88 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≠' ") (Lean.ParserDescr.cat `term 89))

def FirstOrder.ZFC.fv (n k : ℕ) : Language.LZFC.Term (ℕ ⊕ Fin n)

Make a free variable in LSet.

Equations

• FirstOrder.ZFC.fv n k = FirstOrder.Language.var (Sum.inl k)

def FirstOrder.ZFC.bv (n : ℕ) (k : Fin n) : Language.LZFC.Term (ℕ ⊕ Fin n)

Make a to-be bounded variable indexed by k, in which free variables are indexed by ℕ.

Equations

• FirstOrder.ZFC.bv n k = FirstOrder.Language.var (Sum.inr k)

class FirstOrder.ZFC.ModelSets (V : Type u) extends FirstOrder.Language.LZFC.Structure V, Inhabited V : Type u

Model of set theory.

• funMap {n : ℕ} : LZFC.Functions n → (Fin n → V) → V
• RelMap {n : ℕ} : LZFC.Relations n → (Fin n → V) → Prop
• default : V
• isEltOf : V → V → Prop

  The external membership relation interpreting the language's ∈ symbol.

• interpret_is_elt_of {a b : V} : a ∈ b ↔ Language.Structure.RelMap isEltOfTwo ![a, b]

  The external relation matches the language's RelMap.

• extensionality {a b : V} : (∀ (z : V), z ∈ a ↔ z ∈ b) → a = b

  Extensionality: sets with the same elements are equal.

def FirstOrder.ZFC.notIsEltOf {V : Type u} [ModelSets V] (a b : V) : Prop

The negation of ModelSets.isEltOf.

Equations

• a ∉ b = ¬a ∈ b

def FirstOrder.ZFC.«term_∈_» : Lean.TrailingParserDescr

The external membership relation interpreting the language's ∈ symbol.

Equations

• FirstOrder.ZFC.«term_∈_» = Lean.ParserDescr.trailingNode `FirstOrder.ZFC.«term_∈_» 120 121 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ ") (Lean.ParserDescr.cat `term 121))

def FirstOrder.ZFC.«term_∉_» : Lean.TrailingParserDescr

The negation of ModelSets.isEltOf.

Equations

• FirstOrder.ZFC.«term_∉_» = Lean.ParserDescr.trailingNode `FirstOrder.ZFC.«term_∉_» 120 121 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∉ ") (Lean.ParserDescr.cat `term 121))

@[simp]

theorem FirstOrder.ZFC.realize_fv {V : Type u} [ModelSets V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} (k : ℕ) : Language.Term.realize (Sum.elim s xs) (fv n k) = s k

Realize a free varaible.

@[simp]

theorem FirstOrder.ZFC.realize_bv {V : Type u} [ModelSets V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (k : Fin n) : Language.Term.realize (Sum.elim s xs) (bv n k) = xs k

Realize a bounded variable with the type ℕ.

@[simp]

theorem FirstOrder.ZFC.realize_in {V : Type u} [ModelSets V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)} : (ϕelt t₁ t₂).Realize s xs ↔ Language.Term.realize (Sum.elim s xs) t₁ ∈ Language.Term.realize (Sum.elim s xs) t₂

@[simp]

theorem FirstOrder.ZFC.realize_nin {V : Type u} [ModelSets V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)} : (ϕnotElt t₁ t₂).Realize s xs ↔ Language.Term.realize (Sum.elim s xs) t₁ ∉ Language.Term.realize (Sum.elim s xs) t₂

@[simp]

theorem FirstOrder.ZFC.realize_neq {V : Type u} [ModelSets V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {t₁ t₂ : Language.LZFC.Term (ℕ ⊕ Fin n)} : (intNotEqual t₁ t₂).Realize s xs ↔ Language.Term.realize (Sum.elim s xs) t₁ ≠ Language.Term.realize (Sum.elim s xs) t₂

def FirstOrder.ZFC.fv' {n : ℕ} (k : ℕ) : Language.LZFC.Term (ℕ ⊕ Fin n)

Make a free variable in LSet with n implicit.

Equations

• FirstOrder.ZFC.fv' k = FirstOrder.Language.var (Sum.inl k)

def FirstOrder.ZFC.bv' {n : ℕ} (k : Fin n) : Language.LZFC.Term (ℕ ⊕ Fin n)

Make a to-be bounded variable indexed by (k : Fin n), in which free variables are indexed by ℕ with n implicit.

Equations

• FirstOrder.ZFC.bv' k = FirstOrder.Language.var (Sum.inr k)

def FirstOrder.ZFC.bv'' {n : ℕ} [NeZero n] (k : ℕ) : Language.LZFC.Term (ℕ ⊕ Fin n)

Make a to-be bounded variable indexed by (k : ℕ), in which free variables are indexed by ℕ with n implicit.

Equations

• FirstOrder.ZFC.bv'' k = FirstOrder.Language.var (Sum.inr (Fin.ofNat n k))

@[simp]

theorem FirstOrder.ZFC.realize_fv' {V : Type u} [ModelSets V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} (k : ℕ) : Language.Term.realize (Sum.elim s xs) (fv' k) = s k

Realize a free varaible.

@[simp]

theorem FirstOrder.ZFC.realize_bv' {V : Type u} [ModelSets V] {n : ℕ} (s : ℕ → V) (xs : Fin n → V) (k : Fin n) : Language.Term.realize (Sum.elim s xs) (bv' k) = xs k

Realize bv' with the type ℕ.

@[simp]

theorem FirstOrder.ZFC.realize_bv'' {V : Type u} [ModelSets V] {n : ℕ} [NeZero n] (s : ℕ → V) (xs : Fin n → V) (k : ℕ) : Language.Term.realize (Sum.elim s xs) (bv'' k) = xs (Fin.ofNat n k)

Realize bv'' with the type ℕ.