I want to describe a hierarchy of infinitary logics, and show some properties of one of these logics in particular.

First, a speedy review of first order logic. In the language of first order logic we have access to parentheses {(, )}, the propositional connectives {∧, ∨, ¬, →}, the equals sign {=}, quantifiers {∀, ∃}, and a countably infinite store of variables for quantification over {x_{1}, x_{2}, x_{3}, …}. These are the logical symbols common to any first-order language, but to complete the language we additionally specify a set of constant symbols {c_{1}, c_{2}, c_{3}, …}, function symbols {f_{1}, f_{2}, f_{3}, …}, and relation symbols {R_{1}, R_{2}, R_{3}, …}. These sets can be any cardinality whatsoever. We can then define the set of grammatical sentences (“well-formed formulas”) of this language. We also interpret these symbols in a fairly straightforward way: a first-order structure has a universe of objects, and constants are assigned referents within that universe, function symbols are assigned n-ary functions on the universe, and relation symbols are assigned n-ary relations on the universe.

One consequence of the construction is that all of our sentences are finite, which puts an important cap on expressive power. Consider a language of arithmetic with constants for every natural number: {0, 1, 2, 3, …}. We might naturally want to say that the set of constants exhausts all the objects in our universe. But this takes an infinitely long sentence: ∀x (x=0 ∨ x=1 ∨ x=2 ∨ x=3 ∨ …). You might think you could be clever and find a finite expression of this idea, but it turns out that you can’t. (This is a consequence of Gödel’s first incompleteness theorem.)

So a natural extension of first-order-logic is to allow infinitely long sentences. For any two cardinal numbers α and β, define L_{α,β} to be first-order logic, but with conjunctions of any length < α allowed and blocks of quantifiers of any length < β. (Note that infinite conjunctions implies infinite disjunctions as well.) For example, L_{ω,ω} is ordinary first-order logic: conjunctions and quantifier blocks of any finite length. L_{ω1,ω} is first-order logic plus countably infinite conjunctions, but only finite quantifiers. L_{ω,ω1} has finite conjunctions but countably infinite quantifiers. Question: what logic is this equivalent to?

Notice that countably infinitely many quantifiers use countably infinitely many variables, but if you only have finite conjunctions you can only use finitely many of them. So this ends up being equivalent to L_{ω,ω}. For this same reason, if β > α then L_{α,β} is no different from L_{α,α}.

L_{ω1,ω} is especially interesting to logicians, because it’s significantly stronger than first-order logic, but not so much stronger as to lose all nice proof-theoretic properties. In particular, there’s a sound and complete proof system for L_{ω1,ω}! It’s also quite simple: just the FOL proof system plus one new axiom and one infinitary deduction rule:

New axiom

For any m ∈ ω and any set of sentences {φ_{n} | n ∈ ω},

∧_{n∈ω} φ_{n} → φ_{m}

New inference rule

φ_{0}, φ_{1}, φ_{2}, … ⊢ ∧_{n∈ω} φ_{n}

If we allow deductions of any countably infinite (successor) ordinal type, then we get a sound and complete proof system. This means that for any countable set of L_{ω1,ω}-sentences Σ and any L_{ω1,ω}-sentence φ, you can deduce φ from Σ just in case Σ actually (ω_{1},ω)-logically implies φ.

Infinite conjunctions give you a massive boost in expressive power going from FOL to L_{ω1,ω}. You can categorically define the natural numbers: Take Peano arithmetic and add to it the axiom: ∀x ∨_{n∈ω} (x = n). See why this works? We’ll refer back to this theory as PA*.

So L_{ω1,ω} is powerful enough to be able to categorically define the natural numbers. We might wonder if we can also categorically define all other countable structures. It turns out that while we can’t do that, we can do something slightly weaker. For any countable structure, there’s a single L_{ω1,ω}-sentence that defines it up to isomorphism among countable structures. The complexity of this sentence is a way of measuring the complexity of the structure, and has close connections to other measures of structure complexity. (The key word to learn more about this is *Scott rank*.)

What else can you do with L_{ω1,ω}? Here’s something really cool: Tarski’s theorem on the undefinability of truth tells us that in first-order logic you cannot define a truth predicate. But in L_{ω1,ω}, you can! Take a countable first-order language L. Add on the language of arithmetic (0, S, +, ×, ≤) to L. L is still countable, so enumerate all its sentences {φ_{1}, φ_{2}, φ_{3}, …}. Now, the sentence Tr(x) := ∨_{n∈ω} (x=n & φ_{n}) is a truth predicate: for any n, if φ_{n} is true then Tr(n) is true and if φ_{n} is false then Tr(n) is false.

You can express the idea that “infinitely many things satisfy φ(x)” with the following sentence:

∧_{n∈ω} ∀x_{0}∀x_{1}…∀x_{n} ∃y (φ(y) ∧ ∧_{k∈ω}(y ≠ x_{k})).

Expanding this out:

∀x_{0} ∃y (φ(y) ∧ y≠x_{0})

∧

∀x_{0}∀x_{1} ∃y (φ(y) ∧ y≠x_{0} ∧ y≠x_{1})

∧

∀x_{0}∀x_{1}∀x_{2} ∃y (φ(y) ∧ y≠x_{0} ∧ y≠x_{1} ∧ y≠x_{2})

∧

…

The first line says “there’s at least two things satisfying φ”, the second says “there’s at least three things satisfying φ”, and so on forever.

Finally, unlike FOL, L_{ω1,ω} is not compact. This means that there are sets of sentences without models, where every finite subset has a model. But it’s actually even worse than that! L_{ω1,ω} is *strongly* non-compact. You can have an unsatisfiable set of sentences, every **countable** subset of which has a model! Once again, this pretty remarkable fact has a simple proof:

Take the language of Peano arithmetic and add on ℵ_{1}-many constant symbols: {c_{α} | α < ω_{1}}. Now add to PA* the set of sentences {c_{α} ≠ c_{β} | α ≠ β, both in ω_{1}}. Let’s call this theory Σ. Every countable subset of Σ has a model, but Σ itself doesn’t. You can always take countably many constant symbols and assign them distinct referents in ℕ such that some natural numbers are left out. However, you can’t assign *uncountably* many distinct referents in ℕ while still leaving out some natural numbers, by a simple cardinality argument.

There’s an interesting twist here: Consider the set of sentences {c_{α} ≠ c_{β} | α ≠ β, both < ω_{1}^{CK}} ⊂ Σ, where ω_{1}^{CK} is the Church-Kleene ordinal, the smallest uncomputable ordinal. ω_{1}^{CK} is countable, so this is a countable set of sentences. This set of sentences has a model, but to obtain it you must choose a bijection from the set of constants {c_{α} | α < ω_{1}^{CK}} to the natural numbers. By the definition of ω_{1}^{CK}, this bijection is uncomputable! There are uncountably many countable ordinals above ω_{1}^{CK} (there are countably many computable ordinals, and uncountably many countable ordinals), so while every countable subset of Σ has a model, uncountably many of these models will be uncomputable!