Foundation.Logic.HilbertStyle.Context

source

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

Type u_1

ctx : List F

Instances For

source

instance LO.System.FiniteContext.instCoeList {F : Type u_1} {S : Type u_2} {𝓢 : S} :

Coe (List F) (FiniteContext F 𝓢)

Equations

LO.System.FiniteContext.instCoeList = { coe := LO.System.FiniteContext.mk }

source

@[reducible, inline]

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

Equations

Γ.conj = ⋀Γ.ctx

source

@[reducible, inline]

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

Equations

Γ.disj = ⋁Γ.ctx

source

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

EmptyCollection (FiniteContext F 𝓢)

Equations

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

source

instance LO.System.FiniteContext.instMembership {F : Type u_1} {S : Type u_2} {𝓢 : S} :

Membership F (FiniteContext F 𝓢)

Equations

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

source

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

HasSubset (FiniteContext F 𝓢)

Equations

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

source

instance LO.System.FiniteContext.instCons {F : Type u_1} {S : Type u_2} {𝓢 : S} :

Cons F (FiniteContext F 𝓢)

Equations

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

source

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

φ ∈ Γ ↔ φ ∈ Γ.ctx

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

φ ∉ ∅

source

instance LO.System.FiniteContext.instCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} :

Collection F (FiniteContext F 𝓢)

Equations

LO.System.FiniteContext.instCollection = Collection.mk ⋯ ⋯ ⋯

source

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

System F (FiniteContext F 𝓢)

Equations

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

source

@[reducible, inline]

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

Type u_3

Equations

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

source

@[reducible, inline]

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

Prop

Equations

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

source

@[reducible, inline]

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

Prop

Equations

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

source

@[reducible, inline]

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

Type (max u_3 u_1)

Equations

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

source

@[reducible, inline]

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

Prop

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

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

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

source

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

Γ ⊢[𝓢] φ

Equations

LO.System.FiniteContext.ofDef b = b

source

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

𝓢 ⊢ ⋀Γ ➝ φ

Equations

LO.System.FiniteContext.toDef b = b

source

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

𝓢 ⊢! ⋀Γ ➝ φ

source

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

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

source

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

Γ' ⊢[𝓢] φ'

Equations

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

source

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

Axiomatized (FiniteContext F 𝓢)

Equations

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

source

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

Compact (FiniteContext F 𝓢)

Equations

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

source

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

Γ ⊢[𝓢] Γ[n]

Equations

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

source

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

Γ ⊢[𝓢]! Γ[n]

source

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

Γ ⊢[𝓢] φ

Equations

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

source

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

Γ ⊢[𝓢]! φ

source

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

Γ ⊢[𝓢] φ → Δ ⊢[𝓢] φ

Equations

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

source

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

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

source

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

Γ ⊢[𝓢] φ

Equations

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

source

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

[] ⊢[𝓢] φ → 𝓢 ⊢ φ

Equations

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

source

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

𝓢 ⊢! φ ↔ [] ⊢[𝓢]! φ

Equations

⋯ = ⋯

source

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

Γ ⊢[𝓢]! φ

source

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

[φ] ⊢[𝓢] φ

Equations

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

source

@[simp]

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

[φ] ⊢[𝓢]! φ

source

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

(φ :: Γ) ⊢[𝓢] φ

Equations

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

source

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

(φ :: Γ) ⊢[𝓢]! φ

source

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

(φ :: ψ :: Γ) ⊢[𝓢] ψ

Equations

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

source

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

(φ :: ψ :: Γ) ⊢[𝓢]! ψ

source

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

(φ :: ψ :: χ :: Γ) ⊢[𝓢] χ

Equations

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

source

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

(φ :: ψ :: χ :: Γ) ⊢[𝓢]! χ

source

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

ModusPonens Γ

Equations

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

source

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

HasAxiomVerum Γ

Equations

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

source

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

HasAxiomImply₁ Γ

Equations

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

source

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

HasAxiomImply₂ Γ

Equations

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

source

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

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

source

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

HasAxiomAndInst Γ

Equations

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

source

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

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

source

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

HasAxiomOrElim Γ

Equations

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

source

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

NegationEquiv Γ

Equations

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

source

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

System.Minimal Γ

Equations

Γ.instMinimal = LO.System.Minimal.mk

source

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

(Γ ++ Δ) ⊢[𝓢] ψ

Equations

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

source

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

source

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

Γ ⊢[𝓢]! φ ➝ ψ

source

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

source

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

(φ :: Γ) ⊢[𝓢]! ψ

source

theorem LO.System.FiniteContext.deduct_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} [System F S] [LogicalConnective F] [System.Minimal 𝓢] {φ ψ : F} {Γ : List F} :

Γ ⊢[𝓢]! φ ➝ ψ ↔ (φ :: Γ) ⊢[𝓢]! ψ

source

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

[φ] ⊢[𝓢] ψ → 𝓢 ⊢ φ ➝ ψ

Equations

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

source

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

𝓢 ⊢! φ ➝ ψ

source

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

𝓢 ⊢ φ ➝ ψ → [φ] ⊢[𝓢] ψ

Equations

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

source

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

[φ] ⊢[𝓢]! ψ

source

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

Deduction (FiniteContext F 𝓢)

Equations

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

source

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

StrongCut (FiniteContext F 𝓢) (FiniteContext F 𝓢)

Equations

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

source

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

HasAxiomEFQ Γ

Equations

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

source

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

DeductiveExplosion (FiniteContext F 𝓢)

Equations

LO.System.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ = inferInstance

source

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

System.Intuitionistic Γ

Equations

Γ.instIntuitionistic = LO.System.Intuitionistic.mk

source

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

HasAxiomDNE Γ

Equations

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

source

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

System.Classical Γ

Equations

Γ.instClassical = LO.System.Classical.mk

source

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

Type u_1

ctx : Set F

Instances For

source

instance LO.System.Context.instCoeSet {F : Type u_1} {S : Type u_2} {𝓢 : S} :

Coe (Set F) (Context F 𝓢)

Equations

LO.System.Context.instCoeSet = { coe := LO.System.Context.mk }

source

instance LO.System.Context.instEmptyCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} :

EmptyCollection (Context F 𝓢)

Equations

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

source

instance LO.System.Context.instMembership {F : Type u_1} {S : Type u_2} {𝓢 : S} :

Membership F (Context F 𝓢)

Equations

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

source

instance LO.System.Context.instHasSubset {F : Type u_1} {S : Type u_2} {𝓢 : S} :

HasSubset (Context F 𝓢)

Equations

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

source

instance LO.System.Context.instCons {F : Type u_1} {S : Type u_2} {𝓢 : S} :

Cons F (Context F 𝓢)

Equations

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

source

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

φ ∈ Γ ↔ φ ∈ Γ.ctx

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

φ ∉ ∅

source

instance LO.System.Context.instCollection {F : Type u_1} {S : Type u_2} {𝓢 : S} :

Collection F (Context F 𝓢)

Equations

LO.System.Context.instCollection = Collection.mk ⋯ ⋯ ⋯

source

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

Type (max u_1 u_3)

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

source

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

System F (Context F 𝓢)

Equations

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

source

@[reducible, inline]

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

Type (max u_1 u_3)

Equations

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

source

@[reducible, inline]

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

Prop

Equations

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

source

@[reducible, inline]

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

Prop

Equations

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

source

@[reducible, inline]

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

Type (max u_1 u_3)

Equations

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

source

@[reducible, inline]

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

Prop

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

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

Lean.TrailingParserDescr

Equations

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

source

theorem LO.System.Context.provable_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} [LogicalConnective F] [System F S] {Γ : Set F} {φ : F} :

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

source

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

Axiomatized (Context F 𝓢)

Equations

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

source

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

Compact (Context F 𝓢)

Equations

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

source

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

insert φ Γ *⊢[𝓢] ψ → Γ *⊢[𝓢] φ ➝ ψ

Equations

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

source

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

Γ *⊢[𝓢] φ ➝ ψ → insert φ Γ *⊢[𝓢] ψ

Equations

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

source

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

Deduction (Context F 𝓢)

Equations

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

source

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

Γ *⊢[𝓢] φ

Equations

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

source

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

Γ *⊢[𝓢]! φ

source

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

source

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

Γ *⊢[𝓢]! φ

source

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

∅ *⊢[𝓢] φ → 𝓢 ⊢ φ

Equations

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

source

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

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

source

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

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

source

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

System.Minimal Γ

Equations

Γ.minimal = LO.System.Minimal.mk

source

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

HasAxiomEFQ Γ

Equations

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

source

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

HasAxiomDNE Γ

Equations

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

source

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

DeductiveExplosion (FiniteContext F 𝓢)

Equations

LO.System.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ = inferInstance

source

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

System.Intuitionistic Γ

Equations

Γ.instIntuitionisticOfDecidableEq = LO.System.Intuitionistic.mk

source

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

System.Classical Γ

Equations

Γ.instClassicalOfDecidableEq = LO.System.Classical.mk