The Coq mailing list

[Ian Shillito <Ian.Shillito AT anu.edu.au>]

Some remarks about the terminology.

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.​

There are two notions of completeness: one for logics and one for theories. The one you describe Christopher is the one for logics. However, the one Vincent mentions is the one for theories. The latter notion is the notion of completeness dealt with in Gödel's incompleteness theorems. 

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

​I disagree here. The incompleteness theorems are not about logics but about theories. A logic can be conceived of in an axiomatic way as a set of axioms and a set of rules that are expressed using only logical connectives and formula-variables. (Formal) theories are formed using an additional set of axioms involving non-logical symbols (relation symbols like =, function symbols like +, constant symbols like 0). 

What the first incompleteness theorem states is: if a theory T is consistent and is an extension of (the formal theory of) Robinson's arithmetic, then T is not a complete theory (i.e. there is one formula F such that neither F nor its negation is a logical consequence of T).

Best,

Ian​

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Christopher Ernest Sally <christopherernestsally AT gmail.com>
Sent: Monday, 21 June 2021 9:21 AM
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] True arithmetical proposition not provable

 

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).