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

• ctx : List F

instance LO.Entailment.FiniteContext.instCoeList {F : Type u_1} {S : Type u_2} {𝓢 : S} : Coe (List F) (FiniteContext F 𝓢)

Equations

• LO.Entailment.FiniteContext.instCoeList = { coe := LO.Entailment.FiniteContext.mk }

@[reducible, inline]

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

Equations

• Γ.conj = ⋀Γ.ctx

@[reducible, inline]

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

Equations

• Γ.disj = ⋁Γ.ctx

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

Equations

• LO.Entailment.FiniteContext.instEmptyCollection = { emptyCollection := { ctx := [] } }

instance LO.Entailment.FiniteContext.instMembership {F : Type u_1} {S : Type u_2} {𝓢 : S} : Membership F (FiniteContext F 𝓢)

Equations

• LO.Entailment.FiniteContext.instMembership = { mem := fun (Γ : LO.Entailment.FiniteContext F 𝓢) (x : F) => x ∈ Γ.ctx }

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

Equations

• LO.Entailment.FiniteContext.instHasSubset = { Subset := fun (x1 x2 : LO.Entailment.FiniteContext F 𝓢) => x1.ctx ⊆ x2.ctx }

instance LO.Entailment.FiniteContext.instCons {F : Type u_1} {S : Type u_2} {𝓢 : S} : Cons F (FiniteContext F 𝓢)

Equations

• LO.Entailment.FiniteContext.instCons = { cons := fun (x1 : F) (x2 : LO.Entailment.FiniteContext F 𝓢) => { ctx := x1 :: x2.ctx } }

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

@[simp]

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

@[simp]

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

@[simp]

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

instance LO.Entailment.FiniteContext.instCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} : Collection F (FiniteContext F 𝓢)

Equations

• LO.Entailment.FiniteContext.instCollection = Collection.mk ⋯ ⋯ ⋯

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

• LO.Entailment.FiniteContext.ofDef b = b

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

Equations

• LO.Entailment.FiniteContext.toDef b = b

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

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

Equations

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

@[simp]

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Γ.instHasAxiomImply₂ = { imply₂ := fun (x x_1 x_2 : F) => LO.Entailment.FiniteContext.of LO.Entailment.imply₂ }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Γ.instHasAxiomOrElim = { or₃ := fun (x x_1 x_2 : F) => LO.Entailment.FiniteContext.of LO.Entailment.or₃ }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• LO.Entailment.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ = inferInstance

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

Equations

• Γ.instInt = LO.Entailment.Int.mk

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

Equations

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

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

Equations

• Γ.instCl = LO.Entailment.Cl.mk

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

• ctx : Set F

instance LO.Entailment.Context.instCoeSet {F : Type u_1} {S : Type u_2} {𝓢 : S} : Coe (Set F) (Context F 𝓢)

Equations

• LO.Entailment.Context.instCoeSet = { coe := LO.Entailment.Context.mk }

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

Equations

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

instance LO.Entailment.Context.instMembership {F : Type u_1} {S : Type u_2} {𝓢 : S} : Membership F (Context F 𝓢)

Equations

• LO.Entailment.Context.instMembership = { mem := fun (Γ : LO.Entailment.Context F 𝓢) (x : F) => x ∈ Γ.ctx }

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

Equations

• LO.Entailment.Context.instHasSubset = { Subset := fun (x1 x2 : LO.Entailment.Context F 𝓢) => x1.ctx ⊆ x2.ctx }

instance LO.Entailment.Context.instCons {F : Type u_1} {S : Type u_2} {𝓢 : S} : Cons F (Context F 𝓢)

Equations

• LO.Entailment.Context.instCons = { cons := fun (x1 : F) (x2 : LO.Entailment.Context F 𝓢) => { ctx := insert x1 x2.ctx } }

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

@[simp]

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

@[simp]

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

@[simp]

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

instance LO.Entailment.Context.instCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} : Collection F (Context F 𝓢)

Equations

• LO.Entailment.Context.instCollection = Collection.mk ⋯ ⋯ ⋯

structure LO.Entailment.Context.Proof {F : Type u_1} {S : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment F S] (Γ : Context F 𝓢) (φ : F) : Type (max u_1 u_3)

• ctx : List F
• subset (ψ : F) : ψ ∈ self.ctx → ψ ∈ Γ
• prf : self.ctx ⊢[𝓢] φ

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• LO.Entailment.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ = inferInstance

instance LO.Entailment.Context.instIntOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment F S] [DecidableEq F] [Entailment.Int 𝓢] (Γ : Context F 𝓢) : Entailment.Int Γ

Equations

• Γ.instIntOfDecidableEq = LO.Entailment.Int.mk

instance LO.Entailment.Context.instClOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment F S] [DecidableEq F] [Entailment.Cl 𝓢] (Γ : Context F 𝓢) : Entailment.Cl Γ

Equations

• Γ.instClOfDecidableEq = LO.Entailment.Cl.mk