The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

I'm quite ignorant and confused too.
In particular, what does it mean for a statement to be true without
being provable?
That is,
-we have a sound starting system:
    There is no proof of true=false
-our starting system is incomplete:
    There are predicates P where there is no proof for  P and there is
no proof for !P.
-Question:
    Is it always the case that for all such statements P if we add P
or !P to our starting system we still obtain a sound system?
If so, what does it even mean to be 'true' if you are not provable,
since I can still get a sound system by adding either P or !P?

Marco.