Basic definitions and properties of proof system related notions

This file defines a characterization of the system/proof/provability/calculus of formulae. Also defines soundness and completeness.

Main Definitions

• LO.System F S: a general framework of deductive system S for formulae F.
• LO.System.Inconsistent 𝓢: a proposition that states that all formulae in F is provable from 𝓢.
• LO.System.Consistent 𝓢: a proposition that states that 𝓢 is not inconsistent.
• LO.System.Sound 𝓢 𝓜: provability from 𝓢 implies satisfiability on 𝓜.
• LO.System.Complete 𝓢 𝓜: satisfiability on 𝓜 implies provability from 𝓢.

Notation

• 𝓢 ⊢ φ: a type of formalized proofs of φ : F from deductive system 𝓢 : S.
• 𝓢 ⊢! φ: a proposition that states there is a proof of φ from 𝓢, i.e. φ is provable from 𝓢.
• 𝓢 ⊬ φ: a proposition that states φ is not provable from 𝓢.
• 𝓢 ⊢* T: a type of formalized proofs for each formulae in a set T from 𝓢.
• 𝓢 ⊢!* T: a proposition that states each formulae in T is provable from 𝓢.

class LO.System (F : outParam (Type u_1)) (S : Type u_2) : Type (max (max u_1 u_2) (u_3 + 1))

• Prf : S → F → Type u_3

def LO.«term_⊢_» : Lean.TrailingParserDescr

Equations

• LO.«term_⊢_» = Lean.ParserDescr.trailingNode `LO.«term_⊢_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 46))

def LO.System.Provable {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) (f : F) : Prop

Equations

• (𝓢 ⊢! f) = Nonempty (𝓢 ⊢ f)

@[reducible, inline]

abbrev LO.System.Unprovable {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) (f : F) : Prop

Equations

• (𝓢 ⊬ f) = ¬𝓢 ⊢! f

def LO.System.«term_⊢!_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_⊢!_» = Lean.ParserDescr.trailingNode `LO.System.«term_⊢!_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢! ") (Lean.ParserDescr.cat `term 46))

def LO.System.«term_⊬_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_⊬_» = Lean.ParserDescr.trailingNode `LO.System.«term_⊬_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊬ ") (Lean.ParserDescr.cat `term 46))

def LO.System.PrfSet {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) (s : Set F) : Type (max u_1 u_5)

Equations

• (𝓢 ⊢* s) = ({f : F} → f ∈ s → 𝓢 ⊢ f)

def LO.System.ProvableSet {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) (s : Set F) : Prop

Equations

• (𝓢 ⊢!* s) = ∀ {f : F}, f ∈ s → 𝓢 ⊢! f

def LO.System.«term_⊢*_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_⊢*_» = Lean.ParserDescr.trailingNode `LO.System.«term_⊢*_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢* ") (Lean.ParserDescr.cat `term 46))

def LO.System.«term_⊢!*_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_⊢!*_» = Lean.ParserDescr.trailingNode `LO.System.«term_⊢!*_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢!* ") (Lean.ParserDescr.cat `term 46))

def LO.System.theory {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) : Set F

Equations

• LO.System.theory 𝓢 = {f : F | 𝓢 ⊢! f}

theorem LO.System.unprovable_iff_isEmpty {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} {f : F} : 𝓢 ⊬ f ↔ IsEmpty (𝓢 ⊢ f)

noncomputable def LO.System.Provable.get {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} {f : F} (h : 𝓢 ⊢! f) : 𝓢 ⊢ f

Equations

• h.get = Classical.choice h

theorem LO.System.provableSet_iff {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} {s : Set F} : 𝓢 ⊢!* s ↔ Nonempty (𝓢 ⊢* s)

noncomputable def LO.System.ProvableSet.get {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} {s : Set F} (h : 𝓢 ⊢!* s) : 𝓢 ⊢* s

Equations

• h.get = Classical.choice ⋯

def LO.System.WeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] (𝓢 : S) (𝓣 : T) : Prop

Equations

• (𝓢 ≤ₛ 𝓣) = (LO.System.theory 𝓢 ⊆ LO.System.theory 𝓣)

def LO.System.«term_≤ₛ_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_≤ₛ_» = Lean.ParserDescr.trailingNode `LO.System.«term_≤ₛ_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₛ ") (Lean.ParserDescr.cat `term 41))

def LO.System.StrictlyWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] (𝓢 : S) (𝓣 : T) : Prop

Equations

• (𝓢 <ₛ 𝓣) = (𝓢 ≤ₛ 𝓣 ∧ ¬𝓣 ≤ₛ 𝓢)

def LO.System.«term_<ₛ_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_<ₛ_» = Lean.ParserDescr.trailingNode `LO.System.«term_<ₛ_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ₛ ") (Lean.ParserDescr.cat `term 41))

def LO.System.Equiv {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] (𝓢 : S) (𝓣 : T) : Prop

Equations

• (𝓢 =ₛ 𝓣) = (LO.System.theory 𝓢 = LO.System.theory 𝓣)

def LO.System.«term_=ₛ_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_=ₛ_» = Lean.ParserDescr.trailingNode `LO.System.«term_=ₛ_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =ₛ ") (Lean.ParserDescr.cat `term 41))

@[simp]

theorem LO.System.WeakerThan.refl {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) : 𝓢 ≤ₛ 𝓢

theorem LO.System.WeakerThan.trans {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [System F S] [System F T] [System F U] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 ≤ₛ 𝓣 → 𝓣 ≤ₛ 𝓤 → 𝓢 ≤ₛ 𝓤

theorem LO.System.weakerThan_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} : 𝓢 ≤ₛ 𝓣 ↔ ∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f

theorem LO.System.not_weakerThan_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} : ¬𝓢 ≤ₛ 𝓣 ↔ ∃ (f : F), 𝓢 ⊢! f ∧ 𝓣 ⊬ f

theorem LO.System.strictlyWeakerThan_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} : 𝓢 <ₛ 𝓣 ↔ (∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f) ∧ ∃ (f : F), 𝓢 ⊬ f ∧ 𝓣 ⊢! f

theorem LO.System.strictlyWeakerThan.trans {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [System F S] [System F T] [System F U] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 <ₛ 𝓣 → 𝓣 <ₛ 𝓤 → 𝓢 <ₛ 𝓤

theorem LO.System.weakening {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} (h : 𝓢 ≤ₛ 𝓣) {f : F} : 𝓢 ⊢! f → 𝓣 ⊢! f

theorem LO.System.Equiv.iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} : 𝓢 =ₛ 𝓣 ↔ ∀ (f : F), 𝓢 ⊢! f ↔ 𝓣 ⊢! f

@[simp]

theorem LO.System.Equiv.refl {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) : 𝓢 =ₛ 𝓢

theorem LO.System.Equiv.symm {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} : 𝓢 =ₛ 𝓣 → 𝓣 =ₛ 𝓢

theorem LO.System.Equiv.trans {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [System F S] [System F T] [System F U] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 =ₛ 𝓣 → 𝓣 =ₛ 𝓤 → 𝓢 =ₛ 𝓤

theorem LO.System.Equiv.antisymm_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} : 𝓢 =ₛ 𝓣 ↔ 𝓢 ≤ₛ 𝓣 ∧ 𝓣 ≤ₛ 𝓢

theorem LO.System.Equiv.antisymm {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} : 𝓢 ≤ₛ 𝓣 ∧ 𝓣 ≤ₛ 𝓢 → 𝓢 =ₛ 𝓣

Alias of the reverse direction of LO.System.Equiv.antisymm_iff.

theorem LO.System.Equiv.le {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} : 𝓢 =ₛ 𝓣 → 𝓢 ≤ₛ 𝓣

instance LO.System.equiv {F : Type u_1} (S : Type u_2) [System F S] : Setoid S

Equations

• LO.System.equiv S = { r := fun (x1 x2 : S) => x1 =ₛ x2, iseqv := ⋯ }

@[reducible, inline]

abbrev LO.System.Logic {F : Type u_1} (S : Type u_2) [System F S] : Type u_2

Equations

• LO.System.Logic S = Quotient (LO.System.equiv S)

theorem LO.System.equiv_def {F : Type u_1} {S : Type u_2} [System F S] {𝓢 𝓣 : S} : 𝓢 ≈ 𝓣 ↔ theory 𝓢 = theory 𝓣

@[simp]

theorem LO.System.Logic.of_eq_of {F : Type u_1} {S : Type u_2} [System F S] {𝓢 𝓣 : S} : ⟦𝓢⟧ = ⟦𝓣⟧ ↔ 𝓢 ≈ 𝓣

instance LO.System.Logic.instLE {F : Type u_1} {S : Type u_2} [System F S] : LE (Logic S)

Equations

• LO.System.Logic.instLE = { le := Quotient.lift₂ (fun (x1 x2 : S) => x1 ≤ₛ x2) ⋯ }

@[simp]

theorem LO.System.Logic.le_iff {F : Type u_1} {S : Type u_2} [System F S] {𝓢 𝓣 : S} : ⟦𝓢⟧ ≤ ⟦𝓣⟧ ↔ 𝓢 ≤ₛ 𝓣

instance LO.System.Logic.instPartialOrder {F : Type u_1} {S : Type u_2} [System F S] : PartialOrder (Logic S)

Equations

• LO.System.Logic.instPartialOrder = PartialOrder.mk ⋯

@[simp]

theorem LO.System.Logic.lt_iff {F : Type u_1} {S : Type u_2} [System F S] {𝓢 𝓣 : S} : ⟦𝓢⟧ < ⟦𝓣⟧ ↔ 𝓢 <ₛ 𝓣

@[simp]

theorem LO.System.provableSet_theory {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) : 𝓢 ⊢!* theory 𝓢

def LO.System.Inconsistent {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) : Prop

Equations

• LO.System.Inconsistent 𝓢 = ∀ (f : F), 𝓢 ⊢! f

class LO.System.Consistent {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) : Prop

• not_inconsistent : ¬Inconsistent 𝓢

theorem LO.System.inconsistent_def {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : Inconsistent 𝓢 ↔ ∀ (f : F), 𝓢 ⊢! f

theorem LO.System.inconsistent_iff_theory_eq {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : Inconsistent 𝓢 ↔ theory 𝓢 = Set.univ

theorem LO.System.not_inconsistent_iff_consistent {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : ¬Inconsistent 𝓢 ↔ Consistent 𝓢

theorem LO.System.Consistent.not_inc {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : Consistent 𝓢 → ¬Inconsistent 𝓢

Alias of the reverse direction of LO.System.not_inconsistent_iff_consistent.

theorem LO.System.not_consistent_iff_inconsistent {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : ¬Consistent 𝓢 ↔ Inconsistent 𝓢

theorem LO.System.Inconsistent.not_con {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : Inconsistent 𝓢 → ¬Consistent 𝓢

Alias of the reverse direction of LO.System.not_consistent_iff_inconsistent.

theorem LO.System.consistent_iff_exists_unprovable {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : Consistent 𝓢 ↔ ∃ (f : F), 𝓢 ⊬ f

theorem LO.System.Consistent.exists_unprovable {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : Consistent 𝓢 → ∃ (f : F), 𝓢 ⊬ f

Alias of the forward direction of LO.System.consistent_iff_exists_unprovable.

theorem LO.System.Consistent.of_unprovable {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} {f : F} (h : 𝓢 ⊬ f) : Consistent 𝓢

theorem LO.System.inconsistent_iff_theory_eq_univ {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : Inconsistent 𝓢 ↔ theory 𝓢 = Set.univ

theorem LO.System.Inconsistent.theory_eq {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : Inconsistent 𝓢 → theory 𝓢 = Set.univ

Alias of the forward direction of LO.System.inconsistent_iff_theory_eq_univ.

theorem LO.System.Inconsistent.equiv {F : Type u_1} {S : Type u_2} [System F S] {𝓢 𝓣 : S} (h : Inconsistent 𝓢) (h' : Inconsistent 𝓣) : 𝓢 ≈ 𝓣

theorem LO.System.Inconsistent.of_ge {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} (h𝓢 : Inconsistent 𝓢) (h : 𝓢 ≤ₛ 𝓣) : Inconsistent 𝓣

theorem LO.System.Consistent.of_le {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] {𝓢 : S} {𝓣 : T} (h𝓢 : Consistent 𝓢) (h : 𝓣 ≤ₛ 𝓢) : Consistent 𝓣

def LO.System.Logic.Inconsistent {F : Type u_1} {S : Type u_2} [System F S] (Λ : Logic S) : Prop

Equations

• Λ.Inconsistent = Quotient.lift LO.System.Inconsistent ⋯ Λ

@[simp]

theorem LO.System.Logic.inconsistent_mk {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) : Logic.Inconsistent ⟦𝓢⟧ ↔ Inconsistent 𝓢

def LO.System.Logic.Consistent {F : Type u_1} {S : Type u_2} [System F S] (Λ : Logic S) : Prop

Equations

• Λ.Consistent = Quotient.lift LO.System.Consistent ⋯ Λ

@[simp]

theorem LO.System.Logic.consistent_mk {F : Type u_1} {S : Type u_2} [System F S] (𝓢 : S) : Logic.Consistent ⟦𝓢⟧ ↔ Consistent 𝓢

structure LO.System.Translation {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} [System F S] [System F' S'] (𝓢 : S) (𝓣 : S') : Type (max (max (max u_10 u_7) u_8) u_9)

• toFun : F → F'
• prf {f : F} : 𝓢 ⊢ f → 𝓣 ⊢ self.toFun f

theorem LO.System.Translation.ext {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} {inst✝ : System F S} {inst✝¹ : System F' S'} {𝓢 : S} {𝓣 : S'} {x y : 𝓢 ↝ 𝓣} (toFun : x.toFun = y.toFun) (prf : HEq (@prf S S' F F' inst✝ inst✝¹ 𝓢 𝓣 x) (@prf S S' F F' inst✝ inst✝¹ 𝓢 𝓣 y)) : x = y

def LO.System.«term_↝_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_↝_» = Lean.ParserDescr.trailingNode `LO.System.«term_↝_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↝ ") (Lean.ParserDescr.cat `term 41))

structure LO.System.Bitranslation {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} [System F S] [System F' S'] (𝓢 : S) (𝓣 : S') : Type (max (max (max u_10 u_7) u_8) u_9)

• r : 𝓢 ↝ 𝓣
• l : 𝓣 ↝ 𝓢
• r_l : self.r.toFun ∘ self.l.toFun = id
• l_r : self.l.toFun ∘ self.r.toFun = id

theorem LO.System.Bitranslation.ext {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} {inst✝ : System F S} {inst✝¹ : System F' S'} {𝓢 : S} {𝓣 : S'} {x y : 𝓢 ↭ 𝓣} (r : x.r = y.r) (l : x.l = y.l) : x = y

def LO.System.«term_↭_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_↭_» = Lean.ParserDescr.trailingNode `LO.System.«term_↭_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↭ ") (Lean.ParserDescr.cat `term 41))

structure LO.System.FaithfulTranslation {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} [System F S] [System F' S'] (𝓢 : S) (𝓣 : S') extends 𝓢 ↝ 𝓣 : Type (max (max (max u_10 u_7) u_8) u_9)

• toFun : F → F'
• prf {f : F} : 𝓢 ⊢ f → 𝓣 ⊢ self.toFun f
• prfInv {f : F} : 𝓣 ⊢ self.toFun f → 𝓢 ⊢ f

theorem LO.System.FaithfulTranslation.ext {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} {inst✝ : System F S} {inst✝¹ : System F' S'} {𝓢 : S} {𝓣 : S'} {x y : 𝓢 ↝¹ 𝓣} (toFun : x.toFun = y.toFun) (prf : HEq (@Translation.prf S S' F F' inst✝ inst✝¹ 𝓢 𝓣 x.toTranslation) (@Translation.prf S S' F F' inst✝ inst✝¹ 𝓢 𝓣 y.toTranslation)) (prfInv : HEq (@prfInv S S' F F' inst✝ inst✝¹ 𝓢 𝓣 x) (@prfInv S S' F F' inst✝ inst✝¹ 𝓢 𝓣 y)) : x = y

def LO.System.«term_↝¹_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_↝¹_» = Lean.ParserDescr.trailingNode `LO.System.«term_↝¹_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↝¹ ") (Lean.ParserDescr.cat `term 41))

instance LO.System.Translation.instCoeFunForall {S : Type u_5} {S' : Type u_6} {F : Type u_8} {F' : Type u_9} [System F S] [System F' S'] (𝓢 : S) (𝓣 : S') : CoeFun (𝓢 ↝ 𝓣) fun (x : 𝓢 ↝ 𝓣) => F → F'

Equations

• LO.System.Translation.instCoeFunForall 𝓢 𝓣 = { coe := LO.System.Translation.toFun }

def LO.System.Translation.id {S : Type u_5} {F : Type u_8} [System F S] (𝓢 : S) : 𝓢 ↝ 𝓢

Equations

• LO.System.Translation.id 𝓢 = { toFun := id, prf := fun {f : F} => id }

@[simp]

theorem LO.System.Translation.id_app {S : Type u_5} {F : Type u_8} [System F S] (𝓢 : S) (f : F) : (Translation.id 𝓢).toFun f = f

def LO.System.Translation.comp {S : Type u_5} {S' : Type u_6} {S'' : Type u_7} {F : Type u_8} {F' : Type u_9} {F'' : Type u_10} [System F S] [System F' S'] [System F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↝ 𝓤) (ψ : 𝓢 ↝ 𝓣) : 𝓢 ↝ 𝓤

Equations

• φ.comp ψ = { toFun := φ.toFun ∘ ψ.toFun, prf := fun {f : F} => φ.prf ∘ ψ.prf }

@[simp]

theorem LO.System.Translation.comp_app {S : Type u_5} {S' : Type u_6} {S'' : Type u_7} {F : Type u_8} {F' : Type u_9} {F'' : Type u_10} [System F S] [System F' S'] [System F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↝ 𝓤) (ψ : 𝓢 ↝ 𝓣) (f : F) : (φ.comp ψ).toFun f = φ.toFun (ψ.toFun f)

theorem LO.System.Translation.provable {S : Type u_5} {S' : Type u_6} {F : Type u_8} {F' : Type u_9} [System F S] [System F' S'] {𝓢 : S} {𝓣 : S'} (f : 𝓢 ↝ 𝓣) {φ : F} (h : 𝓢 ⊢! φ) : 𝓣 ⊢! f.toFun φ

@[simp]

theorem LO.System.Bitranslation.r_l_app {S : Type u_5} {S' : Type u_6} {F : Type u_8} {F' : Type u_9} [System F S] [System F' S'] {𝓢 : S} {𝓣 : S'} (f : 𝓢 ↭ 𝓣) (φ : F') : f.r.toFun (f.l.toFun φ) = φ

@[simp]

theorem LO.System.Bitranslation.l_r_app {S : Type u_5} {S' : Type u_6} {F : Type u_8} {F' : Type u_9} [System F S] [System F' S'] {𝓢 : S} {𝓣 : S'} (f : 𝓢 ↭ 𝓣) (φ : F) : f.l.toFun (f.r.toFun φ) = φ

def LO.System.Bitranslation.id {S : Type u_5} {F : Type u_8} [System F S] (𝓢 : S) : 𝓢 ↭ 𝓢

Equations

• LO.System.Bitranslation.id 𝓢 = { r := LO.System.Translation.id 𝓢, l := LO.System.Translation.id 𝓢, r_l := ⋯, l_r := ⋯ }

def LO.System.Bitranslation.symm {S : Type u_5} {S' : Type u_6} {F : Type u_8} {F' : Type u_9} [System F S] [System F' S'] {𝓢 : S} {𝓣 : S'} (φ : 𝓢 ↭ 𝓣) : 𝓣 ↭ 𝓢

Equations

• φ.symm = { r := φ.l, l := φ.r, r_l := ⋯, l_r := ⋯ }

def LO.System.Bitranslation.comp {S : Type u_5} {S' : Type u_6} {S'' : Type u_7} {F : Type u_8} {F' : Type u_9} {F'' : Type u_10} [System F S] [System F' S'] [System F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↭ 𝓤) (ψ : 𝓢 ↭ 𝓣) : 𝓢 ↭ 𝓤

Equations

• φ.comp ψ = { r := φ.r.comp ψ.r, l := ψ.l.comp φ.l, r_l := ⋯, l_r := ⋯ }

instance LO.System.FaithfulTranslation.instCoeFunForall {S : Type u_5} {S' : Type u_6} {F : Type u_8} {F' : Type u_9} [System F S] [System F' S'] (𝓢 : S) (𝓣 : S') : CoeFun (𝓢 ↝¹ 𝓣) fun (x : 𝓢 ↝¹ 𝓣) => F → F'

Equations

• LO.System.FaithfulTranslation.instCoeFunForall 𝓢 𝓣 = { coe := fun (t : 𝓢 ↝¹ 𝓣) => t.toFun }

def LO.System.FaithfulTranslation.id {S : Type u_5} {F : Type u_8} [System F S] (𝓢 : S) : 𝓢 ↝¹ 𝓢

Equations

• LO.System.FaithfulTranslation.id 𝓢 = { toFun := id, prf := fun {f : F} => id, prfInv := fun {f : F} => id }

@[simp]

theorem LO.System.FaithfulTranslation.id_app {S : Type u_5} {F : Type u_8} [System F S] (𝓢 : S) (f : F) : (FaithfulTranslation.id 𝓢).toFun f = f

def LO.System.FaithfulTranslation.comp {S : Type u_5} {S' : Type u_6} {S'' : Type u_7} {F : Type u_8} {F' : Type u_9} {F'' : Type u_10} [System F S] [System F' S'] [System F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↝¹ 𝓤) (ψ : 𝓢 ↝¹ 𝓣) : 𝓢 ↝¹ 𝓤

Equations

• φ.comp ψ = { toFun := φ.toFun ∘ ψ.toFun, prf := fun {f : F} => φ.prf ∘ ψ.prf, prfInv := fun {f : F} => ψ.prfInv ∘ φ.prfInv }

@[simp]

theorem LO.System.FaithfulTranslation.comp_app {S : Type u_5} {S' : Type u_6} {S'' : Type u_7} {F : Type u_8} {F' : Type u_9} {F'' : Type u_10} [System F S] [System F' S'] [System F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↝¹ 𝓤) (ψ : 𝓢 ↝¹ 𝓣) (f : F) : (φ.comp ψ).toFun f = φ.toFun (ψ.toFun f)

theorem LO.System.FaithfulTranslation.provable {S : Type u_5} {S' : Type u_6} {F : Type u_8} {F' : Type u_9} [System F S] [System F' S'] {𝓢 : S} {𝓣 : S'} (f : 𝓢 ↝¹ 𝓣) {φ : F} (h : 𝓢 ⊢! φ) : 𝓣 ⊢! f.toFun φ

theorem LO.System.FaithfulTranslation.provable_iff {S : Type u_5} {S' : Type u_6} {F : Type u_8} {F' : Type u_9} [System F S] [System F' S'] {𝓢 : S} {𝓣 : S'} (f : 𝓢 ↝¹ 𝓣) {φ : F} : 𝓣 ⊢! f.toFun φ ↔ 𝓢 ⊢! φ

class LO.System.Subtheory {F : Type u_1} {S : Type u_2} [System F S] (𝓢 𝓣 : S) : Type (max u_1 u_5)

• prf {f : F} : 𝓢 ⊢ f → 𝓣 ⊢ f

def LO.System.«term_≼_» : Lean.TrailingParserDescr

Equations

• LO.System.«term_≼_» = Lean.ParserDescr.trailingNode `LO.System.«term_≼_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼ ") (Lean.ParserDescr.cat `term 41))

instance LO.System.Subtheory.id {F : Type u_1} {S : Type u_2} [System F S] {𝓢 : S} : 𝓢 ≼ 𝓢

Equations

• LO.System.Subtheory.id = { prf := fun {f : F} => id }

def LO.System.Subtheory.comp {F : Type u_1} {S : Type u_2} [System F S] {𝓢 𝓣 𝓤 : S} (t' : 𝓣 ≼ 𝓤) (t : 𝓢 ≼ 𝓣) : 𝓢 ≼ 𝓤

Equations

• t'.comp t = { prf := fun {f : F} => LO.System.Subtheory.prf ∘ LO.System.Subtheory.prf }

def LO.System.Subtheory.translation {F : Type u_1} {S : Type u_2} [System F S] {𝓢 𝓣 : S} [𝓢 ≼ 𝓣] : 𝓢 ↝ 𝓣

Equations

• LO.System.Subtheory.translation = { toFun := id, prf := fun {f : F} => LO.System.Subtheory.prf }

def LO.System.Subtheory.ofTranslation {F : Type u_1} {S : Type u_2} [System F S] {𝓢 𝓣 : S} (t : 𝓢 ↝ 𝓣) (h : ∀ (φ : F), t.toFun φ = φ) : 𝓢 ≼ 𝓣

Equations

• LO.System.Subtheory.ofTranslation t h = { prf := fun {φ : F} (b : 𝓢 ⊢ φ) => ⋯ ▸ t.prf b }

theorem LO.System.Subtheory.prf! {F : Type u_1} {S : Type u_2} [System F S] {𝓢 𝓣 : S} [𝓢 ≼ 𝓣] {f : F} : 𝓢 ⊢! f → 𝓣 ⊢! f

def LO.System.Complete {F : Type u_1} {S : Type u_2} [System F S] [LogicalConnective F] (𝓢 : S) : Prop

Equations

• LO.System.Complete 𝓢 = ∀ (f : F), 𝓢 ⊢! f ∨ 𝓢 ⊢! ∼f

def LO.System.Undecidable {F : Type u_1} {S : Type u_2} [System F S] [LogicalConnective F] (𝓢 : S) (f : F) : Prop

Equations

• LO.System.Undecidable 𝓢 f = (𝓢 ⊬ f ∧ 𝓢 ⊬ ∼f)

theorem LO.System.incomplete_iff_exists_undecidable {F : Type u_1} {S : Type u_2} [System F S] [LogicalConnective F] {𝓢 : S} : ¬Complete 𝓢 ↔ ∃ (f : F), Undecidable 𝓢 f

class LO.System.Axiomatized {F : Type u_1} (S : Type u_2) [System F S] [Collection F S] : Type (max (max u_1 u_2) u_5)

• prfAxm {𝓢 : S} : 𝓢 ⊢* Collection.set 𝓢
• weakening {f : F} {𝓢 𝓣 : S} : 𝓢 ⊆ 𝓣 → 𝓢 ⊢ f → 𝓣 ⊢ f

def LO.System.byAxm {F : Type u_1} {S : Type u_2} {inst✝ : System F S} {inst✝¹ : Collection F S} [self : Axiomatized S] {𝓢 : S} : 𝓢 ⊢* Collection.set 𝓢

Alias of LO.System.Axiomatized.prfAxm.

Equations

• @LO.System.byAxm = @LO.System.Axiomatized.prfAxm

def LO.System.wk {F : Type u_1} {S : Type u_2} {inst✝ : System F S} {inst✝¹ : Collection F S} [self : Axiomatized S] {f : F} {𝓢 𝓣 : S} : 𝓢 ⊆ 𝓣 → 𝓢 ⊢ f → 𝓣 ⊢ f

Alias of LO.System.Axiomatized.weakening.

Equations

• @LO.System.wk = @LO.System.Axiomatized.weakening

class LO.System.StrongCut {F : Type u_1} (S : Type u_2) (T : Type u_3) [System F S] [System F T] [Collection F T] : Type (max (max (max (max u_1 u_2) u_3) u_5) u_6)

• cut {𝓢 : S} {𝓣 : T} {φ : F} : 𝓢 ⊢* Collection.set 𝓣 → 𝓣 ⊢ φ → 𝓢 ⊢ φ

@[simp]

theorem LO.System.Axiomatized.provable_axm {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] (𝓢 : S) : 𝓢 ⊢!* Collection.set 𝓢

theorem LO.System.Axiomatized.axm_subset {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] (𝓢 : S) : Collection.set 𝓢 ⊆ theory 𝓢

theorem LO.System.Axiomatized.le_of_subset {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) : 𝓢 ≤ₛ 𝓣

theorem LO.System.Axiomatized.weakening! {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) {f : F} : 𝓢 ⊢! f → 𝓣 ⊢! f

def LO.System.Axiomatized.subtheoryOfSubset {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) : 𝓢 ≼ 𝓣

Equations

• LO.System.Axiomatized.subtheoryOfSubset h = { prf := fun {f : F} => LO.System.Axiomatized.weakening h }

def LO.System.Axiomatized.translation {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) : 𝓢 ↝ 𝓣

Equations

• LO.System.Axiomatized.translation h = { toFun := id, prf := fun {f : F} => LO.System.Axiomatized.weakening h }

theorem LO.System.by_axm {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] (𝓢 : S) : 𝓢 ⊢!* Collection.set 𝓢

Alias of LO.System.Axiomatized.provable_axm.

theorem LO.System.wk! {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) {f : F} : 𝓢 ⊢! f → 𝓣 ⊢! f

Alias of LO.System.Axiomatized.weakening!.

def LO.System.FiniteAxiomatizable {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] (𝓢 : S) : Prop

Equations

• LO.System.FiniteAxiomatizable 𝓢 = ∃ (𝓕 : S), Collection.Finite 𝓕 ∧ 𝓕 ≈ 𝓢

theorem LO.System.Consistent.of_subset {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h𝓢 : Consistent 𝓢) (h : 𝓣 ⊆ 𝓢) : Consistent 𝓣

theorem LO.System.Inconsistent.of_supset {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h𝓢 : Inconsistent 𝓢) (h : 𝓢 ⊆ 𝓣) : Inconsistent 𝓣

theorem LO.System.StrongCut.cut! {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] [Collection F T] [StrongCut S T] {𝓢 : S} {𝓣 : T} {φ : F} (H : 𝓢 ⊢!* Collection.set 𝓣) (hp : 𝓣 ⊢! φ) : 𝓢 ⊢! φ

def LO.System.StrongCut.translation {F : Type u_1} {S : Type u_2} {T : Type u_3} [System F S] [System F T] [Collection F T] [StrongCut S T] {𝓢 : S} {𝓣 : T} (B : 𝓢 ⊢* Collection.set 𝓣) : 𝓣 ↝ 𝓢

Equations

• LO.System.StrongCut.translation B = { toFun := id, prf := fun {f : F} => LO.System.StrongCut.cut fun {f : F} => B }

def LO.System.Subtheory.ofAxm {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [StrongCut S S] {𝓢₁ 𝓢₂ : S} (B : 𝓢₂ ⊢* Collection.set 𝓢₁) : 𝓢₁ ≼ 𝓢₂

Equations

• LO.System.Subtheory.ofAxm B = { prf := fun {f : F} (b : 𝓢₁ ⊢ f) => LO.System.StrongCut.cut (fun {f : F} => B) b }

noncomputable def LO.System.Subtheory.ofAxm! {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [StrongCut S S] {𝓢₁ 𝓢₂ : S} (B : 𝓢₂ ⊢!* Collection.set 𝓢₁) : 𝓢₁ ≼ 𝓢₂

Equations

• LO.System.Subtheory.ofAxm! B = { prf := fun {f : F} (b : 𝓢₁ ⊢ f) => LO.System.StrongCut.cut (fun {f : F} => B.get) b }

def LO.System.Subtheory.ofSubset {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) : 𝓢 ≼ 𝓣

Equations

• LO.System.Subtheory.ofSubset h = { prf := fun {f : F} => LO.System.wk h }

class LO.System.Compact {F : Type u_1} (S : Type u_2) [System F S] [Collection F S] : Type (max (max u_1 u_2) u_5)

• φ {𝓢 : S} {f : F} : 𝓢 ⊢ f → S
• φPrf {𝓢 : S} {f : F} (b : 𝓢 ⊢ f) : φ b ⊢ f
• φ_subset {𝓢 : S} {f : F} (b : 𝓢 ⊢ f) : φ b ⊆ 𝓢
• φ_finite {𝓢 : S} {f : F} (b : 𝓢 ⊢ f) : Collection.Finite (φ b)

theorem LO.System.Compact.finite_provable {F : Type u_1} {S : Type u_2} [System F S] [Collection F S] [Compact S] {f : F} {𝓢 : S} (h : 𝓢 ⊢! f) : ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ 𝓕 ⊢! f

class LO.System.DeductiveExplosion (S : Type u_1) {F : Type u_2} [LogicalConnective F] [System F S] : Type (max (max u_1 u_2) u_3)

• dexp {𝓢 : S} : 𝓢 ⊢ ⊥ → (φ : F) → 𝓢 ⊢ φ

def LO.System.DeductiveExplosion.dexp! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [DeductiveExplosion S] {𝓢 : S} (h : 𝓢 ⊢! ⊥) (f : F) : 𝓢 ⊢! f

Equations

• ⋯ = ⋯

theorem LO.System.inconsistent_iff_provable_bot {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [DeductiveExplosion S] {𝓢 : S} : Inconsistent 𝓢 ↔ 𝓢 ⊢! ⊥

theorem LO.System.inconsistent_of_provable {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [DeductiveExplosion S] {𝓢 : S} : 𝓢 ⊢! ⊥ → Inconsistent 𝓢

Alias of the reverse direction of LO.System.inconsistent_iff_provable_bot.

theorem LO.System.consistent_iff_unprovable_bot {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [DeductiveExplosion S] {𝓢 : S} : Consistent 𝓢 ↔ 𝓢 ⊬ ⊥

theorem LO.System.Consistent.not_bot {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [DeductiveExplosion S] {𝓢 : S} : Consistent 𝓢 → 𝓢 ⊬ ⊥

Alias of the forward direction of LO.System.consistent_iff_unprovable_bot.

theorem LO.System.inconsistent_compact {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [DeductiveExplosion S] [Collection F S] [Axiomatized S] [Compact S] {𝓢 : S} : Inconsistent 𝓢 ↔ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ Inconsistent 𝓕

theorem LO.System.consistent_compact {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [DeductiveExplosion S] [Collection F S] [Axiomatized S] [Compact S] {𝓢 : S} : Consistent 𝓢 ↔ ∀ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 → Consistent 𝓕

class LO.System.Deduction (S : Type u_1) {F : Type u_2} [LogicalConnective F] [System F S] [Cons F S] : Type (max (max u_1 u_2) u_3)

• ofInsert {φ ψ : F} {𝓢 : S} : cons φ 𝓢 ⊢ ψ → 𝓢 ⊢ φ ➝ ψ
• inv {φ ψ : F} {𝓢 : S} : 𝓢 ⊢ φ ➝ ψ → cons φ 𝓢 ⊢ ψ

def LO.System.deduction {S : Type u_1} {F : Type u_2} {inst✝ : LogicalConnective F} {inst✝¹ : System F S} {inst✝² : Cons F S} [self : Deduction S] {φ ψ : F} {𝓢 : S} : cons φ 𝓢 ⊢ ψ → 𝓢 ⊢ φ ➝ ψ

Alias of LO.System.Deduction.ofInsert.

Equations

• @LO.System.deduction = @LO.System.Deduction.ofInsert

theorem LO.System.Deduction.of_insert! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [Cons F S] [Deduction S] {𝓢 : S} {φ ψ : F} (h : cons φ 𝓢 ⊢! ψ) : 𝓢 ⊢! φ ➝ ψ

theorem LO.System.deduction! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [Cons F S] [Deduction S] {𝓢 : S} {φ ψ : F} (h : cons φ 𝓢 ⊢! ψ) : 𝓢 ⊢! φ ➝ ψ

Alias of LO.System.Deduction.of_insert!.

theorem LO.System.Deduction.inv! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [Cons F S] [Deduction S] {𝓢 : S} {φ ψ : F} (h : 𝓢 ⊢! φ ➝ ψ) : cons φ 𝓢 ⊢! ψ

def LO.System.Deduction.translation {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [Cons F S] [Deduction S] (φ : F) (𝓢 : S) : cons φ 𝓢 ↝ 𝓢

Equations

• LO.System.Deduction.translation φ 𝓢 = { toFun := fun (ψ : F) => φ ➝ ψ, prf := fun {f : F} => LO.System.deduction }

theorem LO.System.deduction_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [System F S] [Cons F S] [Deduction S] {𝓢 : S} {φ ψ : F} : cons φ 𝓢 ⊢! ψ ↔ 𝓢 ⊢! φ ➝ ψ

class LO.Sound {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] (𝓢 : S) (𝓜 : M) : Prop

• sound {f : F} : 𝓢 ⊢! f → 𝓜 ⊧ f

class LO.Complete {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] (𝓢 : S) (𝓜 : M) : Prop

• complete {f : F} : 𝓜 ⊧ f → 𝓢 ⊢! f

theorem LO.Sound.not_provable_of_countermodel {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {𝓜 : M} [Sound 𝓢 𝓜] {φ : F} (hp : ¬𝓜 ⊧ φ) : 𝓢 ⊬ φ

theorem LO.Sound.consistent_of_meaningful {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {𝓜 : M} [Sound 𝓢 𝓜] : Semantics.Meaningful 𝓜 → System.Consistent 𝓢

theorem LO.Sound.consistent_of_model {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} [LogicalConnective F] [Semantics.Bot M] (𝓜 : M) [Sound 𝓢 𝓜] : System.Consistent 𝓢

theorem LO.Sound.realizeSet_of_prfSet {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {𝓜 : M} [Sound 𝓢 𝓜] {T : Set F} (b : 𝓢 ⊢!* T) : 𝓜 ⊧* T

theorem LO.Sound.consequence_of_provable {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {T : Set F} [Sound 𝓢 (Semantics.models M T)] {f : F} : 𝓢 ⊢! f → T ⊨[M] f

theorem LO.Sound.consistent_of_satisfiable {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {T : Set F} [Sound 𝓢 (Semantics.models M T)] [LogicalConnective F] [∀ (𝓜 : M), Semantics.Meaningful 𝓜] : Semantics.Satisfiable M T → System.Consistent 𝓢

theorem LO.Complete.meaningful_of_consistent {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {𝓜 : M} [Complete 𝓢 𝓜] : System.Consistent 𝓢 → Semantics.Meaningful 𝓜

theorem LO.Complete.provable_of_consequence {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {T : Set F} [Complete 𝓢 (Semantics.models M T)] {f : F} : T ⊨[M] f → 𝓢 ⊢! f

theorem LO.Complete.provable_iff_consequence {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {T : Set F} [Complete 𝓢 (Semantics.models M T)] [Sound 𝓢 (Semantics.models M T)] {f : F} : T ⊨[M] f ↔ 𝓢 ⊢! f

theorem LO.Complete.satisfiable_of_consistent {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {T : Set F} [Complete 𝓢 (Semantics.models M T)] [LogicalConnective F] [∀ (𝓜 : M), Semantics.Meaningful 𝓜] : System.Consistent 𝓢 → Semantics.Satisfiable M T

theorem LO.Complete.inconsistent_of_unsatisfiable {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {T : Set F} [Complete 𝓢 (Semantics.models M T)] [LogicalConnective F] [∀ (𝓜 : M), Semantics.Meaningful 𝓜] : ¬Semantics.Satisfiable M T → System.Inconsistent 𝓢

theorem LO.Complete.consistent_iff_satisfiable {S : Type u_1} {F : Type u_2} [System F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {T : Set F} [Complete 𝓢 (Semantics.models M T)] [LogicalConnective F] [∀ (𝓜 : M), Semantics.Meaningful 𝓜] [Sound 𝓢 (Semantics.models M T)] : System.Consistent 𝓢 ↔ Semantics.Satisfiable M T