Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: (temporal TT) are decidable predicates on Time trivial?

Roman Kniazev (Jul 29 2021 at 16:47):

My question requires some familiarity with "Temporal Type Theory" book link to arxiv version.
In section 8.6 of the book, one can find some information on how one can relate the type theory of the book with "standard" temporal logics, such as LTL or MTL. The relation is an embedding of LTL (or rather its first-order incarnation FO(<)) into the type theory. In order to do this, we represent atomic propositions/unary predicates as terms $P: Time\to \Omega$. The problem is that we cannot simply rewrite formulas as in image.png

as it would not be sound for classical LTL (in opposition to some version of intuitionistic temporal logic). One way to avoid this problem is, first, to use double negation, i.e. to represent Until as image.png

and, second, to consider only decidable predicates $P:Time\to\Omega$.

My question concerns exactly this part about decidable predicates. We can say that a predicate is decidable when (in this particular case) $P:Time\to\Omega$ factorizes as $Time\to 2\to\Omega$. I am afraid I severely misunderstand something, but I cannot come up with a non-trivial example of such a predicate. It even seems to me that any such map $Time\to \Omega$ is trivial, i.e. either corresponds to a minimal or maximal subobject of $Time$. The reason is that if $P$ is not trivial, then there is a section $(d,u)\in Time(l)$ such that $P((d,u))$ is neither completely true nor false (that is $P$ is not decidable), even if it is on some restrictions.
So the question is: am I missing something here? Or such predicates are indeed trivial?

Roman Kniazev (Jul 29 2021 at 16:48):

I hesitated about posting this question to #theory: topos theory or to #theory: type theory, so I ended up here. Feel free to move it to some other stream

James Wood (Jul 30 2021 at 07:48):

I'm not familiar with the topic, but I'd guess that $P$ can capture free variables. So you're not dealing with just $\vdash P : \mathtt{Time} → Ω$, but rather $Γ \vdash P : \mathtt{Time} → Ω$, and those $Γ$ could contain types dependent on time or other more interestingly decidable things.

Morgan Rogers (he/him) (Jul 30 2021 at 10:49):

Roman Kniazev said:

It even seems to me that any such map $Time\to \Omega$ is trivial, i.e. either corresponds to a minimal or maximal subobject of $Time$. The reason is that if $P$ is not trivial, then there is a section $(d,u)\in Time(l)$ such that $P((d,u))$ is neither completely true nor false (that is $P$ is not decidable), even if it is on some restrictions.
So the question is: am I missing something here? Or such predicates are indeed trivial?

Time is defined as the sheaf $\mathrm{Time}(\ell) = \{(d,u) \in \mathbb{R}^2 \mid u - d = \ell\}$, with restriction mapping $\langle r,s \rangle ((d,u)) := (d+r,u-s)$ (recalling that we require $\ell,r,s \geq 0$!). I was going to say that we can easily have a non-trivial complemented subobject $U \hookrightarrow \mathrm{Time}$, but it's a little trickier to find them than I instinctively thought...