Yes, your example does give an example of an incomplete system. This is because you took an intentionally weak axiom system but a strong semantics. Another way to get an example is just to take any semantics and throw away all the inference rules. Then nothing is provable.
The reason that the incompleteness theorems are more interesting than this is that they apply to every effective set of inference rules for arithmetic, no matter how strong we try to make the rules.
Here is how to make you question more precise. In general, a formal system consists of:
A formal language $L$ (set of sentences)
A set of inference rules (and axioms, which are a type of inference rule for this purpose)
A semantics, which provides a set of models, or at least a set of valuation functions from $L$ to $\{T,F\}$
Completeness of the system says that if a sentence is sent to $T$ by every valuation function in the semantics, then that sentence is provable from the inference rules.
In the incompleteness theorem, when it says "true", it means "true in a particular, distinguished, standard model". It doesn't mean "true in every model" because every first-order theory is complete in that sense, with its usual inference rules and semantics.
In your framework, you could take $L$ to be the language of ZFC enhanced with an extra unary predicate $I$. For the inference rules, you take the axioms of ZFC, an axiom that says $I$ can only hold of a function $\mathbb{R}\to\mathbb{R}$, axioms that let you prove that every elementary function is integrable, and the usual inference rules for first-order logic. For the distinguished model (valuation function) you take the standard model of ZFC and make $I$ hold of all integrable functions.
In that set-up, there are many functions $f$ for which $I(f)$ is true, and such that you can express $I(f)$ in the language at hand, but where your inference rules can't prove that $I(f)$ holds. For example, $\sin(x)$ is definable in ZFC, so you could let $f = \sin(x)$. You just have to be able to express $I(f)$ without $f$ in the language of ZFC with the extra symbol $I$.
The next problem is that you might wonder about making the inference rules stronger, in an attempt to prove more functions are integrable. In the context of set theory, this will lead you to some more interesting things, like the distinction between extensional and intensional definitions.
Best Answer
See Gödel's Incompleteness Theorems.
"Preliminary" formulation :
Precise formulation :
$\mathsf {ZFC}$ is precisely such a formalized system $F$ (i.e. "a formal system within which a 'certain amount of elementary arithmetic' can be carried out").
Gödel's original proof in his Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I ("On Formally Undecidable Propositions of Principia Mathematica and Related Systems I") does not use $\mathsf {ZFC}$ nor $\mathsf {PA}$.
His proof is relative to a "variant" of Principia Mathematica system; but his proof - in addition to esatblish the result now know as Gödel's Incompleteness Theorems - provides also a method applicable to many formal systems, provided that they satisfy some "initial conditions".
All the systems known as $\mathsf Q, \mathsf {PA}, \mathsf {ZFC}$ satisfy these conditions.
Relevant to your question, you can see :
It can be interesting to note that Melvin Fitting's thesis advisor was Raymond Smullyan.