Infinitary logic

Infinitary logic permits infinitary syntactic operations, such as infinite conjunctions, together with an interpretation of its formulas. The infinitary language $L_{\kappa ,\lambda }$ specifies the permitted conjunction and quantifier lengths.

The infinitary language $L_{\kappa ,\lambda }$ permits conjunctions and disjunctions of fewer than $\kappa$ formulas and simultaneous quantification over fewer than $\lambda$ variables. Ordinary first-order logic is $L_{\omega ,\omega }$.

The logic $L_{{\omega }_1,\omega }$ extends first-order logic by countable logical conjunctions and logical disjunctions. Each formula has finitely many free variables, and quantifier strings are finite. In a countable first-order language, every countable structure has a Scott sentence in this logic that characterizes its isomorphism class among countable structures.

Every countable structure in a countable first-order language has a Scott sentence. Hence countable structures satisfying the same sentences of countable infinitary logic are isomorphic. The proof uses Scott formulas, stabilization on the countable set of finite tuples, and the back-and-forth method.

A Scott sentence for a countable structure is a sentence of countable infinitary logic satisfied, among countable structures in the same first-order language, exactly by its isomorphic copies. It may also have uncountable models. Scott formulas and stabilized back-and-forth method equivalences give its construction.

A Scott formula describes a finite tuple at a transfinite stage of the back-and-forth method. Stage zero specifies the complete atomic description; successor stages specify matching one-element extensions in both directions; limit stages conjoin the earlier descriptions. For a countable structure the equivalences on its finite tuples stabilize at a countable ordinal.