Language of an Axiomatic System in the Incompleteness Theorem

From wikipedia, the statement of Gödel's First Incompleteness Theorem is :

"Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F."

What exactly does the "language of F" mean? From what I can tell, it seems to be statements that involve things referred to by the axioms.

But this doesn't seem to be right, because if it were the case, counterexamples to this Incompleteness Theorem would be trivial.

Consider the axiomatic system A that contains the single axiom: "1 = 1", where 1 is some mathematical object, and = is some relation.

If the "language of A" referred to all things treated by the axioms in A, then only '1' and '=' are in the language of A. In that case, it seems like the only statement you could possibly write in the language of A is "1 = 1". This is true by the first axiom of A, and there's no way to disprove it using any axioms in A. So A is complete and consistent.

There are several places where the issue could be here. My thought is that it's in my understanding of what exactly the "language of A means."

It's also possible that it lies in the phrase "within which a certain amount of elementary arithmetic can be carried out," which doesn't seem to usually be brought up in qualitative descriptions of the theorem. It also seems like an oddly ill-defined statement for a theorem. The first thing makes me think that maybe it's not actually integral to the theorem, but it's also possible that "certain amount of elementary arithmetic" has a formal definition which I'm not aware of, and my system A does not satisfy this part of the hypothesis.

So where exactly is my misunderstanding of this theorem?

• I think the scope of the language of F is bigger than that. Gödel has in mind the set of all statements that can be expressed in F. Commented Feb 28, 2018 at 21:04
• @AdrianKeister "The set of all statements that can be expressed in F." That concept is just as nebulous to me as "the language of F." Commented Feb 28, 2018 at 21:06
• Well, F has a syntax that can be formalized to the point where, given any expression with any symbols in it whatsoever, the syntax rules will determine if the expression is a statement in F. I'm not an expert in syntax schema, but I've seen them. Commented Feb 28, 2018 at 21:07
• @AdrianKeister Interesting. So are the syntax rules required when creating an axiomatic system, or can they be derived from the axioms? Commented Feb 28, 2018 at 21:15
• The syntax rules (for determining the well-formed formulas, or wff's) are distinct from the axioms, but they are axiomatic, in the sense that they are usually assumed. See here: en.wikipedia.org/wiki/Formal_system. Commented Feb 28, 2018 at 21:18

The "language of $F$" will be, for example, first-order logic language (the language part), plus logical axioms and rules (the calculus part) plus specific axioms for e.g. arithmetic, like those for Robinson arithmetic.
The loose statement "a certain amount of elementary arithmetic" alludes to the expressive capabilities of the language, i.e. it must include for example the successor function $s$, and the "deductive" capabilities of the system, i.e. it must include (in addition to logical axioms and rules) also some specific arithmetical axioms.
$1=1$ [which is not an arithmetical axiom, but only an arithmetical instance of the equality axiom: $\forall x \ (x=x)$] will not suffice.