Why does what I've written fail to define truth?

The concept you have defined is usually called "provable", not "true". This is indeed a quite central and important concept, but the point is that it is different from truth.

For example, let $\psi$ be the formula $(\forall x)(\forall y)(x=y)$.

Then $\psi$ is not provable in your system, and $\neg\psi$ is not provable in your system either (these two facts can be proved using some simple model theory).

But that means that according to your definition, $\psi$ is neither "true" nor "false". That is usually not considered a reasonable use of the words "true" and "false".

It is not unheard-of, though. Equating truth with provability (in a somewhat less powerful system than the one you're quoting) was more or less the position of the intuitionistic school of mathematics, which had high-profile adherents in the early 1900s. But it's not mainstream nowadays, to say the least. Contemporary mathematics prefers to be able to speak about a more well-behaved concept of truth too, and the word "provable" is still available when that's what we want to talk about.


The mainstream position is that pure logical formulas are not in themselves true or false, but that true/false is something a formula can be when combined with a particular interpretation of which things the quantifiers range over, and how the non-logical predicate and function letters work for those things.

So when we say that some particular formula is "true" -- say, $(\forall x)(\forall y)(x+y=y+x)$ -- what is really meant is that the formula is true in some particular interpretation, such as the one where quantifiers range over natural numbers, and "$+$" denotes addition of natural numbers (all of which we assume already exists before we start formalizing mathematical logic, as indeed it historically did!). When we're being particularly careful we will state this up front and say "true in the standard naturals" instead of just "true" -- but the latter is a common and conventional shorthand.

Note that this kind of truth does not depend on axioms -- we may work in an axiomatic system that does allow us to prove $(\forall x)(\forall y)(x+y=y+x)$, or we may choose to work with fewer axioms that are not strong enough to prove this. But that doesn't influence what we usually call truth.

But can't we just assume that we have enough axioms that the "provable" formulas are exactly those that are "true in the standard naturals"? Unfortunately not -- Gödel famously showed with the incompleteness theorem that no set of axioms (which is reasonable in the sense that there is a definite way to determine whether a given formula is an axiom or not) can prove exactly all the truths about the standard naturals.


I think what is failing is that your definition above is that you are talking about formulas, which are within a syntactical context while "truth" is a semantic notion (i.e. it depends on the model you are interpreting those formulas) but you can talk about logical validity which holds for example for your logic axioms since they are true in every possible model.

Added: also all logical theorems are logicaly valid (that's precisely what Correctness Theorem states)

Added2: you might find interesting Tarski's definition of truth


The issue is essential incompleteness. If the theory is incomplete, which means that there are well-formed sentences that are neither proved nor disproved by the axioms and rules of the theory, there could be a complete extension and in that case a definition of truth.

For example, the first-order theory of groups is undecidable (hence incomplete), but not essentially undecidable. One can define "true" statements to be the ones that hold for a cyclic group of order $5$, and those can be characterized by a recursive syntactic definition. This is a complete extension of the theory of groups with a decidable definition of truth.

If the theory interprets enough arithmetic, such as Peano or Robinson arithmetic, then any consistent extension is undecidable and there is no reasonable truth definition by Goedel and Tarski theorems.