Documentation

Foundation.Logic.Lindenbaum

def LO.System.ProvablyEquivalent {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) (p : F) (q : F) :
Equations
Instances For
    theorem LO.System.ProvablyEquivalent.refl {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] (p : F) :
    theorem LO.System.ProvablyEquivalent.symm {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓒 : S} [LO.System.Minimal 𝓒] {p : F} {q : F} :
    theorem LO.System.ProvablyEquivalent.trans {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓒 : S} [LO.System.Minimal 𝓒] {p : F} {q : F} {r : F} :
    LO.System.ProvablyEquivalent 𝓒 p q β†’ LO.System.ProvablyEquivalent 𝓒 q r β†’ LO.System.ProvablyEquivalent 𝓒 p r
    theorem LO.System.provable_iff_provablyEquivalent_verum {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓒 : S} [LO.System.Minimal 𝓒] {p : F} :
    def LO.System.ProvablyEquivalent.setoid {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
    Equations
    Instances For
      @[reducible, inline]
      abbrev LO.System.Lindenbaum {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
      Type u_1
      Equations
      Instances For
        theorem LO.System.Lindenbaum.of_eq_of {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] {p : F} {q : F} :
        ⟦p⟧ = ⟦q⟧ ↔ LO.System.ProvablyEquivalent 𝓒 p q
        instance LO.System.Lindenbaum.instLE {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        Equations
        theorem LO.System.Lindenbaum.le_def {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] {p : F} {q : F} :
        ⟦p⟧ ≀ ⟦q⟧ ↔ 𝓒 ⊒! p ➝ q
        instance LO.System.Lindenbaum.instTop {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        Equations
        instance LO.System.Lindenbaum.instBot {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        Equations
        instance LO.System.Lindenbaum.instInf {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        Equations
        instance LO.System.Lindenbaum.instSup {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        Equations
        instance LO.System.Lindenbaum.instHImp {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        Equations
        instance LO.System.Lindenbaum.instHasCompl {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        Equations
        theorem LO.System.Lindenbaum.top_def {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        ⊀ = ⟦⊀⟧
        theorem LO.System.Lindenbaum.bot_def {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        βŠ₯ = ⟦βŠ₯⟧
        theorem LO.System.Lindenbaum.inf_def {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] (p : F) (q : F) :
        ⟦p⟧ βŠ“ ⟦q⟧ = ⟦p ⋏ q⟧
        theorem LO.System.Lindenbaum.sup_def {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] (p : F) (q : F) :
        ⟦p⟧ βŠ” ⟦q⟧ = ⟦p β‹Ž q⟧
        theorem LO.System.Lindenbaum.himp_def {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] (p : F) (q : F) :
        ⟦p⟧ ⇨ ⟦q⟧ = ⟦p ➝ q⟧
        theorem LO.System.Lindenbaum.compl_def {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] (p : F) :
        (⟦p⟧)ᢜ = ⟦∼p⟧
        theorem LO.System.Lindenbaum.provable_iff_eq_top {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓒 : S} [LO.System.Minimal 𝓒] {p : F} :
        𝓒 ⊒! p ↔ ⟦p⟧ = ⊀
        theorem LO.System.Lindenbaum.inconsistent_iff_trivial {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓒 : S} [LO.System.Minimal 𝓒] :
        LO.System.Inconsistent 𝓒 ↔ βˆ€ (p : LO.System.Lindenbaum 𝓒), p = ⊀
        instance LO.System.Lindenbaum.nontrivial_of_consistent {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓒 : S} [LO.System.Minimal 𝓒] [LO.System.Consistent 𝓒] :
        Equations
        • β‹― = β‹―
        instance LO.System.Lindenbaum.boolean {F : Type u_1} {S : Type u_2} [DecidableEq F] [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Classical 𝓒] :
        Equations