This is the +-term example I gave in class on Friday.

1. 0 is a +-term.

2. Any variable is a +-term.

3. If τ, π are +-terms, so is τ + π.

4. Nothing is a +-term except as required by 1, 2, and 3.

To give a formula representing the set of +-terms, we’ll need two other useful formulas, beside what we already have: Var(x) “x is a variable”, i.e., the 5-bit bytes in x are all equal to ^{⌈}ν^{⌉}. concat(u, v, y) “y is the concatenation of u and v”. Concatenating two strings is just putting them together. We have, for any two strings of symbols α, β,

|— ∀y(concat(\overline{^{⌈}α^{⌉}},\overline{^{⌈}β^{⌉}}, y) ↔ y ≈\overline{^{⌈}αβ^{⌉}})

Another handy notation for concatenation is u^{⌢}v. As with any other “defined” function, we use it with the understanding that its occurences within formulas are merely abbreviations for something else: for example, a formula

y ≈ u^{⌢}v abbreviates ∀z(concat(u, v, z) → y ≈ z) You should give definitions for both Var(x) and concat(u, v, y). This is the idea for the representing formula for the set of +-terms:

α is a +-term if and only if there is a sequence such that each term is either 0, or is a variable, or is τ + π for some two previous terms τ and π, and α is a term of this sequence.

Now here is the representing formula itself:

∃z(seq(z) ∧ ∀i(0< i < ln(z) → (z)_{i} ≈\overline{^{⌈}0^{⌉}}∨ Var((z)_{i})∨ ∃j∃k(0< j < i ∧0< k < i ∧ (z)_{i} ≈ (z)_{j}^{⌢}\overline{^{⌈}+^{⌉}}^{⌢} (z)_{k})) ∧ ∃i(x ≈ (z)_{i}))