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

statement).

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.

317-346.

**REINHARDT**W.N.,

**1986**,

*Epistemic Theories and the Interpretation of Gödel's*

Incompleteness Theorems, Journal of Philosophical Logics, 15, pp. 427-474.

Incompleteness Theorems

(From Conscience and Mecanisme, where I make the case that some

form of comp are *absolutely* undecidable).

Bruno