[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
