coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ian Shillito <Ian.Shillito AT anu.edu.au>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] True arithmetical proposition not provable
- Date: Tue, 22 Jun 2021 04:13:34 +0000
- Accept-language: en-AU, en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=3onVR5uGv7g1F1u0lFLtdoUqFKjHnGqvHYu5kJnZ3n4=; b=GDCbcc9RLObDhLQLj4YgepGBEV14PXd0KcRZkwhbs6W3hpeoDyQuPxBnigCn3Q19lnTilihqEwrkbDxrpBP0wR7H4nGSAi7+4UtBEWR7Pm/go8NybRYudG6+L4Z0ELR3GeBvirIMmEgLeWMjQB1q/OTrOaGG/xC2eflFBUUrWzFMQDEgdkNdPpwR2993fG0FVOc+PFWLHYOOQLt9WNEUNcNYCacanybQOvVObPelhktcbZnxlYkmoMQqkugicCrPOfP/ZN7ffqa8sOcktcvy7sG0jgyEiAa7JqUbVUDPdd/W97/+SOlXu3x3azPVpLI5vF+0zydzD+i4ld/1LQREUA==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=JmQyqxCCCBNatLdN2BBu/0HO8v6duvAf10Alafi9wlJq0dl6yHMd7Sm5XEwwhZtXlOn5mvYCsEahbCbOfKyFAP2TSjU6Ahd04nz9Kgcp0Fqr+F1W0Nzy/G4i3F6r633z2nr4gR/ztYW3BZ/IytEIVJVBFZZGRkMVuAT9+lk0P266fwUVd2lw9cyPXrJml7E9xD9bCYxuQNpUgGRLhWLym9DO8+v2dVggYEa6XNzeGbmuFC3gLwP7AU13ECuL6zKoQJMMhPahz5MqzYEkC0XTC6VvN3ygn5wP4hpPWil9e0dM8yLZ3olxvASGt15h+K1tCQyBclk/rszSEvX3qqLmLg==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Ian.Shillito AT anu.edu.au; spf=Pass smtp.mailfrom=Ian.Shillito AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY4-obe.outbound.protection.outlook.com
- Ironport-hdrordr: A9a23:g5XzA6+xzLUzmHRZVphuk+DnI+orL9Y04lQ7vn2ZKCY/TiX8raqTdZsgpHvJYVoqOU3I4OrwXZVoIkmskqKdg7NhX4tKNTOO0FdAR7sSjrcKrQeBJ8QrzIFg/JYlWa1/BNrsZGIXsS+D2mSFOudl/92b+MmT69vj8w==
- Ironport-phdr: A9a23:Ctf9JB34Hr5w9gV8smDO3AMyDhhOgF0UFjAc5pdvsb9SaKPrp82kYBWOo64x1BSRAs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsiq0+2+4ZPebgpUiDayfb9/Lgi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHKTA37X3XhMJzgqJVoh2hpgBwzIHPbY6PKPZyYrnQcc8GSWZcWMtaSixPApm7b4sKF+cPPvxXr4/grFUTrRu+BA2sBOfuyj9UgX/9wKo33ec7HgHAxgAuAtIOsHXQrNXxNacSTee1wbLSwjXFcvNawyny55XVchw7u/6MQKt9fMzMwkYgCw3LlE+fqZD5PzyLzOQNtXCW4/RgWO+hlmMqtgJ8riSgy8oji4TEhYEYx17K+Ct5wIg4JtO1RkF1b9O6DZZduC6UOo95T80iR2xlujo3x6AEtJO9YSMEy4wnygbQZvCbaYSE/w7vWeSLLTtlmH5oeqiziwuu/US90uHxWcm53ExUoidKkdTArHIA2h7J5sSZVvdw8V+t1SiO2gzP5OxJJF04mbbHJJMgx7M8i4YfvEHeEiL2hUr7iaqbelgq9+Wu9u/peK/ppoWGOI9xkgz+Mrohmsi4AekgLgUBUXWV9fih2LH64EP2QrpHguQxkqbCrp/WP8MbprOlAwBO1YYj9hC/ACq83NQAh3kHK05FdwybgIj1OlHOJ/b4Ae24g1SxjDdrw/fGPrriApnXMnfDl7Lhca58605a1gUz0chS6p1IBr0bPf7/Rk38uMbFAhMlMQG42fvrBMlg2o8GXGKAGK6ZMKfcsV+S4eIvJvGBaowPtzb7MfQr+v7ujX49mV8ZfKmpwZwXZWuiEfRgPkWVe2TjjcocEWsQpAU+UfTmiEeeXj5Le3ayQ6U86yknB4KhFIfPX5yigLic3CigBZBWfWBHClWUEXjybYmEWvEMaDiTIsB7iDAEW6KhGMcd0kTkvwjjjrFjM+D8+ysCtJul2sI/r7nYkgh3/jhpBeyc1XuMRid6hDVbaSUx2fVeqEo18VeC1ax5n/sQQf1a4bVyUgY+MZ/AyMRzDc20Vw7cON6UHgX1Cu66CC08G4pii+QFZFxwTo3KZv/r1iy3RbIZivqCGc5tmko593H3OoBwx2uA3bRz1zHOo+NmCFb+3+tExlSWAITE1UKEi6ytaKIQmjbX83uOxnaPu0ceVxNsVaLCXjYUYU6E9LzE
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
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.
- A language --- The logical and non-logical symbols that make up "formula"s)
- 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.
- 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).
- [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/19/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Pierre-Marie Pédrot, 06/19/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Anders Lundstedt, 06/20/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Marco Servetto, 06/20/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Christopher Ernest Sally, 06/21/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Ian Shillito, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Christopher Ernest Sally, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Ian Shillito, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Christopher Ernest Sally, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Ian Shillito, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Peter LeFanu Lumsdaine, 06/21/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vedran Čačić, 06/21/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Xavier Leroy, 06/21/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Peter LeFanu Lumsdaine, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vedran Čačić, 06/21/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Christopher Ernest Sally, 06/21/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Marco Servetto, 06/20/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Pierre-Marie Pédrot, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Andrei Popescu, 06/22/2021
- [Coq-Club] Tacit implications in Goedel's theorems II – Re: True arithmetical proposition not provable, Ken Kubota, 06/23/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Vincent Semeria, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Pierre-Marie Pédrot, 06/22/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Anders Lundstedt, 06/20/2021
- Re: [Coq-Club] True arithmetical proposition not provable, Pierre-Marie Pédrot, 06/19/2021
Archive powered by MHonArc 2.6.19+.