Computability Logic (CoL)

Origin. Giorgi Japaridze (2003). Games semantics for computation. Resources as game positions. Interactive computation. Beyond classical logic.

Models. Formulas are games. Connectives are game operations. Validity = machine-winnable. Computational semantics. Resources and interaction.

Formalism.

Games as formulas: Atomic: elementary games. Compound: built by operations. Winning = resource management. Interactive computation.

Players: ⊤: machine (us). ⊥: environment (them). Adversarial interaction. Winning strategies.

Parallel operations: A ∧ B: play both, win both. A ∨ B: play both, win one. Parallel games. AND/OR of winning.

Choice operations: A ⊓ B: opponent chooses, we must win. A ⊔ B: we choose, must win that. Interactive choice. Branching.

Sequential operations: A; B: first A, then B. Resources consumed. Sequential composition.

Quantifiers: ∀x A(x): opponent picks x. ∃x A(x): we pick x. Game choices.

Recurrence: ⫯A: A repeatedly available. Resource reuse. !A (bang) related. Linear logic connection.

Symbols.

Metatheory. Game semantics. Computational validity. Resource management. Interactive.

Applies to. Theory of computation. Game semantics. Resource logics. Interactive computation.

Limitations. Technical complexity. Unconventional. Limited adoption. Notation dense.