Documentation

Foundation.IntProp.Dialectica.Basic

A Toy Model of Dialectica Interpretation for Intuitionistic Propositional Logic #

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

source
inductive LO.IntProp.Dialectica.Player :
Type
source
@[reducible, inline]
abbrev LO.IntProp.Dialectica.Argument {α : Type u_1} :
Player → Formula α → Type
Equations
source
@[reducible, inline]
abbrev LO.IntProp.Dialectica.Witness {α : Type u_1} (φ : Formula α) :
Type
Equations
source
@[reducible, inline]
abbrev LO.IntProp.Dialectica.Counter {α : Type u_1} (φ : Formula α) :
Type
Equations
source
def LO.IntProp.Dialectica.Interpret {α : Type u_1} (V : α → Prop) (φ : Formula α) :
Witness φ → Counter φ → Prop
Equations
source
def LO.IntProp.Dialectica.«term⟦_|_⟧⊩[_]_» :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.IntProp.Dialectica.Valid {α : Type u_1} (φ : Formula α) :
Prop
Equations
source
def LO.IntProp.Dialectica.NotValid {α : Type u_1} (φ : Formula α) :
Prop
Equations
source
def LO.IntProp.Dialectica.«term⊩_» :
Lean.ParserDescr
Equations
source
def LO.IntProp.Dialectica.«term⊮_» :
Lean.ParserDescr
Equations
source
theorem LO.IntProp.Dialectica.not_valid_iff_notValid {α : Type u_1} {φ : Formula α} :
¬Valid φ ↔ NotValid φ
source
@[simp]
theorem LO.IntProp.Dialectica.interpret_verum {α : Type u_1} {w : Witness ⊤} {c : Counter ⊤} {V : α → Prop} :
Interpret V ⊤ w c
source
@[simp]
theorem LO.IntProp.Dialectica.interpret_falsum {α : Type u_1} {w : Witness ⊥} {c : Counter ⊥} {V : α → Prop} :
¬Interpret V ⊥ w c
source
@[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
source
@[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 π
source
@[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 π
source
@[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
source
@[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
source
@[simp]
theorem LO.IntProp.Dialectica.interpret_not {α : Type u_1} {φ : Formula α} {V : α → Prop} {θ : Counter (∼φ)} {f : Witness (∼φ)} :
Interpret V (∼φ) f θ ↔ ¬Interpret V φ θ (f θ)
source
@[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
source
theorem LO.IntProp.Dialectica.Valid.refl {α : Type u_1} (φ : Formula α) :
Valid (φ ➝ φ)
source
theorem LO.IntProp.Dialectica.NotValid.em {α : Type u_1} (a : α) :
NotValid (Formula.atom a ⋎ ∼Formula.atom a)