Ytukyg

Warning:I am not competent in the field of logic so my questions may be weird or incorrect.

So I heard of infinitary logic. And as I understood it allows for statements of infinite length and proofs of infinite length but with some conditions. And also, as I have heard there can be different types of this logic. So now I have a few questions about it:

1)Can ZFC or PA be both consistent and complete under this logic?

2)Does permission of infinite length sentences and proofs bring some problems?

3)Can any of the types of infinitary logic be considered natural for humans?

Thanks in advance.

Let me begin by linking to the current standard textbook on infinitary logic: Lectures on infinitary logic by Dave Marker. You may also be interested in his primer on the topic.

It's also worth pointing out the huge collection Model-theoretic logics - one of the seminal texts in abstract model theory, the study of logics beyond first-order in general - and in particular its first two chapters:

• On the background and aims of abstract model theory.




• A bit of basics.

To address your questions, I need to go back to the definition. So this first section is just introductory.

The right way to think about infinitary logic is semantically. For our purposes (there are many definitions available, to be fair), a general logic will be a pair $mathfrak{L}=(Sent_mathfrak{L}, models_mathfrak{L})$ where:

• $Sent_mathfrak{L}$ is the class of sentencse in the logic. More precisely, $Sent_mathfrak{L}$ is a map assigning to each language (= set of constant, relation, and function symbols as usual) a set of things we'll call $mathfrak{L}$-sentences. Just like with e.g. group elements, we aren't going to say anything about what sentences are; in particular, we don't demand that they have any particular syntactic structure (although in natural examples of course they will).




• $models_mathfrak{L}$ is the satisfaction relation: a relation between structures and sentences (such that $mathcal{A}models_mathfrak{L}varphi$ only if $varphiin Sent_mathfrak{L}(Sigma)$ where $Sigma$ is the language of $mathcal{A}$).




• This pair satisfies a few basic axioms, which I won't write down here.

(Note that I'm doing a bit of horrible set vs. class juggling here - a general logic, as defined above, is really a proper class kind of object - but let's ignore that sort of thing for now.)

Note that proof systems (whatever that means exactly) are not inherent to general logics! Naturally-occurring general logics do have "reasonably natural proof systems," but this is an after-the-fact phenomenon. (Similarly, I'm not even talking about formulas - we can do everything we want just by thinking about sentences alone.) This is not to say that the proof theory of non-first-order logics is not interesting - indeed, it's incredibly interesting, to me at least - but rather that in initially learning about the subject it's a good idea to focus just on the semantic side.

Now at this point you might have a

Reasonable objection: Infinitary logic is defined syntactically, and I've obviously avoided syntax in my presentation above. So, what gives?

This is a good point. The "general logic" picture above strips things down to their semantic essentials, and this is a deliberate feature: it makes it easier to see the "big picture." So the really right perspective here is that infinitary logics - and really all naturally-occurring logics - are more than just their minimalist semantic behaviors, in the same way that when a group occurs in nature it's more than just a set with a binary operation satisfying some properties (e.g. it usually comes with a natural action on something), but that additional structure isn't always relevant.

So now let's discuss content: what's the difference between one logic and another?

The point is that what changes between one general logic and another - in particular, between classical first-order logic and any of the various infinitary logics - is expressive power: what classes of structures are axiomatizable by a single sentence, or a set of sentences, in the relevant logic? So it's not that infnitary logic proves more - indeed, there's no notion of proof inherent to infinitary logic - but that it says more.

For example, the compactness theorem implies that there is no first-order sentence (in the language ${<}$) characterizing the well-orderings, but there is such a sentence in the infinitary logic $mathcal{L}_{omega_1omega_1}$: $$forall(x_i)_{iinomega}bigvee_{iinomega}neg(x_{i+1}<x_i)$$ (okay fine, we need to also add the usual axioms for linear orders).

There is a natural notion of inclusion of general logics: $mathfrak{L}_0$ is a sublogic of $mathfrak{L}_1$ iff

• For each language $Sigma$, we have $Sent_{mathfrak{L}_0}(Sigma)subseteq Sent_{mathfrak{L}_1}(Sigma)$.




• For each language $Sigma$, each $Sigma$-structure $mathcal{A}$, and each $varphiin Sent_{mathfrak{L}_0}(Sigma)$, we have $$mathcal{A}models_{mathfrak{L}_0}varphiquadiffquadmathcal{A}models_{mathfrak{L}_1}varphi.$$

In particular, if $mathfrak{L}_0$ is a sublogic of $mathfrak{L}_1$ then whenever $T$ is a set of $mathfrak{L}_0$-sentences the class of models of $T$ in the sense of $mathfrak{L}_0$ is the same as the class of models of $T$ in the sense of $mathfrak{L}_1$. So ZFC is satisfiable in the sense of $mathcal{L}_{omega_1omega_1}$ (say) since ZFC is satisfiable in the sense of first-order logic and first-order logic is a sublogic of $mathcal{L}_{omega_1omega_1}$.

So this answers your first question: since classical first-order logic is a sublogic of infinitary logic(s), ZFC is also an infinitary theory (it's a set of first-order sentences, and each first-order sentence is an infinitary sentence), and is satisfiable in the sense of infinitary logic since it's satisfiable in the sense of first-order logic. Asking whether ZFC is consistent in infinitary logic isn't really a meaningful question.

So this handles your first question. Your second question, in my opinion, is where the real "meat" is. Let me rephrase it as:

How is the shift from classical first-order logic to an infinitary logic - or really any other general logic - reflected in a change of logical properties?

For example, the fact that $mathcal{L}_{omega_1omega_1}$ can characterize well-orderings implies that $mathcal{L}_{omega_1omega_1}$ is not compact. More down-to-earth, the infinitary logic $mathcal{L}_{omega_1omega}$ isn't compact either: consider the theory $${forall x(bigvee_{iinomega} S^{(i)}(0)=x)}cup{neg c=S^{(i)}(0): iinomega}$$ (in the language with two constant symbols $0,c$).

Another example is that $mathcal{L}_{omega_1omega_1}$ doesn't satisfy the downward Lowenheim-Skolem property: the sentence $$forall (x_i)_{iinomega}exists ybigwedge_{iinomega}neg x_i=y$$ characterizes exactly the uncountable structures. Similarly, $mathcal{L}_{omega_1omega}$ doesn't satisfy the downward Lowenheim-Skolem property either: take the language in unary relations $U_i$ ($iinomega$), and for each $Ssubseteqomega$ the sentence $$varphi_Sequiv exists x((bigwedge_{iin S}(U_i(x)))wedge(bigwedge_{inotin S}(neg U_i(x)))).$$

So this suggests that everything is terrible forever. However, this isn't the whole situation! A given general logic may still satisfy many interesting nice properties, and abstract model theory (see the links at the second part of the top of this answer) studies precisely this. The passage from classical first-order logic to $mathcal{L}_{omega_1omega}$ is particularly interesting:

• While $mathcal{L}_{omega_1omega}$ doesn't satisfy full downward Lowenheim-Skolem, it does satisfy a weak version: any single satisfiable $mathcal{L}_{omega_1omega}$-sentence has a countable model.




• There is a local analysis of $mathcal{L}_{omega_1omega}$ given by looking at its intersection with individual countable admissible sets. This was pioneered by Barwise, and one fundamental result here is the Barwise compactness theorem (building off the more limited Barwise-Kreisel compactness theorem); while more technical than classical compactness, it is still quite powerful. And this local analysis is quite useful in applications of $mathcal{L}_{omega_1omega}$.

Conversely, it turns out that compactness and the weak downwards Lowenheim-Skolem property characterize first-order logic uniquely (and so do recursive enumerability of validities and the weak downwards Lowenheim-Skolem property); this was proved by Lindstrom and was one of the major motivating results for abstract model theory.

So, does the shift cause problems? I object to the question (good-naturedly of course): "problem" or "cool new thing" is a subjective distinction.

Your final question is a bit harder to answer - what exactly is "natural for humans?"

Let me begin with a negative answer. My understanding is that early hopes - that abstract model theory would lead to lots of applications outside of logic by allowing logical analyses of non-first-order, but still somewhat tame, phenomena - were extremely ambitious and not born out, and that the whole general theory turned out to be much messier than expected at first. On the other hand, the specific logic $mathcal{L}_{omega_1omega}$ has played a seriously important role in descriptive set theory and even classical model theory.

• An aside: there is (to my understanding) a close analogy here with generalized recursion theory, with the whole subject being generally far less useful than initially hoped, and this leading to a major collapse in interest in it - with the exception of hyperarithmetic theory which plays an important role in descriptive set theory; interestingly, there is a tight connection between hyperarithmetic and $mathcal{L}_{omega_1omega}$, and some broader connections between abstract model theory and generalized
  recursion theory (e.g. here), so this is not really a coincidence.

On the other hand, naturality depends on the person. Certainly I find it impossible to resist the lure of the subject (similarly to my fascination with generalized recursion theory). Reiterating the sentiment of the last sentence of the previous section, one human's nonsense is another human's natural - if it interests you, dive in!