On the mortality of Socrates

[Henry Story]

Here is a question I posted over at Mathoverflow thinking there would be some knowledge about HoTT there 

http://mathoverflow.net/questions/231152/on-the-mortality-of-socrates 

and that one could start from simple questions and move over to more complex ones.

But it looks like there is not much experience with philosophical logic there.

------

How would one prove the well known syllogism in Homotopy Type Theory:

All men are mortal

Socrates is a man

------------------

Socrates is mortal

All the examples in the HoTT book deal with mathematical objects. But if it is to be a new way to think about logic, then HoTT needs to also be applied to everyday reasoning like the above too. Perhaps the following will do:

∏x (x: Man) Mortal(x)

socrates: Man

---------------

Mortal(socrates)

But given that we also have

chick: Chicken

∏x (x: Chicken) Mortal(x)

-----------------

Mortal(chick)

Since all animals are mortal too, is that well typed? Can Mortal(x) take chicken and humans too?

On page 44 of the HoTT book it says

> A predicate over a type A is represented as a family P : A -> U,

But here we would need something closer to 

Mortal: Animal -> U 

I kind of feel that it would be actually very useful to try out  a bunch of really simple examples like that and collect the answers, as that would help show how thinking in HoTT would work.

[Jon Sterling]

Henry,

First, I will answer your question in terms of Martin-Löf-style type
theory in general, before moving onto HoTT. In any case, the answer to
your question hinges on the specifics of the type theory involved, and
also on the particular definitions of predicates like Mortal(–), and of
types like Man and Chicken and Animal. I stress the importance of being
precise about the definitions of these things—it's not really a matter
of bringing type theory to bear on philosophical logic or everyday
reasoning so much as a much more general question of the meaning of
typehood and membership in type theory.

If your type theory supports subtyping (which is implicitly supported in
Martin-Löf's type theory starting in 1979 and ending in the mid 1980s),
then the Mortal(—) predicate could be an Animal-indexed family of
propositions (types), and your examples would work out fine, assuming
that Man and Chicken are subtypes of Animal.

HoTT as formulated in the book, however, is unlikely to support this
exact kind of subtyping, because this form of subtyping only makes sense
when you have defined typehood in a particular style (which, depending
on your perspective, is either overly intensional or overly
extensional), namely that a type is defined by its elements and by the
equalities of those elements. That was the meaning explanation on which
Martin-Löf's type theory was based, and in that setting, this kind of
subtyping makes sense. In current incarnations of HoTT, however, this
kind of subtyping probably cannot be made to work, because HoTT (hopes
to) takes a more abstract view of the meaning of a type.

Instead, one could imagine a directed version of HoTT (which would be
[conjectured to be] the type theory of infinity-categories rather than
infinity-groupoids); so paths wouldn't necessarily be invertible. In
this case, such a directed path in the universe would be the evidence of
a subtyping relation between two types. Then, as usual in HoTT, you
would have to coerce values across this directed path in order to use
them in the type that lies at the end of it, so the corrected version of
your examples would be a bit noisier.

Hope this helps,
Jon

> --
> You received this message because you are subscribed to the Google Groups
> "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Gershom B]

I agree the immediate way the question is asked seems to require subtyping. But there are plenty of ways to encode this in plain ITT.

In particular, henry asks for

> Mortal: Animal -> U 

But instead take

> Mortal: Sigma(A:U) a.A -> U

for example.

But more realistically one would want man to be not a type but a type family itself I think.

So we have Man classifying types that “are Men"

Man: U -> U

Then Mortal classifies types that “are Mortal”

Mortal: U -> U

And now you have a function

Pi (A:U,ManA:Man(A)). Mortal(A).

And if you did similarly for animals you would have

Pi (A:U,AnimalA:Animal(A)). Mortal(A).

Or something similar. For example we might have. Pi (Sigma(A:U).Man(A)). Mortal(A) instead.

In any case, I think it is important to move “is a” from reading “has type” to instead reading “satisfies a predicate”. We see this pervasively in the HoTT book in fact. A type for example “is a truncated type” or “is a contractable type” or “is a group” but we get this by adding proof structure to the type by means of sigmas, not by denoting it as a “subtype” as such. We can switch to the other perspective by looking only at those “subuniverses” of types that satisfy a given predicate, and the book does this as well.

—Gershom

[Andrej Bauer]

The question is not specific to HoTT as it pertains to type theory in general.

> ∏x (x: Man) Mortal(x)
> socrates: Man
> ---------------
> Mortal(socrates)

The first line contains a syntactic error and should read instead ∏
(x: Man) Mortal(x).

From what you wrote we also have to guess that we have

Man : Type

and

Mortal : Man -> Type

Then what you wrote makes sense.

> But given that we also have
>
> chick: Chicken
> ∏x (x: Chicken) Mortal(x)
> -----------------
> Mortal(chick)
>
> Since all animals are mortal too, is that well typed? Can Mortal(x) take
> chicken and humans too?

Again, you have to write ∏(x: Chicken) Mortal(x) for the syntact to make sense.

Now, if you intend to continue the previous example, then what you
wrote is not well typed because, I am guessing, you meant:

Chicken : Type

and you are still using the same Mortal as before. Therefore, you
cannot apply Mortal to chick as the type of chick is not Man. You
should

(a) either warn us that you suddenly changed Mortal so that its type
is Chicken -> Type, or
(b) call this new Mortal something else, e.g., Mortal'

That is, there is lack of precision in what you are saying. That would
be the first thing to fix before you try to understand what Jon and
Gershom wrote.

You might think there should be a single notion of Mortal. Sure, you
could try that, but whatever you do, first make sure that every symbol
you introduce has a precisely given type, and only that type, and that
you never form invalid terms.

With kind regards,

Andrej

[Henry Story]

On Monday, 15 February 2016 15:26:33 UTC, Andrej Bauer wrote:

The question is not specific to HoTT as it pertains to type theory in general.

> ∏x (x: Man) Mortal(x)
> socrates: Man
> ---------------
> Mortal(socrates)

The first line contains a syntactic error and should read instead ∏
(x: Man) Mortal(x).

yes, silly typo...

 

From what you wrote we also have to guess that we have

Man : Type

and

Mortal : Man -> Type

[snip] 

 

Again, you have to write ∏(x: Chicken) Mortal(x) for the syntact to make sense.

Now, if you intend to continue the previous example, then what you
wrote is not well typed because, I am guessing, you meant:

Chicken : Type

and you are still using the same Mortal as before. Therefore, you
cannot apply Mortal to chick as the type of chick is not Man. You
should

(a) either warn us that you suddenly changed Mortal so that its type
is Chicken -> Type, or
(b) call this new Mortal something else, e.g., Mortal'

That is, there is lack of precision in what you are saying. That would
be the first thing to fix before you try to understand what Jon and
Gershom wrote.

Yes, you correctly interpreted my intention there.

 

You might think there should be a single notion of Mortal. Sure, you
could try that, but whatever you do, first make sure that every symbol
you introduce has a precisely given type, and only that type, and that
you never form invalid terms.

yes, I was thinking of the same notion of mortal for both humans and animals.

 In the semantic web this is helped by every symbol being a URI - a 

Universal/Uniform Resource identifier - which helps create a global web

of data, without name clashes.  

I updated the issue on Mathoverflow so that there is a clear consultable version

 http://mathoverflow.net/questions/231152/on-the-mortality-of-socrates

 

With kind regards,

Andrej

[Henry Story]

> On 15 Feb 2016, at 01:02, Gershom B <gers...@gmail.com> wrote:
>
> I agree the immediate way the question is asked seems to require subtyping. But there are plenty of ways to encode this in plain ITT.
>
> In particular, henry asks for
>
>> Mortal: Animal -> U
>
> But instead take
>
>> Mortal: Sigma(A:U) a.A -> U
>
> for example.
>
> But more realistically one would want man to be not a type but a type family itself I think.
>
> So we have Man classifying types that “are Men"
>
> Man: U -> U

So this would mean that Socrates would be a type.
This is reminiscent of Bertrand Russel's theory of description where
he argued that "The present king of France is bald" should be rendered
as ( see https://en.wikipedia.org/wiki/Definite_description )

∃x[PKoF(x) & ∀y[PKoF(y) → y=x] & B(x)]

Ie. Here PKoF would be the predicate describing the Present King of France,
for which there could or not be an instance.

This is not that dissimilar to having

Socrates: U

In HoTT we would have

PKoF: U

If I try to write the above in HoTT I think I get

Σ(x: PKoF). ( ∏(y: PKoF). (x=y, Bald(x)) )

with

Bald: PKoF -> U

(Except that we want Bald to be a predicate on people, not just on the present king of france)

Anyway, thinking of individuals as descriptions (and so related to concepts - ie. Types -
and this as ways of explaining a-priori reasoning) is not unheard of. Furthermore this idea that concepts relate to descriptions has come back in vogue via 2 philosophers such as Chalmers's work on 2 dimensional semantics in articles such as:

http://consc.net/papers/twodim.html
http://plato.stanford.edu/entries/two-dimensional-semantics/

>
> Then Mortal classifies types that “are Mortal”
>
> Mortal: U -> U
>
> And now you have a function
>
> Pi (A:U,ManA:Man(A)). Mortal(A).

which is interesting because now we have something that is close to first order logic's way of doing things which would be

∀a (Man(a) -> Mortal(a))

Ie we have a universal quantification, that then is restricted via a conditional to a specific subtype. I am thinking here of the note on page 18 of the book:

> Thus, when we say informally “let x be a natural number”, in set theory this is shorthand for “let x be a thing and assume that x ∈ N”, whereas in type theory “let x : N” is an atomic statement: we cannot introduce a variable without specifying its type.

And here we have the same thing: we now have a notion of "let x be a type, and assume it is something for which Man(x) has a value."

>
> And if you did similarly for animals you would have
>
> Pi (A:U,AnimalA:Animal(A)). Mortal(A).
>
> Or something similar. For example we might have. Pi (Sigma(A:U).Man(A)). Mortal(A) instead.
>
> In any case, I think it is important to move “is a” from reading “has type” to instead reading “satisfies a predicate”. We see this pervasively in the HoTT book in fact. A type for example “is a truncated type” or “is a contractable type” or “is a group” but we get this by adding proof structure to the type by means of sigmas, not by denoting it as a “subtype” as such. We can switch to the other perspective by looking only at those “subuniverses” of types that satisfy a given predicate, and the book does this as well.

Thanks, that answer is very helpful.

It may be useful next to formalise this and other answers to simple problems
like that in Coq or other such languages so that I and other beginners like
me can start learning how to use those tools.

Henry

[Julian Michael]

Henry,

I'm afraid coming at things from the perspective of natural language might result in unnecessary confusion because language is itself difficult and complicated and there are many degrees of freedom in how you choose to represent it. But if you think that angle would be helpful for you, it might be a good idea to take a look at the existing literature on using dependent type theory for natural language semantics. Aarne Ranta's book, Robin Cooper's publications, or Zhaohui Luo's project page are all possible starting points.

Best,

Julian

[Henry Story]

I'll reply to a few threads here:

On 16 Feb 2016, at 01:24, Julian Michael <julianjo...@gmail.com> wrote:

Henry,

I'm afraid coming at things from the perspective of natural language might result in unnecessary confusion because language is itself difficult and complicated and there are many degrees of freedom in how you choose to represent it. But if you think that angle would be helpful for you, it might be a good idea to take a look at the existing literature on using dependent type theory for natural language semantics. Aarne Ranta's book, Robin Cooper's publications, or Zhaohui Luo's project page are all possible starting points.

Best,

Julian

Thanks. Very interesting links. 

It looks like it is going to be a bit difficult to get access to Aarne Rank's book.

Robin Cooper's Type Acts, seems intruiging, but I wonder how compatible that is to HoTT's notion that token must have a Type, since there there must be tokens that are not yet typed in that system....

Jon Sterling wrote:

[snip]

If your type theory supports subtyping (which is implicitly supported in
Martin-Löf's type theory starting in 1979 and ending in the mid 1980s),
then the Mortal(—) predicate could be an Animal-indexed family of
propositions (types), and your examples would work out fine, assuming
that Man and Chicken are subtypes of Animal.

Thanks. It's good I asked these questions. As inheritance is part of Scala and as

the syntax of Scala and HoTT are so close, I keep forgetting that inheritance is not

been built into it. 

[snip]

Instead, one could imagine a directed version of HoTT (which would be
[conjectured to be] the type theory of infinity-categories rather than
infinity-groupoids); so paths wouldn't necessarily be invertible. In
this case, such a directed path in the universe would be the evidence of
a subtyping relation between two types. Then, as usual in HoTT, you
would have to coerce values across this directed path in order to use
them in the type that lies at the end of it, so the corrected version of
your examples would be a bit noisier.

thanks.

Gershom wrote:

I agree the immediate way the question is asked seems to require subtyping. But there are plenty of ways to encode this in plain ITT. [...]

But more realistically one would want man to be not a type but a type family itself I think.

Thanks. That'll give me something to think about. 

I'll start trying to see how I can use my intuitions on this from working with Scala's dependent types, and type classes....

Henry