The Coq mailing list

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

Dear Christopher,

Before answering let me clarify some vague elements of my first email.

Completeness of a proof system with respect to a semantics (meaning n°1) is usually restricted to logics (i.e. defined by a proof system). Another terminology used is "adequation": a proof system is adequate with respect to a semantics.

The other type of completeness (meaning n°2) can be applied to any theory, defined as a set of expressions closed under logical consequence. Consequently, this meaning of completeness can be applied to logics (after all a logic is a set of expressions closed under logical consequence), and theories which are not logics (e.g. contain non-logical axioms).

Though I would not quite say that the former is "for logics" and the latter "for theories", as surely his completeness theorem shows that first-order theories are semantically complete?

I would rather say that the completeness theorem you mention is still about first-order classical logic. It says that for any theory T and sentence A, we have that if T |= A then T |- A. So, the proof system of first order classical logic is adequate. Sometimes we use the notion of strong completeness (T |= A => T |- A) in contrast to weak completeness (|= A => |- A). So, we could speak of strong and weak adequation.

In this light, the incompleteness theorem is not talking about the strong or weak adequation of first-order classical logic, but about the completeness of a (recursively axiomatisable) theory T which is consistent and an extension of the theory Q (Robinson's arithmetic): there is a formula A s.t. it is neither the case that T |- A nor the case that T |- NOT A.

The way you can link this to the semantics is that in the standard model for arithmetic (i.e. the natural numbers) A is either true or false. So, intuitively speaking the standard model "can tell" whether A is true or not, while the theory T cannot.

Hope that makes sense.

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: Tuesday, 22 June 2021 12:54 PM
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] True arithmetical proposition not provable

 

Dear Ian

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

You are quite right; somehow I got turned around and said that the incompleteness theorems talked about semantic completeness, when of course they talk about syntactic completeness. Mea culpa. Though I would not quite say that the former is "for logics" and the latter "for theories", as surely his completeness theorem shows that first-order theories are semantically complete?

And yes, Logics don't make Theories, we want to have interesting things to talk about, like sets or naturals; but there, I was being imprecise on purpose.

 

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