A system of complete and consistent truth (Q1893134)

The system FS (in honor of Friedman and Sheard, according to the author) is obtained from PA (= Peano arithmetic with all the primitive recursive functions) by adding the truth predicate \(T(\;)\). New axioms dictate that \(T\) commutes with quantifiers and connectives, and new rules are: from \(\varphi\), infer \(T\varphi\); and, conversely, from \(T \varphi\), infer \(\varphi\). [Here and below, sentences, their Gödel numbers, and their numerals are written the same.] By model theory, the author shows that FS is consistent but is \(\omega\)-inconsistent. He also considers RT, the theory of ramified truth, that has \(T_n(\;)\) for all \(n \in \mathbb{N}\), and the axiom \(T_n T_k \varphi \leftrightarrow T_n \varphi\) for \(k < n\). Both FS and RT are filtrated. Namely, in \(\text{FS}_n\) the new rules are applied less than \(n\) times, and in \(\text{RT}_n\), \(T_k\) can be used only if \(k < n\). A stage-by-stage comparison is given. Roughly, \(\text{RT}_n \vdash \varphi\) then \(\text{FS}_n \vdash h_n (\varphi)\), and \(\text{FS}_n \vdash \psi\) then \(\text{RT}_{2n} \vdash g_n (\psi)\), where \(h_n\) and \(g_n\) translate one language into the other. From this, the author shows that FS is arithmetically sound (despite its \(\omega\)-inconsistency), and is conservative over PA if the induction axioms are restricted to arithmetical formulas. He also considers global translations between FS and RT.