Godel's incompleteness theorem states there will be unprovable statements in some language. Can it be proven that the unprovable statements in some language $F$ are necessarily not just "trivially unprovable" statements such as:
Clearly we have the category "Proof that something, which is not a theorem of the axioms, does not exist." into which falls the example of the continuum hypothesis in ZFC which is thought unlikely to fit into any of the above categories - so it would seem likely that there must be non-trivial statements in some languages which are unprovable, but is it proven, or provable, that there necessarily exist unprovable statements not fitting into any of these "trivial" categories, in every language? (Note bolding added later as the meaning was missed by some readers before)
What I'm trying to do here, is to categorise in some sense the types of unprovable statements and circumstances in which they arise.
Note with respect to Illogical Statements: In response to advice I'm defining more explicitly what I consider an illogical statement and why I think the Liar Paradox is one. Please correct any misconception!
Definition: An illogical statement is a statement whose truth value is the inverse of its own truth value.
1: (Sentence $s_1$ is illogical if $s_1\implies\neg s_1$ or $\neg s_1\implies s_1$)
2: Let $s_1$ be the Liar Paradox "This sentence is false.".
3: Rewriting 2: $s_1\implies \neg s_1$
4: From 3,1: $\implies s_1$ is illogical.
And for the modified Liar: Modified Liar: This sentence is unprovable:
5: Let $s_2$ be "This sentence is unprovable."
6: $(s_2\implies s_2)\implies\neg s_2$
7: $s_2\implies\neg s_2$
8: From 7,1: $\implies s_2$ is illogical.
Please don't shower the question with downvotes... I'm still learning! Give me a chance to improve the question.
It seems you are confused about the statement of Godel's theorem:
None of the examples you give are examples of such a sentence!
The axioms of a theory $T$ are provable in $T$.
Statements like "This statement is false" cannot be expressed in first-order logic.
I'm not sure what "True is true" means, but if you're going to express it in first-order logic, it would presumably be "$\top\iff \top$," which is indeed a theorem, as is "$\neg(\top\iff\bot)$."
I think the following might help explain why Godel isn't trivial:
Let's work with the theory $PA$ (Peano arithmetic) for simplicity. It's language is $\{+, \times, <, 0, 1\}$, which means that a first-order sentence in this language is built out of
Those symbols,
variables - which are interpreted as ranging over numbers,
quantifiers $\exists$ and $\forall$ - again, ranging over numbers,
Booleans $\wedge, \vee, \implies$, and $\neg$,
and okay fine we also want parentheses "$($" and "$)$".
At this point it's a good exercise to sit down and try to express "This statement is false" in this way. You'll quickly find that it seems to be impossible: the language simply isn't expressive enough to talk about sentences and truth. Now, the genius of Godel's proof is the realization that actually the language of arithmetic can talk about sentences and provability (if not truth) in an indirect-but-still-powerful way, via Godel numbering. And then a modified version of the Liar paradox - specifically, the sentence $$\mbox{"This sentence is not provable in $PA$"}$$ (or better yet, Rosser's variation - "For every $PA$-proof of this sentence, there is a shorter $T$-disproof of this sentence") - lets us show that $PA$ is incomplete.
But this is extremely non-trivial, since at the outset it's not clear at all how to form sentences which talk about sentences, let alone sentences which talk about themselves, in the very narrow first-order language of $PA$!
EDIT, in reply to your comments below: Let's start with your last comment. The notion of "proof" in Godel's theorem is "proof from the axioms of $T$"; there is simply no relevant notion of ex nihilo proof. So yes, the axioms of $T$ are trivially provable from $T$.
This is a good point, though - in my above formulation of the Godel sentence, I used "prove" as shorthand for "prove in $PA$," which I should not have done. I've fixed it now.
As to expressing the Liar Paradox in the language of arithmetic - no, those don't work, for a number of reasons:
First, a very minor point: "$x\not=x$" and "$x=y\iff x\not=y$" aren't sentences, they're formulas - they have free variables. So you'd need to quantify them out first - e.g. "$\forall x(x\not=x)$," or similarly.
Second, those sentences (even when made into genuine sentences) aren't paradoxical, they're just wrong. Think about it: "$0\not=0$" isn't a paradox, it's just a false statement.
Third, more fundamentally, you seem to be treating the variables as ranging over sentences (motivating e.g. "$x\not=x$" as "a sentence is not equal to itself"). But they don't do this: the variables range only over numbers.
Fourth, even if they did range over sentences (and they can be treated as doing so in certain contexts, via Godel number, if we're careful), there's nothing forcing the variable "$x$" in "$x\not=x$" to refer to the formula "$x\not=x$" itself - and self-reference is critical to the Liar Paradox. "This statement is false" is a paradox; "some other statement is false" isn't, really.
Finally, there's your objection that the Godel sentence is "illogical." I'm not really sure what that means, but I think you're still assuming that the language of arithmetic is broader than it actually is. The Godel sentence (and its many variations) is just a statement about natural numbers; the fact that it has any self-referential character at all is surprising. And we can do even more concretely: as a corollary of the MRDP theorem, as long as $T$ is a true, computably axiomatizable theory, there is a Diophantine equation $E_T$ such that
$E_T$ has no solutions, but
$T$ cannot prove "$E_T$ has no solutions."
This is about as concrete as it gets; I don't know any way that Diophantine equations are "illogical." Recall: a Diophantine equation is an equation of the form $p(x_1, . . . , x_n)=q(x_1, . . . , x_n)$ where $p$ and $q$ are polynomials with natural number coefficients; and a solution to a Diophantine equation is a set of natural numbers which solves it.
In fact, the construction of $E_T$ from $T$ is effective: there is a computable function $f$ such that, if $e$ is a code (i.e. Turing machine index) for a true computably axiomatizable theory $T$ in the language of arithmetic, then $f(e)$ is a code for a Diophantine equation which has no solutions but which $T$ can't prove has no solutions.
Tl;dr: I think you should go back and read the proof of Godel's theorem, and the surrounding definitions in mathematical logic, carefully. It is not trivial, nor is the Godel sentence illogical. Peter Smith's book does a very good job explicating it.