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: Choice (constructive) quantifiers — a player actually selects a value: ⊓x A(x): opponent picks x, and we must then win A(x). ⊔x A(x): we pick x, and must win the A(x) we picked.

Blind quantifiers — nobody picks: ∀x A(x): we must win A(x) without ever being told which x it is, so one strategy has to work uniformly. ∃x A(x): its dual.

∀ and ∃ are not the choice quantifiers, and the difference is the point of the system: ⊓x A(x) demands a solution computable as a function of x, while ∀x A(x) demands a single strategy good for every x at once — the second is the stronger requirement.

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.

© 2026 Lingenic LLC