structure Semantics.Dynamic.Core.PLAPoss (E : Type u_1) : Type u_1

PLA-style possibility: assignment + witness sequence (no world)

• assignment : ℕ → E
• witnesses : ℕ → E

def Semantics.Dynamic.Core.PLAInfoState (E : Type u_1) : Type u_1

PLA-style information state

Equations

• Semantics.Dynamic.Core.PLAInfoState E = Set (Semantics.Dynamic.Core.PLAPoss E)

def Semantics.Dynamic.Core.PLAPoss.toCore {E : Type u_1} (p : PLAPoss E) : Possibility Unit E

Embed PLA possibility into Core possibility.

Uses Unit world and combines assignment/witnesses into single assignment. Pronouns are offset by a large constant to avoid collision.

Equations

• p.toCore = { world := (), assignment := fun (n : ℕ) => if n < 1000 then p.assignment n else p.witnesses (n - 1000) }

def Semantics.Dynamic.Core.PLAInfoState.toCore {E : Type u_1} (s : PLAInfoState E) : InfoState Unit E

Lift PLA state to Core state

Equations

• s.toCore = Semantics.Dynamic.Core.PLAPoss.toCore '' s

def Semantics.Dynamic.Core.Possibility.toPLA {W : Type u_1} {E : Type u_2} (p : Possibility W E) : PLAPoss E

Project Core possibility to PLA possibility.

Discards world, splits assignment into variable/pronoun parts.

Equations

• p.toPLA = { assignment := fun (n : ℕ) => p.assignment n, witnesses := fun (n : ℕ) => p.assignment (n + 1000) }

def Semantics.Dynamic.Core.InfoState.toPLA {W : Type u_1} {E : Type u_2} (s : InfoState W E) : PLAInfoState E

Project Core state to PLA state

Equations

• s.toPLA = Semantics.Dynamic.Core.Possibility.toPLA '' s

theorem Semantics.Dynamic.Core.pla_core_pla_assignment {E : Type u_1} (p : PLAPoss E) (n : ℕ) (h : n < 1000) : p.toCore.toPLA.assignment n = p.assignment n

PLA → Core → PLA is identity on the relevant components

theorem Semantics.Dynamic.Core.pla_core_pla_witnesses {E : Type u_1} (p : PLAPoss E) (n : ℕ) : p.toCore.toPLA.witnesses n = p.witnesses n

PLA → Core → PLA preserves witnesses

theorem Semantics.Dynamic.Core.embedding_preserves_agreement {E : Type u_1} (p q : PLAPoss E) (hv : ∀ (n : ℕ), n < 1000 → p.assignment n = q.assignment n) (hw : ∀ (n : ℕ), p.witnesses n = q.witnesses n) (n : ℕ) : p.toCore.assignment n = q.toCore.assignment n

Embedding preservation: the translation preserves state structure.

If two PLA possibilities agree on all variables and witnesses, their Core translations agree on all assignments.

def Semantics.Dynamic.Core.PLACCP (E : Type u_1) : Type u_1

PLA-style CCP: no world dependency.

Equations

• Semantics.Dynamic.Core.PLACCP E = (Semantics.Dynamic.Core.PLAInfoState E → Semantics.Dynamic.Core.PLAInfoState E)

def Semantics.Dynamic.Core.PLACCP.toCoreCCP {E : Type u_1} (φ : PLACCP E) : CCP (Possibility Unit E)

Lift PLA CCP to Core CCP.

Equations

• φ.toCoreCCP s = (φ (Semantics.Dynamic.Core.InfoState.toPLA s)).toCore

def Semantics.Dynamic.Core.CCP.toPLACCP {E : Type u_1} (φ : CCP (Possibility Unit E)) : PLACCP E

Project Core CCP to PLA CCP (for Unit world).

Equations

• φ.toPLACCP s = Semantics.Dynamic.Core.InfoState.toPLA (φ s.toCore)

Why This Works

@cite{muskens-1996}

The embedding PLAPoss.toCore is injective: different PLA possibilities map to different Core possibilities.

The projection Possibility.toPLA is surjective onto Unit-world states: every PLA possibility is the projection of some Core possibility.

For Unit-world states, this gives an isomorphism between PLA and Core:

  PLAInfoState E ≃ InfoState Unit E

This is the formal content of @cite{muskens-1996}'s claim that DPL embeds into CDRT: the "worldless" setting is just the W = Unit case. The PLA embedding follows analogously via @cite{dekker-2012}'s elaboration.

Bilateral Extension

For BUS (bilateral semantics), we need:

• Positive dimension: s.toCore for positive updates
• Negative dimension: s.toCore for negative updates

The bilateral structure is orthogonal to the PLA/Core distinction. Both PLA and Core can have bilateral variants.