How can we define in set theory, for each n, a partial truth predicate $Tr_n$ for $\Sigma_n$ ($\Pi_n$) formulae wich is itself $\Sigma_n$ ($\Pi_n$)?

Question

At the very beginning of the paper Classes and truths in set theory (2012, APAL) by Kentaro Fujimoto, you can find this proposition:

For each n ≥ 1, we can define in KPω [Kripke-Platek set theory with infinity] a partial truth predicate $Tr_n$ for $\Sigma_n$-formulae ($\Pi_n$-formulae) which in itself is $\Sigma_n$ ($\Pi_n$); we mean here by a partial truth predicate a predicate which satisfies the Tarskian truth axioms restricted to bounded complexity, where the Tarskian truth axioms are the following:

1. $\forall x \forall y\ [(\ Tr\ \ulcorner \dot x = \dot y \urcorner \leftrightarrow x = y) \ \land \ (\ Tr\ \ulcorner \dot x \in\dot y \urcorner \leftrightarrow x \in y)] ;$
2. $\forall \ulcorner \sigma \urcorner\ [ Tr \ulcorner \lnot \sigma \urcorner \leftrightarrow \lnot Tr\ulcorner\sigma\urcorner \ ] ;$
3. $\forall \ulcorner \sigma \urcorner \forall \ulcorner \tau \urcorner\ [ Tr \ulcorner \sigma \land \tau \urcorner \leftrightarrow Tr\ulcorner \sigma \urcorner \land Tr\ulcorner\tau\urcorner\ ] ;$
4. $\forall \ulcorner \phi (u) \urcorner\ [ Tr \ulcorner \forall u \phi(u) \urcorner \leftrightarrow \forall x Tr \ulcorner \phi(\dot x) \urcorner \ ]. $

Here, $\sigma$ and $\tau$ range over (codes of) sentences, and $\phi$ ranges over (codes of) formulae. We are working with a formalized (in set theory) language $\mathscr L_\in^\infty$ $\supseteq \mathscr L_\in$, in wich we have a constant symbol $\dot x$ for each x $\in \pmb V$ (the standard set's universe).
The strategy for the "coding" of the syntax of $\mathscr L_\in^\infty$ is the same strategy that can be found, for example, in Devlin's book "Constructibility".

Well, in this context, how can we find the desidered partial truth predicates?

Answer 1

Assume KP + "$\omega$ exists". Then for each transitive set $X$ there is a $\Sigma_0$ satisfaction relation, which is a set, i.e. the set $$S_0(X)=\{(\varphi,\vec{x})\bigm|\varphi\text{ is a (formal) }\Sigma_0\text{-formula and }\vec{x}\in X^{<\omega}\text{ and }X\models\varphi(\vec{x})\}.$$ (For $n<\omega$, say an $n$-partial-$\Sigma_0$ satisfaction relation is as above, but just has to work for the first $n$ formulas $\varphi$ (but still all $\vec{x}\in X^{<\omega}$). By induction, for all $n<\omega$ there is an $n$-partial-$\Sigma_0$ satisfaction relation. The statement "$n<\omega$ and $S$ is an $n$-partial-$\Sigma_0$ satisfaction relation for $X$" is $\Sigma_0$ (in free variables $(n,X,S)$). So by KP we can collect a set containing one for each $n$, and then separate them out and take their union, which is $S_0(X)$ as desired.)

Also, for every set $X$ the transitive closure of $X$ exists (by a simpler argument than the previous one).

The functions $X\mapsto\mathrm{trancl}(X)$ and $X\mapsto S_0(X)$ are, moreover, $\Sigma_1$-definable (in fact the graphs of these functions are $\Sigma_0$-definable).

It is now routine to deduce the existence of the truth predicates you asked about. For $n=1$: Define $\mathrm{Sat}_{\Sigma_1}(\varphi,\vec{x})$ to say "$\varphi$ is a (formal) $\Sigma_1$ formula of the form $$\varphi(\vec{z})\iff\exists\vec{y}\psi(\vec{y},\vec{z}),$$ in free variables $\vec{z}$, where $\psi$ is a (formal) $\Sigma_0$ formula and $\mathrm{lh}(\vec{z})=\mathrm{lh}(\vec{x})$, and there are $\vec{w}$ and a transitive set $X$ with $\vec{x},\vec{w}\in X$ and there is $S=S_0(X)$, and $(\varphi,\vec{w}\frown\vec{x})\in S$".

Then for all meta $\Sigma_1$ formulas $\varphi$, we get $\mathrm{Sat}_{\Sigma_1}(\mathrm{G}(\varphi),\vec{x})$ iff $\varphi(\vec{x})$, where $G(\varphi)$ is the code of $\varphi$ as a formal formula.

This easily leads to the formula for $\mathrm{Sat}_{\Pi_1}$ also.

Then $\mathrm{Sat}_{\Sigma_2}(\varphi,\vec{x})$ says "$\varphi$ is (formal) $\Sigma_2$ formula of the form $\exists\vec{y}\psi(\vec{y},\vec{z})$, where $\psi$ is $\Pi_1$ and $\vec{z}$ are free with $\mathrm{lh}(\vec{z})=\mathrm{lh}(\vec{x})$, and there is $\vec{w}$ such that $\mathrm{Sat}_{\Pi_1}(\psi,\vec{w}\frown\vec{x})$".