LeanPool.FormalizationOfBoundedArithmetic.Complexity

theorem FirstOrder.Language.BoundedFormula.IsAtomic.relabelEquiv.mpr {L : Language} {α β : Type u} {n : ℕ} {φ : L.BoundedFormula α n} {f : α ≃ β} (h : φ.IsAtomic) : ((BoundedFormula.relabelEquiv f) φ).IsAtomic

theorem FirstOrder.Language.BoundedFormula.IsAtomic.relabelEquiv.mp {L : Language} {α β : Type u} {n : ℕ} {φ : L.BoundedFormula α n} {f : α ≃ β} (h : ((BoundedFormula.relabelEquiv f) φ).IsAtomic) : φ.IsAtomic

theorem FirstOrder.Language.BoundedFormula.IsAtomic.relabelEquiv {L : Language} {α β : Type u} {n : ℕ} {φ : L.BoundedFormula α n} {f : α ≃ β} : ((BoundedFormula.relabelEquiv f) φ).IsAtomic ↔ φ.IsAtomic

theorem FirstOrder.Language.Formula.IsAtomic.display1 {L : Language} {n1 : FvName} {phi : L.Formula (Vars1 n1)} : BoundedFormula.IsAtomic phi.display1 ↔ BoundedFormula.IsAtomic phi

theorem FirstOrder.Language.Formula.IsAtomic.display2 {L : Language} {n1 n2 : FvName} {phi : L.Formula (Vars2 n1 n2)} : BoundedFormula.IsAtomic (Formula.display2 n1 phi) ↔ BoundedFormula.IsAtomic phi

theorem FirstOrder.Language.Formula.IsAtomic.display3 {L : Language} {n1 n2 n3 : FvName} {phi : L.Formula (Vars3 n1 n2 n3)} : BoundedFormula.IsAtomic (Formula.display3 n1 phi) ↔ BoundedFormula.IsAtomic phi

theorem FirstOrder.Language.BoundedFormula.IsQF.imp.mpr {L : Language} {α : Type u_3} {m : ℕ} {φ ψ : L.BoundedFormula α m} : (φ.imp ψ).IsQF ↔ φ.IsQF ∧ ψ.IsQF

theorem FirstOrder.Language.BoundedFormula.IsQF.relabelEquiv.mp {L : Language} {α : Type u_3} {β : Type u_4} {m : ℕ} {φ : L.BoundedFormula α m} (f : α ≃ β) (h : φ.IsQF) : ((BoundedFormula.relabelEquiv f) φ).IsQF

theorem FirstOrder.Language.BoundedFormula.IsQF.relabelEquiv.mpr {L : Language} {α : Type u_3} {β : Type u_4} {m : ℕ} {φ : L.BoundedFormula α m} (f : α ≃ β) (h : ((BoundedFormula.relabelEquiv f) φ).IsQF) : φ.IsQF

theorem FirstOrder.Language.BoundedFormula.IsQF.relabelEquiv {L : Language} {α : Type u_3} {β : Type u_4} {m : ℕ} {φ : L.BoundedFormula α m} (f : α ≃ β) : ((BoundedFormula.relabelEquiv f) φ).IsQF ↔ φ.IsQF

@[reducible, inline]

abbrev FirstOrder.Language.BoundedFormula.IsOpen {L : Language} {α : Type u} {n : ℕ} (formula : L.BoundedFormula α n) : Prop

Open formulas are quantifier-free bounded formulas.

Equations

• formula.IsOpen = formula.IsQF

theorem FirstOrder.Language.BoundedFormula.IsOpen.equal {L : Language} {α : Type u} {n : ℕ} (t1 t2 : L.Term (α ⊕ Fin n)) : (t1.bdEqual t2).IsOpen

theorem FirstOrder.Language.BoundedFormula.IsOpen.imp.mpr.left {L : Language} {α : Type u} {n : ℕ} {phi psi : L.BoundedFormula α n} : (phi.imp psi).IsOpen → phi.IsOpen

theorem FirstOrder.Language.BoundedFormula.IsOpen.imp.mpr.right {L : Language} {α : Type u} {n : ℕ} {phi psi : L.BoundedFormula α n} : (phi.imp psi).IsOpen → psi.IsOpen

theorem FirstOrder.Language.BoundedFormula.IsOpen.not {L : Language} {α : Type u} {n : ℕ} {phi : L.BoundedFormula α n} : phi.not.IsOpen ↔ phi.IsOpen

theorem FirstOrder.Language.BoundedFormula.IsOpen.relabelEquiv {L : Language} {α β : Type u} {n : ℕ} {phi : L.BoundedFormula α n} {f : α ≃ β} : ((BoundedFormula.relabelEquiv f) phi).IsOpen ↔ phi.IsOpen

theorem FirstOrder.Language.Formula.IsOpen.display1 {L : Language} {n1 : FvName} {phi : L.Formula (Vars1 n1)} : BoundedFormula.IsOpen phi.display1 ↔ BoundedFormula.IsOpen phi

theorem FirstOrder.Language.Formula.IsOpen.display2 {L : Language} {n1 n2 : FvName} {phi : L.Formula (Vars2 n1 n2)} : BoundedFormula.IsOpen (Formula.display2 n1 phi) ↔ BoundedFormula.IsOpen phi

theorem FirstOrder.Language.Formula.IsOpen.display3 {L : Language} {n1 n2 n3 : FvName} {phi : L.Formula (Vars3 n1 n2 n3)} : BoundedFormula.IsOpen (Formula.display3 n1 phi) ↔ BoundedFormula.IsOpen phi

inductive FirstOrder.Language.BoundedFormula.IsDelta0 {L : Language} [L.IsOrdered] {a : Type} {n : ℕ} : L.BoundedFormula a n → Prop

Delta-zero formulas, built from quantifier-free formulas and bounded number quantifiers.

• bdEx {L : Language} [L.IsOrdered] {a : Type} {n : FvName} {phi : L.Formula (a ⊕ Vars1 n)} (t : L.Term (a ⊕ Fin 0)) : IsDelta0 phi → IsDelta0 (Formula.iBdEx' t phi)
• bdAll {L : Language} [L.IsOrdered] {a : Type} {n : FvName} {phi : L.Formula (a ⊕ Vars1 n)} (t : L.Term (a ⊕ Fin 0)) : IsDelta0 phi → IsDelta0 (Formula.iBdAll' t phi)
• imp {L : Language} [L.IsOrdered] {a : Type} {n : ℕ} {phi1 phi2 : L.BoundedFormula a n} : phi1.IsDelta0 → phi2.IsDelta0 → (phi1.imp phi2).IsDelta0
• of_isQF {L : Language} [L.IsOrdered] {a : Type} {n : ℕ} {phi : L.BoundedFormula a n} : phi.IsQF → phi.IsDelta0

theorem FirstOrder.Language.IsDelta0.bot {L : Language} [L.IsOrdered] {a : Type} {n : ℕ} : ⊥.IsDelta0

theorem FirstOrder.Language.IsDelta0.equal {L : Language} [L.IsOrdered] {a : Type} {n : ℕ} (t1 t2 : L.Term (a ⊕ Fin n)) : (t1.bdEqual t2).IsDelta0

theorem FirstOrder.Language.IsDelta0.of_open.imp {L : Language} [L.IsOrdered] {a : Type} {n : ℕ} {phi psi : L.BoundedFormula a n} (h : phi.IsOpen) : (phi.imp psi).IsDelta0 ↔ phi.IsDelta0 ∧ psi.IsDelta0

theorem FirstOrder.Language.IsDelta0.of_notfalsum.imp {L : Language} [L.IsOrdered] {a : Type} {n : ℕ} {phi psi : L.BoundedFormula a n} (h : psi ≠ BoundedFormula.falsum) : (phi.imp psi).IsDelta0 ↔ phi.IsDelta0 ∧ psi.IsDelta0

theorem FirstOrder.Language.IsDelta0.neq {L : Language} [L.IsOrdered] {a : Type} {n : ℕ} (t1 t2 : L.Term (a ⊕ Fin n)) : (Term.neq t1 t2).IsDelta0

theorem FirstOrder.Language.IsDelta0.of_open.not {L : Language} [L.IsOrdered] {a : Type} {n : ℕ} {phi : L.BoundedFormula a n} (h : phi.IsOpen) : phi.not.IsDelta0 ↔ phi.IsDelta0

theorem FirstOrder.Language.IsDelta0.relabelEquiv.mpAux {a b : Type} {n : ℕ} {phi : peano.BoundedFormula a n} (g : a ≃ b) (h : phi.IsDelta0) : ((BoundedFormula.relabelEquiv g) phi).IsDelta0

theorem FirstOrder.Language.IsDelta0.relabelEquiv.gSumCongr {a b c : Type} {phi : peano.Formula (a ⊕ c)} (g : a ≃ b) (h : BoundedFormula.IsDelta0 phi) : ((BoundedFormula.relabelEquiv (g.sumCongr (_root_.Equiv.refl c))) phi).IsDelta0

theorem FirstOrder.Language.IsDelta0.relabelEquiv.mp {a b : Type} {phi : peano.Formula a} (g : a ≃ b) (h : BoundedFormula.IsDelta0 phi) : ((BoundedFormula.relabelEquiv g) phi).IsDelta0

theorem FirstOrder.Language.IsDelta0.relabelEquiv.mpr {α β : Type} {φ : peano.Formula α} (f : α ≃ β) (h : ((BoundedFormula.relabelEquiv f) φ).IsDelta0) : BoundedFormula.IsDelta0 φ

theorem FirstOrder.Language.IsDelta0.relabelEquiv {α β : Type} (φ : peano.Formula α) {f : α ≃ β} : ((BoundedFormula.relabelEquiv f) φ).IsDelta0 ↔ BoundedFormula.IsDelta0 φ

theorem FirstOrder.Language.IsDelta0.display1 {n : FvName} (phi : peano.Formula (Vars1 n)) : BoundedFormula.IsDelta0 phi.display1 ↔ BoundedFormula.IsDelta0 phi

theorem FirstOrder.Language.IsDelta0.display2 {n1 n2 : FvName} (phi : peano.Formula (Vars2 n1 n2)) : BoundedFormula.IsDelta0 (Formula.display2 n1 phi) ↔ BoundedFormula.IsDelta0 phi

theorem FirstOrder.Language.IsDelta0.display3 {n1 n2 n3 : FvName} (phi : peano.Formula (Vars3 n1 n2 n3)) : BoundedFormula.IsDelta0 (Formula.display3 n1 phi) ↔ BoundedFormula.IsDelta0 phi

theorem FirstOrder.Language.IsDelta0.flip {a b : Type} (phi : peano.Formula (a ⊕ b)) : BoundedFormula.IsDelta0 phi.flip ↔ BoundedFormula.IsDelta0 phi

inductive FirstOrder.Language.BoundedFormula.IsSigma0B {a : Type} {n : ℕ} : zambella.BoundedFormula a n → Prop

Sigma-zero-B formulas in the two-sorted Zambella language.

• imp {a : Type} {x✝ : ℕ} {phi1 phi2 : zambella.BoundedFormula a x✝} (h1 : phi1.IsSigma0B) (h2 : phi2.IsSigma0B) : (phi1.imp phi2).IsSigma0B
• bdEx {a : Type} {n : FvName} (phi : zambella.Formula (a ⊕ Vars1 n)) (t : zambella.Term (a ⊕ Fin 0)) : IsSigma0B (Formula.iBdEx' t (rel ZambellaRel.isnum ![var (Sum.inl (Sum.inr Vars1.fv1))] ⊓ phi))
• bdAll {a : Type} {n : FvName} (phi : zambella.Formula (a ⊕ Vars1 n)) (t : zambella.Term (a ⊕ Fin 0)) : IsSigma0B (Formula.iBdAllNum' t phi)
• bdAllLt {a : Type} {n : FvName} (phi : zambella.Formula (a ⊕ Vars1 n)) (t : zambella.Term (a ⊕ Fin 0)) : IsSigma0B (Formula.iBdAllLt' t (rel ZambellaRel.isnum ![var (Sum.inl (Sum.inr Vars1.fv1))] ⊓ phi))
• of_isQF {a : Type} {x✝ : ℕ} {phi : zambella.BoundedFormula a x✝} (h : phi.IsQF) : phi.IsSigma0B

theorem FirstOrder.Language.Sigma0B.relabelEquiv.mpAux {a b : Type} {n : ℕ} {phi : zambella.BoundedFormula a n} (g : a ≃ b) (h : phi.IsSigma0B) : ((BoundedFormula.relabelEquiv g) phi).IsSigma0B

theorem FirstOrder.Language.Sigma0B.relabelEquiv.mprAux {a b : Type} {n : ℕ} {phi : zambella.BoundedFormula a n} (g : a ≃ b) (h : ((BoundedFormula.relabelEquiv g) phi).IsSigma0B) : phi.IsSigma0B

theorem FirstOrder.Language.Sigma0B.relabelEquiv {a b : Type} {g : a ≃ b} (phi : zambella.Formula a) : ((BoundedFormula.relabelEquiv g) phi).IsSigma0B ↔ BoundedFormula.IsSigma0B phi

def FirstOrder.Language.Sigma0B.tacticSigma0bViaRelabel_ : Lean.ParserDescr

Discharge a Sigma0B closure lemma for a Formula.* reshaping.

Equations

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

theorem FirstOrder.Language.Sigma0B.display1 {n1 : FvName} (phi : zambella.Formula (Vars1 n1)) : BoundedFormula.IsSigma0B phi.display1 ↔ BoundedFormula.IsSigma0B phi

theorem FirstOrder.Language.Sigma0B.display2 {n1 n2 : FvName} (phi : zambella.Formula (Vars2 n1 n2)) : BoundedFormula.IsSigma0B (Formula.display2 n1 phi) ↔ BoundedFormula.IsSigma0B phi

theorem FirstOrder.Language.Sigma0B.display3 {n1 n2 n3 : FvName} (phi : zambella.Formula (Vars3 n1 n2 n3)) : BoundedFormula.IsSigma0B (Formula.display3 n1 phi) ↔ BoundedFormula.IsSigma0B phi

theorem FirstOrder.Language.Sigma0B.display4 {n1 n2 n3 n4 : FvName} (phi : zambella.Formula (Vars4 n1 n2 n3 n4)) : BoundedFormula.IsSigma0B (Formula.display4 n1 phi) ↔ BoundedFormula.IsSigma0B phi

theorem FirstOrder.Language.Sigma0B.displaySwapleft {n1 n2 n3 : FvName} (phi : zambella.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) : BoundedFormula.IsSigma0B phi.displaySwapleft ↔ BoundedFormula.IsSigma0B phi

theorem FirstOrder.Language.Sigma0B.displaySwapleft' {n1 n2 n3 : FvName} (phi : zambella.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) : BoundedFormula.IsSigma0B phi.displaySwapleft' ↔ BoundedFormula.IsSigma0B phi

theorem FirstOrder.Language.Sigma0B.rotate21 {n1 n2 : FvName} (phi : zambella.Formula (Vars2 n1 n2)) : BoundedFormula.IsSigma0B phi.rotate21 ↔ BoundedFormula.IsSigma0B phi

theorem FirstOrder.Language.Sigma0B.rotate213 {n1 n2 n3 : FvName} (phi : zambella.Formula (Vars3 n1 n2 n3)) : BoundedFormula.IsSigma0B (Formula.rotate213 n1 n2 n3 phi) ↔ BoundedFormula.IsSigma0B phi

theorem FirstOrder.Language.Sigma0B.rotate231 {n1 n2 n3 : FvName} (phi : zambella.Formula (Vars3 n1 n2 n3)) : BoundedFormula.IsSigma0B (Formula.rotate231 n1 n2 n3 phi) ↔ BoundedFormula.IsSigma0B phi

theorem FirstOrder.Language.Sigma0B.flip {a b : Type} (phi : zambella.Formula (a ⊕ b)) : BoundedFormula.IsSigma0B phi.flip ↔ BoundedFormula.IsSigma0B phi

def FirstOrder.Language.simpComplexity : Lean.ParserDescr

Simplify complexity side conditions in a hypothesis.

Equations

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