Documentation

Foundation.Logic.LindenbaumAlgebra

def LO.System.ProvablyEquivalent {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) (Ο† ψ : 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 𝓒] (Ο† : F) :
    LO.System.ProvablyEquivalent 𝓒 Ο† Ο†
    theorem LO.System.ProvablyEquivalent.symm {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓒 : S} [LO.System.Minimal 𝓒] {Ο† ψ : F} :
    LO.System.ProvablyEquivalent 𝓒 Ο† ψ β†’ LO.System.ProvablyEquivalent 𝓒 ψ Ο†
    theorem LO.System.ProvablyEquivalent.trans {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓒 : S} [LO.System.Minimal 𝓒] {Ο† ψ Ο‡ : F} :
    LO.System.ProvablyEquivalent 𝓒 Ο† ψ β†’ LO.System.ProvablyEquivalent 𝓒 ψ Ο‡ β†’ LO.System.ProvablyEquivalent 𝓒 Ο† Ο‡
    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 𝓒] {Ο† : F} :
    𝓒 ⊒! Ο† ↔ LO.System.ProvablyEquivalent 𝓒 Ο† ⊀
    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.LindenbaumAlgebra {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.LindenbaumAlgebra.of_eq_of {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] {Ο† ψ : F} :
        βŸ¦Ο†βŸ§ = ⟦ψ⟧ ↔ LO.System.ProvablyEquivalent 𝓒 Ο† ψ
        Equations
        theorem LO.System.LindenbaumAlgebra.le_def {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] [DecidableEq F] {Ο† ψ : F} :
        βŸ¦Ο†βŸ§ ≀ ⟦ψ⟧ ↔ 𝓒 ⊒! Ο† ➝ ψ
        instance LO.System.LindenbaumAlgebra.instTop {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        Equations
        instance LO.System.LindenbaumAlgebra.instBot {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        Equations
        Equations
        Equations
        Equations
        Equations
        theorem LO.System.LindenbaumAlgebra.top_def {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        ⊀ = ⟦⊀⟧
        theorem LO.System.LindenbaumAlgebra.bot_def {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] :
        βŠ₯ = ⟦βŠ₯⟧
        theorem LO.System.LindenbaumAlgebra.inf_def {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] [DecidableEq F] (Ο† ψ : F) :
        βŸ¦Ο†βŸ§ βŠ“ ⟦ψ⟧ = βŸ¦Ο† ⋏ ψ⟧
        theorem LO.System.LindenbaumAlgebra.sup_def {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] [DecidableEq F] (Ο† ψ : F) :
        βŸ¦Ο†βŸ§ βŠ” ⟦ψ⟧ = βŸ¦Ο† β‹Ž ψ⟧
        theorem LO.System.LindenbaumAlgebra.himp_def {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] [DecidableEq F] (Ο† ψ : F) :
        βŸ¦Ο†βŸ§ ⇨ ⟦ψ⟧ = βŸ¦Ο† ➝ ψ⟧
        theorem LO.System.LindenbaumAlgebra.compl_def {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓒 : S) [LO.System.Minimal 𝓒] [DecidableEq F] (Ο† : F) :
        (βŸ¦Ο†βŸ§)ᢜ = βŸ¦βˆΌΟ†βŸ§
        theorem LO.System.LindenbaumAlgebra.provable_iff_eq_top {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] {𝓒 : S} [LO.System.Minimal 𝓒] {Ο† : F} :
        𝓒 ⊒! Ο† ↔ βŸ¦Ο†βŸ§ = ⊀
        theorem LO.System.LindenbaumAlgebra.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 𝓒 ↔ βˆ€ (Ο† : LO.System.LindenbaumAlgebra 𝓒), Ο† = ⊀
        Equations
        • β‹― = β‹―
        Equations