Ordinal logics

By an ordinal logic is meant any uniform effective means of associating a logic (that is, an effectively generated formal system) with each effective ordinal representation. This notion was first introduced and studied by Alan Turing in 1939 as a means to overcome the incompleteness of sufficiently strong consistent formal systems, established by Kurt Gödel in 1931.

The first ordinal logic to consider, in view of Gödel’s results, would be that obtained by iterating into the constructive transfinite the process of adjoining to each system the formal statement expressing its consistency. For that ordinal logic, Turing obtained a completeness result for the class of true statements of the form that all natural numbers have a given effectively decidable property. However, he also showed that any ordinal logic (such as this) which is strictly increasing with increasing ordinal representation cannot have the property of invariance: in general, different representations of the same ordinal will have different sets of theorems attached to them. This makes the choice of representation a crucial one, and without a clear rationale as to how that is to be made, the notion of ordinal logic becomes problematic for its intended use.

Research on ordinal logics lapsed until the late 1950s, when it was taken up again for more systematic development. Besides leading to improvements of Turing’s results in various respects (both positive and negative), the newer research turned to restrictions of ordinal logics by an autonomy (or ‘boot-strap’) condition which limits the choice of ordinal representations admitted, by requiring their recognition as such in advance.