Re: topos logic arising nicely
I don't know Isabelle too well BUT in Higher Order Logic one may well assume inhabitedness of all types when these are built up from N (and 1) via x,-> and P(-). In higher order logic one cannot form subtypes in the logical sense and that's the only way how one can build types that aren't inhabited. Of course, even if type sigma is inhabited from (1) \forall x:\sigma. A(x)->B one must not conclude (2) \exists x:\sigma. A(x) /\ B BUT only (3) \exists x:\sigma. A(x) -> B BTW concluding (2) from (1) is false also classically. Thomas
Thomas Streicher wrote:
In Higher Order Logic one may well assume inhabitedness of all types when these are built up from N (and 1) via x,-> and P(-). In higher order logic one cannot form subtypes in the logical sense and that's the only way how one can build types that aren't inhabited.
That may be the only way that one can *construct* such a type, hence the only way that one can *prove* that such a type exists, but how do you know that some unspecified type variable \sigma doesn't refer to an uninhabited type to begin with? The answer will depend on the interpretation, I suppose; some logics simply aren't applicable to some semantics.
Of course, even if type sigma is inhabited from (1) \forall x:\sigma. A(x)->B one must not conclude (2) \exists x:\sigma. A(x) /\ B BUT only (3) \exists x:\sigma. A(x) -> B
Of course. Only with \exists x:\sigma. A(x) will (2) follow. -- Toby
On Tue, 3 Jun 2003, Thomas Streicher wrote:
I don't know Isabelle too well BUT in Higher Order Logic one may well assume inhabitedness of all types when these are built up from N (and 1) via x,-> and P(-). In higher order logic one cannot form subtypes in the logical sense and that's the only way how one can build types that aren't inhabited.
"The neglect of sum types is the root of all evil." Paul
Toby Bartels wrote
That may be the only way that one can *construct* such a type, hence the only way that one can *prove* that such a type exists, but how do you know that some unspecified type variable \sigma doesn't refer to an uninhabited type to begin with? The answer will depend on the interpretation, I suppose; some logics simply aren't applicable to some semantics.
Of course, even if type sigma is inhabited from (1) \forall x:\sigma. A(x)->B one must not conclude (2) \exists x:\sigma. A(x) /\ B BUT only (3) \exists x:\sigma. A(x) -> B
Of course. Only with \exists x:\sigma. A(x) will (2) follow.
Certainly, if you allow type variables then the problem crops up. I don't really see the point why one would like to have type variables unless one can perform constructions with types in a uniform way, e.g. when considering logic on top of system F, system F\omega or even on top of a dependent type theory (possibly with an impredicative universe). I guess that in case of HOL type variables were rather motivated by the analogy to functional languages with their "shallow" polymorphism. The point of my mail rather was that so-called topos logic admits subtype formation, i.e. that {x:A|phi(x)} is a type whenever \phi is a predicate on A. This, of course, allows one to introduce types with undecided inhabitedness. See W.Phoa's Edinburgh lecture notes for a calculus extending HOL with subtypes (or Bart Jacob's book). But I would be surprised if HOL has subtype formation as from a logical point of view subtypes are neither necessary nor convenient. Adding subtypes is only necessary for getting a topos out of a model of HOL. Thomas
Hi Paul,
"The neglect of sum types is the root of all evil."
To some extent this may be true for programming languages (but see recent work of Jim Laird). For logics it is less clear. Actually you mean the empty type, isn't it? Moreover, sunset types are slightly heavier than ordinary sum types. Subset types are rather dependent sum types. Thomas
On Thu, 5 Jun 2003, Thomas Streicher wrote:
Hi Paul,
"The neglect of sum types is the root of all evil."
To some extent this may be true for programming languages (but see recent work of Jim Laird). For logics it is less clear. Actually you mean the empty type, isn't it?
which is the n=0 instance of the n-ary sum connective. So it should be included in even the simply typed setting. Paul
Moreover, sunset types are slightly heavier than ordinary sum types. Subset types are rather dependent sum types.
Dear Steve,
Coincidentally, for quite different reasons I have just been looking at the Fourman/Scott theory as a way to deal with partial functions.
Scott's system for existence and identity is given a Hilbert style presentation, and I suppose - I may be wrong - that that is why Fourman's interpretation makes such heavy use of the higher order structure of toposes. Do you know of any sequent presentations?
I think it is straightforward to give a sequent style formulation of the Fourman/Scott interpretation. BTW one has to take care of inhabitedness of types (in the general case) because variables of type A range over A whereas terms of type A receive there interpretation in \tilde{A}, the partial map clasifier of A. See e.g. Troelstra and van Dalen 2nd Chapter for a traetment of what they call E-logic. Just as example the rules for \forall look as follows \Gamma |- A(x) x \not\in FV(\Gamma) --------------------------------------- \Gamma |- \forall x. A(x) \Gamma |- \forall x. A(x) \Gamma |- t\downarrow ------------------------------------------------------ \Gamma |- A[t/x] where t\downarrow stand for "t defined". What I meant with my remark is that if one allows partial terms then one need not have subtypes. Best, Thomas PS Fourman and Scott exploit higher order aspects already at first order level because \tilde{A} is a subobject of P(A) , namely the subsingletons.
Hi, Thomas Streicher writes: Date: Thu, 5 Jun 2003 13:08:14 +0200 (CEST) Subject: categories: Re: topos logic arising nicely But I would be surprised if HOL has subtype formation as from a logical point of view subtypes are neither necessary nor convenient. Adding subtypes is only necessary for getting a topos out of a model of HOL. I don't know, if I miss the point here. However, PVS has a HOL system with predicate subtypes. And it is _very very_ convenient (because of the predicate subtypes). I don't know if it is a necessity, but the absence of subtypes in Isabelle/HOL leads to a representation of partial functions, that allows you to prove unexpected results. Despite what the Isabelle tutorial says at page 187, you _can_ prove hd [] = last [] (saying that the head of the empy list equals its last element) Bye, Hendrik
Dear Hendrik,
But I would be surprised if HOL has subtype formation as from a logical point of view subtypes are neither necessary nor convenient. Adding subtypes is only necessary for getting a topos out of a model of HOL.
I don't know, if I miss the point here. However, PVS has a HOL system with predicate subtypes. And it is _very very_ convenient (because of the predicate subtypes).
I don't know if it is a necessity, but the absence of subtypes in Isabelle/HOL leads to a representation of partial functions, that allows you to prove unexpected results. Despite what the Isabelle tutorial says at page 187, you _can_ prove
hd [] = last []
(saying that the head of the empy list equals its last element)
thanks for the interesting information; you really pinpoint why subtypes are used in practice, namely for avoiding partial functions; if one wants to avoid subtypes and treat partial functions directly one might use the Fourman/Scott variant of the interpretation of topos logic; an alternative and actually the one common in mathematical practice is to introduce subtypes; however, to do this constructively one is forced to either treat partial functions as single-valued realtions OR to explicitly introduce proof objects as in Martin-Loef type theory; I am pretty certain that in systems like HA_\omega one cannot quantify over partial functions as these subsume prediacte types; but if one has Higher Order Logic already it seems more natural to treat partial functions as single valued relations; quantification over subtypes can then be reduced to pure Higher Order Logic via a straightforward translation (which, however, needs some care as one sees from HOL) Thomas
participants (4)
-
Hendrik Tews -
Paul B Levy -
Thomas Streicher -
Toby Bartels