As I understand it, mathematics is concerned with correct deductions using postulates and rules of inference. From what I have seen, statements are called true if they are correct deductions and false if they are incorrect deductions. If this is the case, then there is no need for the words true and false. I have read something along the lines that Godel's incompleteness theorems prove that there are true statements which are unprovable, but if you cannot prove a statement, how can you be certain that it is true? And if a statement is unprovable, what does it mean to say that it is true?

2$\begingroup$ Philosophers argue ad infinitum about correspondence versus coherence theories of truth. $\endgroup$ – Robin Chapman May 12 '10 at 9:10

2$\begingroup$ For many mathematicians, the truth/untruth of a statement is not quite the same as whether it can be formally deduced from a given set of axioms! For instance, I might regard a given axiom as "false". $\endgroup$ – GS May 12 '10 at 12:22

17$\begingroup$ As I understand it, writing is concerned with putting words together into grammatically correct sentences. $\endgroup$ – Harald HancheOlsen May 12 '10 at 17:03

1$\begingroup$ @Harald: mathoverflow.net/questions/7155/famousmathematicalquotes/… $\endgroup$ – Qiaochu Yuan May 12 '10 at 20:11

$\begingroup$ @Qiaochu: Yes, I knew I had the idea from somewhere, but couldn't remember where. Information overload and all that. $\endgroup$ – Harald HancheOlsen May 13 '10 at 16:18
Tarski defined what it means to say that a firstorder statement is true in a structure $M\models \varphi$ by a simple induction on formulas. This is a completely mathematical definition of truth.
Goedel defined what it means to say that a statement $\varphi$ is provable from a theory $T$, namely, there should be a finite sequence of statements constituting a proof, meaning that each statement is either an axiom or follows from earlier statements by certain logical rules. (There are numerous equivalent proof systems, useful for various purposes.)
The Completeness Theorem of first order logic, proved by Goedel, asserts that a statement $\varphi$ is true in all models of a theory $T$ if and only if there is a proof of $\varphi$ from $T$. Thus, for example, any statement in the language of group theory is true in all groups if and only if there is a proof of that statement from the basic group axioms.
The Incompleteness Theorem, also proved by Goedel, asserts that any consistent theory $T$ extending some a very weak theory of arithmetic admits statements $\varphi$ that are not provable from $T$, but which are true in the intended model of the natural numbers. That is, we prove in a stronger theory that is able to speak of this intended model that $\varphi$ is true there, and we also prove that $\varphi$ is not provable in $T$. This is the sense in which there are truebutunprovable statements.
The situation can be confusing if you think of provable as a notion by itself, without thinking much about varying the collection of axioms. After all, as the background theory becomes stronger, we can of course prove more and more. The truebutunprovable statement is really unprovablein$T$, but provable in a stronger theory.
Actually, although ZFC proves that every arithmetic statement is either true or false in the standard model of the natural numbers, nevertheless there are certain statements for which ZFC does not prove which of these situations occurs.
Much or almost all of mathematics can be viewed with the settheoretical axioms ZFC as the background theory, and so for most of mathematics, the naive view equating true with provable in ZFC will not get you into trouble. But the independence phenomenon will eventually arrive, making such a view ultimately unsustainable. The fact is that there are numerous mathematical questions that cannot be settled on the basis of ZFC, such as the Continuum Hypothesis and many other examples. We have of course many strengthenings of ZFC to stronger theories, involving large cardinals and other settheoretic principles, and these stronger theories settle many of those independent questions. Some set theorists have a view that these various stronger theories are approaching some kind of undescribable limit theory, and that it is that limit theory that is the true theory of sets. Others have a view that settheoretic truth is inherently unsettled, and that we really have a multiverse of different concepts of set. On that view, the situation is that we seem to have no standard model of sets, in the way that we seem to have a standard model of arithmetic.

$\begingroup$ Can the phrase "these various stronger theories are approaching some kind of undescribable limit theory" be made formally precise in some sense? $\endgroup$ – Qfwfq May 12 '10 at 17:27

$\begingroup$ It is extremely difficult and is the subject of current philosophical work by Woodin, Koellner, Maddy, Hauser and others. But many large cardinal set theorists seem to espouse a view of this sort. $\endgroup$ – Joel David Hamkins May 12 '10 at 17:31

$\begingroup$ Interesting! Do you know any reference graspable by nonlogicians? $\endgroup$ – Qfwfq May 12 '10 at 18:35

$\begingroup$ Can you clarify what the "intended model of arithmetic" is? It seems to me that the Incompleteness Theorem is really a statement about this model, that no theory can prove every statement that is true in it. $\endgroup$ – Kevin Casto May 14 '10 at 20:46

$\begingroup$ The intended model is $\langle N,+,\cdot,0,1,\lt\rangle$, also known as the standard model of arithmetic. And you are right that one way to understand the Incompleteness Theorem is that it says we cannot write down a complete axiomatization of the theory of this structure. $\endgroup$ – Joel David Hamkins May 15 '10 at 10:43
Part of the reason for the confusion here is that the word "true" is sometimes used informally, and at other times it is used as a technical mathematical term.
Informally, asserting that "X is true" is usually just another way to assert X itself. When I say, "I believe that the Riemann hypothesis is true," I just mean that I believe that all the nontrivial zeros of the Riemann zetafunction lie on the critical line. (Note in particular that I'm not claiming to have a proof of the Riemann hypothesis!) This insight is due to Tarski. If you know what a mathematical statement X asserts, then "X is true" states no more and no less than what X itself asserts. Now, there is a slight caveat here: Mathematicians being cautious folk, some of them will refrain from asserting that X is true unless they know how to prove X or at least believe that X has been proved. So in some informal contexts, "X is true" actually means "X is proved." As we would expect of informal discourse, the usage of the word is not always consistent.
The word "true" can, however, be defined mathematically. Truth is a property of sentences. If you have defined a formal language $L$, such as the firstorder language of arithmetic, then you can define a sentence $S$ in $L$ to be true if and only if $S$ holds of the natural numbers. So for example the sentence $\exists x: x > 0$ is true because there does indeed exist a natural number greater than 0. Here it is important to note that true is not the same as provable. The formal sentence corresponding to the twin prime conjecture (which I won't bother writing out here) is true if and only if there are infinitely many twin primes, and it doesn't matter that we have no idea how to prove or disprove the conjecture.
Now, perhaps this bothers you. Is it legitimate to define truth in this manner? Some people don't think so. However, note that there is really nothing different going on here from what we normally do in mathematics. When we were sitting in our number theory class, we all knew what it meant for there to be infinitely many twin primes. Why should we suddenly stop understanding what this means when we move to the mathematical logic classroom? If we understand what it means, then there should be no problem with defining some particular formal sentence to be true if and only if there are infinitely many twin primes. It is as legitimate a mathematical definition as any other mathematical definition.
Now, how can we have true but unprovable statements? And if we had one how would we know? Joel David Hamkins explained this well, but in brief, "unprovable" is always with respect to some set of axioms. Therefore it is possible for some statement to be true but unprovable from some particular set of axioms $A$. In order to know that it's true, of course, we still have to prove it, but that will be a proof from some other set of axioms besides $A$.
I say that $$ \int_{\infty}^{+\infty} e^{x^2} dx = \sqrt{\pi} $$ is true .... and any talk about "correct deductions using postulates" is a rationalization added later. Mathematicians knew this fact (yes, fact) even before the field of mathematical logic began.

5$\begingroup$ Do you have a similar view about the Continuum Hypothesis? This question was also asked before math logic began, first by Cantor, and then famously, as the first Hilbert problem. $\endgroup$ – Joel David Hamkins May 12 '10 at 12:41

2$\begingroup$ If it was not possible to prove this, would you still be confident in calling this true? $\endgroup$ – teil May 12 '10 at 12:42

1$\begingroup$ 1, as it is a particularly antimathematical viewpoint! ;) $\endgroup$ – Qfwfq May 12 '10 at 17:14

8$\begingroup$ If someone asks you why it is true, then you will deduce it from something more basic. And if they ask you why that is true, you will deduce it from something more basic still. What you won't say (unless you want to leave your questioner very dissatisfied) is that it's just a Platonic fact about the mathematical universe. Obviously these "why" questions have to come to an end eventually, and ... bingo ... there are your postulates. $\endgroup$ – gowers May 12 '10 at 21:25

5$\begingroup$ The "truth" of the above integral equality is only possible because "we know what you mean". But the movement to establish foundations for calculus, etc. only arose because people started to lose confidence that they really did know what was meant.  How do we know what you mean? Because the integral is defined in a certain way; specifically, with sufficient detail that it becomes possible to demonstrate the truth of the equality above. Intuitions regarding interesting relationships do not become "true" or "false" until crystallized into axiomatizable definitions admitting proofs. $\endgroup$ – Niel de Beaudrap May 13 '10 at 9:40
Both the optimistic view that all true mathematical statements can be proven and its denial are respectable positions in the philosophy of mathematics, with the pessimistic view being more popular. The question is more philosophical than mathematical, hence, I guess, your question's downvotes.
Neil Tennant 's Taming of the True (1997) argues for the optimistic thesis, and covers a lot of ground on the way. I recommend it to you if you want to explore the issue.

1$\begingroup$ How can it be philosophical? Godel's theorem is mathematics, so the terms have to be defined. $\endgroup$ – teil May 12 '10 at 9:27

$\begingroup$ @NR: it's worth noting that Gödel's incompleteness and completeness results deal with a vey specific kind of hypotheses and proofs; that is to say, first order. In general, a statement is true if whenever the hypotheses are true, the conclusion is. In the case of first order logic this can be restated as: for any model where the hypotheses are true, the conclusion is. However, whether or not you're in first order, what you really care about is whether there's an example where the hypotheses are true but the conclusion is wrong. $\endgroup$ – H. Hasson May 12 '10 at 10:41

$\begingroup$ It occurred to me that there's another point to make here. Even if you care about groups, fields, etc., your theorem can be stated in the language of sets. You may, if it's first order in the language of groups, etc., treat it as such. But the more general notion is being first order in sets. $\endgroup$ – H. Hasson May 12 '10 at 10:50

1$\begingroup$ @Negative What if the terms can't be defined? en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem $\endgroup$ – Dan Piponi May 12 '10 at 16:11

$\begingroup$ @H Hasson: First sentence is true, but misses the depth of the result. Because the Halting Problem is undecidable and individual cases can be encoded as 1storder sentences of number theory, the set Th(N) of true 1storder sentences of number theory is not computable, and therefore is not computably enumerable. Now for any proof system worthy of the name, the set of provable [1storder number theory] sentences is c.e. It therefore cannot coincide with Th(N) — either the system proves false sentences, or (preferably) fails to prove true ones. One only need encompass 1storder theory. $\endgroup$ – Chad Groft May 13 '10 at 13:18
The Stanford Encyclopedia of Philosophy has several articles on theories of truth, which may be helpful for getting acquainted with what is known in the area. Their toplevel article is
http://plato.stanford.edu/entries/truth/
There are several more specialized articles in the table of contents.
Let me offer an explanation of the difference between truth and provability from postulates which is (I think) slightly different from those already presented. (Although perhaps close in spirit to that of Gerald Edgars's.)
First of all, if we are talking about results of the form "for all groups, ..." or "for all topological spaces, ... " then in this case truth and provability are essentially the same: a result is true if it can be deduced from the axioms. (There is the caveat that the notion of group or topological space involves the underlying notion of set, and so the choice of ambient set theory plays a role. This role is usually tacit, but for certain questions becomes overt and important; nevertheless, I will ignore it here, possibly at my peril.)
But other results, e.g in number theory, reason not from axioms but from the natural numbers. Of course, along the way, you may use results from group theory, field theory, topology, ..., which will be applicable provided that you apply them to structures that satisfy the axioms of the relevant theory. But in the end, everything rests on the properties of the natural numbers, which (by Godel) we know can't be captured by the Peano axioms (or any other finitary axiom scheme). How do we agree on what is true then? Well, experience shows that humans have a common conception of the natural numbers, from which they can reason in a consistent fashion; and so there is agreement on truth.
If you like, this is not so different from the model theoretic description of truth, except that I want to add that we are given certain models (e.g. the standard model of the natural numbers) on which we agree and which form the basis for much of our mathematics. (Again, certain types of reasoning, e.g. about arbitrary subsets of the natural numbers, can lead to settheoretic complications, and hence (at least potential) disagreement, but let me also ignore that here.)
In summary: certain areas of mathematics (e.g. number theory) are not about deductions from systems of axioms, but rather about studying properties of certain fundamental mathematical objects. Axiomatic reasoning then plays a role, but is not the fundamental point.

$\begingroup$ But ultimately, won't the independence phenomenon still arrive? After all, even for the strongest known axiomatizations of mathematics, such as ZFC+large cardinals, Goedel's theorem still provides arithmetic statements that are neither provable nor refutable. Although ZFC proves that there is a standard model of arithmetic, different models of ZFC can have nonisomorphic standard models (and even nonelementarily equivalent). So the question of what is true in the standard model depends on the settheoretic background. $\endgroup$ – Joel David Hamkins May 13 '10 at 12:31

2$\begingroup$ Dear Joel, This is the question swept under the rug by my parenthetical decisions to ignore settheoretic issues. My own position on this is unabashedly platonist, in that I believe that there is a true standard model for the natural numbers (the one in my imagination!), and perhaps a little naive. Thankfully, the comment box doesn't give me enough space to try to seriously defend my position! $\endgroup$ – Emerton May 13 '10 at 14:02
There are two answers to your question:
• A statement is true in absolute if it can be proven formally from the axioms.
• A statement is true in a model if, using the interpretation of the formulas inside the model, it is a valid statement about those interpretations.
Assuming your set of axioms is consistent (which is equivalent to the existence of a model), then
$\qquad$ truth in absolute $\Rightarrow$ truth in any model.
Conversely, if a statement is not true in absolute, then there exists a model in which it is false.
Let's take an example to illustrate all this.
Let $P$ be a property of integer numbers, and let's assume that you want to know whether the formula $\exists n\in \mathbb Z : P(n)$ is true.
Three situations can occur:
• You're able to find $n\in \mathbb Z$ such that $P(n)$.
• You're able to prove that $\not\exists n\in \mathbb Z : P(n)$
• Neither of the above.
In the latter case, there will exist a model $\tilde{\mathbb Z}$ of the integers (it's going to be some ring, probably much bigger than $\mathbb Z$, and that satisfies all the axioms that "characterize" $\mathbb Z$) that contains an element $n\in \tilde {\mathbb Z}$ satisgying $P$.
This is a question which I spent some time thinking about myself when first encountering Goedel's incompleteness theorems. I should add the disclaimer that I am no expert in logic and set theory, but I think I can answer this question sufficiently well to understand statements such as Goedel's incompleteness theorems (at least, sufficiently well to satisfy myself).
One one end of the scale, there are statements such as CH and AOC which are independent of ZF set theory, so it is not at all clear if they are really true and we could argue about such things forever. Even for statements which are true in the sense that it is possible to prove that they hold in all models of ZF, it is still possible that in an alternative theory they could fail. Even things like the intermediate value theorem, which I think we can agree is true, can fail with intuitionistic logic.
On the other end of the scale, there are statements which we should agree are true independently of any model of set theory or foundation of maths. For example, I know that 3+4=7. There are simple rules for addition of integers which we just have to follow to determine that such an identity holds. You might come up with some freaky model of integer addition following different rules where 3+4=6, but that is really a different statement involving a different operation from what is commonly understood by addition. Similarly, I know that there are positive integral solutions to $x^2+y^2=z^2$. To verify that such equations have a solution we just need to iterate through all possible triples $(x,y,z)\in\mathbb{N}^3$ and test whether $x^2+y^2=z^2$, stopping when a solution is reached. In this case we are guaranteed to arrive at some solution, such as (3,4,5), proving that there is indeed a solution to the equation.
More generally, consider any statement which can be interpreted in terms of a deterministic, computable, algorithm. If we simply follow through that algorithm and find that, after some finite number of steps, the algorithm terminates in some state then the truth of that statement should hold regardless of the logic system we are founding our mathematical universe on.
So, there are statements of the following form: "A specified program (P) for some Turing machine and given initial state (S0) will eventually terminate in some specified final state (S1)". If such a statement is true, then we can prove it by simply running the program  step by step until it reaches the final state. Such statements, I would say, must be true in all reasonable foundations of logic & maths. Identities involving addition and multiplication of integers fall into this category, as there are standard rules of addition & multiplication which we can program. So does the existence of solutions to diophantine equations like $x^2+y^2=z^2$. Existence in any one reasonable logic system implies existence in any other.
At the next level, there are statements which are falsifiable by a computable algorithm, which are of the following form: "A specified program (P) for some Turing machine with initial state (S0) will never terminate". For example, "There are no positive integer solutions to $x^3+y^3=z^3$" fall into this category. You can write a program to iterate through all triples (x,y,z) checking whether $x^3+y^3=z^3$. Fermat's last theorem tells us that this will never terminate. We can never prove this by running such a program, as it would take forever. However, the negation of statement such as this is just of the previous form, whose truth I just argued, holds independently of the "reasonable" logic system used (this is basically $\omega$consistency, used by Goedel). That is, if I can write an algorithm which I can prove is never going to terminate, then I wouldn't believe some alternative logic which claimed that it did. In the same way, if you came up with some alternative logical theory claiming that there there are positive integer solutions to $x^3+y^3=z^3$ (without providing any explicit solutions, of course), then I wouldn't hesitate in saying that the theory is wrong. Statements like $$ \int_{\infty}^\infty e^{x^2}\\,dx=\sqrt{\pi} $$ are also of this form. Assuming we agree on what integration, $e^{x^2}$, $\pi$ and $\sqrt{\ }$ mean, then we can write a program which will evaluate both sides of this identity to ever increasing levels of accuracy, and terminates if the two sides disagree to this accuracy. The identity is then equivalent to the statement that this program never terminates.
Going through the proof of Goedels incompleteness theorem generates a statement of the above form. i.e., "Program P with initial state S0 never terminates" with two properties. (1) If the program P terminates it returns a proof that the program never terminates in the logic system. (2) If there exists a proof that P terminates in the logic system, then P never terminates.
So, if P terminated then it would generate a proof that the logic system is inconsistent and, similarly, if the program never terminates then it is not possible to prove this within the given logic system.
In fact, P can be constructed as a program which searches through all possible proof strings in the logic system until it finds a proof of "P never terminates", at which point it terminates. The assumptions required for the logic system are that is "effectively generated", basically meaning that it is possible to write a program checking all possible proofs of a statement.

$\begingroup$ Doesn't this use Church's thesis  which states that recursive and computable functions are the same thing? $\endgroup$ – teil May 13 '10 at 3:13
This is a philosophical question, rather than a matehmatical one. Anyway personally (it's a metter of personal taste!) I totally agree that mathematics is more about correctness than about truth.
In the following paragraphs I will try to (partially) answer your specific doubts about Goedel incompleteness in a down to earth way, with the caveat that I'm no expert in logic nor I am a philosopher. (See also this MO question, from which I will borrow a piece of notation). I had some doubts about whether to post this answer, as it resulted being a bit too verbose, but in the end I thought it may help to clarify the related philosophical questions to a nonmathematician, and also to myself.
The point is that there are several "levels" in which you can "state" a certain mathematical statement; more: in theory, in order to make clear what you formally want to state, along with the informal "verbal" mathematical statement itself (such as $2+2=4$) you should specify in which "level" it sits. (Of course, as mathematicians don't want to get crazy, in everyday practice all of this is left completely as understood, even in mathematical logic).
For example, suppose we work in the framework of ZermeloFrenkel set theory ZF (plus a formal logical deduction system, such as HilbertFrege HF): let's call it Set1. In this setting, you can talk formally about sets and draw correct (relative to the deduction system) inferences about sets from the axioms. You can also formally talk and prove things about other mathematical entities (such as $\mathbb{N}$, $\mathbb{R}$, algebraic varieties or operators on Hilbert spaces), but everything always boils down to sets.
Still in this framework (that we called Set1) you can also play the game that logicians play: talking, and proving things, about theories $T$. How? Well, you only have sets, and in terms of sets alone you can define "logical symbols", the "language" $L$ of the theory you want to talk about, the "well formed formulae" in $L$, and also the set of "axioms" of your theory. Examples of such theories are Peano arithmetic PA (that in this incarnation we should perhaps call PA2), group theory, and (which is the reason of your perplexity) a version of ZermeloFrenkel set theory ZF as well (that we will call Set2). Note that every piece of Set2 "is" a set of Set1: even the "$\in$" symbol, or the "$=$" symbol, of Set2 is itself a set (e.g. a string of 0's and 1's specifying it's ascii character code...) of which we can formally talk within Set1, likewise every logical formula regardless of its "truth" or even wellformedness. Stating that a certain formula can be deduced from the axioms in Set2 reduces to a certain "combinatorial" (syntactical) assertion in Set1 about sets that describe sentences of Set2.
The good think about having a metatheory Set1 in which to construct (or from which to see) other formal theories $T$ is that you can compare different theories, and the good thing of this metatheory being a set theory is that you can talk of models of these theories: you have a notion of semantics.
In the light of what we've said so far, you can think of the statement "$2+2=4$" either as a statement about natural numbers (elements of $\mathbb{N}$, constructed as "finite von Neumann ordinals" within Set1, for which $0:=\emptyset$, $1:=${$\emptyset$} etc.); or as a sentence of PA2 (which is actually itself a bare set, of which Set1 can talk).
An interesting (or quite obvious?) thing is that in some cases it makes sense to go on to "construct theories" also within the lower levels. For example, within Set2 you can easily mimick what you did at the above level and have formal theories, such as ZF set theory itself, again (which we can call Set3)! A crucial observation of Goedel's is that you can construct a version of Peano arithmetic not only within Set2 but even within PA2 itself (not surprisingly we'll call such a theory PA3). So you have natural numbers (of which PA2 formulae talk of) codifying sentences of Peano arithmetic!
So, if we loosely write "$A\triangleright B$" to indicate that the theory or structure $B$ can be "constructed" (or "formalized") within the theory $A$, we have a picture like this:
Set1 $\triangleright$ ($\mathbb{N}$; PA2 $\triangleright$ PA3; Set2 $\triangleright$ Set3; T2 $\triangleright$ T3; ...).
So, you see that in some cases a theory can "talk about itself": PA2 talks about sentences of PA3 (as they are just natural numbers!), and there is a formally precise way of stating and proving, within Set1, that "PA3 is essentially the same thing as PA2 in disguise".
Furthermore, you can make sense of otherwise loose questions such as "Can the theory $T$ prove it's own consistency?". How? Well, you construct (within Set1) a version of $T$, say T2, and within T2 formalize another theory T3 that also "works exatly as $T$". Then you have to formalize the notion of proof.
So, the Goedel incompleteness result stating that
"Peano arithmetic cannot prove its own consistency"
is really a theorem of Set1 asserting that "PA2 cannot prove the consistency of PA3". This means: however you've codified the axioms and formulae of PA as natural numbers and the deduction rules as sentences about natural numbers (all within PA2), there is no way, manipulating correctly the formulae of PA2, to obtain a formula (expressed of course in terms of logical relations between natural numbers, according to your codification) that reads like "It is not true that axioms of PA3 imply $1\neq 1$".
You can say an exactly analogous thing about Set2 $\triangleright$ Set3, and likewise about every theory "at least compliceted as PA".
Now, about truth. First of all, the distinction between provability a and truth, as far as I understand it. It is easy to say what being "provable" means for a formula in a formal theory $T$: it means that you can obtain it applying correct inferences starting from the axioms of $T$. This is a purely syntactical notion.
The concept of "truth", as understood in the semantic sense, poses some problems, as it depends on a settheorylike metatheory within which you are supposed to work (say, Set1). Saying that a certain formula of $T$ is true means that it holds true once interpreted in every model of $T$ (Of course for this definition to be of any use, $T$ must have models!).
If we could convince ourselves in a rigorous way that ZF was a consistent theory (and hence had "models"), it would be great because then we could simply define a sentence to be "true" if it holds in every model. This was Hilbert's program. Unfortunately, as said above, it is impossible to rigorously (within ZF itself for example) prove the consistency of ZF.
About true undecidable statements.
The assertion of Goedel's that
"There is a property of natural numbers that is true but unprovable from the axioms of Peano arithmetic"
is a theorem of Set1 stating that there is a sentence of PA2 that holds true* in any model of PA2 (such as $\mathbb{N}$) but is not obtainable as the conclusion of a finite set of correct logical inference steps from the axioms of PA2.
*(that a sentence of PA2 is "true in any model" here means: "the corresponding interpretation of that sentence in each model, which is a sentence of Set1, is a consequence of the axioms of Set1")
According to Goedel's theorems, you can find undecidable statements in any consistent theory which is rich enough to describe elementary arithmetic. That is, such a theory is either inconsistent or incomplete.
About meaning of "truth".
Foundational problems about the absolute meaning of truth arise in the "zeroth" level, i.e. about sentences expressed in what is supposed to be the foundational theory Th0 for all of mathematics According to some, this Th0 ought to be itself a formal theory, such as ZF or some theory of classes or something weaker or different; and according to others it cannot be prescribed but in an informal way and reflect some ontological or psychological entity such as the "real universe of sets". I would roughly classify the former viewpoint as "formalism" and the second as "platonism".
One point in favour of the platonism is that you have an absolute concept of truth in mathematics. One drawback is that you have to commit an act of faith about the existence of some "true universe of sets" on which you have no rigorous control (and hence the absolute concept of truth is not formally well defined). According to platonism, the Goedel incompleteness results say that
"Logic cannot capture all of mathematical truth".
On the other hand, one point in favour of "formalism" (in my sense) is that you don't need any ontological commitment about mathematics, but you still have a perfectly rigorous though relative control of your statements via checking the correctness of their derivation from some set of axioms (axioms that vary according to what you want to do). One consequence (not necessarily a drawback in my opinion) is that the Goedel incompleteness results assume the meaning:
"There is no place for an absolute concept of truth: you must accept that mathematics (unlike the natural sciences) is more a science about correctness than a science about truth".
In my humble opinion, the best reference for this kind of questions is Bourbaki's "Set Theory" ... Actually, I would recommend Bourbaki's book to people who, like me, have trouble to understand other texts on the same subject.

3$\begingroup$ See mathoverflow.net/questions/16174 for logician Adrian Mathias' review of this text. $\endgroup$ – Joel David Hamkins May 12 '10 at 12:43

1$\begingroup$ Thank you! Unfortunately, I don't understand Adrian Mathias' review. But I feel I understand Bourbaki's book. $\endgroup$ – PierreYves Gaillard May 12 '10 at 13:16
The answer to the "unprovable but true" question is found on Wikipedia:
For each consistent formal theory T having the required small amount of number theory, the corresponding Gödel sentence G asserts: “G cannot be proved to be true within the theory T”...
If G is true: G cannot be proved within the theory, and the theory is incomplete. If G is false: then G can be proved within the theory and then the theory is inconsistent, since G is both provable and refutable from T.
If ‘true’ isn’t the same as provable according to a set of specific axioms and rules, then, since every such provable statement is true, then there must be ‘true’ statements that are not provable – otherwise provable and true would be synonymous. That means that as long as you define true as being different to provable, you don’t actually need Godel's incompleteness theorems to show that there are true statements which are unprovable.
Tarski’s definition of truth assumes that there can be a statement A which is true because there can exist a infinite number of proofs of an infinite number of individual statements that together constitute a proof of statement A  even if no proof of the entirety of these infinite number of individual statements exists. So Tarksi’s proof is basically reliant on a Platonist viewpoint that an infinite number of proofs of infinite number of particular individual statements exists, even though no proof can be shown that this is the case. Whether Tarski’s definition is a clarification of truth is a matter of opinion, not a matter of fact.
This may help: http://www.ditext.com/tarski/tarski.html.
Is it Philosophy or Mathematics? Both?
I think it is Philosophical Question having a Mathematical Response.
This question cannot be rigorously expressed nor solved mathematically, nevertheless a philosopher may "understand" the question and may even "find" the response. This response obviously exists because it can only be YES or NO (and this is a binary mathematical response), unfortunately the correct answer is not yet known. Despite the fact no rigorous argument may lead (even by a philosopher) to discover the correct response, the response may be discovered empirically in say some billion years simply by oberving if all nowadays mathematical conjectures have been solved or not.
I am attonished by how little is known about logic by mathematicians. I am sorry, I dont want to insult anyone, it is just a realisation about the common "metaknowledege" about what we are doing. (This is not the first question that I see here that should be solved in an undergraduate course in mathematical logic)

3$\begingroup$ Dear nickname, I don't believe your assertions are true. There are genuine disagreements about what the foundations of our subject are (e.g. platonic vs. formalistic, to indicate too useful extreme positions, between which many other positions can be usefully plotted.) I don't think that these issues can be resolved by a course in logic. (E.g. I don't think a genuine belief in/disbelief in the existence of the standard model of the natural numbers, or a true settheoretic world, is something that can be decided by mathematical logic alone.) $\endgroup$ – Emerton May 25 '10 at 21:25

3$\begingroup$ But Nickname, perhaps the algebraic geometers here might be equally astonished by how litttle algebraic geometry the average logician knows? My view is that this is a great strength of MathOverflow, that it allows us to learn about other areas so easily and so well. $\endgroup$ – Joel David Hamkins May 25 '10 at 21:29