Difference between revisions of "Infinitary logic"
Zetapology (Talk  contribs) (Definition of the Hilberttype logic, expressiveness of Hilberttype logic) 
(No difference)

Latest revision as of 07:55, 6 September 2018
Infinitary logic is a type of logic which is used in the standard characterizations of several large cardinals, such as weakly compact cardinals and strongly compact cardinals. It also is used in alternate characterizations of other large cardinals such as supercompact cardinals and extendible cardinals.
More formally, an infinitary logic is a formal logic which has strings of infinite length. Generally, there is only one type of infinitary logic which is classically studied: Hilberttype infinitary logic.
HilbertType Infinitary Logic
The idea behind the infinitary logic $\mathcal{L}_{\kappa,\lambda}$ is that you can have $\kappa$many logical additions and logical products in a row, and $\lambda$many quantifiers in a row. This is called Hilberttype Infinitary Logic. You can also use $(n+1)$th order quantifiers in $\mathcal{L}_{\kappa,\lambda}^n$.
Formal Definition
Let $\kappa$ and $\lambda$ be regular cardinals. Then, $\mathcal{L}_{\kappa,\lambda}$ allows for all firstorder finitary assertions (made in $\mathcal{L}_{\omega,\omega}$) along with:
 For any set of $\mathcal{L}_{\kappa,\lambda}$formulae $P$ where $P<\kappa$, $\bigwedge_{\varphi\in P} \varphi$ and $\bigvee_{\varphi\in P}\varphi$
 For any set of variables $A$ where $A<\kappa$, $\forall_{v\in A}\varphi$ where $\varphi$ is an $\mathcal{L}_{\kappa,\lambda}$formula
 For any $\varphi$ which is an $\mathcal{L}_{\kappa,\lambda}$formula, $\neg\varphi$
There is also $\mathcal{L}_{\infty,\lambda}$, $\mathcal{L}_{\kappa,\infty}$, and $\mathcal{L}_{\infty,\infty}$ where $\infty$ is treated like $\text{ORD}$, allowing for statements of any ordinal length. You can even have $\mathcal{L}_{\infty^+,\infty^+}$ which allows for $\text{ORD}$length statements.
Expressiveness
$\mathcal{L}_{\kappa,\kappa}$ is unable to express some $\Pi_1^1$formulae under ZFC. Contrastively, $\mathcal{L}^1_{\omega,\omega}$ is unable to express $\mathcal{L}_{\omega_1,\omega_1}$, so firstorder infinitary logic and secondorder finitary logic both have expressiveness advantages. For why, see this question on MathOverflow.