structure LO.System.FiniteContext (F : Type u_1) {S : Type u_2} (𝓢 : S) : Type u_1

• ctx : List F

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} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] (Γ : LO.System.FiniteContext F 𝓢) : F

Equations

• Γ.conj = ⋀Γ.ctx

@[reducible, inline]

abbrev LO.System.FiniteContext.disj {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] (Γ : LO.System.FiniteContext F 𝓢) : F

Equations

• Γ.disj = ⋁Γ.ctx

instance LO.System.FiniteContext.instEmptyCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} : EmptyCollection (LO.System.FiniteContext F 𝓢)

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 (Γ : LO.System.FiniteContext F 𝓢) (x : F) => x ∈ Γ.ctx }

instance LO.System.FiniteContext.instHasSubset {F : Type u_1} {S : Type u_2} {𝓢 : S} : HasSubset (LO.System.FiniteContext F 𝓢)

Equations

• LO.System.FiniteContext.instHasSubset = { Subset := fun (x1 x2 : LO.System.FiniteContext F 𝓢) => x1.ctx ⊆ x2.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 (x1 : F) (x2 : LO.System.FiniteContext F 𝓢) => { ctx := x1 :: x2.ctx } }

theorem LO.System.FiniteContext.mem_def {F : Type u_1} {S : Type u_2} {𝓢 : S} {φ : F} {Γ : LO.System.FiniteContext F 𝓢} : φ ∈ Γ ↔ φ ∈ Γ.ctx

@[simp]

theorem LO.System.FiniteContext.coe_subset_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {Γ Δ : List F} : { ctx := Γ } ⊆ { ctx := Δ } ↔ Γ ⊆ Δ

@[simp]

theorem LO.System.FiniteContext.mem_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {φ : F} {Γ : List F} : φ ∈ { ctx := Γ } ↔ φ ∈ Γ

@[simp]

theorem LO.System.FiniteContext.not_mem_empty {F : Type u_1} {S : Type u_2} {𝓢 : S} (φ : F) : φ ∉ ∅

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} {S : Type u_2} [LO.System F S] [LO.LogicalConnective F] (𝓢 : S) : LO.System F (LO.System.FiniteContext F 𝓢)

Equations

• LO.System.FiniteContext.inst 𝓢 = { Prf := fun (x1 : LO.System.FiniteContext F 𝓢) (x2 : F) => 𝓢 ⊢ x1.conj ➝ x2 }

@[reducible, inline]

abbrev LO.System.FiniteContext.Prf {F : Type u_1} {S : Type u_2} [LO.System F S] [LO.LogicalConnective F] (𝓢 : S) (Γ : List F) (φ : F) : Type u_3

Equations

• (Γ ⊢[𝓢] φ) = ({ ctx := Γ } ⊢ φ)

@[reducible, inline]

abbrev LO.System.FiniteContext.Provable {F : Type u_1} {S : Type u_2} [LO.System F S] [LO.LogicalConnective F] (𝓢 : S) (Γ : List F) (φ : F) : Prop

Equations

• (Γ ⊢[𝓢]! φ) = ({ ctx := Γ } ⊢! φ)

@[reducible, inline]

abbrev LO.System.FiniteContext.Unprovable {F : Type u_1} {S : Type u_2} [LO.System F S] [LO.LogicalConnective F] (𝓢 : S) (Γ : List F) (φ : F) : Prop

Equations

• (Γ ⊬[𝓢] φ) = ({ ctx := Γ } ⊬ φ)

@[reducible, inline]

abbrev LO.System.FiniteContext.PrfSet {F : Type u_1} {S : Type u_2} [LO.System F S] [LO.LogicalConnective F] (𝓢 : S) (Γ : List F) (s : Set F) : Type (max u_3 u_1)

Equations

• (Γ ⊢[𝓢]* s) = ({ ctx := Γ } ⊢* s)

@[reducible, inline]

abbrev LO.System.FiniteContext.ProvableSet {F : Type u_1} {S : Type u_2} [LO.System F S] [LO.LogicalConnective F] (𝓢 : S) (Γ : List F) (s : Set F) : Prop

Equations

• (Γ ⊢[𝓢]*! s) = ({ ctx := Γ } ⊢!* s)

def LO.System.FiniteContext.«term_⊢[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.System.FiniteContext.«term_⊢[_]!_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.System.FiniteContext.«term_⊬[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.System.FiniteContext.«term_⊢[_]*_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.System.FiniteContext.«term_⊢[_]*!_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem LO.System.FiniteContext.system_def {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] (Γ : LO.System.FiniteContext F 𝓢) (φ : F) : (Γ ⊢ φ) = (𝓢 ⊢ Γ.conj ➝ φ)

def LO.System.FiniteContext.ofDef {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} {φ : F} (b : 𝓢 ⊢ ⋀Γ ➝ φ) : Γ ⊢[𝓢] φ

Equations

• LO.System.FiniteContext.ofDef b = b

def LO.System.FiniteContext.toDef {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} {φ : F} (b : Γ ⊢[𝓢] φ) : 𝓢 ⊢ ⋀Γ ➝ φ

Equations

• LO.System.FiniteContext.toDef b = b

theorem LO.System.FiniteContext.toₛ! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} {φ : F} (b : Γ ⊢[𝓢]! φ) : 𝓢 ⊢! ⋀Γ ➝ φ

theorem LO.System.FiniteContext.provable_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} {φ : F} : Γ ⊢[𝓢]! φ ↔ 𝓢 ⊢! ⋀Γ ➝ φ

def LO.System.FiniteContext.cast {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ' : List F} {φ' : F} {Γ : List F} {φ : F} (d : Γ ⊢[𝓢] φ) (eΓ : Γ = Γ') (eφ : φ = φ') : Γ' ⊢[𝓢] φ'

Equations

• LO.System.FiniteContext.cast d eΓ eφ = eΓ ▸ eφ ▸ d

instance LO.System.FiniteContext.instAxiomatizedOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] [DecidableEq F] : LO.System.Axiomatized (LO.System.FiniteContext F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

instance LO.System.FiniteContext.instCompact {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] : LO.System.Compact (LO.System.FiniteContext F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

def LO.System.FiniteContext.nthAxm {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {Γ : List F} (n : ℕ) (h : n < Γ.length := by simp) : Γ ⊢[𝓢] Γ[n]

Equations

• LO.System.FiniteContext.nthAxm n h = LO.System.conj₂Nth Γ n h

theorem LO.System.FiniteContext.nth_axm! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {Γ : List F} (n : ℕ) (h : n < Γ.length := by simp) : Γ ⊢[𝓢]! Γ[n]

def LO.System.FiniteContext.byAxm {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] [DecidableEq F] {φ : F} (h : φ ∈ Γ := by simp) : Γ ⊢[𝓢] φ

Equations

• LO.System.FiniteContext.byAxm h = LO.System.Axiomatized.prfAxm ⋯

theorem LO.System.FiniteContext.by_axm! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] [DecidableEq F] {φ : F} (h : φ ∈ Γ := by simp) : Γ ⊢[𝓢]! φ

def LO.System.FiniteContext.weakening {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ Δ : List F} [LO.System.Minimal 𝓢] [DecidableEq F] (h : Γ ⊆ Δ) {φ : F} : Γ ⊢[𝓢] φ → Δ ⊢[𝓢] φ

Equations

• LO.System.FiniteContext.weakening h = LO.System.Axiomatized.weakening ⋯

theorem LO.System.FiniteContext.weakening! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ Δ : List F} [LO.System.Minimal 𝓢] [DecidableEq F] (h : Γ ⊆ Δ) {φ : F} : Γ ⊢[𝓢]! φ → Δ ⊢[𝓢]! φ

def LO.System.FiniteContext.of {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ : F} (b : 𝓢 ⊢ φ) : Γ ⊢[𝓢] φ

Equations

• LO.System.FiniteContext.of b = LO.System.imply₁' b

def LO.System.FiniteContext.emptyPrf {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ : F} : [] ⊢[𝓢] φ → 𝓢 ⊢ φ

Equations

• LO.System.FiniteContext.emptyPrf b = b⨀LO.System.verum

def LO.System.FiniteContext.provable_iff_provable {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ : F} : 𝓢 ⊢! φ ↔ [] ⊢[𝓢]! φ

Equations

• ⋯ = ⋯

theorem LO.System.FiniteContext.of'! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ : F} [DecidableEq F] (h : 𝓢 ⊢! φ) : Γ ⊢[𝓢]! φ

def LO.System.FiniteContext.id {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ : F} : [φ] ⊢[𝓢] φ

Equations

• LO.System.FiniteContext.id = LO.System.FiniteContext.nthAxm 0 LO.System.FiniteContext.id.proof_1

@[simp]

theorem LO.System.FiniteContext.id! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ : F} : [φ] ⊢[𝓢]! φ

def LO.System.FiniteContext.byAxm₀ {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ : F} : (φ :: Γ) ⊢[𝓢] φ

Equations

• LO.System.FiniteContext.byAxm₀ = LO.System.FiniteContext.nthAxm 0 ⋯

theorem LO.System.FiniteContext.by_axm₀! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ : F} : (φ :: Γ) ⊢[𝓢]! φ

def LO.System.FiniteContext.byAxm₁ {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ ψ : F} : (φ :: ψ :: Γ) ⊢[𝓢] ψ

Equations

• LO.System.FiniteContext.byAxm₁ = LO.System.FiniteContext.nthAxm 1 ⋯

theorem LO.System.FiniteContext.by_axm₁! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ ψ : F} : (φ :: ψ :: Γ) ⊢[𝓢]! ψ

def LO.System.FiniteContext.byAxm₂ {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ ψ χ : F} : (φ :: ψ :: χ :: Γ) ⊢[𝓢] χ

Equations

• LO.System.FiniteContext.byAxm₂ = LO.System.FiniteContext.nthAxm 2 ⋯

theorem LO.System.FiniteContext.by_axm₂! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ ψ χ : F} : (φ :: ψ :: χ :: Γ) ⊢[𝓢]! χ

instance LO.System.FiniteContext.instModusPonens {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.ModusPonens Γ

Equations

• Γ.instModusPonens = { mdp := fun {φ ψ : F} => LO.System.mdp₁ }

instance LO.System.FiniteContext.instHasAxiomVerum {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomVerum Γ

Equations

• Γ.instHasAxiomVerum = { verum := LO.System.FiniteContext.of LO.System.verum }

instance LO.System.FiniteContext.instHasAxiomImply₁ {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomImply₁ Γ

Equations

• Γ.instHasAxiomImply₁ = { imply₁ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.imply₁ }

instance LO.System.FiniteContext.instHasAxiomImply₂ {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomImply₂ Γ

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} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomAndElim Γ

Equations

• Γ.instHasAxiomAndElim = { and₁ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.and₁, and₂ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.and₂ }

instance LO.System.FiniteContext.instHasAxiomAndInst {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomAndInst Γ

Equations

• Γ.instHasAxiomAndInst = { and₃ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.and₃ }

instance LO.System.FiniteContext.instHasAxiomOrInst {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomOrInst Γ

Equations

• Γ.instHasAxiomOrInst = { or₁ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.or₁, or₂ := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.or₂ }

instance LO.System.FiniteContext.instHasAxiomOrElim {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomOrElim Γ

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} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.NegationEquiv Γ

Equations

• Γ.instNegationEquiv = { neg_equiv := fun (x : F) => LO.System.FiniteContext.of LO.System.neg_equiv }

instance LO.System.FiniteContext.instMinimal {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.Minimal Γ

Equations

• Γ.instMinimal = LO.System.Minimal.mk

def LO.System.FiniteContext.mdp' {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ Δ : List F} [LO.System.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (bΓ : Γ ⊢[𝓢] φ ➝ ψ) (bΔ : Δ ⊢[𝓢] φ) : (Γ ++ Δ) ⊢[𝓢] ψ

Equations

• LO.System.FiniteContext.mdp' bΓ bΔ = LO.System.wk ⋯ bΓ⨀LO.System.wk ⋯ bΔ

def LO.System.FiniteContext.deduct {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ ψ : F} {Γ : List F} : (φ :: Γ) ⊢[𝓢] ψ → Γ ⊢[𝓢] φ ➝ ψ

Equations

• One or more equations did not get rendered due to their size.
• LO.System.FiniteContext.deduct = fun (b : [φ] ⊢[𝓢] ψ) => LO.System.FiniteContext.ofDef (LO.System.imply₁' (LO.System.FiniteContext.toDef b))

theorem LO.System.FiniteContext.deduct! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ ψ : F} (h : (φ :: Γ) ⊢[𝓢]! ψ) : Γ ⊢[𝓢]! φ ➝ ψ

def LO.System.FiniteContext.deductInv {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ ψ : F} {Γ : List F} : Γ ⊢[𝓢] φ ➝ ψ → (φ :: Γ) ⊢[𝓢] ψ

Equations

• One or more equations did not get rendered due to their size.
• LO.System.FiniteContext.deductInv = fun (b : [] ⊢[𝓢] φ ➝ ψ) => LO.System.FiniteContext.ofDef (LO.System.FiniteContext.toDef b⨀LO.System.verum)

theorem LO.System.FiniteContext.deductInv! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] {Γ : List F} [LO.System.Minimal 𝓢] {φ ψ : F} (h : Γ ⊢[𝓢]! φ ➝ ψ) : (φ :: Γ) ⊢[𝓢]! ψ

theorem LO.System.FiniteContext.deduct_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ ψ : F} {Γ : List F} : Γ ⊢[𝓢]! φ ➝ ψ ↔ (φ :: Γ) ⊢[𝓢]! ψ

def LO.System.FiniteContext.deduct' {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ ψ : F} : [φ] ⊢[𝓢] ψ → 𝓢 ⊢ φ ➝ ψ

Equations

• LO.System.FiniteContext.deduct' b = LO.System.FiniteContext.emptyPrf (LO.System.FiniteContext.deduct b)

theorem LO.System.FiniteContext.deduct'! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ ψ : F} (h : [φ] ⊢[𝓢]! ψ) : 𝓢 ⊢! φ ➝ ψ

def LO.System.FiniteContext.deductInv' {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ➝ ψ → [φ] ⊢[𝓢] ψ

Equations

• LO.System.FiniteContext.deductInv' b = LO.System.FiniteContext.deductInv (LO.System.FiniteContext.of b)

theorem LO.System.FiniteContext.deductInv'! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢! φ ➝ ψ) : [φ] ⊢[𝓢]! ψ

instance LO.System.FiniteContext.deduction {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] : LO.System.Deduction (LO.System.FiniteContext F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

instance LO.System.FiniteContext.instStrongCutOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] [DecidableEq F] : LO.System.StrongCut (LO.System.FiniteContext F 𝓢) (LO.System.FiniteContext F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

instance LO.System.FiniteContext.instHasAxiomEFQ {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] [LO.System.HasAxiomEFQ 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomEFQ Γ

Equations

• Γ.instHasAxiomEFQ = { efq := fun (x : F) => LO.System.FiniteContext.of LO.System.efq }

instance LO.System.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] [LO.System.HasAxiomEFQ 𝓢] : LO.System.DeductiveExplosion (LO.System.FiniteContext F 𝓢)

Equations

• LO.System.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ = inferInstance

instance LO.System.FiniteContext.instIntuitionistic {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] [LO.System.Intuitionistic 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.Intuitionistic Γ

Equations

• Γ.instIntuitionistic = LO.System.Intuitionistic.mk

instance LO.System.FiniteContext.instHasAxiomDNE {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] [LO.System.HasAxiomDNE 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.HasAxiomDNE Γ

Equations

• Γ.instHasAxiomDNE = { dne := fun (φ : F) => LO.System.FiniteContext.of (LO.System.HasAxiomDNE.dne φ) }

instance LO.System.FiniteContext.instClassical {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.System F S] [LO.LogicalConnective F] [LO.System.Minimal 𝓢] [LO.System.Classical 𝓢] (Γ : LO.System.FiniteContext F 𝓢) : LO.System.Classical Γ

Equations

• Γ.instClassical = LO.System.Classical.mk

structure LO.System.Context (F : Type u_1) {S : Type u_2} (𝓢 : S) : Type u_1

• ctx : Set F

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.instEmptyCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} : EmptyCollection (LO.System.Context F 𝓢)

Equations

• LO.System.Context.instEmptyCollection = { emptyCollection := { ctx := ∅ } }

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 (Γ : LO.System.Context F 𝓢) (x : F) => x ∈ Γ.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 (x1 x2 : LO.System.Context F 𝓢) => x1.ctx ⊆ x2.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 (x1 : F) (x2 : LO.System.Context F 𝓢) => { ctx := insert x1 x2.ctx } }

theorem LO.System.Context.mem_def {F : Type u_1} {S : Type u_2} {𝓢 : S} {φ : F} {Γ : LO.System.Context F 𝓢} : φ ∈ Γ ↔ φ ∈ Γ.ctx

@[simp]

theorem LO.System.Context.coe_subset_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {Γ Δ : Set F} : { ctx := Γ } ⊆ { ctx := Δ } ↔ Γ ⊆ Δ

@[simp]

theorem LO.System.Context.mem_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {φ : F} {Γ : Set F} : φ ∈ { ctx := Γ } ↔ φ ∈ Γ

@[simp]

theorem LO.System.Context.not_mem_empty {F : Type u_1} {S : Type u_2} {𝓢 : S} (φ : F) : φ ∉ ∅

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} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] (Γ : LO.System.Context F 𝓢) (φ : F) : Type (max u_1 u_3)

• ctx : List F
• subset : ∀ ψ ∈ self.ctx, ψ ∈ Γ
• prf : self.ctx ⊢[𝓢] φ

instance LO.System.Context.inst {F : Type u_1} {S : Type u_2} [LO.LogicalConnective F] [LO.System F S] (𝓢 : S) : LO.System F (LO.System.Context F 𝓢)

Equations

• LO.System.Context.inst 𝓢 = { Prf := LO.System.Context.Proof }

@[reducible, inline]

abbrev LO.System.Context.Prf {F : Type u_1} {S : Type u_2} (𝓢 : S) [LO.LogicalConnective F] [LO.System F S] (Γ : Set F) (φ : F) : Type (max u_1 u_3)

Equations

• (Γ *⊢[𝓢] φ) = ({ ctx := Γ } ⊢ φ)

@[reducible, inline]

abbrev LO.System.Context.Provable {F : Type u_1} {S : Type u_2} (𝓢 : S) [LO.LogicalConnective F] [LO.System F S] (Γ : Set F) (φ : F) : Prop

Equations

• (Γ *⊢[𝓢]! φ) = ({ ctx := Γ } ⊢! φ)

@[reducible, inline]

abbrev LO.System.Context.Unprovable {F : Type u_1} {S : Type u_2} (𝓢 : S) [LO.LogicalConnective F] [LO.System F S] (Γ : Set F) (φ : F) : Prop

Equations

• (Γ *⊬[𝓢] φ) = ({ ctx := Γ } ⊬ φ)

@[reducible, inline]

abbrev LO.System.Context.PrfSet {F : Type u_1} {S : Type u_2} (𝓢 : S) [LO.LogicalConnective F] [LO.System F S] (Γ s : Set F) : Type (max u_1 u_3)

Equations

• (Γ *⊢[𝓢]* s) = ({ ctx := Γ } ⊢* s)

@[reducible, inline]

abbrev LO.System.Context.ProvableSet {F : Type u_1} {S : Type u_2} (𝓢 : S) [LO.LogicalConnective F] [LO.System F S] (Γ s : Set F) : Prop

Equations

• (Γ *⊢[𝓢]*! s) = ({ ctx := Γ } ⊢!* s)

def LO.System.Context.«term_*⊢[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.System.Context.«term_*⊢[_]!_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.System.Context.«term_*⊬[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.System.Context.«term_*⊢[_]*_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.System.Context.«term_*⊢[_]*!_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem LO.System.Context.provable_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] {Γ : Set F} {φ : F} : Γ *⊢[𝓢]! φ ↔ ∃ (Δ : List F), (∀ ψ ∈ Δ, ψ ∈ Γ) ∧ Δ ⊢[𝓢]! φ

instance LO.System.Context.instAxiomatizedOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] [DecidableEq F] : LO.System.Axiomatized (LO.System.Context F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

instance LO.System.Context.instCompact {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] : LO.System.Compact (LO.System.Context F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

def LO.System.Context.deduct {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] [DecidableEq F] {φ ψ : F} {Γ : Set F} : insert φ Γ *⊢[𝓢] ψ → Γ *⊢[𝓢] φ ➝ ψ

Equations

• One or more equations did not get rendered due to their size.

def LO.System.Context.deductInv {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] {φ ψ : F} {Γ : Set F} : Γ *⊢[𝓢] φ ➝ ψ → insert φ Γ *⊢[𝓢] ψ

Equations

• LO.System.Context.deductInv { ctx := Δ, subset := h, prf := b } = { ctx := φ :: Δ, subset := ⋯, prf := LO.System.FiniteContext.deductInv b }

instance LO.System.Context.deduction {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] [DecidableEq F] : LO.System.Deduction (LO.System.Context F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

def LO.System.Context.of {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] {Γ : Set F} {φ : F} (b : 𝓢 ⊢ φ) : Γ *⊢[𝓢] φ

Equations

• LO.System.Context.of b = { ctx := [], subset := ⋯, prf := LO.System.FiniteContext.of b }

theorem LO.System.Context.of! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] {φ : F} {Γ : Set F} (b : 𝓢 ⊢! φ) : Γ *⊢[𝓢]! φ

def LO.System.Context.mdp {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] {φ ψ : F} [DecidableEq F] {Γ : Set F} (bpq : Γ *⊢[𝓢] φ ➝ ψ) (bp : Γ *⊢[𝓢] φ) : Γ *⊢[𝓢] ψ

Equations

• LO.System.Context.mdp bpq bp = { ctx := bpq.ctx ++ bp.ctx, subset := ⋯, prf := LO.System.FiniteContext.mdp' bpq.prf bp.prf }

theorem LO.System.Context.by_axm! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] {Γ : Set F} {φ : F} [DecidableEq F] (h : φ ∈ Γ) : Γ *⊢[𝓢]! φ

def LO.System.Context.emptyPrf {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] {φ : F} : ∅ *⊢[𝓢] φ → 𝓢 ⊢ φ

Equations

• One or more equations did not get rendered due to their size.

theorem LO.System.Context.emptyPrf! {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] {φ : F} : ∅ *⊢[𝓢]! φ → 𝓢 ⊢! φ

theorem LO.System.Context.provable_iff_provable {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] {φ : F} : 𝓢 ⊢! φ ↔ ∅ *⊢[𝓢]! φ

instance LO.System.Context.minimal {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] [DecidableEq F] (Γ : LO.System.Context F 𝓢) : LO.System.Minimal Γ

Equations

• Γ.minimal = LO.System.Minimal.mk

instance LO.System.Context.instHasAxiomEFQ {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] [LO.System.HasAxiomEFQ 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.HasAxiomEFQ Γ

Equations

• Γ.instHasAxiomEFQ = { efq := fun (x : F) => LO.System.Context.of LO.System.efq }

instance LO.System.Context.instHasAxiomDNE {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] [LO.System.HasAxiomDNE 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.HasAxiomDNE Γ

Equations

• Γ.instHasAxiomDNE = { dne := fun (φ : F) => LO.System.Context.of (LO.System.HasAxiomDNE.dne φ) }

instance LO.System.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [LO.System.Minimal 𝓢] [LO.System.HasAxiomEFQ 𝓢] : LO.System.DeductiveExplosion (LO.System.FiniteContext F 𝓢)

Equations

• LO.System.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ = inferInstance

instance LO.System.Context.instIntuitionisticOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [DecidableEq F] [LO.System.Intuitionistic 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.Intuitionistic Γ

Equations

• Γ.instIntuitionisticOfDecidableEq = LO.System.Intuitionistic.mk

instance LO.System.Context.instClassicalOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [LO.LogicalConnective F] [LO.System F S] [DecidableEq F] [LO.System.Classical 𝓢] (Γ : LO.System.Context F 𝓢) : LO.System.Classical Γ

Equations

• Γ.instClassicalOfDecidableEq = LO.System.Classical.mk