summaryrefslogtreecommitdiffstats
path: root/content/zettel/4b2.md
blob: 7a68b866439adc4a98f04e95210203018071f8ca (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
+++
title = "Arithmetic Hierarchy"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["4b1"]
forwardlinks = []
zettelid = "4b2"
+++

This is a hierarchy constructed in the following way, where $k$ is the
type. $k=0$ is the type of $\mathbb{N}$, whereas $k=1$ gives the type of
$\mathbb{N}\rightarrow \mathbb{N}$:

-   the formula is $\Sigma^k_{n+1}$ if the outermost quantifier is
    $\exists^k$, and there are $n$ alternations between blocks of
    $\exists^k$ and $\forall^k$ at the front of the formula.

-   the formula is $\Pi^k_{n+1}$ if the outermost quantifier is
    $\forall^k$, and there are $n$ alternations between blocks of
    $\exists^k$ and $\forall^k$ at the front of the formula.