Some Facts
The alphabet used in EA is finite, and the rules used in constructing formulas are well-defined, which means that we can list the formulas of EA in lexical order. When we say F(n), to refer to the n-th formula in the lexical order, we are referring to an unique formula of EA. A proof is a well-defined formula, and hence the proofs of EA can be listed in lexical order. When we say D(n), we mean that there is a proof for F(n) in the list of proofs. We define Sentient Arithmetic with the same vocabulary as EA, but
with three additional derivation rules.
These are some important facts we want to use. See the frame below for more facts.