The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

>> [...]  Also no universes, so it cannot be proven that
>> booleans true and false are different.
> Do you have a reference showing the latter point about universes?

The Independence of Peano's Fourth Axiom from Martin-Löf's Type Theory
without Universes. Journal of Symbolic Logic, 53(3), 1988.

This paper shows (Suc n) ~= n is unprovable without universes, for the
same reason as what I said.  If you make the one (consistent)
assumption that true ~= false (Church booleans), you can the prove
distinctness of all constructors of all Church datatypes.

Randy
--
On Tue, May 28, 2013 at 11:47 PM, Harley D. Eades III
<harley.eades AT gmail.com>
 wrote:
> Hi, Randy.
>
> On May 28, 2013, at 2:33 PM, Randy Pollack 
> <rpollack AT inf.ed.ac.uk>
>  wrote:
>
>> If you want to know how the (pure) Calculus of Conctructions works,
>> read the Coquand/Huet paper in EUROCAL '85 (LNCS 203) and
>> Paulin-Mohring's paper in LICS 1986.
>>
>> There are no inductive types, and definition by impredicative
>> intersection gives only "weak" iterators; so no constant time
>> predecessor function.  Also no universes, so it cannot be proven that
>> booleans true and false are different.
> Do you have a reference showing the latter point about universes?
>
> Thanks,
> .\ Harley
>
>>  On the other hand some
>> non-strictly-positive types can be defined impredicatively, although
>> you can't do much with them.
>>
>> Randy
>>
>>
>>
>> On Tue, May 28, 2013 at 12:17 AM, Kenneth Adam Miller
>> <kennethadammiller AT gmail.com>
>>  wrote:
>>> My impression is that the Calculus of Constructions would be something
>>> incredibly valuable to know and be able to wield. Since it was born 
>>> within the
>>> past few decades, I had surmised that it hadn't hit mainstream because the
>>> learning curve is incredibly high and because its so new; are these 
>>> correct?
>>>
>>> Also, when reading the Coq'Art book, I find that there are a number of 
>>> subtle
>>> and even explicit references to the CoC, and I want to be able to 
>>> understand
>>> the CoC fundamentally in order to draw the most out of this book. I 
>>> searched
>>> everywhere for the original publication that was cited in the book, but
>>> couldn't find it available on the open web. Would anybody know where a 
>>> good
>>> set of materials might be, other than the Software Foundations or Coq'Art
>>> book, both of which I already have access to?
>>>
>
>