Documentation

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)

Instances For

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

Equations

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

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

not_inconsistent : ¬Inconsistent 𝓢

Instances

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

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

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

Instances For

LO.System.Translation.instCoeFunForall

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_↝_» :

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_↭_» :

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

Instances For

LO.System.FaithfulTranslation.instCoeFunForall

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_↝¹_» :

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

Instances

def LO.System.«term_≼_» :

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

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

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

Instances

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 𝓣 → 𝓣 ⊢ φ → 𝓢 ⊢ φ

Instances

@[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) :

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)

Instances

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) → 𝓢 ⊢ φ

Instances

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 φ 𝓢 ⊢ ψ

Instances

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

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

Instances

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

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

Instances

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 𝓢