A Toy Model of Dialectica Interpretation for Intuitionistic Propositional Logic

References: https://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/

inductive LO.IntProp.Dialectica.Player : Type

• w : Player
• c : Player

@[reducible, inline]

abbrev LO.IntProp.Dialectica.Argument {α : Type u_1} : Player → Formula α → Type

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 φ

@[reducible, inline]

abbrev LO.IntProp.Dialectica.Witness {α : Type u_1} (φ : Formula α) : Type

Equations

• LO.IntProp.Dialectica.Witness φ = LO.IntProp.Dialectica.Argument LO.IntProp.Dialectica.Player.w φ

@[reducible, inline]

abbrev LO.IntProp.Dialectica.Counter {α : Type u_1} (φ : Formula α) : Type

Equations

• LO.IntProp.Dialectica.Counter φ = LO.IntProp.Dialectica.Argument LO.IntProp.Dialectica.Player.c φ

def LO.IntProp.Dialectica.Interpret {α : Type u_1} (V : α → Prop) (φ : Formula α) : Witness φ → Counter φ → Prop

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 θ) π)

def LO.IntProp.Dialectica.«term⟦_|_⟧⊩[_]_» : Lean.ParserDescr

Equations

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

def LO.IntProp.Dialectica.Valid {α : Type u_1} (φ : Formula α) : Prop

Equations

• LO.IntProp.Dialectica.Valid φ = ∃ (w : LO.IntProp.Dialectica.Witness φ), ∀ (V : α → Prop) (c : LO.IntProp.Dialectica.Counter φ), LO.IntProp.Dialectica.Interpret V φ w c

def LO.IntProp.Dialectica.NotValid {α : Type u_1} (φ : Formula α) : Prop

Equations

• LO.IntProp.Dialectica.NotValid φ = ∀ (w : LO.IntProp.Dialectica.Witness φ), ∃ (V : α → Prop) (c : LO.IntProp.Dialectica.Counter φ), ¬LO.IntProp.Dialectica.Interpret V φ w c

def LO.IntProp.Dialectica.«term⊩_» : Lean.ParserDescr

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

def LO.IntProp.Dialectica.«term⊮_» : Lean.ParserDescr

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

theorem LO.IntProp.Dialectica.not_valid_iff_notValid {α : Type u_1} {φ : Formula α} : ¬Valid φ ↔ NotValid φ

@[simp]

theorem LO.IntProp.Dialectica.interpret_verum {α : Type u_1} {w : Witness ⊤} {c : Counter ⊤} {V : α → Prop} : Interpret V ⊤ w c

@[simp]

theorem LO.IntProp.Dialectica.interpret_falsum {α : Type u_1} {w : Witness ⊥} {c : Counter ⊥} {V : α → Prop} : ¬Interpret V ⊥ w c

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

@[simp]

theorem LO.IntProp.Dialectica.interpret_and_left {α : Type u_1} {φ ψ : Formula α} {V : α → Prop} {θ : Witness (φ ⋏ ψ)} {π : Argument Player.c φ} : Interpret V (φ ⋏ ψ) θ (Sum.inl π) ↔ Interpret V φ θ.1 π

@[simp]

theorem LO.IntProp.Dialectica.interpret_and_right {α : Type u_1} {φ ψ : Formula α} {V : α → Prop} {θ : Witness (φ ⋏ ψ)} {π : Argument Player.c ψ} : Interpret V (φ ⋏ ψ) θ (Sum.inr π) ↔ Interpret V ψ θ.2 π

@[simp]

theorem LO.IntProp.Dialectica.interpret_or_left {α : Type u_1} {φ ψ : Formula α} {V : α → Prop} {θ : Argument Player.w φ} {π : Counter (φ ⋎ ψ)} : Interpret V (φ ⋎ ψ) (Sum.inl θ) π ↔ Interpret V φ θ π.1

@[simp]

theorem LO.IntProp.Dialectica.interpret_or_right {α : Type u_1} {φ ψ : Formula α} {V : α → Prop} {θ : Argument Player.w ψ} {π : Counter (φ ⋎ ψ)} : Interpret V (φ ⋎ ψ) (Sum.inr θ) π ↔ Interpret V ψ θ π.2

@[simp]

theorem LO.IntProp.Dialectica.interpret_not {α : Type u_1} {φ : Formula α} {V : α → Prop} {θ : Counter (∼φ)} {f : Witness (∼φ)} : Interpret V (∼φ) f θ ↔ ¬Interpret V φ θ (f θ)

@[simp]

theorem LO.IntProp.Dialectica.interpret_imply {α : Type u_1} {φ ψ : Formula α} {V : α → Prop} {f : Witness (φ ➝ ψ)} {π : Counter (φ ➝ ψ)} : Interpret V (φ ➝ ψ) f π ↔ Interpret V φ π.1 (f.2 π.1 π.2) → Interpret V ψ (f.1 π.1) π.2

theorem LO.IntProp.Dialectica.Valid.refl {α : Type u_1} (φ : Formula α) : Valid (φ ➝ φ)

theorem LO.IntProp.Dialectica.NotValid.em {α : Type u_1} (a : α) : NotValid (Formula.atom a ⋎ ∼Formula.atom a)