LeanPool.FormalizationOfBoundedArithmetic.Semantics

theorem FirstOrder.Language.Term.realize_zero {M : Type u_1} [peano.Structure M] {a : Type u_4} {env : a → M} : realize env 0 = 0

theorem FirstOrder.Language.Term.realize_one {M : Type u_1} [peano.Structure M] {a : Type u_4} {env : a → M} : realize env 1 = 1

theorem FirstOrder.Language.Term.realize_add {M : Type u_1} [h : peano.Structure M] {a : Type u_4} {env : a → M} (t u : peano.Term a) : realize env (t + u) = realize env t + realize env u

theorem FirstOrder.Language.Term.realize_mul {M : Type u_1} [peano.Structure M] {a : Type u_4} {env : a → M} (t u : peano.Term a) : realize env (t * u) = realize env t * realize env u

def FirstOrder.Language.Formula.tacticRealizeViaRelabel_ : Lean.ParserDescr

Discharge a realize_* lemma whose displayed form is a relabelEquiv. The target is the Formula.* reshaping definition being unfolded.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.Formula.realize_flip {L : Language} {M : Type u_1} [L.Structure M] {a : Type u_5} {b : Type u_4} (phi : L.Formula (a ⊕ b)) {v : b ⊕ a → M} : phi.flip.Realize v ↔ phi.Realize (v ∘ Sum.swap)

theorem FirstOrder.Language.Formula.realize_rotate_21 {L : Language} {M : Type u_1} [L.Structure M] {n1 n2 : FvName} (phi : L.Formula (Vars2 n1 n2)) {v : Vars2 n2 n1 → M} : phi.rotate21.Realize v ↔ phi.Realize (v ∘ fun (fv : Vars2 n1 n2) => match fv with | Vars2.fv1 => Vars2.fv2 | Vars2.fv2 => Vars2.fv1)

theorem FirstOrder.Language.Formula.realize_rotate_213 {L : Language} {M : Type u_1} [L.Structure M] {n1 n2 n3 : FvName} (phi : L.Formula (Vars3 n1 n2 n3)) {v : Vars3 n2 n1 n3 → M} : (rotate213 n1 n2 n3 phi).Realize v ↔ phi.Realize (v ∘ fun (fv : Vars3 n1 n2 n3) => match fv with | Vars3.fv1 => Vars3.fv2 | Vars3.fv2 => Vars3.fv1 | Vars3.fv3 => Vars3.fv3)

theorem FirstOrder.Language.Formula.realize_mkInl {L : Language} {M : Type u_1} [L.Structure M] {a : Type u_4} (phi : L.Formula a) {v : a ⊕ Empty → M} : phi.mkInl.Realize v ↔ phi.Realize (v ∘ Sum.inl)

theorem FirstOrder.Language.Formula.realize_display1 {L : Language} {M : Type u_1} [L.Structure M] {n1 : FvName} (phi : L.Formula (Vars1 n1)) {v : Vars1 n1 ⊕ Empty → M} : phi.display1.Realize v ↔ phi.Realize (v ∘ Sum.inl)

theorem FirstOrder.Language.Formula.realize_display2 {L : Language} {M : Type u_1} [L.Structure M] {n1 n2 : FvName} (phi : L.Formula (Vars2 n1 n2)) {v : Vars1 n1 ⊕ Vars1 n2 → M} : (display2 n1 phi).Realize v ↔ phi.Realize (v ∘ fun (fv : Vars2 n1 n2) => match fv with | Vars2.fv1 => Sum.inl Vars1.fv1 | Vars2.fv2 => Sum.inr Vars1.fv1)

theorem FirstOrder.Language.Formula.realize_display3 {L : Language} {M : Type u_1} [L.Structure M] {n1 n2 n3 : FvName} (phi : L.Formula (Vars3 n1 n2 n3)) {v : Vars1 n1 ⊕ Vars2 n2 n3 → M} : (display3 n1 phi).Realize v ↔ phi.Realize (v ∘ fun (fv : Vars3 n1 n2 n3) => match fv with | Vars3.fv1 => Sum.inl Vars1.fv1 | Vars3.fv2 => Sum.inr Vars2.fv1 | Vars3.fv3 => Sum.inr Vars2.fv2)

theorem FirstOrder.Language.Formula.realize_display4 {L : Language} {M : Type u_1} [L.Structure M] {n1 n2 n3 n4 : FvName} (phi : L.Formula (Vars4 n1 n2 n3 n4)) {v : Vars1 n1 ⊕ Vars3 n2 n3 n4 → M} : (display4 n1 phi).Realize v ↔ phi.Realize (v ∘ fun (fv : Vars4 n1 n2 n3 n4) => match fv with | Vars4.fv1 => Sum.inl Vars1.fv1 | Vars4.fv2 => Sum.inr Vars3.fv1 | Vars4.fv3 => Sum.inr Vars3.fv2 | Vars4.fv4 => Sum.inr Vars3.fv3)

theorem FirstOrder.Language.Formula.realize_display_swapleft {L : Language} {M : Type u_1} [L.Structure M] {n1 n2 n3 : FvName} (phi : L.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) {v : Vars2 n1 n2 ⊕ Vars1 n3 → M} : phi.displaySwapleft.Realize v ↔ phi.Realize (v ∘ fun (fv : Vars1 n1 ⊕ Vars2 n2 n3) => match fv with | Sum.inl Vars1.fv1 => Sum.inl Vars2.fv1 | Sum.inr Vars2.fv1 => Sum.inl Vars2.fv2 | Sum.inr Vars2.fv2 => Sum.inr Vars1.fv1)

theorem FirstOrder.Language.Formula.realize_display_swapleft' {L : Language} {M : Type u_1} [L.Structure M] {n1 n2 n3 : FvName} (phi : L.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) {v : (Vars1 n1 ⊕ Vars1 n2) ⊕ Vars1 n3 → M} : phi.displaySwapleft'.Realize v ↔ phi.Realize (v ∘ fun (fv : Vars1 n1 ⊕ Vars2 n2 n3) => match fv with | Sum.inl Vars1.fv1 => Sum.inl (Sum.inl Vars1.fv1) | Sum.inr Vars2.fv1 => Sum.inl (Sum.inr Vars1.fv1) | Sum.inr Vars2.fv2 => Sum.inr Vars1.fv1)

def FirstOrder.Language.Formula.peelIAlls : Lean.ParserDescr

peel_iAlls' k rewrites (iAlls' φ).Realize by peeling exactly k quantifiers (realize_all; intro).

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.Formula.peelIExs : Lean.ParserDescr

peel_iExs' k rewrites (iExs' φ).Realize by peeling exactly k quantifiers (realize_ex; intro).

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.Formula.realize_iAlls'.Empty {L : Language} {M : Type u_1} [L.Structure M] {a : Type} (phi : L.Formula (a ⊕ _root_.Empty)) {v : a → M} : phi.iAlls'.Realize v ↔ phi.Realize (Sum.elim v Empty.elim)

theorem FirstOrder.Language.Formula.realize_iAlls'.Vars1 {L : Language} {M : Type u_1} [L.Structure M] {a : Type} {n1 : FvName} (phi : L.Formula (a ⊕ _root_.Vars1 n1)) {v : a → M} : phi.iAlls'.Realize v ↔ ∀ (x : M), phi.Realize (Sum.elim v fun (fv : _root_.Vars1 n1) => match fv with | Vars1.fv1 => x)

theorem FirstOrder.Language.Formula.realize_iAlls'.Vars2 {L : Language} {M : Type u_1} [L.Structure M] {a : Type} {n1 n2 : FvName} (phi : L.Formula (a ⊕ _root_.Vars2 n1 n2)) {v : a → M} : phi.iAlls'.Realize v ↔ ∀ (x y : M), phi.Realize (Sum.elim v fun (fv : _root_.Vars2 n1 n2) => match fv with | Vars2.fv1 => x | Vars2.fv2 => y)

theorem FirstOrder.Language.Formula.realize_iAlls'.Vars3 {L : Language} {M : Type u_1} [L.Structure M] {a : Type} {n1 n2 n3 : FvName} (phi : L.Formula (a ⊕ _root_.Vars3 n1 n2 n3)) {v : a → M} : phi.iAlls'.Realize v ↔ ∀ (x y z : M), phi.Realize (Sum.elim v fun (fv : _root_.Vars3 n1 n2 n3) => match fv with | Vars3.fv1 => x | Vars3.fv2 => y | Vars3.fv3 => z)

theorem FirstOrder.Language.Formula.realize_iExs'.Vars1 {L : Language} {M : Type u_1} [L.Structure M] {a : Type} {n1 : FvName} (phi : L.Formula (a ⊕ _root_.Vars1 n1)) {v : a → M} : phi.iExs'.Realize v ↔ ∃ (x : M), phi.Realize (Sum.elim v fun (fv : _root_.Vars1 n1) => match fv with | Vars1.fv1 => x)

theorem FirstOrder.Term.realize_isnum {num str : Type u} [Language.ZambellaModel num str] {a : Type} {t : Language.zambella.Term (a ⊕ Fin 0)} {v : a → num ⊕ str} : t.IsNum.Realize v ↔ (Language.Term.realize (Sum.elim v Fin.elim0) t).isLeft = true

theorem FirstOrder.Term.realize_isstr {num str : Type u} [Language.ZambellaModel num str] {a : Type} {t : Language.zambella.Term (a ⊕ Fin 0)} {v : a → num ⊕ str} : t.IsStr.Realize v ↔ (Language.Term.realize (Sum.elim v Fin.elim0) t).isRight = true

theorem FirstOrder.Term.realize_in {num str : Type u} [Language.ZambellaModel num str] {a : Type} {n : ℕ} {t1 t2 : Language.zambella.Term (a ⊕ Fin n)} {v : a → num ⊕ str} {xs : Fin n → num ⊕ str} : («in» t1 t2).Realize v xs ↔ Language.Term.realize (Sum.elim v xs) t1 ∈ Language.Term.realize (Sum.elim v xs) t2

theorem FirstOrder.Language.Formula.realize_in {num str : Type u} [ZambellaModel num str] {a : Type} {t1 t2 : zambella.Term (a ⊕ Fin 0)} {v : a → num ⊕ str} : Realize (Term.in t1 t2) v ↔ Term.realize (Sum.elim v default) t1 ∈ Term.realize (Sum.elim v default) t2

theorem FirstOrder.Language.Formula.realize_notin {num str : Type u} [ZambellaModel num str] {a : Type} {t1 t2 : zambella.Term (a ⊕ Fin 0)} {v : a → num ⊕ str} {xs : Fin 0 → num ⊕ str} : (Term.notin t1 t2).Realize v xs ↔ Term.realize (Sum.elim v default) t1 ∉ Term.realize (Sum.elim v default) t2

theorem FirstOrder.Language.Formula.realize_iBdEx' {a : Type} {n1 : FvName} {M : Type u_2} [peano.Structure M] {t : peano.Term (a ⊕ Fin 0)} (phi : peano.Formula (a ⊕ Vars1 n1)) {v : a → M} : (iBdEx' t phi).Realize v ↔ ∃ x ≤ Term.realize (Sum.elim v Fin.elim0) t, phi.Realize (Sum.elim v fun (x_1 : Vars1 n1) => x)

theorem FirstOrder.Language.Formula.realize_iBdAll'.Vars1 {a : Type} {n1 : FvName} {num str : Type u_2} [inst1 : ZambellaModel num str] (phi : zambella.Formula (a ⊕ _root_.Vars1 n1)) {t : zambella.Term (a ⊕ Fin 0)} {v : a → num ⊕ str} : (iBdAll' t phi).Realize v ↔ ∀ x ≤ Term.realize (Sum.elim v default) t, phi.Realize (Sum.elim v fun (fv : _root_.Vars1 n1) => match fv with | Vars1.fv1 => x)

theorem FirstOrder.Language.Formula.realize_iBdAllLt'.Vars1 {L : Language} {a : Type} {n1 : FvName} {M : Type u_2} [L.IsOrdered] [L.Structure M] [Preorder M] [h : L.OrderedStructure M] (phi : L.Formula (a ⊕ _root_.Vars1 n1)) {t : L.Term (a ⊕ Fin 0)} {v : a → M} : (iBdAllLt' t phi).Realize v ↔ ∀ x < Term.realize (Sum.elim v default) t, phi.Realize (Sum.elim v fun (fv : _root_.Vars1 n1) => match fv with | Vars1.fv1 => x)

theorem FirstOrder.Language.Formula.realize_iBdAllNum'.Vars1 {a : Type} {n1 : FvName} {num str : Type u_2} [inst1 : ZambellaModel num str] (phi : zambella.Formula (a ⊕ _root_.Vars1 n1)) {t : zambella.Term (a ⊕ Fin 0)} {v : a → num ⊕ str} : (iBdAllNum' t phi).Realize v ↔ ∀ x ≤ Term.realize (Sum.elim v default) t, x.isLeft = true → phi.Realize (Sum.elim v fun (fv : _root_.Vars1 n1) => match fv with | Vars1.fv1 => x)