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
- LO.System.ProvablyEquivalent π’ p q = (π’ β’! p β€ q)
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)
:
LO.System.ProvablyEquivalent π’ p p
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}
:
LO.System.ProvablyEquivalent π’ p q β LO.System.ProvablyEquivalent π’ q p
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}
:
π’ β’! p β LO.System.ProvablyEquivalent π’ p β€
def
LO.System.ProvablyEquivalent.setoid
{F : Type u_1}
{S : Type u_2}
[LO.LogicalConnective F]
[LO.System F S]
(π’ : S)
[LO.System.Minimal π’]
:
Setoid F
Equations
- LO.System.ProvablyEquivalent.setoid π’ = { r := fun (x x_1 : F) => LO.System.ProvablyEquivalent π’ x x_1, iseqv := β― }
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 π’]
:
LE (LO.System.Lindenbaum π’)
Equations
- LO.System.Lindenbaum.instLE π’ = { le := Quotient.liftβ (fun (p q : F) => π’ β’! p β q) β― }
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}
:
instance
LO.System.Lindenbaum.instTop
{F : Type u_1}
{S : Type u_2}
[LO.LogicalConnective F]
[LO.System F S]
(π’ : S)
[LO.System.Minimal π’]
:
Top (LO.System.Lindenbaum π’)
Equations
- LO.System.Lindenbaum.instTop π’ = { top := β¦β€β§ }
instance
LO.System.Lindenbaum.instBot
{F : Type u_1}
{S : Type u_2}
[LO.LogicalConnective F]
[LO.System F S]
(π’ : S)
[LO.System.Minimal π’]
:
Bot (LO.System.Lindenbaum π’)
Equations
- LO.System.Lindenbaum.instBot π’ = { bot := β¦β₯β§ }
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 π’]
:
Inf (LO.System.Lindenbaum π’)
Equations
- LO.System.Lindenbaum.instInf π’ = { inf := Quotient.liftβ (fun (p q : F) => β¦p β qβ§) β― }
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 π’]
:
Sup (LO.System.Lindenbaum π’)
Equations
- LO.System.Lindenbaum.instSup π’ = { sup := Quotient.liftβ (fun (p q : F) => β¦p β qβ§) β― }
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 π’]
:
HImp (LO.System.Lindenbaum π’)
Equations
- LO.System.Lindenbaum.instHImp π’ = { himp := Quotient.liftβ (fun (p q : F) => β¦p β qβ§) β― }
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 π’]
:
HasCompl (LO.System.Lindenbaum π’)
Equations
- LO.System.Lindenbaum.instHasCompl π’ = { compl := Quotient.lift (fun (p : F) => β¦βΌpβ§) β― }
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)
:
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)
:
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)
:
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)
:
instance
LO.System.Lindenbaum.instGeneralizedHeytingAlgebra
{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.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}
:
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 = β€
theorem
LO.System.Lindenbaum.consistent_iff_nontrivial
{F : Type u_1}
{S : Type u_2}
[LO.LogicalConnective F]
[LO.System F S]
{π’ : S}
[LO.System.Minimal π’]
:
LO.System.Consistent π’ β Nontrivial (LO.System.Lindenbaum π’)
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 π’]
:
Nontrivial (LO.System.Lindenbaum π’)
Equations
- β― = β―
instance
LO.System.Lindenbaum.heyting
{F : Type u_1}
{S : Type u_2}
[DecidableEq F]
[LO.LogicalConnective F]
[LO.System F S]
(π’ : S)
[LO.System.Intuitionistic π’]
:
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
- LO.System.Lindenbaum.boolean π’ = BooleanAlgebra.mk β― β― β― β― β― β―