instance
LO.System.FiniteContext.instCoeList
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
:
Coe (List F) (LO.System.FiniteContext F 𝓢)
Equations
- LO.System.FiniteContext.instCoeList = { coe := LO.System.FiniteContext.mk }
@[reducible, inline]
abbrev
LO.System.FiniteContext.conj
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
{𝓢 : S}
(Γ : LO.System.FiniteContext F 𝓢)
:
F
Instances For
@[reducible, inline]
abbrev
LO.System.FiniteContext.disj
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
{𝓢 : S}
(Γ : LO.System.FiniteContext F 𝓢)
:
F
Instances For
Equations
- LO.System.FiniteContext.instEmptyCollection = { emptyCollection := { ctx := [] } }
instance
LO.System.FiniteContext.instMembership
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
:
Membership F (LO.System.FiniteContext F 𝓢)
Equations
- LO.System.FiniteContext.instMembership = { mem := fun (x : F) (x_1 : LO.System.FiniteContext F 𝓢) => x ∈ x_1.ctx }
Equations
- LO.System.FiniteContext.instHasSubset = { Subset := fun (x x_1 : LO.System.FiniteContext F 𝓢) => x.ctx ⊆ x_1.ctx }
instance
LO.System.FiniteContext.instCons
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
:
Cons F (LO.System.FiniteContext F 𝓢)
Equations
- LO.System.FiniteContext.instCons = { cons := fun (x : F) (x_1 : LO.System.FiniteContext F 𝓢) => { ctx := x :: x_1.ctx } }
theorem
LO.System.FiniteContext.mem_def
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
{p : F}
{Γ : LO.System.FiniteContext F 𝓢}
:
@[simp]
instance
LO.System.FiniteContext.instCollection
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
:
Collection F (LO.System.FiniteContext F 𝓢)
Equations
- LO.System.FiniteContext.instCollection = Collection.mk ⋯ ⋯ ⋯
instance
LO.System.FiniteContext.inst
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
(𝓢 : S)
:
LO.System F (LO.System.FiniteContext F 𝓢)
Equations
- LO.System.FiniteContext.inst 𝓢 = { Prf := fun (x : LO.System.FiniteContext F 𝓢) (x_1 : F) => 𝓢 ⊢ x.conj ➝ x_1 }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.FiniteContext.system_def
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
(Γ : LO.System.FiniteContext F 𝓢)
(p : F)
:
def
LO.System.FiniteContext.ofDef
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
{p : F}
(b : 𝓢 ⊢ ⋀Γ ➝ p)
:
Equations
Instances For
def
LO.System.FiniteContext.toDef
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
{p : F}
(b : Γ ⊢[𝓢] p)
:
Equations
Instances For
instance
LO.System.FiniteContext.instAxiomatized
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.System.FiniteContext.instCompact
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
:
Equations
- One or more equations did not get rendered due to their size.
def
LO.System.FiniteContext.byAxm
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
(h : autoParam (p ∈ Γ) _auto✝)
:
Equations
Instances For
theorem
LO.System.FiniteContext.by_axm!
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
(h : autoParam (p ∈ Γ) _auto✝)
:
def
LO.System.FiniteContext.weakening
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
{Δ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
(h : Γ ⊆ Δ)
{p : F}
:
Instances For
theorem
LO.System.FiniteContext.weakening!
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
{Δ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
(h : Γ ⊆ Δ)
{p : F}
:
def
LO.System.FiniteContext.of
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
{p : F}
(b : 𝓢 ⊢ p)
:
Equations
Instances For
def
LO.System.FiniteContext.emptyPrf
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
{p : F}
:
Equations
- LO.System.FiniteContext.emptyPrf b = b⨀LO.System.verum
Instances For
def
LO.System.FiniteContext.provable_iff_provable
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
{p : F}
:
Equations
- ⋯ = ⋯
Instances For
theorem
LO.System.FiniteContext.of'!
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
(h : 𝓢 ⊢! p)
:
def
LO.System.FiniteContext.id
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
:
Equations
- LO.System.FiniteContext.id = LO.System.FiniteContext.byAxm ⋯
Instances For
def
LO.System.FiniteContext.byAxm₀
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
:
Equations
- LO.System.FiniteContext.byAxm₀ = LO.System.FiniteContext.byAxm ⋯
Instances For
def
LO.System.FiniteContext.byAxm₁
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
:
Equations
- LO.System.FiniteContext.byAxm₁ = LO.System.FiniteContext.byAxm ⋯
Instances For
def
LO.System.FiniteContext.byAxm₂
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
{r : F}
:
Equations
- LO.System.FiniteContext.byAxm₂ = LO.System.FiniteContext.byAxm ⋯
Instances For
theorem
LO.System.FiniteContext.by_axm₀!
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
:
theorem
LO.System.FiniteContext.by_axm₁!
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
:
theorem
LO.System.FiniteContext.by_axm₂!
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
{r : F}
:
@[simp]
theorem
LO.System.FiniteContext.id!
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
:
instance
LO.System.FiniteContext.instModusPonens
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instModusPonens = { mdp := fun {p q : F} => LO.System.mdp₁ }
instance
LO.System.FiniteContext.instHasAxiomVerum
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomVerum = { verum := LO.System.FiniteContext.of LO.System.verum }
instance
LO.System.FiniteContext.instHasAxiomImply₁
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomImply₁ = { imply₁ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.imply₁ }
instance
LO.System.FiniteContext.instHasAxiomImply₂
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomImply₂ = { imply₂ := fun (x x_1 x_2 : F) => LO.System.FiniteContext.of LO.System.imply₂ }
instance
LO.System.FiniteContext.instHasAxiomAndElim₁
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomAndElim₁ = { and₁ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.and₁ }
instance
LO.System.FiniteContext.instHasAxiomAndElim₂
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomAndElim₂ = { and₂ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.and₂ }
instance
LO.System.FiniteContext.instHasAxiomAndInst
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomAndInst = { and₃ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.and₃ }
instance
LO.System.FiniteContext.instHasAxiomOrInst₁
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomOrInst₁ 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomOrInst₁ = { or₁ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.or₁ }
instance
LO.System.FiniteContext.instHasAxiomOrInst₂
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomOrInst₂ 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomOrInst₂ = { or₂ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.or₂ }
instance
LO.System.FiniteContext.instHasAxiomOrElim
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomOrElim 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomOrElim = { or₃ := fun (x x_1 x_2 : F) => LO.System.FiniteContext.of LO.System.or₃ }
instance
LO.System.FiniteContext.instNegationEquiv
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.NegationEquiv 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instNegationEquiv = { neg_equiv := fun (x : F) => LO.System.FiniteContext.of LO.System.neg_equiv }
def
LO.System.FiniteContext.mdp'
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
{Δ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
(bΓ : Γ ⊢[𝓢] p ➝ q)
(bΔ : Δ ⊢[𝓢] p)
:
Equations
- LO.System.FiniteContext.mdp' bΓ bΔ = LO.System.wk ⋯ bΓ⨀LO.System.wk ⋯ bΔ
Instances For
def
LO.System.FiniteContext.deduct
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
{Γ : List F}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.FiniteContext.deduct!
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
(h : (p :: Γ) ⊢[𝓢]! q)
:
def
LO.System.FiniteContext.deductInv
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
{Γ : List F}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.FiniteContext.deductInv!
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : List F}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
(h : Γ ⊢[𝓢]! p ➝ q)
:
theorem
LO.System.FiniteContext.deduct_iff
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
{Γ : List F}
:
def
LO.System.FiniteContext.deduct'
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
:
Equations
Instances For
theorem
LO.System.FiniteContext.deduct'!
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
(h : [p] ⊢[𝓢]! q)
:
def
LO.System.FiniteContext.deductInv'
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
:
Equations
Instances For
theorem
LO.System.FiniteContext.deductInv'!
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
{p : F}
{q : F}
(h : 𝓢 ⊢! p ➝ q)
:
instance
LO.System.FiniteContext.deduction
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.System.FiniteContext.instStrongCut
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.System.FiniteContext.instHasAxiomEFQ
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomEFQ 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomEFQ = { efq := fun (x : F) => LO.System.FiniteContext.of LO.System.efq }
instance
LO.System.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomEFQ 𝓢]
:
Equations
- LO.System.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ = inferInstance
instance
LO.System.FiniteContext.instHasAxiomDNE
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomDNE 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instHasAxiomDNE = { dne := fun (p : F) => LO.System.FiniteContext.of (LO.System.HasAxiomDNE.dne p) }
instance
LO.System.FiniteContext.instMinimal
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
[LO.System.HasAxiomOrInst₁ 𝓢]
[LO.System.HasAxiomOrInst₂ 𝓢]
[LO.System.Minimal 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instMinimal = LO.System.Minimal.mk
instance
LO.System.FiniteContext.instIntuitionistic
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
[LO.System.HasAxiomOrInst₁ 𝓢]
[LO.System.HasAxiomOrInst₂ 𝓢]
[LO.System.Intuitionistic 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instIntuitionistic = LO.System.Intuitionistic.mk
instance
LO.System.FiniteContext.instClassical
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.ModusPonens 𝓢]
[LO.System.HasAxiomVerum 𝓢]
[LO.System.HasAxiomImply₁ 𝓢]
[LO.System.HasAxiomImply₂ 𝓢]
[LO.System.HasAxiomAndElim₁ 𝓢]
[LO.System.HasAxiomAndElim₂ 𝓢]
[LO.System.HasAxiomAndInst 𝓢]
[LO.System.HasAxiomOrInst₁ 𝓢]
[LO.System.HasAxiomOrInst₂ 𝓢]
[LO.System.Classical 𝓢]
(Γ : LO.System.FiniteContext F 𝓢)
:
Equations
- Γ.instClassical = LO.System.Classical.mk
instance
LO.System.Context.instCoeSet
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
:
Coe (Set F) (LO.System.Context F 𝓢)
Equations
- LO.System.Context.instCoeSet = { coe := LO.System.Context.mk }
instance
LO.System.Context.instMembership
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
:
Membership F (LO.System.Context F 𝓢)
Equations
- LO.System.Context.instMembership = { mem := fun (x : F) (x_1 : LO.System.Context F 𝓢) => x ∈ x_1.ctx }
instance
LO.System.Context.instHasSubset
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
:
HasSubset (LO.System.Context F 𝓢)
Equations
- LO.System.Context.instHasSubset = { Subset := fun (x x_1 : LO.System.Context F 𝓢) => x.ctx ⊆ x_1.ctx }
instance
LO.System.Context.instCons
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
:
Cons F (LO.System.Context F 𝓢)
Equations
- LO.System.Context.instCons = { cons := fun (x : F) (x_1 : LO.System.Context F 𝓢) => { ctx := insert x x_1.ctx } }
theorem
LO.System.Context.mem_def
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
{p : F}
{Γ : LO.System.Context F 𝓢}
:
@[simp]
instance
LO.System.Context.instCollection
{F : Type u_1}
{S : Type u_2}
{𝓢 : S}
:
Collection F (LO.System.Context F 𝓢)
Equations
- LO.System.Context.instCollection = Collection.mk ⋯ ⋯ ⋯
structure
LO.System.Context.Proof
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
(Γ : LO.System.Context F 𝓢)
(p : F)
:
Type (max u_1 u_3)
Instances For
theorem
LO.System.Context.Proof.subset
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
{Γ : LO.System.Context F 𝓢}
{p : F}
(self : Γ.Proof p)
(q : F)
:
instance
LO.System.Context.inst
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
(𝓢 : S)
:
LO.System F (LO.System.Context F 𝓢)
Equations
- LO.System.Context.inst 𝓢 = { Prf := LO.System.Context.Proof }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
LO.System.Context.instAxiomatized
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.System.Context.instCompact
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
:
Equations
- One or more equations did not get rendered due to their size.
def
LO.System.Context.deduct
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
[DecidableEq F]
{p : F}
{q : F}
{Γ : Set F}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.System.Context.deductInv
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
{p : F}
{q : F}
{Γ : Set F}
:
Equations
- LO.System.Context.deductInv x = match x with | { ctx := Δ, subset := h, prf := b } => { ctx := p :: Δ, subset := ⋯, prf := LO.System.FiniteContext.deductInv b }
Instances For
instance
LO.System.Context.deduction
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
:
Equations
- One or more equations did not get rendered due to their size.
def
LO.System.Context.of
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
{Γ : Set F}
{p : F}
(b : 𝓢 ⊢ p)
:
Equations
- LO.System.Context.of b = { ctx := [], subset := ⋯, prf := LO.System.FiniteContext.of b }
Instances For
theorem
LO.System.Context.of!
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
{p : F}
{Γ : Set F}
(b : 𝓢 ⊢! p)
:
def
LO.System.Context.mdp
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
{p : F}
{q : F}
{Γ : Set F}
(bpq : Γ *⊢[𝓢] p ➝ q)
(bp : Γ *⊢[𝓢] p)
:
Equations
- LO.System.Context.mdp bpq bp = { ctx := bpq.ctx ++ bp.ctx, subset := ⋯, prf := LO.System.FiniteContext.mdp' bpq.prf bp.prf }
Instances For
theorem
LO.System.Context.by_axm!
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
{p : F}
{Γ : Set F}
(h : p ∈ Γ)
:
def
LO.System.Context.emptyPrf
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
{p : F}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.System.Context.emptyPrf!
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
{p : F}
:
theorem
LO.System.Context.provable_iff_provable
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
{p : F}
:
instance
LO.System.Context.minimal
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- Γ.minimal = LO.System.Minimal.mk
instance
LO.System.Context.instHasAxiomEFQ
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
[LO.System.HasAxiomEFQ 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- Γ.instHasAxiomEFQ = { efq := fun (x : F) => LO.System.Context.of LO.System.efq }
instance
LO.System.Context.instHasAxiomDNE
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
[LO.System.HasAxiomDNE 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- Γ.instHasAxiomDNE = { dne := fun (p : F) => LO.System.Context.of (LO.System.HasAxiomDNE.dne p) }
instance
LO.System.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ
{F : Type u_1}
[LO.LogicalConnective F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Minimal 𝓢]
[LO.System.HasAxiomEFQ 𝓢]
:
Equations
- LO.System.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ = inferInstance
instance
LO.System.Context.instIntuitionistic
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Intuitionistic 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- Γ.instIntuitionistic = LO.System.Intuitionistic.mk
instance
LO.System.Context.instClassical
{F : Type u_1}
[LO.LogicalConnective F]
[DecidableEq F]
{S : Type u_2}
[LO.System F S]
{𝓢 : S}
[LO.System.Classical 𝓢]
(Γ : LO.System.Context F 𝓢)
:
Equations
- Γ.instClassical = LO.System.Classical.mk