I think this clarifies things a little. My original way of writing what I
interpreted the incompleteness theorem to be was to say that there exist (in
sufficiently complex axiomatic) systems in which there are true propositions
without proof. I think that this is misleading on reflection. It is more
accurate to say that there exist in complex axiomatic systems (like, for
example, arithmetic) propositions (or well formed formulae) that cannot be
proved either true nor false, that is, which are undecidable.
Such propositions do have a truth value - the law of the excluded middle
still holds - so, being reasonable we have to assume that there do indeed
exist statements that are true but unprovable.
You should say: unprovable ... *by the system in question*
Let us call S the system in question (S for some consistent System).
Godel's proof entails that there are true proposition P that S cannot prove.
This means also that if you add P as axiom to S, you will not get a
contradiction (if not, S would prove the false statement "not P"), this means
that S+P is (another) consistent system S'. And, obviously S' can prove P,
because P is an axiom for S' so that S' proves it in one line.
The other half of this way of
speaking is to say that 'there also exist false statements that are
unprovable' (but this, technically - is quite redundant as proving a
statement is false is the same as proving as true the negation of that same
Does this make sense?
Sure. But when you talk about a non provable proposition, you should
always mention who (or which system) cannot prove it.
Godel really has shown that formal provability is a relative notion (relative
to the system considered). This is in total contrast with formal
computability which seems to be an absolute notion not depending on any
system (and that's the basic conceptual motivation for Church Thesis).
As I said in another post, there is a case for *absolutely undecidable*
statement. But this is trickier and is related to some formalization of
"informal provability". If you are interested look at the reference:
REINHARDT W.N., 1985, Absolute Version of Incompleteness Theorems, Noûs, 19, pp.
REINHARDT W.N., 1986, Epistemic Theories and the Interpretation of Gödel's
Incompleteness Theorems, Journal of Philosophical Logics, 15, pp. 427-474.
(From Conscience and Mecanisme, where I make the case that some
form of comp are *absolutely* undecidable).