Re: A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

Re: A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

[james...]

[-- Attachment #1.1: Type: text/plain, Size: 3750 bytes --]

Just a comment on this:

This is one of the reasons why I have some problems to trust proofs of 
> properties of natural numbers formalized in CIC : Are some people “proving” 
> properties of natural numbers that are already assumed in order to define 
> CIC ?
>

This is a general foundational problem, which exists even for first-order 
logic. It is impossible to avoid circularity entirely in foundations.

There are models of ZFC which have a non-standard version of the natural 
numbers (easy to construct by compactness theorem, if we really believe ZFC 
is consistent). Let's pick such a model V*, and this non-standard version 
of the natural numbers N*. Then inside V*, it evaluates to true that ``N* 
embeds into every other model of PA, and every model of PA which embeds 
into N* is isomorphic to N*". From outside V*, however, we see that the 
standard natural numbers, N, embeds into N*, but is not-isomorphic to N*. 

What this means is that the statement "I am (isomorphic to) the standard 
natural numbers" is not absolute over all models of set theory.

But the natural numbers are used to define such primitive notions as 
"string", "formula", and "language". This means that, depending on what 
ambient model of set theory we are working in, the "set of first order 
fomulas in the langauge of (0,1,+,x)" is not absolute. Different ambient 
universes will disagree over whether something counts as a formula. From an 
outside perspective, V* has formulas which look to us to be 
infinite-length. But V* sees them as having finite length, generated by 
only finitely many applications of logical operations.

For example, there are well-formed terms in V* which look like 1+1+1+...  
...+1+1+1+...  ... +1+1+1+...   ...+1+1+1+1+... ...+1+1+1+1, where there 
are infinitely many 1's appearing here. This means that if you were to look 
at the "models of PA" in V*, *all *of them would be non-standard from our 
outside perspective, because they would all have to interpret the term 
1+1+1+...  ...+1+1+1+...  ... +1+1+1+...   ...+1+1+1+1+... ...+1+1+1+1. So 
definitions like "the initial model of PA" won't work like we expect in V*.

This means if we hoped to somehow use first-order logic to pin down the 
natural numbers, we find ourselves not even being able to pin down the 
language of arithmetic. We cannot define the language of arithmetic without 
first defining something like the natural numbers, and we cannot define the 
natural numbers without defining something like the langauge of arithmetic. 

How do set theorists fix this in practice? Well, they restrict to focus 
only on what are known as "transtive" models of set theory. To do this, 
they essentially need to fix a "standard" model of set theory, V, and then 
only look at models of set theory which, roughly, agree with V about the 
element-of relation. But if we were skeptical about fixing a standard model 
of the natural numbers, we surely should be skeptical about fixing a 
standard model of set theory, as this is much stronger.

Another fix is to move to second-order logic. But this is basically the 
same as fixing a standard model V of set theory, which again is much 
stronger (thus philosophically less justified) than just fixing a standard 
model of PA.

Whenever you have inductive types, you are of course in the background 
assuming that you have a standard model N of arithmetic. Because if you 
don't assume this, then it is ambiguous what the initial model should be, 
or even what counts as a model at all. 

One of the lessons from Godel should be that there is no way of removing 
this ambiguity which does not itself introduce more ambiguity.

James Moody



[-- Attachment #1.2: Type: text/html, Size: 4075 bytes --]

Re: [HoTT] Re: A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

[Andrej Bauer]

I doubt much can be added to a discussion of "using natural numbers
before defining natural numbers" on this list, but just because this
list if about type theory, let me point out two things.

1. Various worries about non-standard natural numbers and lack of
absolute definitions are an artifact of first-order logic and the
insistence that natural numbers be defined on their own, without
reference to anything at all. As soon as one realizes that the natural
numbers can be characterized by a universal property within a larger
universe (either as an initial algebra in a category, or a type with a
suitable elimnator in type theory), the mystery goes away. Within any
universe of mathematics, the natural numbers are unique up to unique
isomprphism. And since there are many universes of mathematics, it is
not suprising that we see many incarnations of natural numbers. But
each one first perfectly and uniquely in the ambient in which it
lives. (In case this isn't clear, the non-standard models of PA
constructed with ultrapowers are just normal natural numbers objects
in an ultrapower model of set theory).

2. The idea that there can be no natural numbers before we define
natural numbers, as well as statements such as "it is impossible to
avoid circularity in foundations" arises from mistaken and unrealistic
expectations that it is the task of the foundations of mathematics to
provide something out of nothing. I explain to myself the yearning for
such foundations from the fact that the human psyche is comforted by
an illusion of absolute security. I have written about this on
Mathoverflow (https://mathoverflow.net/a/23077/1176).

With kind regards,

Andrej

Re: A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)

[Russell O'Connor]

[-- Attachment #1.1: Type: text/plain, Size: 4771 bytes --]

The claim that Coq proves PA is consistent, is formally speaking, simply a 
statement that a particular type (on line 18 of PAconsistent.v 
<https://github.com/coq-contribs/goedel/blob/c3f922cd5cf2345e1be55ba2ec976afcdc6f4b13/PAconsistent.v#L18>) 
is inhabited.  You can chase the definitions used in constructing that type 
through folProof.v 
<https://github.com/coq-contribs/goedel/blob/a232fade79805c9339aaa4ec2c641723095e2c4e/folProof.v#L109> 
and so forth.

How you choose to interpret the fact that this type is inhabited is up to 
you.  However, since we are dealing with type theory here, I might suggest 
that there is at least one obvious interpretation, which is that this 
inhabitant is a pair of a value of type Formula (which in this case is the 
Formula (notH LNT (equal LNT (var LNT 0) (var LNT 0)))) and a typed 
function.  The typed function is such that if you ever fulfill its 
argument, it will produce a value belonging to an empty type.

I believe the description of this value as a "proof of the completeness of 
PA" is a fair description, and if you dislike that description that you are 
welcome to analyze the type and its inhabitant and come up with a better 
description of what it means.  That said, proving the consistency of PA is 
hardly supernatural and is, in fact, a fairly pedestrian result by today's 
mathematical standards.  As Carl Mummert notes on stack exchange 
<https://math.stackexchange.com/a/56117>:

There are (at least) three proofs of the consistency of PA that are 
> important: 
>    
>    - 
>    
>    The proof in ZFC, which proceeeds by just verifying that N is a model 
>    of PA. 
>    - 
>    
>    The proof by Gentzen. Here consistency is proved in a much weaker 
>    theory than ZFC (but of course the theory is not included in PA). 
>    - 
>    
>    The proof by Gödel using what is now called the *Dialectica* 
>    interpretation. This proof uses a completely different method than 
>    Gentzen's proof, but obtains the same result. It is also conducted in a 
>    weak system, but a different weak system than Gentzen's proof. 
>    
> The consistently of PA isn't a magical result; it is a well studied 
theorem that is equivalent to a combinatorial problem that roughly states 
that there is always a strategy to win at the Hydra game 
<https://www.youtube.com/watch?v=uWwUpEY4c8o> (see Laurie Kirby and Jeff 
Paris. "Accessible independence results for Peano arithmetic"). (Turns out 
that it is the case that every strategy wins the Hydra game.)


The paper "Essential Incompleteness of Arithmetic Verified by Coq" isn't 
novel for its mathematical result. No one doubted that the consistency of 
PA could be deduced in Coq in principle.  The only novel result of that 
paper is that such a deduction could be carried out in practice (arguably 
even this isn't all that novel of a result either).


I also want to point out that proving that PA is consistent doesn't by 
itself mean that there isn't a proof that PA is inconsistent.  To go from 
the existence of a deduction of some sentence S in some formal system T to 
the claim that S is actually true relies the assumption that the formal 
system T is sound, and to go from the existence of a deduction of some 
sentence S in some formal system T to the claim that there is no deduction 
of ¬S in T relies the assumption that the formal system T is consistent.  
In our case S is the sentence that "PA is consistent" and T is Coq.  I 
don't explicitly claim that Coq is consistent as a logic.  Of course the 
same issue holds for deductions in ZFC; however mathematicians don't 
generally go around prefacing every mathematical paper with a note saying 
that "this result of our deduction is only true under the assumption that 
ZFC is sound", although perhaps we should. ;)


I personally think there are good reasons to believe Martin-Lof style type 
theory (which I mean to cover systems such as CIC) is consistent.  If we 
believe that Coq is normalizing then of course we cannot provide arguments 
to the function defined as the second component of the value that denotes 
the proof of the consistency of PA.  Otherwise we could execute said 
function and normalize it to produce a constructor of the empty type, and 
there are no such constructors.  The argument that terms in type theory are 
normalizing and amounts to another combinatorial problem that is going to 
be equivalent to finding a winning strategy against a hydra that is even 
more difficult to slay than Kirby and Paris's hydra.


You can prove Martin-Lof type theory is consistent using ZFC, and you can 
prove CIC is consistent using ZFC with some large cardinal assumptions.

[-- Attachment #1.2: Type: text/html, Size: 6127 bytes --]