---
tag: FTNXZ74D8N
kind: definition
name: Infinitary logic
msc: [03C75]
defines: PQG7VAZ1R2
uses: [086QKPF0A6, 0EBACQFAZW, HYJ10AF6RT, 983GZBQYT4]
sources:
  - url: https://en.wikipedia.org/wiki/Infinitary_logic
---

## Definition

Let $L$ be a signature and let $\kappa \ge \lambda$ be infinite [[cardinals|0EBACQFAZW]].
The formulas of the infinitary logic $L_{\kappa\lambda}$ are generated by the following rules.

1. Each atomic [[formula|HYJ10AF6RT]] of [[first-order logic|086QKPF0A6]] over $L$ is a formula.
2. If $\varphi$ is a formula, then $\neg\varphi$ is a formula.
3. If $\Phi$ is a set of formulas with $\abs{\Phi} < \kappa$ whose free variables together number fewer than $\lambda$, then $\bigwedge \Phi$ and $\bigvee \Phi$ are formulas.
4. If $\varphi$ is a formula and $V$ is a set of variables with $\abs{V} < \lambda$, then $\forall V \, \varphi$ and $\exists V \, \varphi$ are formulas.

Truth in an $L$-[[structure|983GZBQYT4]] is defined as in first-order logic: $\bigwedge \Phi$ holds when every member of $\Phi$ holds, and $\bigvee \Phi$ when some member holds.

## Remarks

The logic $L_{\omega\omega}$ is first-order logic, since then all conjunctions, disjunctions and quantifier blocks are finite.
The logic $L_{\omega_1\omega}$ allows countable conjunctions and disjunctions and finite quantifier blocks.

Example: in the signature of groups, the $L_{\omega_1\omega}$ sentence $\forall x \, \bigvee_{n \ge 1} (x^n = e)$ holds exactly in the torsion groups.
Here $x^n$ is the term $x \cdot x \cdots x$ with $n$ factors.

Non-example: the expression $\forall x_1 \, \forall x_2 \, \forall x_3 \cdots \varphi$ with infinitely many quantified variables is not a formula of $L_{\omega_1\omega}$, because clause 4 allows only finite sets of variables when $\lambda = \omega$.
It is a formula of $L_{\omega_1\omega_1}$ when $\varphi$ is.

The compactness theorem fails for $L_{\omega_1\omega}$, but the downward Löwenheim–Skolem theorem holds for its countable fragments.

## Explanations

### L1 human

Infinitary logic is first-order logic with permission to write infinitely long "and" and "or".
The two cardinals bound how long these may be and how many variables a quantifier may bind at once.