Why does what I've written fail to define truth?
I stumbled across a set of axioms for first order logic a bit ago. Intrigued, I decided to try to write it all down and organise what I read. After I did that, it seemed to me as though one could quite simply define 'truth' using these axioms and deduction rules.
If $\beta, \gamma, \delta$ are wfs, $x, y$ are variables, and $t$ is a term, then the following wfs are called logical axioms:
$\beta \Rightarrow (\gamma \Rightarrow \beta)$
$(\beta \Rightarrow (\gamma \Rightarrow \delta)) \Rightarrow ((\beta \Rightarrow \gamma) \Rightarrow (\beta \Rightarrow \delta))$
$(\lnot \beta \Rightarrow \lnot \gamma) \Rightarrow ((\lnot \beta \Rightarrow \gamma) \Rightarrow \beta)$
$((\forall x) \beta) \Rightarrow \beta[t/x]$ if $t$ is free for $x$ in $\beta$.
$(\forall x)(\beta \Rightarrow \gamma) \Rightarrow (\beta \Rightarrow (\forall x) \gamma)$ if $\beta$ contains no free occurances of $x$.
$(\forall x)(x=x)$
$(\forall x)(\forall y)((x=y)\Rightarrow (\beta \Rightarrow \beta[y/x]))$
(Then give one's particular set of mathematical axioms, if one intends for them to be thought of as true).
We then define a subclass of wfs which we call the true statements. If $\alpha, \beta$ are wfs, and $x$ is a variable, then:
All logical axioms are true, as are all mathematical axioms.
If $\alpha$, and $\alpha \Rightarrow \beta$ are true, then $\beta$ is true.
If $\beta$ is true, then $(\forall x)\beta$ is true.
Finally, a statement $\phi$ is false if and only if $\lnot \phi$ is true.
When I showed this to some of my philosophy of mathematics friends, they thought for quite a while before deciding that the above did not suffice to define truth within such a formal system. When pressed as to why not, they weren't entirely sure, though a few possible places where issues could arise were discussed. We couldn't figure out what sort of true statement would not fall under such a definition, however.
My question is therefore - does the above fail to define truth? If so, why does it fail? Are there any amendments that could be made to fix the above? What sort of true statements would not be "true" in the above sense? What have I defined above?
Additionally, any sources for further reading on this topic would be of great, great interest to me, and would be appreciated.
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.