David Corfield
temporal type theory

Time has usually been considered by logicians to be what is called ‘extra-logical’ matter. I have never shared this opinion. But I have thought that logic had not yet reached the state of development at which the introduction of temporal modifications of its forms would not result in great confusion; and I am much of that way of thinking yet. C.S. Peirce [CP 4.523]

Idea

Since natural language expressions are replete with temporal expressions, it should be possible to use type theory to represent them.

See the relevant section of my modal type theory chapter.

Tests

We ought to be able to express temporal statements, and so see their presuppositions and consequences. E.g.,

It took me two days to learn to play the Minute Waltz in 60 seconds for more than an hour.

Ever since he met her for the first time, he could not stop thinking about her and kept calling her several times every night until she would give him a brush-off, and then after being silent for a while he would phone again.

At the exact moment in which the train passes over the sensor, the rail crossing bar starts to close; the bar will start to open again a while after the train passes over the second sensor.

Formalism

Use an internal construction to model time: poset, tree, category. See nLab: Temporal Logic in Terms of Adjoints.

No syntactical way to pick out slice categories.

The operators FF, PP etc. are applied to time-dependent types, including propositions.

It is possible to specify a temporal type theory in the context of adjoint logic. Consider a category 𝒞\mathcal{C}, and an internal category given by b,e:Time 1Time 0b, e: Time_1 \rightrightarrows Time_0. Here we understand elements of Time 1Time_1 as time intervals, and bb and ee as marking their beginning and end points. We may choose to impose additional structure on TimeTime, e.g., that it be an internal poset, or a linear order.

Now each arrow, bb and ee, generates an adjoint triple, e.g., bb * b\sum_b \dashv b^{\ast} \dashv \prod_b, formed of dependent sum, base change, dependent product, going between the slices 𝒞/Time 0\mathcal{C}/Time_0 and 𝒞/Time 1\mathcal{C}/Time_1.

Then we find two adjunctions be * eb *\sum_b e^{\ast} \dashv \prod_e b^{\ast} and eb * be *\sum_e b^{\ast} \dashv \prod_b e^{\ast}, e.g.,

Hom( be *C(t),D(t))=Hom(e *C(t),b *D(t))=Hom(C(t), eb *D(t)). Hom(\sum_b e^{\ast} C(t), D(t)) = Hom(e^{\ast} C(t), b^{\ast} D(t)) = Hom(C(t), \prod_e b^{\ast} D(t)).

Now consider for the moment that CC and DD are propositions. Then be *C\sum_b e^*C means “there is some interval beginning now and such that CC is true at its end”, i.e. FCF C; while eb *D\prod_e b^*D means “for all intervals ending now, DD is true at their beginning”, i.e. HDH D. Hence our adjunction is FHF \dashv H. Similarly, interchanging bb and ee, we find PGP \dashv G. Note that we don’t have to assume the classical principle Gϕ=¬F¬ϕG\phi = \neg F\neg \phi and Hϕ=¬P¬ϕH\phi = \neg P\neg \phi.

In the setting of dependent type theory, we do not need to restrict to propositions, but can treat the temporal operators on general time-dependent types. So if People(t)People(t) is the type of people alive at tt, FPeople(t)F People(t) is the type of people alive at a point in the future of tt, and GPeople(t)G People(t) is a function from future times to people alive at that time, e.g., an element of this is ‘The oldest person alive(t)’.

Since TimeTime is a category, we have in addition to the two projections p,q:Time 1× Time 0Time 1Time 1p,q:Time_1\times_{Time_0} Time_1 \to Time_1, composition c:Time 1× Time 0Time 1Time 1c:Time_1\times_{Time_0} Time_1 \to Time_1. This allows us to express more subtle temporal expressions, such as ‘ϕ\phi has been true since a time when ψ\psi was true’, denoted ϕSψ\phi S \psi.

ϕSψ:=Σ e(b *ψ×Π c(ep) *ϕ)\phi S \psi := \Sigma_e (b^* \psi \times \Pi_c (e p)^* \phi)

(note ep=bqe p = b q). That is, there is a subinterval ending now such that ψ\psi was true at its beginning and ϕ\phi was true at all points inside it. Similarly, ‘ϕ\phi will be true until a time when ψ\psi is true’ is

ϕUψ:=Σ b(e *ψ×Π c(ep) *ϕ).\phi U \psi := \Sigma_b (e^* \psi \times \Pi_c (e p)^* \phi).

Temporal logicians have debated the relevant advantages of instant-based and interval-based approaches. Some have also considered hybrid approaches (Balb11). The analysis of this section suggests that working with intervals and instants together in the form of an internal category allows for a natural treatment via adjoint logic?.

An important construction in interval-based temporal logics is the chop operator, CC. This applies to two interval properties, α\alpha, β\beta, so that αCβ\alpha C \beta denotes the property of an interval that it may be divided into two sub-intervals such that α\alpha holds of the first and β\beta of the second. In our current framework we have αCβ:Σ c(p *α×q *β)\alpha C \beta : \equiv \Sigma_c(p^{\ast}\alpha \times q^{\ast} \beta).

One of the consequences of taking TimeTime as an internal category is that the future includes the present, so that ϕ\phi could be true now and at no other instant but we would have that FϕF \phi is true when it is supposed to say “ϕ\phi will be true at some Future time”. Similarly, we would have that ϕUψ\phi U \psi holds now if ψ\psi and ϕ\phi both hold now (in general, as defined above it requires ϕ\phi to still hold at the instant when ψ\psi becomes true).

If we wish to change these consequences, we could let Time 1Time_1 be the <\lt-intervals instead of the \le-ones. In other words, we could take TimeTime to be a semicategory. While this accords with standard practice, the original alternative has been proposed:

The most common practice in temporal logic is to regard time as an irreflexive ordering, so that “henceforth”, meaning “at all future times”, does not refer to the present moment. On the other hand, the Greek philosopher Diodorus proposed that the necessary be identified with that which is now and will always be the case. This suggests a temporal interpretation of \Box that is naturally formalised by using reflexive orderings. The same interpretation is adopted in the logic of concurrent programs to be discussed. (Gold92, p. 44)

On the other hand, some temporal logicians look to represent both forms of ‘henceforth’.

Consider a particular time n:1T 0n: 1 \to T_0, then N=n *:H/T 0HN = n^{*}: \mathbf{H}/T_0 \to \mathbf{H}, B(t)B(n)B(t) \mapsto B(n).

So, e.g., NPϕ(t)N P \phi(t) means ‘ϕ\phi was the case at some time before nn’. Often we rely indexically on now. In which case we use the straight past.

Uttering things at a time makes no difference if the utterance is not being actualised indexically at the moment now. So I can say ‘2+2 = 4’. This is already ‘saturated’, i.e., a time-independent proposition.

‘Caesar stormed Bigbury in 54 BC’ implies ‘Caesar stormed Bigbury’.

What is it as P of something? PC(t)= eb *C(t)P C(t)= \sum_e b^*C(t)

P(Caesar storms Bigbury)(t) = Occasions on which Caesar stormed Bigbury prior to(t)

Truncate ||P(Caesar storms Bigbury)(t)|| = That Caesar stormed Bigbury prior to (t)

Apply N: Caesar stormed Bigbury in the past of n

One way: ‘54BC is a time in which Caesar stormed Bigbury’ implies ‘there was a time at which Caesar stormed Bigbury.’

(54BC,a):( eb *(CaesarstormsBigbury))(n)(54 BC, a) : (\sum_e b^*(Caesar\;storms\; Bigbury))(n) (where a: Caesar storms Bigbury in 54 BC) entails

|(54BC,a)|:||( e(b *(CaesarstormsBigbury))(n)|||(54 BC, a)|: ||(\sum_e (b^*(Caesar\; storms \;Bigbury))(n)||

So why not a tt-dependent form

t:T 0( eb *(CaesarstormsBigbury))(t)||( e(b *(CaesarstormsBigbury))(t)||t: T_0 \vdash (\sum_e b^*(Caesar\;storms\; Bigbury))(t) \to \vert \vert(\sum_e (b^*(Caesar\; storms \; Bigbury))(t)\vert \vert

Does ||A(n)|| = ||N A(t)|| = N||A(t)||?

How do P, N and || || interact?

NPA(t)=(PA)(n)N P A(t) = (P A)(n), but PNA(t)P N A(t) is not well formed.

Reasonable to think there is an implicit time index in any temporal statement. We ask ‘When was that written?’ Before there was a dating system, we must have said ‘C so many days ago’.

Caesar stormed Bigbury 2074 years ago(t)

Map d:T 1Rd: T_1 \to R (or non-negative reals) measuring duration in years.

e(d *(2074)&b *(CaesarstormsBigbury))(t)\sum_e (d^*(2074) \& b^*(Caesar\;storms\; Bigbury))(t)

Jennan Ishmael, Passage Flow, and the logic of temporal perspectives.

Lowe More kinds of Being

Last revised on June 22, 2021 at 03:55:30. See the history of this page for a list of all contributions to it.