def
LO.System.ProvablyEquivalent
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
(Ο Ο : F)
:
Equations
- LO.System.ProvablyEquivalent π’ Ο Ο = (π’ β’! Ο β€ Ο)
Instances For
theorem
LO.System.ProvablyEquivalent.refl
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
(Ο : F)
:
ProvablyEquivalent π’ Ο Ο
theorem
LO.System.ProvablyEquivalent.symm
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
{π’ : S}
[System.Minimal π’]
{Ο Ο : F}
:
ProvablyEquivalent π’ Ο Ο β ProvablyEquivalent π’ Ο Ο
theorem
LO.System.ProvablyEquivalent.trans
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
{π’ : S}
[System.Minimal π’]
{Ο Ο Ο : F}
:
ProvablyEquivalent π’ Ο Ο β ProvablyEquivalent π’ Ο Ο β ProvablyEquivalent π’ Ο Ο
theorem
LO.System.provable_iff_provablyEquivalent_verum
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
{π’ : S}
[System.Minimal π’]
{Ο : F}
:
π’ β’! Ο β ProvablyEquivalent π’ Ο β€
def
LO.System.ProvablyEquivalent.setoid
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
:
Setoid F
Equations
- LO.System.ProvablyEquivalent.setoid π’ = { r := fun (x1 x2 : F) => LO.System.ProvablyEquivalent π’ x1 x2, iseqv := β― }
Instances For
@[reducible, inline]
abbrev
LO.System.LindenbaumAlgebra
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
:
Type u_1
Equations
Instances For
theorem
LO.System.LindenbaumAlgebra.of_eq_of
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
{Ο Ο : F}
:
instance
LO.System.LindenbaumAlgebra.instLEOfDecidableEq
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
:
LE (LindenbaumAlgebra π’)
Equations
- LO.System.LindenbaumAlgebra.instLEOfDecidableEq π’ = { le := Quotient.liftβ (fun (Ο Ο : F) => π’ β’! Ο β Ο) β― }
theorem
LO.System.LindenbaumAlgebra.le_def
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
{Ο Ο : F}
:
instance
LO.System.LindenbaumAlgebra.instTop
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
:
Top (LindenbaumAlgebra π’)
Equations
- LO.System.LindenbaumAlgebra.instTop π’ = { top := β¦β€β§ }
instance
LO.System.LindenbaumAlgebra.instBot
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
:
Bot (LindenbaumAlgebra π’)
Equations
- LO.System.LindenbaumAlgebra.instBot π’ = { bot := β¦β₯β§ }
instance
LO.System.LindenbaumAlgebra.instMinOfDecidableEq
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
:
Min (LindenbaumAlgebra π’)
Equations
- LO.System.LindenbaumAlgebra.instMinOfDecidableEq π’ = { min := Quotient.liftβ (fun (Ο Ο : F) => β¦Ο β Οβ§) β― }
instance
LO.System.LindenbaumAlgebra.instMaxOfDecidableEq
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
:
Max (LindenbaumAlgebra π’)
Equations
- LO.System.LindenbaumAlgebra.instMaxOfDecidableEq π’ = { max := Quotient.liftβ (fun (Ο Ο : F) => β¦Ο β Οβ§) β― }
instance
LO.System.LindenbaumAlgebra.instHImpOfDecidableEq
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
:
HImp (LindenbaumAlgebra π’)
Equations
- LO.System.LindenbaumAlgebra.instHImpOfDecidableEq π’ = { himp := Quotient.liftβ (fun (Ο Ο : F) => β¦Ο β Οβ§) β― }
instance
LO.System.LindenbaumAlgebra.instHasComplOfDecidableEq
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
:
HasCompl (LindenbaumAlgebra π’)
Equations
- LO.System.LindenbaumAlgebra.instHasComplOfDecidableEq π’ = { compl := Quotient.lift (fun (Ο : F) => β¦βΌΟβ§) β― }
theorem
LO.System.LindenbaumAlgebra.top_def
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
:
theorem
LO.System.LindenbaumAlgebra.bot_def
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
:
theorem
LO.System.LindenbaumAlgebra.inf_def
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
(Ο Ο : F)
:
theorem
LO.System.LindenbaumAlgebra.sup_def
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
(Ο Ο : F)
:
theorem
LO.System.LindenbaumAlgebra.himp_def
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
(Ο Ο : F)
:
theorem
LO.System.LindenbaumAlgebra.compl_def
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
(Ο : F)
:
instance
LO.System.LindenbaumAlgebra.instGeneralizedHeytingAlgebraOfDecidableEq
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Minimal π’]
[DecidableEq F]
:
theorem
LO.System.LindenbaumAlgebra.provable_iff_eq_top
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
{π’ : S}
[System.Minimal π’]
{Ο : F}
:
theorem
LO.System.LindenbaumAlgebra.inconsistent_iff_trivial
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
{π’ : S}
[System.Minimal π’]
:
Inconsistent π’ β β (Ο : LindenbaumAlgebra π’), Ο = β€
theorem
LO.System.LindenbaumAlgebra.consistent_iff_nontrivial
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
{π’ : S}
[System.Minimal π’]
:
Consistent π’ β Nontrivial (LindenbaumAlgebra π’)
instance
LO.System.LindenbaumAlgebra.nontrivial_of_consistent
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
{π’ : S}
[System.Minimal π’]
[Consistent π’]
:
Nontrivial (LindenbaumAlgebra π’)
instance
LO.System.LindenbaumAlgebra.heyting
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Intuitionistic π’]
[DecidableEq F]
:
HeytingAlgebra (LindenbaumAlgebra π’)
Equations
instance
LO.System.LindenbaumAlgebra.boolean
{F : Type u_1}
{S : Type u_2}
[LogicalConnective F]
[System F S]
(π’ : S)
[System.Classical π’]
[DecidableEq F]
:
BooleanAlgebra (LindenbaumAlgebra π’)
Equations
- LO.System.LindenbaumAlgebra.boolean π’ = BooleanAlgebra.mk β― β― β― β― β― β―