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/ #

inductive LO.IntProp.Dialectica.Player :

Instances For

@[reducible, inline]

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

LO.IntProp.Dialectica.Player → LO.IntProp.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 φ

Instances For

@[reducible, inline]

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

Equations

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

Instances For

@[reducible, inline]

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

Equations

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

Instances For

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

LO.IntProp.Dialectica.Witness φ → LO.IntProp.Dialectica.Counter φ → Prop

Instances For

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

Lean.ParserDescr

Equations

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

Instances For

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

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

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

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

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

Instances For

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

Instances For

theorem LO.IntProp.Dialectica.not_valid_iff_notValid {α : Type u_1} {φ : LO.IntProp.Formula α} :

¬LO.IntProp.Dialectica.Valid φ ↔ LO.IntProp.Dialectica.NotValid φ

@[simp]

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

LO.IntProp.Dialectica.Interpret V ⊤ w c

@[simp]

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

¬LO.IntProp.Dialectica.Interpret V ⊥ w c

@[simp]

theorem LO.IntProp.Dialectica.interpret_atom {α : Type u_1} {w c : PUnit.{1}} {V : α → Prop} {a : α} :

LO.IntProp.Dialectica.Interpret V (LO.IntProp.Formula.atom a) w c ↔ V a

@[simp]

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

LO.IntProp.Dialectica.Interpret V (φ ⋏ ψ) θ (Sum.inl π) ↔ LO.IntProp.Dialectica.Interpret V φ θ.1 π

@[simp]

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

LO.IntProp.Dialectica.Interpret V (φ ⋏ ψ) θ (Sum.inr π) ↔ LO.IntProp.Dialectica.Interpret V ψ θ.2 π

@[simp]

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

LO.IntProp.Dialectica.Interpret V (φ ⋎ ψ) (Sum.inl θ) π ↔ LO.IntProp.Dialectica.Interpret V φ θ π.1

@[simp]

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

LO.IntProp.Dialectica.Interpret V (φ ⋎ ψ) (Sum.inr θ) π ↔ LO.IntProp.Dialectica.Interpret V ψ θ π.2

@[simp]

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

LO.IntProp.Dialectica.Interpret V (∼φ) f θ ↔ ¬LO.IntProp.Dialectica.Interpret V φ θ (f θ)

@[simp]

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

LO.IntProp.Dialectica.Interpret V (φ ➝ ψ) f π ↔ LO.IntProp.Dialectica.Interpret V φ π.1 (f.2 π.1 π.2) → LO.IntProp.Dialectica.Interpret V ψ (f.1 π.1) π.2

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

LO.IntProp.Dialectica.Valid (φ ➝ φ)

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

LO.IntProp.Dialectica.NotValid (LO.IntProp.Formula.atom a ⋎ ∼LO.IntProp.Formula.atom a)