The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

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

I take it you mean that we cannot prove False (the Prop) in Coq. This makes the system "consistent" not "sound".

-our starting system is incomplete:
    There are predicates P where there is no proof for  P and there is
no proof for !P.

This doesn't not make the system incomplete, it just means there are Props that are "independent" of it.

The issue is that a Logic (typically) defines three things.

1. A language --- The logical and non-logical symbols that make up "formula"s)
2. A semantics --- A subset of formulas, or a way to calculate a subset of formulas that shall be defined to be "true". For example, the typically, boolean/truth table semantics used from Propositional logic defines P \/ ~ P to be true. The usual intuitionistic kripke semantics for Propositional logic does not define P \/ ~P to be true. This is usually denoted with the entailment symbol |=. |= usually also talks about what is true, given some other formulas. e.g. {A, B} |= A /\ B. The logic may also define a (possibly empty) set of formulas, which are just taken to be true. These are called axioms.
   
3. A proof calculus --- A set of rules that allow us to derive formulas from others. Formulas that can be derived from the (possibly empty) set of axioms are "provable"/"derivable". This is usually denoted with the turnstile symbol |-
   

A logic's proof calculi is sound, with respect to it's semantics, if a formula P is true whenever it is derivable: |- P -> |= P

A logic's proof calculi is complete, with respect to it's semantics, if a formula P is derivable whenever it is true: |= P  ->  |- P.

The (1st) incompleteness theorem simply states that when you logic gets powerful enough (to encode arithmetic) it cannot be complete.

I don't know if CIC defines a semantics (and would love to hear from someone who does) but the language Prop has a proof calculi but no semantics. So it doesn't quite make sense to talk about the soundness, or completeness of Prop. Though people often worry about it's consistency (for obvious reasons).

At any rate, these are soundness and completeness meta properties of the logic, that is, they cannot be discussed within the logic itself, but must be discussed in more powerful logic "outside" it. If this is confusing, remember that there are concept that Propositional logic can't "discuss", like quantification.

However, I think what the OP was doing was embedding, or modelling a logic (or part of CIC) and trying to give that a semantics (so that it was possible to start talking about these meta properties).