A Toy Model of Dialectica Interpretation for Intuitionistic Propositional Logic #
References: https://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/ #
@[reducible, inline]
Equations
- One or more equations did not get rendered due to their size.
- LO.IntProp.Dialectica.Argument x✝ LO.IntProp.Formula.verum = Unit
- LO.IntProp.Dialectica.Argument x✝ LO.IntProp.Formula.falsum = Unit
- LO.IntProp.Dialectica.Argument LO.IntProp.Dialectica.Player.w (LO.IntProp.Formula.atom a) = Unit
- LO.IntProp.Dialectica.Argument LO.IntProp.Dialectica.Player.c (LO.IntProp.Formula.atom a) = Unit
- LO.IntProp.Dialectica.Argument LO.IntProp.Dialectica.Player.c φ.neg = LO.IntProp.Dialectica.Argument LO.IntProp.Dialectica.Player.w φ
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.IntProp.Dialectica.Interpret V LO.IntProp.Formula.verum PUnit.unit PUnit.unit = True
- LO.IntProp.Dialectica.Interpret V LO.IntProp.Formula.falsum PUnit.unit PUnit.unit = False
- LO.IntProp.Dialectica.Interpret V (LO.IntProp.Formula.atom a) PUnit.unit PUnit.unit = V a
- LO.IntProp.Dialectica.Interpret V (φ.and a) (θ₁, snd) (Sum.inl π₁) = LO.IntProp.Dialectica.Interpret V φ θ₁ π₁
- LO.IntProp.Dialectica.Interpret V (a.and ψ) (fst, θ₂) (Sum.inr π₂) = LO.IntProp.Dialectica.Interpret V ψ θ₂ π₂
- LO.IntProp.Dialectica.Interpret V (φ.or a) (Sum.inl θ₁) (π₁, snd) = LO.IntProp.Dialectica.Interpret V φ θ₁ π₁
- LO.IntProp.Dialectica.Interpret V (a.or ψ) (Sum.inr θ₂) (fst, π₂) = LO.IntProp.Dialectica.Interpret V ψ θ₂ π₂
- LO.IntProp.Dialectica.Interpret V φ.neg f θ = ¬LO.IntProp.Dialectica.Interpret V φ θ (f θ)
- LO.IntProp.Dialectica.Interpret V (φ.imp ψ) (f, g) (θ, π) = (LO.IntProp.Dialectica.Interpret V φ θ (g θ π) → LO.IntProp.Dialectica.Interpret V ψ (f θ) π)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LO.IntProp.Dialectica.Valid φ = ∃ (w : LO.IntProp.Dialectica.Witness φ), ∀ (V : α → Prop) (c : LO.IntProp.Dialectica.Counter φ), LO.IntProp.Dialectica.Interpret V φ w c
Instances For
Equations
- LO.IntProp.Dialectica.NotValid φ = ∀ (w : LO.IntProp.Dialectica.Witness φ), ∃ (V : α → Prop) (c : LO.IntProp.Dialectica.Counter φ), ¬LO.IntProp.Dialectica.Interpret V φ w c
Instances For
Equations
- LO.IntProp.Dialectica.«term⊩_» = Lean.ParserDescr.node `LO.IntProp.Dialectica.«term⊩_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊩ ") (Lean.ParserDescr.cat `term 0))
Instances For
Equations
- LO.IntProp.Dialectica.«term⊮_» = Lean.ParserDescr.node `LO.IntProp.Dialectica.«term⊮_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊮ ") (Lean.ParserDescr.cat `term 0))
Instances For
@[simp]
theorem
LO.IntProp.Dialectica.interpret_atom
{α : Type u_1}
{w c : PUnit.{1}}
{V : α → Prop}
{a : α}
:
Interpret V (Formula.atom a) w c ↔ V a
theorem
LO.IntProp.Dialectica.NotValid.em
{α : Type u_1}
(a : α)
:
NotValid (Formula.atom a ⋎ ∼Formula.atom a)