Formal systems or axiomatized formal theories

In chapter 3, Peter Smith defines formal systems or, as he calls them, axiomatized formal theories (I will use AFT as an abbreviation for this phrase).

A theory T is an AFT if...

Mappings and Gödel numbering

Section VI of Nagel and Newman's book describes mappings. A mapping is an operation that applies to two sets called the domain and the co-domain. More specifically, a mapping associates to each element of the domain one or more elements of the co-domain.

Formal systems, axioms, inference rules, formal proofs

I'll start this post by describing a simple formal system that I made up.

A formal system is comprised of axioms and inference rules. Each axiom and inference rule is defined syntactically, that is, by ordered sequences of symbols that follow strict syntactic rules but do not (necessarily) have any meaning. The set of all symbols allowed in a formal system are explicitly listed in its alphabet, simply, a finite, non-empty set of symbols.

My formal system, let's call it FS,  uses the alphabet {E,0,1} and has only one axiom and two inference rules. Here is the axiom (in the box below):