Abstract We introduce two weak first-order theories of weighted and labelled finite trees, T*† and T*‡, respectively. It is proved that T*† and T*‡ are mutually interpretable with other previously studied elementary theories of ‘undecorated’ finite trees, as well as with Robinson Arithmetic, Q, and a host of other weak first-order theories of numbers, strings, sets and sequences.

Abstract Kristiansen and Murwanashyaka recently proved that Robinson arithmetic, Q, is interpretable in an elementary theory of full binary trees, T. We prove that, conversely, T is interpretable in Q by producing a formal interpretation of T in an elementary concatenation theory QT+, thereby also establishing mutual interpretability of T with several well-known weak essentially undecidable theories of numbers, strings, and sets. We also introduce a “hybrid” elementary theory of strings and trees, WQT*, and establish its mutual interpretability with Robinson’s weak arithmetic R, the weak theory of trees WT of Kristiansen and Murwanashyaka, and the weak concatenation theory WTCε of Higuchi and Horihata.

Abstract A new method of “minimal” readability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)—functions f such that HA ⊢ ∀x∃!yA(x, y) ⇒ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of ℒ(HA) with only x,y free—are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the < ε0-recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be chosen to be < ε0-recursive. The method is extended to intuitionistic finite-type arithmetic, , and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derived.

Abstract A realizability notion that employs only primitive recursive functions is defined, and, relative to it, the soundness of the fragment of Heyting Arithmetic (HA) in which induction is restricted to formulae is proved. A dual concept of falsifiability is proposed and an analogous soundness result is established for a further restricted fragment of HA.

Abstract It is well known that the following features hold of AR + T under the strong Kleene scheme, regardless of the way the language is Gödel numbered: 1. There exist sentences that are neither paradoxical nor grounded. 2. There are fixed points. 3. In the minimal fixed point the weakly definable sets (i.e., sets definable as {n ∣ A(n) is true in the minimal fixed point}, where A(x) is a formula of AR + T) are precisely the sets. 4. In the minimal fixed point the totally defined sets (sets weakly defined by formulae all of whose instances are true or false) are precisely the sets. 5. The closure ordinal for Kripke's construction of the minimal fixed point is . In contrast, we show that under the weak Kleene scheme, depending on the way the Gödel numbering is chosen: 1. There may or may not exist nonparadoxical, ungrounded sentences. 2. The number of fixed points may be any positive finite number, ℵ0, or . 3. In the minimal fixed point, the sets that are weakly definable may range from a subclass of the sets 1-1 reducible to the truth set of AR to the sets, including intermediate cases. 4. Similarly, the totally definable sets in the minimal fixed point range from precisely the arithmetical sets up to precisely the sets. 5. The closure ordinal for the construction of the minimal fixed point may be ω, , or any successor limit ordinal in between. In addition we suggest how one may supplement AR + T with a function symbol interpreted by a certain primitive recursive function so that, irrespective of the choice of the Gödel numbering, the resulting language based on the weak Kleene scheme has the five features noted above for the strong Kleene language.