Equivalence between two definitions of infinitary logic

Question

The common definition of $ \omega $-logic (a.k.a $\mathcal{L}_{\omega_1,\omega}$ logic) is the usual first order logic allowing infinite conjunctions and infinite proof.

Chang and Keisler, in section 2.2 of their book, define $\omega$-logic differently*.

They restrict to the language $\{S,+,\cdot,1\}$ of Peano arithmetic and add the following inference rule (the $\omega$-rule):

If $\varphi(0), \varphi(1), \varphi(2),... $ all hold then we may infer $\forall x \varphi(x)$

A theory in the Peano arithmetic language is then said to be "$\omega$-consistent" if it is consistent and the $\omega$-rule hold.

My question is, is the $\omega$ logic on the language of Peano arithmetic as given in Chang Keisler equivalent to $\mathcal{L}_{\omega_1,\omega}$ where $\mathcal{L}$ is the same language?

I couldn't find they way to "translate" the definition from the semantic context to the syntactic context or vice versa.

*This is actually a private case which they later extend to what they call "generalized $\omega$-logic"

Answer 1

Perhaps there is an inconsistency in the terminology of the literature, but the following are simply different logics:

• $\mathcal{L}_{\omega_1, \omega}$ has infinitary formulas. I would call this infinitary logic.

• Peano arithmetic with the $\omega$-rule has the same formulas as regular Peano arithmetic, but adds an infinitary rule of inference, the $\omega$-rule, which is of the form $$ P(0),P(1),P(2),\ldots \vdash (\forall x)P(x) $$ I would call this $\omega$-logic.

These logics have quite different properties. For example:

• The upward Lowenheim-Skolem theorem fails for $\mathcal{L}_{\omega_1, \omega}$, because the infinitary sentence $$(\forall x)(x = 0 \lor x = 1 \lor x=2\lor\cdots)$$ is only satisfied in models whose domain is $\{0,1,2,\ldots\}$.
• The upward Lowenheim-Skolem theorem does hold for the closure of PA under the $\omega$-rule. It turns out that this theory is exactly the set of arithmetical statments that are true in the standard model - which is a complete first-order theory. For a proof, see this blog post. So, if we take a model of this theory of any larger cardinality, that will still be closed under the $\omega$-rule.

In general, $\mathcal{L}_{\omega_1, \omega}$ is used more often in model theory, because it is more expressive. In particular, Scott's isomorphism theorem relies explicity on infinitary logic to characterize countable models up to isomorphism.

On the other hand, the $\omega$-rule is used more often in proof theory. In the ordinal analysis of theories of arithmetic, the induction axioms are a problem, because they introduce "cuts" in derivations (applications of modus ponens) that are difficult to remove. The ingenious solution to this problem is to replace the usual finite derivations with corresponding infinite derivations that use the $\omega$-rule.

Answer 2

I don't see any reason to assume they would be the same. If I understand you correctly, the formulas of Chang and Keisler are the same as the formulas of ordinary arithmetic; they just have a more permissive consequence relation.

In contrast, what you describe as $\mathcal L_{\omega_1,\omega}$ has formulas that are more expressive than those of ordinary first-order formulas. For example, you can use diagonalization at the metalevel to produce a set of integers that isn't definable by any (ordinary finite) arithmetic formula, and then $\mathcal L_{\omega_1,\omega}$ would still allow you to claim that such-and-such holds about all of those integers and perhaps even prove it. Chang and Keisler can't even express that.

A more interesting example may be that $\mathcal L_{\omega_1,\omega}$ has a formula expressing "$x$ is a standard integer" (namely the infinite disjunction $x=0 \lor x=S(0) \lor x=S(S(0)) \lor \cdots$), so you can write down a theory that has $\mathbb N$ as its only model, up to isomorphism. In contrast it looks like $\omega$-logic in the Chang/Keisler sense doesn't give a way to rule out models that are elementarily equivalent to $\mathbb N$, such as an ultrapower of $\mathbb N$s.