@[reducible, inline]

abbrev Builder : Player

Equations

• Builder = Player.A

@[reducible, inline]

abbrev Prover : Player

Equations

• Prover = Player.B

The GL-proof game.

Builder-Prover game for constructive counter-models/proofs. Builder gets a rule application R and plays an applicable sequent Γ in order to construct a counter-model. Prover get a sequent Γ and plays rule applications R in order to construct a proof.

def Sequent.ruleApps (Γ : Sequent) : Finset RuleApp

The available rule applications for a sequent Γ.

Equations

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

def RuleApp.sequents (R : RuleApp) : Finset Sequent

The sequents possible after a rule application R.

Equations

• (RuleApp.top Δ a).sequents = ∅
• (RuleApp.ax Δ n a).sequents = ∅
• (RuleApp.and Δ φ ψ a).sequents = {Δ \ {φ&ψ} ∪ {φ}, Δ \ {φ&ψ} ∪ {ψ}}
• (RuleApp.or Δ φ ψ a).sequents = {Δ \ {φ v ψ} ∪ {φ, ψ}}
• (RuleApp.box Δ φ a).sequents = {(Δ \ {□φ}).D ∪ {φ}}

@[reducible, inline]

abbrev GamePos : Type

Note: the game stores the history of which rule applications have come prior.

Equations

• GamePos = ((Sequent ⊕ RuleApp) × List Sequent × List RuleApp)

inductive Move : GamePos → GamePos → Prop

• prover {R : RuleApp} {Rs : List RuleApp} {Γ : Sequent} {Γs : List Sequent} : R ∈ Γ.ruleApps → Move (Sum.inl Γ, Γs, Rs) (Sum.inr R, Γ :: Γs, Rs)
• builder {R : RuleApp} {Rs : List RuleApp} {Γ : Sequent} {Γs : List Sequent} : Γ ∈ R.sequents → Γ ∉ Γs → Move (Sum.inr R, Γs, Rs) (Sum.inl Γ, Γs, R :: Rs)

theorem move_move_in_FL {g1 g2 : GamePos} (h1 : g1.1.isLeft = true) (h3 : g2.1.isLeft = true) (g1_g2 : Relation.ReflTransGen (Relation.Comp Move Move) g1 g2) : g2.1.getLeft h3 ∈ Finset.powerset (g1.1.getLeft h1).FL

Given two consecutive Prover moves, the latter move is in the FL closure of the prior.

theorem no_inf_chain_from_prover (g : ℕ → GamePos) (g_rel : ∀ (n : ℕ), Function.swap Move (g (n + 1)) (g n)) (h : (g 0).1.isLeft = true) : False

theorem matches_finite : WellFounded (Function.swap Move)

The game is converse well-founded.

def coalgebraGame : Game

Equations

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

theorem move_iff_in_moves {g g' : Game.Pos} : Move g g' ↔ g' ∈ Game.moves g

Move relation and being in the set of game moves are equivalant.

@[reducible, inline]

abbrev startPos (Γ : Sequent) : GamePos

We will always start the game from a sequent Γ and no history.

Equations

• startPos Γ = (Sum.inl Γ, [], [])