FLAP Journal 2016 Journal Article
A Translation Theorem For Restricted R-Formulas.
- Joan Rand Moschovakis
The three-sorted formal system RLS described in [5] is like RLS(≺) in [4] but without the ≺. IRLS is a strictly intuitionistic subsystem of RLS. This note gives a natural, syntactically defined translation ϕ mapping each restricted formula E with only number and lawlike sequence variables free, to a formula ϕ(E) containing only number and lawlike sequence variables, such that IRLS proves E ↔ ϕ(E). If E contains no choice sequence variables then ϕ(E) is E. 1 The systems RLS, IRLS, R, IR and C 1. 1 A three-sorted language L The language, extending the two-sorted language of [2] and [1], contains three sorts of variables with or without subscripts, also used as metavariables: i, j, k, l, m, n, w, x, y, z over natural numbers, a, b, c, d, e, g, h over lawlike sequences, α, β, γ, .. . over arbitrary choice sequences; finitely many constants f0 (= 0), f1 (= 0 ) (successor), f2 (= +), f3 (= ·), f4 (= exp), f5, .. ., fp for primitive recursive functions and functionals; the binary predicate constant = (between terms); Church’s λ denoting function abstraction; parentheses (,) denoting function application; and the logical symbols &, ∨, →, ¬ and quantifiers ∀, ∃ over each sort of variable. I thank Sean Walsh and Kai Wehmeyer of UC Irvine, and the organizers of the 2014 Chiemsee Summer School, for giving me new opportunities to talk about this subject, resulting in this theorem. I am also very grateful to an anonymous referee whose careful reading led to many improvements.