Documentation

Logic.Logic.HilbertStyle.Context

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

Type u_1

ctx : List F

Instances For

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

Equations

Γ.conj = ⋀Γ.ctx

@[reducible, inline]

abbrev LO.System.FiniteContext.disj {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} {𝓢 : S} (Γ : 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 (x : F) (x_1 : LO.System.FiniteContext F 𝓢) => x ∈ x_1.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 (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 𝓢} :

p ∈ Γ ↔ p ∈ Γ.ctx

@[simp]

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

{ ctx := Γ } ⊆ { ctx := Δ } ↔ Γ ⊆ Δ

@[simp]

theorem LO.System.FiniteContext.mem_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {p : F} {Γ : List F} :

p ∈ { ctx := Γ } ↔ p ∈ Γ

@[simp]

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

p ∉ ∅

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 }

@[reducible, inline]

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

Type u_3

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

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

(Γ ⊢ p) = (𝓢 ⊢ Γ.conj ➝ p)

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) :

Γ ⊢[𝓢] p

Equations

LO.System.FiniteContext.ofDef b = b

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) :

𝓢 ⊢ ⋀Γ ➝ p

Equations

LO.System.FiniteContext.toDef b = b

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

𝓢 ⊢! ⋀Γ ➝ p

theorem LO.System.FiniteContext.provable_iff {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} {Γ : List F} {p : F} :

Γ ⊢[𝓢]! p ↔ 𝓢 ⊢! ⋀Γ ➝ p

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 𝓢] :

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

LO.System.Compact (LO.System.FiniteContext F 𝓢)

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✝) :

Γ ⊢[𝓢] p

Equations

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

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✝) :

Γ ⊢[𝓢]! p

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} :

Γ ⊢[𝓢] p → Δ ⊢[𝓢] p

Equations

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

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} :

Γ ⊢[𝓢]! p → Δ ⊢[𝓢]! p

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) :

Γ ⊢[𝓢] p

Equations

LO.System.FiniteContext.of b = LO.System.dhyp (⋀Γ) b

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} :

[] ⊢[𝓢] p → 𝓢 ⊢ p

Equations

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

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} :

𝓢 ⊢! p ↔ [] ⊢[𝓢]! p

Equations

⋯ = ⋯

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) :

Γ ⊢[𝓢]! 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} :

[p] ⊢[𝓢] p

Equations

LO.System.FiniteContext.id = LO.System.FiniteContext.byAxm ⋯

@[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} :

[p] ⊢[𝓢]! p

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 𝓢) :

LO.System.ModusPonens Γ

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 𝓢) :

LO.System.HasAxiomVerum Γ

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 𝓢) :

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} [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 𝓢) :

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} [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 𝓢) :

LO.System.HasAxiomAndElim₁ Γ

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 𝓢) :

LO.System.HasAxiomAndElim₂ Γ

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 𝓢) :

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} [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 𝓢) :

LO.System.HasAxiomOrInst₁ Γ

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 𝓢) :

LO.System.HasAxiomOrInst₂ Γ

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 𝓢) :

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} [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 𝓢) :

LO.System.NegationEquiv Γ

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) :

(Γ ++ Δ) ⊢[𝓢] q

Equations

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

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} :

(p :: Γ) ⊢[𝓢] q → Γ ⊢[𝓢] p ➝ q

Equations

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

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) :

Γ ⊢[𝓢]! 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} :

Γ ⊢[𝓢] p ➝ q → (p :: Γ) ⊢[𝓢] q

Equations

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

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) :

(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} :

Γ ⊢[𝓢]! p ➝ q ↔ (p :: Γ) ⊢[𝓢]! q

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} :

[p] ⊢[𝓢] q → 𝓢 ⊢ p ➝ q

Equations

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

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) :

𝓢 ⊢! 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} :

𝓢 ⊢ p ➝ q → [p] ⊢[𝓢] q

Equations

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

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) :

[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 𝓢] :

LO.System.Deduction (LO.System.FiniteContext F 𝓢)

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 𝓢] :

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} [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 𝓢) :

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} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.ModusPonens 𝓢] [LO.System.HasAxiomImply₁ 𝓢] [LO.System.HasAxiomImply₂ 𝓢] [LO.System.HasAxiomEFQ 𝓢] :

LO.System.DeductiveExplosion (LO.System.FiniteContext F 𝓢)

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 𝓢) :

LO.System.HasAxiomDNE Γ

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 𝓢) :

LO.System.Minimal Γ

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 𝓢) :

LO.System.Intuitionistic Γ

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 𝓢) :

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

Instances For

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 (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 𝓢} :

p ∈ Γ ↔ p ∈ Γ.ctx

@[simp]

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

{ ctx := Γ } ⊆ { ctx := Δ } ↔ Γ ⊆ Δ

@[simp]

theorem LO.System.Context.mem_coe_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} {p : F} {Γ : Set F} :

p ∈ { ctx := Γ } ↔ p ∈ Γ

@[simp]

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

p ∉ ∅

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)

ctx : List F
subset : ∀ q ∈ self.ctx, q ∈ Γ
prf : self.ctx ⊢[𝓢] p

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) :

q ∈ self.ctx → q ∈ Γ

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 }

@[reducible, inline]

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

Type (max u_1 u_3)

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Type (max u_1 u_3)

Equations

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

@[reducible, inline]

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

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

Γ *⊢[𝓢]! p ↔ ∃ (Δ : List F), (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p

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 𝓢] :

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} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : 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} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] [DecidableEq F] {p : F} {q : F} {Γ : Set F} :

insert p Γ *⊢[𝓢] q → Γ *⊢[𝓢] p ➝ q

Equations

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

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} :

Γ *⊢[𝓢] p ➝ q → insert p Γ *⊢[𝓢] q

Equations

LO.System.Context.deductInv x = match x with | { ctx := Δ, subset := h, prf := b } => { ctx := p :: Δ, subset := ⋯, prf := LO.System.FiniteContext.deductInv b }

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 𝓢] :

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

Γ *⊢[𝓢] p

Equations

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

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) :

Γ *⊢[𝓢]! 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) :

Γ *⊢[𝓢] q

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} [LO.LogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Minimal 𝓢] {p : F} {Γ : Set F} (h : p ∈ Γ) :

Γ *⊢[𝓢]! 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} :

∅ *⊢[𝓢] p → 𝓢 ⊢ p

Equations

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

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} :

∅ *⊢[𝓢]! p → 𝓢 ⊢! p

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} :

𝓢 ⊢! p ↔ ∅ *⊢[𝓢]! p

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 𝓢) :

LO.System.Minimal Γ

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 𝓢) :

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

LO.System.HasAxiomDNE Γ

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 𝓢] :

LO.System.DeductiveExplosion (LO.System.FiniteContext F 𝓢)

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 𝓢) :

LO.System.Intuitionistic Γ

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 𝓢) :

LO.System.Classical Γ

Equations

Γ.instClassical = LO.System.Classical.mk