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.

Symbol	Unicode	Name	Meaning
⊓	U+2293	Square cap / Choice conjunction	Opponent picks a conjunct; we must win it
⊔	U+2294	Square cup / Choice disjunction	We pick a disjunct and must win it
∧	U+2227	Parallel conjunction	Both games played at once; we must win both
∨	U+2228	Parallel disjunction	Both played at once; we must win one
∀	U+2200	Blind universal quantifier	One strategy must win for every value, unseen
∃	U+2203	Blind existential quantifier	Dual of the blind universal
⫰	U+2AF0	Branching recurrence	A made repeatedly available
⊤	U+22A4	Down tack / Machine	The player whose strategies define validity
⊥	U+22A5	Up tack / Environment	The adversary
⊓x	—	Choice universal quantifier	Opponent supplies x; we must win A(x)
⊔x	—	Choice existential quantifier	We supply x and must win the A(x) chosen
;	—	Sequential composition	Play A, then B

Metatheory. Formulas denote games between the machine ⊤ and the environment ⊥, and a formula is valid iff a single algorithmic strategy wins it under every interpretation of its atoms; Japaridze distinguishes this uniform validity from the weaker non-uniform notion of being winnable separately under each interpretation, and it is uniform validity the calculi axiomatize. Classical logic sits inside as an exact fragment: when every atom is an elementary, moveless game, ¬, ∧, ∨, ∀ and ∃ collapse to the classical connectives and quantifiers, so classical first-order logic is precisely the elementary fragment and computability logic is a conservative extension of it. The choice operations carry the constructive content — validity of ⊔x A(x) requires a computable witness function, and validity of ⊓x A(x) a solution uniform in a value the environment supplies — which is why ⊓ and ⊔ behave like the additives of linear logic and ⫰ like its exponential. Soundness and completeness have been proved for a graded series of fragments, not for the language as a whole.

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

Limitations. There is no complete axiomatization of the full language; the results are a graded series of calculi for fragments, and each additional game operation needs its own soundness and completeness proof rather than following from a general theorem. Because classical first-order logic embeds as the elementary fragment, validity is already undecidable there, and the richer operations only add to it. Validity is defined against a machine model — the existence of an algorithmic winning strategy — rather than against a class of structures, so compactness, Löwenheim–Skolem and canonical-model arguments are unavailable, and refuting a formula means diagonalizing against every machine instead of exhibiting a countermodel. The semantics is restricted to static games, in which a player cannot be harmed by delay, so genuinely timing-sensitive interaction falls outside the framework.