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

• 𝓢 ⊢ p: a type of formalized proofs of p : F from deductive system 𝓢 : S.
• 𝓢 ⊢! p: a proposition that states there is a proof of p from 𝓢, i.e. p is provable from 𝓢.
• 𝓢 ⊬ p: a proposition that states p 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} [LO.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} [LO.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} [LO.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} [LO.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} [LO.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} [LO.System F S] {𝓢 : S} {f : F} : 𝓢 ⊬ f ↔ IsEmpty (𝓢 ⊢ f)

noncomputable def LO.System.Provable.get {F : Type u_1} {S : Type u_2} [LO.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} [LO.System F S] {𝓢 : S} {s : Set F} : 𝓢 ⊢!* s ↔ Nonempty (𝓢 ⊢* s)

noncomputable def LO.System.ProvableSet.get {F : Type u_1} {S : Type u_2} [LO.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} [LO.System F S] [LO.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} [LO.System F S] [LO.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} [LO.System F S] [LO.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} [LO.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} [LO.System F S] [LO.System F T] [LO.System F U] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 ≤ₛ 𝓣 → 𝓣 ≤ₛ 𝓤 → 𝓢 ≤ₛ 𝓤

theorem LO.System.weakerThan_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [LO.System F S] [LO.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} [LO.System F S] [LO.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} [LO.System F S] [LO.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} [LO.System F S] [LO.System F T] [LO.System F U] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 <ₛ 𝓣 → 𝓣 <ₛ 𝓤 → 𝓢 <ₛ 𝓤

theorem LO.System.weakening {F : Type u_1} {S : Type u_2} {T : Type u_3} [LO.System F S] [LO.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} [LO.System F S] [LO.System F T] {𝓢 : S} {𝓣 : T} : 𝓢 =ₛ 𝓣 ↔ ∀ (f : F), 𝓢 ⊢! f ↔ 𝓣 ⊢! f

@[simp]

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

theorem LO.System.Equiv.symm {F : Type u_1} {S : Type u_2} {T : Type u_3} [LO.System F S] [LO.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} [LO.System F S] [LO.System F T] [LO.System F U] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 =ₛ 𝓣 → 𝓣 =ₛ 𝓤 → 𝓢 =ₛ 𝓤

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

theorem LO.System.Equiv.antisymm {F : Type u_1} {S : Type u_2} {T : Type u_3} [LO.System F S] [LO.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} [LO.System F S] [LO.System F T] {𝓢 : S} {𝓣 : T} : 𝓢 =ₛ 𝓣 → 𝓢 ≤ₛ 𝓣

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

Equations

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

@[reducible, inline]

abbrev LO.System.Logic {F : Type u_1} (S : Type u_2) [LO.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} [LO.System F S] {𝓢 : S} {𝓣 : S} : 𝓢 ≈ 𝓣 ↔ LO.System.theory 𝓢 = LO.System.theory 𝓣

@[simp]

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

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

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

• not_inconsistent : ¬LO.System.Inconsistent 𝓢

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

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

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

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

theorem LO.System.Consistent.not_inc {F : Type u_1} {S : Type u_2} [LO.System F S] {𝓢 : S} : LO.System.Consistent 𝓢 → ¬LO.System.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} [LO.System F S] {𝓢 : S} : ¬LO.System.Consistent 𝓢 ↔ LO.System.Inconsistent 𝓢

theorem LO.System.Inconsistent.not_con {F : Type u_1} {S : Type u_2} [LO.System F S] {𝓢 : S} : LO.System.Inconsistent 𝓢 → ¬LO.System.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} [LO.System F S] {𝓢 : S} : LO.System.Consistent 𝓢 ↔ ∃ (f : F), 𝓢 ⊬ f

theorem LO.System.Consistent.exists_unprovable {F : Type u_1} {S : Type u_2} [LO.System F S] {𝓢 : S} : LO.System.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} [LO.System F S] {𝓢 : S} {f : F} (h : 𝓢 ⊬ f) : LO.System.Consistent 𝓢

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

theorem LO.System.Inconsistent.theory_eq {F : Type u_1} {S : Type u_2} [LO.System F S] {𝓢 : S} : LO.System.Inconsistent 𝓢 → LO.System.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} [LO.System F S] {𝓢 : S} {𝓣 : S} (h : LO.System.Inconsistent 𝓢) (h' : LO.System.Inconsistent 𝓣) : 𝓢 ≈ 𝓣

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

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

def LO.System.Logic.Inconsistent {F : Type u_1} {S : Type u_2} [LO.System F S] (Λ : LO.System.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} [LO.System F S] (𝓢 : S) : LO.System.Logic.Inconsistent ⟦𝓢⟧ ↔ LO.System.Inconsistent 𝓢

def LO.System.Logic.Consistent {F : Type u_1} {S : Type u_2} [LO.System F S] (Λ : LO.System.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} [LO.System F S] (𝓢 : S) : LO.System.Logic.Consistent ⟦𝓢⟧ ↔ LO.System.Consistent 𝓢

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

theorem LO.System.Translation.ext_iff {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} : ∀ {inst : LO.System F S} {inst_1 : LO.System F' S'} {𝓢 : S} {𝓣 : S'} (x y : 𝓢 ↝ 𝓣), x = y ↔ x.toFun = y.toFun ∧ HEq (@LO.System.Translation.prf S S' F F' inst inst_1 𝓢 𝓣 x) (@LO.System.Translation.prf S S' F F' inst inst_1 𝓢 𝓣 y)

structure LO.System.Translation {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} [LO.System F S] [LO.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

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))

theorem LO.System.Bitranslation.ext_iff {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} : ∀ {inst : LO.System F S} {inst_1 : LO.System F' S'} {𝓢 : S} {𝓣 : S'} (x y : 𝓢 ↭ 𝓣), x = y ↔ x.r = y.r ∧ x.l = y.l

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

structure LO.System.Bitranslation {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} [LO.System F S] [LO.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.r_l {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} [LO.System F S] [LO.System F' S'] {𝓢 : S} {𝓣 : S'} (self : 𝓢 ↭ 𝓣) : self.r.toFun ∘ self.l.toFun = id

theorem LO.System.Bitranslation.l_r {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} [LO.System F S] [LO.System F' S'] {𝓢 : S} {𝓣 : S'} (self : 𝓢 ↭ 𝓣) : self.l.toFun ∘ self.r.toFun = id

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))

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

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

structure LO.System.FaithfulTranslation {S : Type u_5} {S' : Type u_6} {F : Type u_7} {F' : Type u_8} [LO.System F S] [LO.System F' S'] (𝓢 : S) (𝓣 : S') extends LO.System.Translation : 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

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} [LO.System F S] [LO.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} [LO.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} [LO.System F S] (𝓢 : S) (f : F) : (LO.System.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} [LO.System F S] [LO.System F' S'] [LO.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} [LO.System F S] [LO.System F' S'] [LO.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} [LO.System F S] [LO.System F' S'] {𝓢 : S} {𝓣 : S'} (φ : 𝓢 ↝ 𝓣) {p : F} (h : 𝓢 ⊢! p) : 𝓣 ⊢! φ.toFun p

@[simp]

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

@[simp]

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

def LO.System.Bitranslation.id {S : Type u_5} {F : Type u_8} [LO.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} [LO.System F S] [LO.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} [LO.System F S] [LO.System F' S'] [LO.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} [LO.System F S] [LO.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} [LO.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} [LO.System F S] (𝓢 : S) (f : F) : (LO.System.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} [LO.System F S] [LO.System F' S'] [LO.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} [LO.System F S] [LO.System F' S'] [LO.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} [LO.System F S] [LO.System F' S'] {𝓢 : S} {𝓣 : S'} (φ : 𝓢 ↝¹ 𝓣) {p : F} (h : 𝓢 ⊢! p) : 𝓣 ⊢! φ.toFun p

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

class LO.System.Subtheory {F : Type u_1} {S : Type u_2} [LO.System F S] (𝓢 : 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} [LO.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} [LO.System F S] {𝓢 : S} {𝓣 : 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} [LO.System F S] {𝓢 : 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} [LO.System F S] {𝓢 : S} {𝓣 : S} (t : 𝓢 ↝ 𝓣) (h : ∀ (p : F), t.toFun p = p) : 𝓢 ≼ 𝓣

Equations

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

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

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

Equations

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

def LO.System.Undecidable {F : Type u_1} {S : Type u_2} [LO.System F S] [LO.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} [LO.System F S] [LO.LogicalConnective F] {𝓢 : S} : ¬LO.System.Complete 𝓢 ↔ ∃ (f : F), LO.System.Undecidable 𝓢 f

class LO.System.Axiomatized {F : Type u_1} (S : Type u_2) [LO.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} [LO.System F S] [Collection F S] [self : LO.System.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} [LO.System F S] [Collection F S] [self : LO.System.Axiomatized S] {f : F} {𝓢 : S} {𝓣 : 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) [LO.System F S] [LO.System F T] [Collection F T] : Type (max (max (max (max u_1 u_2) u_3) u_5) u_6)

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

@[simp]

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

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

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

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

def LO.System.Axiomatized.subtheoryOfSubset {F : Type u_1} {S : Type u_2} [LO.System F S] [Collection F S] [LO.System.Axiomatized S] {𝓢 : 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} [LO.System F S] [Collection F S] [LO.System.Axiomatized S] {𝓢 : 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} [LO.System F S] [Collection F S] [LO.System.Axiomatized S] (𝓢 : S) : 𝓢 ⊢!* Collection.set 𝓢

Alias of LO.System.Axiomatized.provable_axm.

theorem LO.System.wk! {F : Type u_1} {S : Type u_2} [LO.System F S] [Collection F S] [LO.System.Axiomatized S] {𝓢 : 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} [LO.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} [LO.System F S] [Collection F S] [LO.System.Axiomatized S] {𝓢 : S} {𝓣 : S} (h𝓢 : LO.System.Consistent 𝓢) (h : 𝓣 ⊆ 𝓢) : LO.System.Consistent 𝓣

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

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

def LO.System.StrongCut.translation {F : Type u_1} {S : Type u_2} {T : Type u_3} [LO.System F S] [LO.System F T] [Collection F T] [LO.System.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} [LO.System F S] [Collection F S] [LO.System.StrongCut S 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} [LO.System F S] [Collection F S] [LO.System.StrongCut S 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} [LO.System F S] [Collection F S] [LO.System.Axiomatized S] {𝓢 : 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) [LO.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) → LO.System.Compact.φ b ⊢ f
• φ_subset : ∀ {𝓢 : S} {f : F} (b : 𝓢 ⊢ f), LO.System.Compact.φ b ⊆ 𝓢
• φ_finite : ∀ {𝓢 : S} {f : F} (b : 𝓢 ⊢ f), Collection.Finite (LO.System.Compact.φ b)

theorem LO.System.Compact.φ_subset {F : Type u_1} {S : Type u_2} [LO.System F S] [Collection F S] [self : LO.System.Compact S] {𝓢 : S} {f : F} (b : 𝓢 ⊢ f) : LO.System.Compact.φ b ⊆ 𝓢

theorem LO.System.Compact.φ_finite {F : Type u_1} {S : Type u_2} [LO.System F S] [Collection F S] [self : LO.System.Compact S] {𝓢 : S} {f : F} (b : 𝓢 ⊢ f) : Collection.Finite (LO.System.Compact.φ b)

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

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

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

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

Equations

• ⋯ = ⋯

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

theorem LO.System.inconsistent_of_provable {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] [LO.System.DeductiveExplosion S] {𝓢 : S} : 𝓢 ⊢! ⊥ → LO.System.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} [LO.LogicalConnective F] [LO.System F S] [LO.System.DeductiveExplosion S] {𝓢 : S} : LO.System.Consistent 𝓢 ↔ 𝓢 ⊬ ⊥

theorem LO.System.Consistent.not_bot {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] [LO.System.DeductiveExplosion S] {𝓢 : S} : LO.System.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} [LO.LogicalConnective F] [LO.System F S] [LO.System.DeductiveExplosion S] [Collection F S] [LO.System.Axiomatized S] [LO.System.Compact S] {𝓢 : S} : LO.System.Inconsistent 𝓢 ↔ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ LO.System.Inconsistent 𝓕

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

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

• ofInsert : {p q : F} → {𝓢 : S} → cons p 𝓢 ⊢ q → 𝓢 ⊢ p ➝ q
• inv : {p q : F} → {𝓢 : S} → 𝓢 ⊢ p ➝ q → cons p 𝓢 ⊢ q

def LO.System.deduction {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.System F S] [Cons F S] [self : LO.System.Deduction S] {p : F} {q : F} {𝓢 : S} : cons p 𝓢 ⊢ q → 𝓢 ⊢ p ➝ q

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} [LO.LogicalConnective F] [LO.System F S] [Cons F S] [LO.System.Deduction S] {𝓢 : S} {p : F} {q : F} (h : cons p 𝓢 ⊢! q) : 𝓢 ⊢! p ➝ q

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

Alias of LO.System.Deduction.of_insert!.

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

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

Equations

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

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

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

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

theorem LO.Sound.sound {S : Type u_1} {F : Type u_2} [LO.System F S] {M : Type u_3} [LO.Semantics F M] {𝓢 : S} {𝓜 : M} [self : LO.Sound 𝓢 𝓜] {f : F} : 𝓢 ⊢! f → 𝓜 ⊧ f

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

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

theorem LO.Complete.complete {S : Type u_1} {F : Type u_2} [LO.System F S] {M : Type u_3} [LO.Semantics F M] {𝓢 : S} {𝓜 : M} [self : LO.Complete 𝓢 𝓜] {f : F} : 𝓜 ⊧ f → 𝓢 ⊢! f

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

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

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

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

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

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

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

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

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

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

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

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