[TYPES] What's a program? (Seriously)

[Hendrik Boom]

On Tue, May 18, 2021 at 10:51:56PM +0100, Martin Escardo wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> 
> On 18/05/2021 22:18, Talia Ringer wrote:
...
...

> > 
> >  What makes it more specific? In my mind, you can certainly view any
> > program in any language as a proof in some logical system, even if the
> > logical system is not actually implemented as the language's type
> > checker, and even if the corresponding logic is unsound.
> > A proof in an
> > unsound logic is still a proof, I think---just a possibly useless one
> > (possibly useful, though, since you can have incorrect assumptions and
> > still sometimes prove things that in no way rely on them).
> 
> I am not sure I understand this, but I would be willing to discuss it to
> clarify it.

Example of a useful inconsistent logic.  Useful only if used properly, 
of course, but it leaves it to the user to determine wnat is proper.

Take a usual univers-hierarchy type theory, one with u0 : U1, U1 : U2 an 
so forth.
How far to follow that hierarchy?  Two levels? an infinite sequence?  
Index the U's with all the ordinals:

There are always limits on expressing things that generalise over 
universes.

The obvious thing to do is to introduce a type of all universes, and to 
consider it a universe.

U : U

Of course, that's inconsistent.

But it allows you to take any type to index universes by using a 
constant function that always returns U.

And then you'll be able to construct any infinite herarchy you want.  
You could even make a reasonable one and prove its reasonable 
properties.

Afterward, you can use this hierarchy consitently as long as you forget 
you ever had U : U lying around, because using U : U directly can lead 
to trouble.

-- hendrik