Re: topos logic arising nicely

Re: topos logic arising nicely

[Thomas Streicher]

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

Re: topos logic arising nicely

[Hendrik Tews]

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

Re: topos logic arising nicely

[Thomas Streicher]

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

Re: topos logic arising nicely

[Thomas Streicher]

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.

Re: topos logic arising nicely

[Paul B Levy]

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.

Re: topos logic arising nicely

[Thomas Streicher]

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

Re: topos logic arising nicely

[Paul B Levy]

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

Re: topos logic arising nicely

[Toby Bartels]

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

Re: topos logic arising nicely

[Thomas Streicher]

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