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.Entailment F S: a general framework of deductive system S for formulae F.
• LO.Entailment.Inconsistent 𝓢: a proposition that states that all formulae in F is provable
• from 𝓢.
• LO.Entailment.Consistent 𝓢: a proposition that states that 𝓢 is not inconsistent.
• LO.Entailment.Sound 𝓢 𝓜: provability from 𝓢 implies satisfiability on 𝓜.
• LO.Entailment.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.Entailment (F : outParam (Type u_1)) (S : Type u_2) : Type (max (max u_1 u_2) (u_3 + 1))

Imported declaration from the Incompleteness formalization.

• Prf : S → F → Type u_3

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

• h.get = Classical.choice h

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

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

Imported declaration from the Incompleteness formalization.

Equations

• h.get = Classical.choice ⋯

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

Imported declaration from the Incompleteness formalization.

• subset : theory 𝓢 ⊆ theory 𝓣

def LO.Entailment.term_Wkn_ : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.term_Wkn_ = Lean.ParserDescr.trailingNode `LO.Entailment.term_Wkn_ 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " wkn ") (Lean.ParserDescr.cat `term 41))

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

Imported declaration from the Incompleteness formalization.

• weakerThan : 𝓢 wkn 𝓣
• notWT : ¬𝓣 wkn 𝓢

def LO.Entailment.term_Swkn_ : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.term_Swkn_ = Lean.ParserDescr.trailingNode `LO.Entailment.term_Swkn_ 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " swkn ") (Lean.ParserDescr.cat `term 41))

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

Imported declaration from the Incompleteness formalization.

• eq : theory 𝓢 = theory 𝓣

def LO.Entailment.«term_≊_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

instance LO.Entailment.WeakerThan.refl {F : Type u_1} {S : Type u_2} [Entailment F S] (𝓢 : S) : 𝓢 wkn 𝓢

theorem LO.Entailment.WeakerThan.wk {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment F S] [Entailment F T] {𝓢 : S} {𝓣 : T} (h : 𝓢 wkn 𝓣) {φ : F} : 𝓢 ⊢! φ → 𝓣 ⊢! φ

theorem LO.Entailment.WeakerThan.pbl {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment F S] [Entailment F T] {𝓢 : S} {𝓣 : T} [h : 𝓢 wkn 𝓣] {φ : F} : 𝓢 ⊢! φ → 𝓣 ⊢! φ

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

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

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

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

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

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

theorem LO.Entailment.StrictlyWeakerThan.of_unprovable_provable {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment F S] [Entailment F T] {𝓢 : S} {𝓣 : T} [𝓢 wkn 𝓣] {φ : F} (hS : 𝓢 ⊬ φ) (hT : 𝓣 ⊢! φ) : 𝓢 swkn 𝓣

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

@[simp]

instance LO.Entailment.Equiv.refl {F : Type u_1} {S : Type u_2} [Entailment F S] (𝓢 : S) : 𝓢 ≊ 𝓢

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

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

theorem LO.Entailment.Equiv.antisymm_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment F S] [Entailment F T] {𝓢 : S} {𝓣 : T} : 𝓢 ≊ 𝓣 ↔ 𝓢 wkn 𝓣 ∧ 𝓣 wkn 𝓢

theorem LO.Entailment.Equiv.antisymm {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment F S] [Entailment F T] {𝓢 : S} {𝓣 : T} : 𝓢 wkn 𝓣 ∧ 𝓣 wkn 𝓢 → 𝓢 ≊ 𝓣

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

theorem LO.Entailment.Equiv.le {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment F S] [Entailment F T] {𝓢 : S} {𝓣 : T} : 𝓢 ≊ 𝓣 → 𝓢 wkn 𝓣

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• not_inconsistent : ¬Inconsistent 𝓢

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

• toFun : F → F'

  Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

theorem LO.Entailment.Translation.ext_iff {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} {inst✝ : Entailment F S} {inst✝¹ : Entailment F' S'} {𝓢 : S} {𝓣 : S'} {x y : 𝓢 ↝ 𝓣} : x = y ↔ x.toFun = y.toFun ∧ @prf S S' F F' inst✝ inst✝¹ 𝓢 𝓣 x ≍ @prf S S' F F' inst✝ inst✝¹ 𝓢 𝓣 y

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• r : 𝓢 ↝ 𝓣

  Imported declaration from the Incompleteness formalization.

• l : 𝓣 ↝ 𝓢

  Imported declaration from the Incompleteness formalization.

• r_l : self.r.toFun ∘ self.l.toFun = id

  Imported declaration from the Incompleteness formalization.

• l_r : self.l.toFun ∘ self.r.toFun = id

  Imported declaration from the Incompleteness formalization.

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

theorem LO.Entailment.Bitranslation.ext_iff {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} {inst✝ : Entailment F S} {inst✝¹ : Entailment F' S'} {𝓢 : S} {𝓣 : S'} {x y : 𝓢 ↭ 𝓣} : x = y ↔ x.r = y.r ∧ x.l = y.l

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

theorem LO.Entailment.FaithfulTranslation.ext_iff {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} {inst✝ : Entailment F S} {inst✝¹ : Entailment F' S'} {𝓢 : S} {𝓣 : S'} {x y : 𝓢 ↝¹ 𝓣} : x = y ↔ x.toFun = y.toFun ∧ @Translation.prf S S' F F' inst✝ inst✝¹ 𝓢 𝓣 x.toTranslation ≍ @Translation.prf S S' F F' inst✝ inst✝¹ 𝓢 𝓣 y.toTranslation ∧ @prfInv S S' F F' inst✝ inst✝¹ 𝓢 𝓣 x ≍ @prfInv S S' F F' inst✝ inst✝¹ 𝓢 𝓣 y

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

def LO.Entailment.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} [Entailment F S] [Entailment F' S'] [Entailment F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↝ 𝓤) (ψ : 𝓢 ↝ 𝓣) : 𝓢 ↝ 𝓤

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.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} [Entailment F S] [Entailment F' S'] [Entailment F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↝ 𝓤) (ψ : 𝓢 ↝ 𝓣) (f : F) : (φ.comp ψ).toFun f = φ.toFun (ψ.toFun f)

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

@[simp]

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Entailment.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} [Entailment F S] [Entailment F' S'] [Entailment F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↭ 𝓤) (ψ : 𝓢 ↭ 𝓣) : 𝓢 ↭ 𝓤

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

def LO.Entailment.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} [Entailment F S] [Entailment F' S'] [Entailment F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↝¹ 𝓤) (ψ : 𝓢 ↝¹ 𝓣) : 𝓢 ↝¹ 𝓤

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.Entailment.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} [Entailment F S] [Entailment F' S'] [Entailment F'' S''] {𝓢 : S} {𝓣 : S'} {𝓤 : S''} (φ : 𝓣 ↝¹ 𝓤) (ψ : 𝓢 ↝¹ 𝓣) (f : F) : (φ.comp ψ).toFun f = φ.toFun (ψ.toFun f)

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

• prfAxm {𝓢 : S} : 𝓢 ⊢* Collection.set 𝓢

  Imported declaration from the Incompleteness formalization.

• weakening {f : F} {𝓢 𝓣 : S} : 𝓢 ⊆ 𝓣 → 𝓢 ⊢ f → 𝓣 ⊢ f

  Imported declaration from the Incompleteness formalization.

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

Alias of LO.Entailment.Axiomatized.prfAxm.

---

Imported declaration from the Incompleteness formalization.

Equations

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

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

Alias of LO.Entailment.Axiomatized.weakening.

---

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

@[simp]

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

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

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

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

theorem LO.Entailment.Axiomatized.weakerThanOfSubset {F : Type u_1} {S : Type u_2} [Entailment F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) : 𝓢 wkn 𝓣

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Alias of LO.Entailment.Axiomatized.provable_axm.

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

Alias of LO.Entailment.Axiomatized.weakening!.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Entailment.WeakerThan.ofAxm! {F : Type u_1} {S : Type u_2} [Entailment F S] [Collection F S] [StrongCut S S] {𝓢₁ 𝓢₂ : S} (B : 𝓢₂ ⊢!* Collection.set 𝓢₁) : 𝓢₁ wkn 𝓢₂

Imported declaration from the Incompleteness formalization.

theorem LO.Entailment.WeakerThan.ofSubset {F : Type u_1} {S : Type u_2} [Entailment F S] [Collection F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) : 𝓢 wkn 𝓣

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

• φ {𝓢 : S} {f : F} : 𝓢 ⊢ f → S

  Imported declaration from the Incompleteness formalization.

• φPrf {𝓢 : S} {f : F} (b : 𝓢 ⊢ f) : φ b ⊢ f

  Imported declaration from the Incompleteness formalization.

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

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

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

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

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

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

• ofInsert {φ ψ : F} {𝓢 : S} : cons φ 𝓢 ⊢ ψ → 𝓢 ⊢ φ ==> ψ

  Imported declaration from the Incompleteness formalization.

• inv {φ ψ : F} {𝓢 : S} : 𝓢 ⊢ φ ==> ψ → cons φ 𝓢 ⊢ ψ

  Imported declaration from the Incompleteness formalization.

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

Alias of LO.Entailment.Deduction.ofInsert.

---

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Alias of LO.Entailment.Deduction.of_insert!.

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

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

theorem LO.Sound.not_provable_of_countermodel {S : Type u_1} {F : Type u_2} [Entailment 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} [Entailment F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {𝓜 : M} [Sound 𝓢 𝓜] : Semantics.Meaningful 𝓜 → Entailment.Consistent 𝓢

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

theorem LO.Sound.realizeSet_of_prfSet {S : Type u_1} {F : Type u_2} [Entailment 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} [Entailment 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} [Entailment 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 → Entailment.Consistent 𝓢

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

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

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

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

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

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

theorem LO.Complete.weakerthan_of_models {S : Type u_1} {F : Type u_2} [Entailment F S] {M : Type u_3} [Semantics F M] {𝓢 : S} {s : Set F} [Complete 𝓢 (Semantics.models M s)] {𝓣 : S} {t : Set F} [Sound 𝓣 (Semantics.models M t)] (H : ∀ (𝓜 : M), 𝓜 ⊧* s → 𝓜 ⊧* t) : 𝓣 wkn 𝓢