- axiomSet : LO.IntProp.Theory α
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances
theorem
LO.IntProp.Hilbert.IncludeEFQ.include_EFQ
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
[self : Λ.IncludeEFQ]
:
Instances
theorem
LO.IntProp.Hilbert.IncludeLEM.include_LEM
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
[self : Λ.IncludeLEM]
:
Instances
theorem
LO.IntProp.Hilbert.IncludeDNE.include_DNE
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
[self : Λ.IncludeDNE]
:
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)
Instances For
Equations
- LO.IntProp.instSystemFormulaHilbert = { Prf := LO.IntProp.Deduction }
Equations
- LO.IntProp.instMinimalHilbertFormula = LO.System.Minimal.mk
instance
LO.IntProp.instHasAxiomEFQHilbertFormulaOfIncludeEFQ
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
[Λ.IncludeEFQ]
:
Equations
- LO.IntProp.instHasAxiomEFQHilbertFormulaOfIncludeEFQ = { efq := fun (x : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }
instance
LO.IntProp.instHasAxiomLEMHilbertFormulaOfIncludeLEM
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
[Λ.IncludeLEM]
:
Equations
- LO.IntProp.instHasAxiomLEMHilbertFormulaOfIncludeLEM = { lem := fun (x : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }
instance
LO.IntProp.instHasAxiomDNEHilbertFormulaOfIncludeDNE
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
[Λ.IncludeDNE]
:
Equations
- LO.IntProp.instHasAxiomDNEHilbertFormulaOfIncludeDNE = { dne := fun (x : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }
instance
LO.IntProp.instIntuitionisticHilbertFormulaOfIncludeEFQ
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
[Λ.IncludeEFQ]
:
Equations
- LO.IntProp.instIntuitionisticHilbertFormulaOfIncludeEFQ = LO.System.Intuitionistic.mk
instance
LO.IntProp.instClassicalHilbertFormulaOfIncludeDNE
{α : Type u}
{Λ : LO.IntProp.Hilbert α}
[Λ.IncludeDNE]
:
Equations
- LO.IntProp.instClassicalHilbertFormulaOfIncludeDNE = LO.System.Classical.mk
instance
LO.IntProp.instClassicalHilbertFormulaOfIncludeEFQOfIncludeLEM
{α : Type u}
[DecidableEq α]
{Λ : LO.IntProp.Hilbert α}
[Λ.IncludeEFQ]
[Λ.IncludeLEM]
:
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]
Equations
- Λ.theorems = LO.System.theory Λ
Instances For
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
Equations
- LO.IntProp.Hilbert.«term𝐈𝐧𝐭» = Lean.ParserDescr.node `LO.IntProp.Hilbert.term𝐈𝐧𝐭 1024 (Lean.ParserDescr.symbol "𝐈𝐧𝐭")
Instances For
Equations
- LO.IntProp.Hilbert.instIncludeEFQIntuitionistic = { include_EFQ := ⋯ }
Equations
- LO.IntProp.Hilbert.instIntuitionisticFormulaIntuitionistic = LO.System.Intuitionistic.mk
@[reducible, inline]
Instances For
Equations
- LO.IntProp.Hilbert.«term𝐂𝐥» = Lean.ParserDescr.node `LO.IntProp.Hilbert.term𝐂𝐥 1024 (Lean.ParserDescr.symbol "𝐂𝐥")
Instances For
Equations
- LO.IntProp.Hilbert.instIncludeLEMClassical = { include_LEM := ⋯ }
Equations
- LO.IntProp.Hilbert.instIncludeEFQClassical = { include_EFQ := ⋯ }
@[reducible, inline]
Instances For
Equations
- LO.IntProp.Hilbert.«term𝐊𝐂» = Lean.ParserDescr.node `LO.IntProp.Hilbert.term𝐊𝐂 1024 (Lean.ParserDescr.symbol "𝐊𝐂")
Instances For
Equations
- LO.IntProp.Hilbert.instIncludeEFQKC = { include_EFQ := ⋯ }
Equations
- LO.IntProp.Hilbert.instHasAxiomWeakLEMFormulaKC = { wlem := fun (p : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }
@[reducible, inline]
Instances For
Equations
- LO.IntProp.Hilbert.«term𝐋𝐂» = Lean.ParserDescr.node `LO.IntProp.Hilbert.term𝐋𝐂 1024 (Lean.ParserDescr.symbol "𝐋𝐂")
Instances For
Equations
- LO.IntProp.Hilbert.instIncludeEFQLC = { include_EFQ := ⋯ }
Equations
- LO.IntProp.Hilbert.instHasAxiomDummettFormulaLC = { dummett := fun (p q : LO.IntProp.Formula α) => LO.IntProp.Deduction.eaxm ⋯ }
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
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.
Instances For
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.iff_provable_dn_efq_dne_provable
{α : Type u}
[DecidableEq α]
{p : LO.IntProp.Formula α}
:
theorem
LO.IntProp.iff_provable_neg_efq_provable_neg_efq
{α : Type u}
[DecidableEq α]
{p : LO.IntProp.Formula α}
: