Completeness for Infinitary Logic?

Question

I have heard a rumor that there is a proof system for certain infinitary logics, given by Carol Karp (?) in her thesis, but I can't find a copy. The result that I'm told exists is the following:

• A sentence $\phi$, from $L_{\omega_1\omega}$, has a model if and only if it is consistent; that is, there is no proof (in the above sense) from $\phi$ of a false sentence (e.g. $\exists x (x\not=x)$)
• This is not true for general $L_{\infty\omega}$ sentences; that is, there is a consistent sentence with no model. (The converse should be trivial; any sentence with a model should be consistent)

What I would really appreciate is a description of this proof system. I thought I could "guess" it on my own, but I guess I can't. I suspect, once given, that the proofs of the above theorems are relatively easy. In fact I have the sentence which is consistent with no models, although clearly I don't have a precise argument for consistency without the proof system.

I'm aware of some model existence theorems (e.g. Makkai's) which are probably equivalent to the above. But I'm really hunting for the proof system.

Answer 1

So I don't know about Karp's work in this setting (and google doesn't seem to know either), but I do know that Lopez-Escobar developed a proof system for $L_{\omega_1\omega}$. I believe this was originally done in his Ph.D. thesis, "Infinitely long formulas with countable quantifier degrees," which I don't have access to. However, his paper http://matwbn.icm.edu.pl/ksiazki/fm/fm57/fm57119.pdf describes it, and shows that it satisfies a cut elimination theorem. At a glance, it seems easy to generalize that proof system (but not the metatheorems of course) to $L_{\infty\omega}$, so this may be what you're looking for.

Side note: Barwise greatly improved on this, by developing proof systems for fragments of $L_{\omega_1\omega}$: given an admissible set $A$, let $L_A=L_{\omega_1\omega}\cap A$. Then Barwise defined a collection $P$ of proof-objects such that $P\cap A$ is $\Delta_1$ over $A$ and complete for $L_A$; see page 14 of "Barwise: infinitary logic and admissible sets" by Keisler and Knight. I believe Barwise' proof system(s) are discussed in Keisler's "Model theory of infinitary logic" and Barwise' "Admissible sets and structures," but I've never actually used it. I do know that it has a reputation of being tedious to work with directly, although the metatheorems one gets are quite useful. (E.g., the Barwise Compactness Theorem can be proved using this system if I recall correctly.)

Answer 2

I see this is a pretty old question, but I recently checked out a copy of Karp's book from the library.

These are from Chapters 5 & 11, if you manage to find a copy. The axiom schemes of the (Hilbert-style) system for $L_{\alpha \beta}$ ($\alpha$ is regular, infinite; $\beta$ is $0$ or $\omega \leq \beta \leq \alpha$) are as follows:

(A1) $A \to (B \to A)$

(A2) $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

(A3) $(\neg{A} \to \neg{B}) \to (B \to A)$

(A4. 1, $\delta$) $$\left({\Large\land}_{\xi < \delta}\, (A_\delta \to A_{\xi})\right) \to \left(A_\delta \to {\Large\land}_{\xi < \delta} \, A_{\xi}\right)$$ where $\{A_\xi: \xi < \delta\}$ is a sequence and $0 < \delta < \alpha$.

(A4. 2, $\delta$, $\nu$) $$\left({\Large\land}_{\xi < \delta}\, A_{\xi}\right) \to A_\nu$$

where $\{A_\xi: \xi < \delta\}$ is a sequence, $0 < \delta < \alpha$, and $\nu < \delta$.

(I should mention that if we stop here and take modus ponens and conjunction (see below) as rules of inference, we get a proof system for the propositional language $L_\alpha$.)

(A5) For $\overline{x} = \langle{x_{\xi}: \xi < \gamma\rangle}$ a sequence of variables with $\gamma < \beta$ and $\forall \overline{x}$ the abbreviation for $\forall x_{0} \dots \forall x_{\xi} \dots$:

$$\forall \overline{x} (A \to B) \to (A \to \forall \overline{x} B)$$

provided no variable in $\overline{x}$ is free in $A$.

(A6) Abbreviations are as in (A5); $f$ is any function from $\{x_\xi: \xi < \gamma\}$ to $L$-terms and $\mathsf{SF}_{f}^{\overline{x}}(A)$ is the result of replacing each $x_\xi$ in $A$ with $f(x_\xi)$:

$$\forall \overline{x} A \to \mathsf{SF}_{f}^{\overline{x}}(A)$$ provided that $A$ has no free occurrences of any $x_\xi$ bound by $\mathsf{FV}(f(x))$.

And as inference rules:

(MP) From $A$, $A \to B$ infer $B$.

(Conj) From $A_\xi$ for all $\xi < \delta$ for some $0 < \delta < \alpha$, infer ${\Large \land}_{\xi < \delta} A_\xi$.

(Gen) Where $\overline{y}$ and $\overline{x}$ are $\gamma$-sequences for $\gamma < \beta$: From $A$, infer $\forall \overline{x} \mathsf{SF}^{\overline{y}}(A)$ provided that $\overline{y} = \overline{x}$ or the variables of $\overline{y}$ are not among $\mathsf{FV}(A)$.

---

And then Karp gives other axiom schemes which I think are only needed for predicate logics with infinitary atomic formulas. I'd have to finish reading the text to be sure.

Edit: I forgot the equality axioms. Here's a paper with Karp's axiomatization in full.