Documentation

Logic.IntProp.Deduction

structure LO.IntProp.Hilbert (α : Type u_1) :

Type u_1

axiomSet : LO.IntProp.Theory α

Instances For

LO.IntProp.instSystemFormulaHilbert

def LO.IntProp.«termAx(_)» :

Lean.ParserDescr

Equations

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

class LO.IntProp.Hilbert.IncludeEFQ {α : Type u} (Λ : LO.IntProp.Hilbert α) :

include_EFQ : 𝗘𝗙𝗤 ⊆ Ax(Λ)

Instances

theorem LO.IntProp.Hilbert.IncludeEFQ.include_EFQ {α : Type u} {Λ : LO.IntProp.Hilbert α} [self : Λ.IncludeEFQ] :

𝗘𝗙𝗤 ⊆ Ax(Λ)

class LO.IntProp.Hilbert.IncludeLEM {α : Type u} (Λ : LO.IntProp.Hilbert α) :

include_LEM : 𝗟𝗘𝗠 ⊆ Ax(Λ)

Instances

LO.IntProp.Hilbert.instIncludeLEMClassical

theorem LO.IntProp.Hilbert.IncludeLEM.include_LEM {α : Type u} {Λ : LO.IntProp.Hilbert α} [self : Λ.IncludeLEM] :

𝗟𝗘𝗠 ⊆ Ax(Λ)

class LO.IntProp.Hilbert.IncludeDNE {α : Type u} (Λ : LO.IntProp.Hilbert α) :

include_DNE : 𝗗𝗡𝗘 ⊆ Ax(Λ)

Instances

theorem LO.IntProp.Hilbert.IncludeDNE.include_DNE {α : Type u} {Λ : LO.IntProp.Hilbert α} [self : Λ.IncludeDNE] :

𝗗𝗡𝗘 ⊆ Ax(Λ)

inductive LO.IntProp.Deduction {α : Type u} (Λ : LO.IntProp.Hilbert α) :

LO.IntProp.Formula α → Type u

eaxm: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → {p : LO.IntProp.Formula α} → p ∈ Ax(Λ) → LO.IntProp.Deduction Λ p
mdp: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → {p q : LO.IntProp.Formula α} → LO.IntProp.Deduction Λ (p ➝ q) → LO.IntProp.Deduction Λ p → LO.IntProp.Deduction Λ q
verum: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → LO.IntProp.Deduction Λ ⊤
imply₁: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → (p q : LO.IntProp.Formula α) → LO.IntProp.Deduction Λ (p ➝ q ➝ p)
imply₂: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → (p q r : LO.IntProp.Formula α) → LO.IntProp.Deduction Λ ((p ➝ q ➝ r) ➝ (p ➝ q) ➝ p ➝ r)
and₁: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → (p q : LO.IntProp.Formula α) → LO.IntProp.Deduction Λ (p ⋏ q ➝ p)
and₂: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → (p q : LO.IntProp.Formula α) → LO.IntProp.Deduction Λ (p ⋏ q ➝ q)
and₃: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → (p q : LO.IntProp.Formula α) → LO.IntProp.Deduction Λ (p ➝ q ➝ p ⋏ q)
or₁: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → (p q : LO.IntProp.Formula α) → LO.IntProp.Deduction Λ (p ➝ p ⋎ q)
or₂: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → (p q : LO.IntProp.Formula α) → LO.IntProp.Deduction Λ (q ➝ p ⋎ q)
or₃: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → (p q r : LO.IntProp.Formula α) → LO.IntProp.Deduction Λ ((p ➝ r) ➝ (q ➝ r) ➝ p ⋎ q ➝ r)
neg_equiv: {α : Type u} → {Λ : LO.IntProp.Hilbert α} → (p : LO.IntProp.Formula α) → LO.IntProp.Deduction Λ (LO.Axioms.NegEquiv p)

instance LO.IntProp.instSystemFormulaHilbert {α : Type u} :

LO.System (LO.IntProp.Formula α) (LO.IntProp.Hilbert α)

Equations

LO.IntProp.instSystemFormulaHilbert = { Prf := LO.IntProp.Deduction }

instance LO.IntProp.instMinimalHilbertFormula {α : Type u} {Λ : LO.IntProp.Hilbert α} :

LO.System.Minimal Λ

Equations

LO.IntProp.instMinimalHilbertFormula = LO.System.Minimal.mk

instance LO.IntProp.instHasAxiomEFQHilbertFormulaOfIncludeEFQ {α : Type u} {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] :

LO.System.HasAxiomEFQ Λ

Equations

LO.IntProp.instHasAxiomEFQHilbertFormulaOfIncludeEFQ = { efq := fun (x : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }

instance LO.IntProp.instHasAxiomLEMHilbertFormulaOfIncludeLEM {α : Type u} {Λ : LO.IntProp.Hilbert α} [Λ.IncludeLEM] :

LO.System.HasAxiomLEM Λ

Equations

LO.IntProp.instHasAxiomLEMHilbertFormulaOfIncludeLEM = { lem := fun (x : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }

instance LO.IntProp.instHasAxiomDNEHilbertFormulaOfIncludeDNE {α : Type u} {Λ : LO.IntProp.Hilbert α} [Λ.IncludeDNE] :

LO.System.HasAxiomDNE Λ

Equations

LO.IntProp.instHasAxiomDNEHilbertFormulaOfIncludeDNE = { dne := fun (x : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }

instance LO.IntProp.instIntuitionisticHilbertFormulaOfIncludeEFQ {α : Type u} {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] :

LO.System.Intuitionistic Λ

Equations

LO.IntProp.instIntuitionisticHilbertFormulaOfIncludeEFQ = LO.System.Intuitionistic.mk

instance LO.IntProp.instClassicalHilbertFormulaOfIncludeDNE {α : Type u} {Λ : LO.IntProp.Hilbert α} [Λ.IncludeDNE] :

LO.System.Classical Λ

Equations

LO.IntProp.instClassicalHilbertFormulaOfIncludeDNE = LO.System.Classical.mk

instance LO.IntProp.instClassicalHilbertFormulaOfIncludeEFQOfIncludeLEM {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Λ.IncludeLEM] :

LO.System.Classical Λ

Equations

LO.IntProp.instClassicalHilbertFormulaOfIncludeEFQOfIncludeLEM = LO.System.Classical.mk

theorem LO.IntProp.Deduction.eaxm! {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} (h : p ∈ Ax(Λ)) :

Λ ⊢! p

@[reducible, inline]

abbrev LO.IntProp.Hilbert.theorems {α : Type u} (Λ : LO.IntProp.Hilbert α) :

Set (LO.IntProp.Formula α)

Equations

Λ.theorems = LO.System.theory Λ

@[reducible, inline]

abbrev LO.IntProp.Hilbert.Minimal {α : Type u} :

LO.IntProp.Hilbert α

Equations

LO.IntProp.Hilbert.Minimal = { axiomSet := ∅ }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.Intuitionistic {α : Type u} :

LO.IntProp.Hilbert α

Equations

𝐈𝐧𝐭 = { axiomSet := 𝗘𝗙𝗤 }

Instances For

def LO.IntProp.Hilbert.«term𝐈𝐧𝐭» :

Lean.ParserDescr

Equations

LO.IntProp.Hilbert.«term𝐈𝐧𝐭» = Lean.ParserDescr.node `LO.IntProp.Hilbert.term𝐈𝐧𝐭 1024 (Lean.ParserDescr.symbol "𝐈𝐧𝐭")

instance LO.IntProp.Hilbert.instIncludeEFQIntuitionistic {α : Type u} :

𝐈𝐧𝐭.IncludeEFQ

Equations

LO.IntProp.Hilbert.instIncludeEFQIntuitionistic = { include_EFQ := ⋯ }

instance LO.IntProp.Hilbert.instIntuitionisticFormulaIntuitionistic {α : Type u} :

LO.System.Intuitionistic 𝐈𝐧𝐭

Equations

LO.IntProp.Hilbert.instIntuitionisticFormulaIntuitionistic = LO.System.Intuitionistic.mk

@[reducible, inline]

abbrev LO.IntProp.Hilbert.Classical {α : Type u} :

LO.IntProp.Hilbert α

Equations

𝐂𝐥 = { axiomSet := 𝗘𝗙𝗤 ∪ 𝗟𝗘𝗠 }

Instances For

def LO.IntProp.Hilbert.«term𝐂𝐥» :

Lean.ParserDescr

Equations

LO.IntProp.Hilbert.«term𝐂𝐥» = Lean.ParserDescr.node `LO.IntProp.Hilbert.term𝐂𝐥 1024 (Lean.ParserDescr.symbol "𝐂𝐥")

instance LO.IntProp.Hilbert.instIncludeLEMClassical {α : Type u} :

𝐂𝐥.IncludeLEM

Equations

LO.IntProp.Hilbert.instIncludeLEMClassical = { include_LEM := ⋯ }

instance LO.IntProp.Hilbert.instIncludeEFQClassical {α : Type u} :

𝐂𝐥.IncludeEFQ

Equations

LO.IntProp.Hilbert.instIncludeEFQClassical = { include_EFQ := ⋯ }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.KC {α : Type u} :

LO.IntProp.Hilbert α

Equations

𝐊𝐂 = { axiomSet := 𝗘𝗙𝗤 ∪ 𝗪𝗟𝗘𝗠 }

Instances For

def LO.IntProp.Hilbert.«term𝐊𝐂» :

Lean.ParserDescr

Equations

LO.IntProp.Hilbert.«term𝐊𝐂» = Lean.ParserDescr.node `LO.IntProp.Hilbert.term𝐊𝐂 1024 (Lean.ParserDescr.symbol "𝐊𝐂")

instance LO.IntProp.Hilbert.instIncludeEFQKC {α : Type u} :

𝐊𝐂.IncludeEFQ

Equations

LO.IntProp.Hilbert.instIncludeEFQKC = { include_EFQ := ⋯ }

instance LO.IntProp.Hilbert.instHasAxiomWeakLEMFormulaKC {α : Type u} :

LO.System.HasAxiomWeakLEM 𝐊𝐂

Equations

LO.IntProp.Hilbert.instHasAxiomWeakLEMFormulaKC = { wlem := fun (p : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.LC {α : Type u} :

LO.IntProp.Hilbert α

Equations

𝐋𝐂 = { axiomSet := 𝗘𝗙𝗤 ∪ 𝗗𝘂𝗺 }

Instances For

def LO.IntProp.Hilbert.«term𝐋𝐂» :

Lean.ParserDescr

Equations

LO.IntProp.Hilbert.«term𝐋𝐂» = Lean.ParserDescr.node `LO.IntProp.Hilbert.term𝐋𝐂 1024 (Lean.ParserDescr.symbol "𝐋𝐂")

instance LO.IntProp.Hilbert.instIncludeEFQLC {α : Type u} :

𝐋𝐂.IncludeEFQ

Equations

LO.IntProp.Hilbert.instIncludeEFQLC = { include_EFQ := ⋯ }

instance LO.IntProp.Hilbert.instHasAxiomDummettFormulaLC {α : Type u} :

LO.System.HasAxiomDummett 𝐋𝐂

Equations

LO.IntProp.Hilbert.instHasAxiomDummettFormulaLC = { dummett := fun (p q : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.WeakMinimal {α : Type u} :

LO.IntProp.Hilbert α

Equations

LO.IntProp.Hilbert.WeakMinimal = { axiomSet := 𝗟𝗘𝗠 }

@[reducible, inline]

abbrev LO.IntProp.Hilbert.WeakClassical {α : Type u} :

LO.IntProp.Hilbert α

Equations

LO.IntProp.Hilbert.WeakClassical = { axiomSet := 𝗣𝗲 }

noncomputable def LO.IntProp.Deduction.rec! {α : Type u} {Λ : LO.IntProp.Hilbert α} {motive : (a : LO.IntProp.Formula α) → Λ ⊢! a → Sort u_1} (eaxm : {p : LO.IntProp.Formula α} → (a : p ∈ Ax(Λ)) → motive p ⋯) (mdp : {p q : LO.IntProp.Formula α} → {hpq : Λ ⊢! p ➝ q} → {hp : Λ ⊢! p} → motive (p ➝ q) hpq → motive p hp → motive q ⋯) (verum : motive ⊤ ⋯) (imply₁ : {p q : LO.IntProp.Formula α} → motive (p ➝ q ➝ p) ⋯) (imply₂ : {p q r : LO.IntProp.Formula α} → motive ((p ➝ q ➝ r) ➝ (p ➝ q) ➝ p ➝ r) ⋯) (and₁ : {p q : LO.IntProp.Formula α} → motive (p ⋏ q ➝ p) ⋯) (and₂ : {p q : LO.IntProp.Formula α} → motive (p ⋏ q ➝ q) ⋯) (and₃ : {p q : LO.IntProp.Formula α} → motive (p ➝ q ➝ p ⋏ q) ⋯) (or₁ : {p q : LO.IntProp.Formula α} → motive (p ➝ p ⋎ q) ⋯) (or₂ : {p q : LO.IntProp.Formula α} → motive (q ➝ p ⋎ q) ⋯) (or₃ : {p q r : LO.IntProp.Formula α} → motive ((p ➝ r) ➝ (q ➝ r) ➝ p ⋎ q ➝ r) ⋯) (neg_equiv : {p : LO.IntProp.Formula α} → motive (LO.Axioms.NegEquiv p) ⋯) {a : LO.IntProp.Formula α} (t : Λ ⊢! a) :

motive a t

Equations

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

theorem LO.IntProp.weaker_than_of_subset_axiomset' {α : Type u} {Λ₁ : LO.IntProp.Hilbert α} {Λ₂ : LO.IntProp.Hilbert α} (hMaxm : ∀ {p : LO.IntProp.Formula α}, p ∈ Ax(Λ₁) → Λ₂ ⊢! p) :

Λ₁ ≤ₛ Λ₂

theorem LO.IntProp.weaker_than_of_subset_axiomset {α : Type u} {Λ₁ : LO.IntProp.Hilbert α} {Λ₂ : LO.IntProp.Hilbert α} (hSubset : autoParam (Ax(Λ₁) ⊆ Ax(Λ₂)) _auto✝) :

Λ₁ ≤ₛ Λ₂

theorem LO.IntProp.Int_weaker_than_Cl {α : Type u} :

𝐈𝐧𝐭 ≤ₛ 𝐂𝐥

theorem LO.IntProp.Int_weaker_than_KC {α : Type u} :

𝐈𝐧𝐭 ≤ₛ 𝐊𝐂

theorem LO.IntProp.Int_weaker_than_LC {α : Type u} :

𝐈𝐧𝐭 ≤ₛ 𝐋𝐂

theorem LO.IntProp.KC_weaker_than_Cl {α : Type u} :

𝐊𝐂 ≤ₛ 𝐂𝐥

theorem LO.IntProp.LC_weaker_than_Cl {α : Type u} [DecidableEq α] :

𝐋𝐂 ≤ₛ 𝐂𝐥

theorem LO.IntProp.iff_provable_dn_efq_dne_provable {α : Type u} [DecidableEq α] {p : LO.IntProp.Formula α} :

𝐈𝐧𝐭 ⊢! ∼∼p ↔ 𝐂𝐥 ⊢! p

theorem LO.IntProp.glivenko {α : Type u} [DecidableEq α] {p : LO.IntProp.Formula α} :

𝐈𝐧𝐭 ⊢! ∼∼p ↔ 𝐂𝐥 ⊢! p

Alias of LO.IntProp.iff_provable_dn_efq_dne_provable.

theorem LO.IntProp.iff_provable_neg_efq_provable_neg_efq {α : Type u} [DecidableEq α] {p : LO.IntProp.Formula α} :

𝐈𝐧𝐭 ⊢! ∼p ↔ 𝐂𝐥 ⊢! ∼p