ontology of time. This work aims to make tense logic a more robust tool for ontologists, philosophers, knowledge engineers and programmers by outlining a fusion of tense logic and ontology of time. In order to make tense logic better understandable, the central formal primitives of standard tense logic are derived as theorems from an informal and intuitive ontology of time. In order to make formulation of temporal propositions easier, temporal operators that were introduced by Georg Henrik von Wright are developed, and mapped to the ifrst-order tense logic, branching time logic, temporal logic, ontology of time, temporal operators, georg henrik von wright, unification of ontology and logic, computable tense logic, programmable tense logic FOUST 2021: 5th Workshop on Foundational Ontology, held at JOWO 2021: Episode VII The Bolzano Summer of
A firm understanding of tense logic is indispensable for ontologists, philosophers, knowledge engineers and programmers who need to formulate exact temporal propositions about the actual world, viz., propositions qualified by time. The standard approach to tense logic has two major drawbacks: it is not easily understandable for non-specialists; standard temporal operators are too coarse-grained for many purposes. This work aims to overcome the drawbacks by founding a system of tense logic and compact temporal operators on an intuitive ontology of time.
The underlying methodology is called the method of unification (Styrman [1][2, §4]). The central idea and goal here is to bring deep intuition to tense logic and to make time-related concepts and semantics understandable, by founding them on an intuitive ontology of time. This is in dire contrast with the standard approach, that is devoid of openly explicated ontological commitments. Yet, every system of tense logic formalizes some ontology of time. It is therefore intelligible to ask how the basic principles, concepts and semantics of tense logic can be founded on ontology, i.e., how can a primitive principle be derived as a theorem from ontology, how is a concept defined in terms of ontology, and how is semantics mapped to ontology. Conversely, there is some logic in every consistent ontology of time. Explicated mappings between an ontology of time and a system of tense logic exactify the applied ontology and secure that it is a suficient foundation for the system of tense logic. By studying a unified whole of tense logic and ontology of time, a non-expert may acquire a better understanding of both disciplines than by studying each of them separately.
Temporal propositions are formulated by applying temporal operators. Standard temporal operators are too coarse-grained for many purposes. They can express propositions such as “It is possible from the aspect of the present time that an event will take place at some time in the future as a whole” and “It is necessary from the aspect of the present time that an event took place at some time in the past as a whole”, but they cannot express more specific propositions such as “It is possible from the aspect of the present time that it will rain tomorrow in Helsinki” or that “It is necessary from the aspect of the present time that it was raining last year in Helsinki.” Point-accessibility (PA) operators are intuitive and suficiently fine-grained for formalizing such propositions. PA operators are inspired by Georg Henrik von Wright [3].
Some reservations are in place. This work is not a finalized account of the relations of tense logic and ontology of time, nor of the associated semantics and terminology, but an attempt of building a simple prototype which shows that it is in the first place possible to formulate their coherent fusions. Relatedly, a presentist ontology of time is applied because it is straightforward and conforms to common intuitions;1 a discrete prototype is formulated, because this is easier than formulation of a continuous one.
The article is organized into a form of a cumulative buildup, where virtually every earlier step is applied directly or indirectly in every later step. In §2, a generic fusion of causal presentism (CP) and instant-based tense logic is formulated. In §3 time and PA operators are founded on the generic fusion of CP and tense logic. In §4, it is pointed out that PA operators save the functionality of standard temporal operators. In §5, interaction axioms of standard tense logic are derived as theorems from CP, by applying the PA operators. In §6 the concluding remarks are given. The below abbreviations and logical notation are used.
causal presentism, independently of determinism vs. indeterminism. linear causal presentism: CP + determinism. branching causal presentism: CP + indeterminism. point-accessibility. temporal state of the Universe. the present temporal state of the Universe. points of time on a linear timeline.
variables for an individual T or a set of T s.
CP LCP BCP PA T P , , , ∧
¬ ∀
→ ⊆ , ′, ″, ‴
= ∪ = / ⃖⃗ and . not . for every . if , then .
is a subset of .
is the union of and . causal successors of . is the diference of and . ∨ ≔ ∃ ↔ ⊂ = ⃖⃖ or . is defined as.
there exists . ∩ ′ if and only if . if . is a proper subset of .
is the intersection of and . causal predecessors of .
1A relativistic ontology of time is not a feasible starting point in exemplifying an understandable fusion of tense Suntola [4] for a system of physics that saves relativistic phenomena while sustaining absolute simultaneity. 2. Causal Presentism and the Kripke Frame A generic fusion of causal presentism (CP) and instant-based tense logic (IBTL) is outlined by formulating axioms of CP, by deriving primitives of IBTL from CP, and by defining primitive (and other) concepts of IBTL in terms of CP. First, an intuitive picture of CP is given. Second, the primitives of IBTL are characterized. Third, the steps of the buildup of the fusion of CP and IBTL are listed. Fourth, their fusion is formulated.
Fig. 1 illustrates linear causal presentism (LCP) and branching causal presentism (BCP). The big dots represent the present temporal state of the universe (P ) which is the only temporal state of the Universe (T ) that exists, i.e., is realized. Stars represent causal predecessors of P , i.e., past T s, which did exist and were realized in the past but exist no longer. Dashes represent causal successors of P , i.e., possible future T that do not exist at P but are realizable in the future. In LCP there is only one realizable future, i.e., one possible future. Therefore, in LCP every assigned future possibility will be realized, i.e., will necessarily come into existence by becoming present; after a T has become present, it becomes past and remains past forever. In BCP there are several possible futures, and each assigned future possibility may be realized and may come into existence by becoming present, i.e., realization of a future possibility is contingent, not necessary. In BCP, an assigned possible future T either becomes the present and then becomes forever past, or it becomes disconnected from the present (def. 6). The dots in BCP represent T which were future possibilities in the past but were not realized, i.e., T that became disconnected from P .2 The passage of time is the process of transitions from one present into a causally succeeding present. These transitions are called forward-directed, i.e., the passage of time takes time forward. Fig. 2 illustrates the passage of time as the process of causally successive T s coming into existence and ceasing to exist.
IBTL starts from possible worlds semantics where the primitive Kripke frame (, >) consist of a set of possible worlds and an accessibility relation > which may hold between two worlds in . The possible worlds are interpreted as instants of time, and > as a temporal succession relation between the instants. > is virtually always considered transitive to express the passage and/or direction of time, and irreflexive and asymmetric when circular time is ruled out.
The fusion of CP and IBTL is built up as follows. Presentism is postulated (ax. 1). Positive duration of T s is postulated (ax. 2). Causality (ax. 3) is postulated.3 The relation of direct causal succession (⋖) is defined (def. 1). The transitory aspect of time, or the passage of time, is derived 2Dummett [5, p. 73-4] and Putnam [6, p. 240] give congenial characterizations of presentism. 3Axioms 1-3 are expressed in natural language. The definitions, theorems and axiom 4 are expressed in first-order predicate logic that is complemented by rank 1 sets and set theoretic relations, time qualifications and modalities. The set theoretic expressions could be replaced by expressions of discrete mereology (Styrman and Halko [7, §5.1]). (th. 1). The set P⃖⃖⃗ of causal successors of P (cor. 1), the set P⃖⃖⃖ of causal predecessors of P (cor. 2), and the set of causal successors of causal predecessors of P (th. 2) are derived. The relation of causal succession (<) is defined (def. 2). Causal successors (def. 3), causal predecessors (def. 4), T s connected to (def. 5) and T s disconnected from (def. 6) a point of evaluation (an arbitrary T ) are defined. Transitivity of < is derived (th. 3). Irreflexivity of < is postulated (ax. 4) and asymmetricity of < is derived (th. 4).
all that exists. It is called the present T , abbreviated as P . Is present and exists are the same property, which belongs only to P and its proper parts. P consists of various proper parts which exist absolutely simultaneously, and may be in diferent states of motion and gravitation, such as the Moon, the Earth and distant galaxies.
Axiom 2. Positive duration. The duration of P is positive, i.e., seconds, where is a real number greater than zero.4 Together with the other axioms and definitions, positive duration of T s entails5 discrete motion and time, i.e., that a positive period of time consists of finitely many positive instants of time, and that every history (def. 18) is ordered discretely like the integers: an arbitrary T in a history can be considered as 0, its causal predecessors as −1, −2, −3, … and its causal successors as 1, 2, 3, ….
Axiom 3. Causality. P is the efect of exactly one T : the direct causal predecessor of P . In the context of determinism P causes the possibility of coming into existence of exactly one direct causal successor. In the context of indeterminism P causes the possibility of coming into existence of several direct causal successors, i.e., an irreducible element of randomness is involved. In both cases exactly one direct causal successor of P will come into existence (th. 1). Definition 1. Direct causal successor. ⋖ the direct causal predecessor of P .
P ≔ P is a direct causal successor of , and is 4Van Bendegem [8] contemplates positive duration.
5When it is supposed that there are no gaps between consecutive T s, and that there are no higher transfinite orderings of histories than the ordering of the natural numbers.
Theorem 1. The passage of time as the process of transitions. It is proved that CP entails
an active process of transitions from one present to a causally successive present. Once time
has been defined (def. 7) this process may called the passage of time. (
Definition 3. Causal successors of a point of evaluation. ⃖⃗ = { ∣ < }, where , ∈ is the set of all causal successors of .
Definition 4. Causal predecessors of a point of evaluation. ⃖⃖ = { ∣ < }, where , ∈ ⃖⃖ is the set of all causal predecessors of . . ⃖⃗ .
Definition 5. T s connected to a point of evaluation. ( ) = ⃖⃖∪ { } ∪ ⃖⃗, where ∈ . ( ) is the union of the set of causal predecessors of , the singleton set of , and the set of causal successors of .
6Compare to Belnap [9, p. 387] who in the contex of Special Relativity accommodates indeterminism “by including those point events that either are now future possibilities or were future possibilities.” Definition 6. T s disconnected from a point of evaluation. ( ) = / ( ), where ∈ . ( ) is the diference of and the set of all T s connected to .
Theorem 3. Transitivity of causal succession. ∀, , ∈ ( < < → < ). For all
, , that are elements of , if is a causal successor of , and is a causal successor of , then
is a causal successor of . That < holds (def. 2) is trivial in CP, for < < means that
there is a chain of direct causal successors from to (that contains in the middle). Consider a
proof that CP and < < imply < , for all , , ∈ . (
not a causal successor of itself. Together with the other axioms, irreflexivity excludes causal cycles and entails e.g. that a present T is not realizable in the future.
Theorem 4. Asymmetricity of causal succession. ∀, ∈ ( < → ¬( < )). For all elements and of , if a causal predecessor of , then is not a causal predecessor of . Proof by contradiction: causal chains of the type < ∧ < violate ax. 4. ∎
Time and point-accessibility (PA) are founded on the generic fusion of CP and tense logic in the following order. Time is defined as linear, relational and superimposed (def. 7). A PA schema (def. 8) and a PA operator schema (def. 9) are formulated. It is shown how CP yields truth values of forward-directed (def. 10), backward-directed and synchronic PA propositions (def. 11). Quantified PA operators are formulated (defs. 12-13).
Definition 7. Time: linear, relational and superimposed. Points of time are linearly ordered, i.e., elements of a linear timeline: for all points of time and ′, either = ′ or < ′ or > ′. Time is not absolute nor primitive but relational, i.e., all references to time are references to one or more T s, viz., elements of the linear timeline are mapped to T s.7 In CP, the present time is P, and the past times are causal predecessors of P (cor. 2). In LCP, each future time is an element of the linear sequence of causal successors of P (cor. 1). In BCP each future time denotes several mutually disconnected (def. 6) causal successors of P, i.e., mutually disconnected possible future T s. In McDermott’s [12] terminology, a future time is superimposed by several T s. The expressions ‘ denotes several T s’ and ‘ is superimposed by several T s’ are interchangeable.8 The expression = ′ is read as: is the same time as ′. = ′ is true when and ′ denote the same T or the same T s. The expression < ′ is read as: is earlier than ′. < ′ is true when each T denoted by ′ is causal successor of some T denoted by , and each T denoted by is a 7See Ballard [10, p. 61] and Galton [11, p. 185] for the Leibnizean notion of relational time.
8Linear time enables applying all PA operators in LCP and BCP. Superimposition and linear time are a natural pair in BCP. Also branching time requires superimposition in practice, as it requires (a) the ontology of T s that are possible in the future within a specific distance from P, (b) ‘individual times’ for each of these T s, and (c) a superimposed ‘extra time’ that denotes all the individual times. causal predecessor of some T denoted by ′. Formally, where s(t) and s(t’) denote sets of T s denoted by and ′, respectively:
< ′ ≔ ∀ ∃ ( ∈ ( ′) → ∈ ( ) ∧ < ) ∧ ∀∃ ( ∈ ( ) → ∈ ( ′) ∧ < ).
Distance between points of time can be defined in terms of superimposition. For instance, when P < holds and is associated with a distance of one second in Earth’s geoid (sea level), is superimposed by the last T s of all chains of causally successive T s that start from P and end at a T where a caesium-133 atom in Earth’s geoid has oscillated 9192631770 times. Similarly, when P < holds and is associated with a distance of one Earth day or one Earth year, is superimposed by the last T s of all chains of causally successive T s that start from P and end at a T where the Earth has rotated once around its own axis or once around the Sun, respectively. Definition 8. PA schema: ′, where is the aspect time, is the point-accessibility relation, and ′ is the target time. In a temporal proposition (def. 9), and ′ are assigned and ′ is replaced by a set of one or more T s that are, were or will be accessible at ′ from the aspect of . In def. 9 modalities are defined as quantifiers over ′. In the following, it is show how CP determines the elements of ′ with all combinations of , ′, P , where ≤ P .9 Combinations where = P are represented first. Second, combinations where < P are represented.
P -forward: P ′, where ′ > P . In LCP P ′ is a set of exactly one causal successor of P , which is realizable at ′ from the aspect of P . In BCP P ′ is a set of several mutually disconnected causal successors of P that are realizable at ′ from the aspect of P (Fig. 3).
P -backward: P ′, where ′ < P . The only element of P ′ is a single causal predecessor of P that was realized at ′ from the aspect of P (Fig. 3).
P -synchronic: P ′, where ′ = P . The only element of P P is P , which is realized from the aspect of P .
< P < ′ ∶ ′ is a set of one T that was realizable (LCP) or several T s that were realizable (BCP) at ′ from the aspect of . From the aspect of P , the same T is realizable at ′ (LCP), or the elements of P ′ ⊂ ′ are realizable at ′ (BCP).
< ′ = P ∶ ′ is a set of one T that was realizable (LCP) or several T s which were realizable (BCP) at ′ from the aspect of . Exactly one of them is realized at ′ = P .
< ′ < P ∶ ′ is a set of one T that was realizable (LCP) or several T s which were realizable (BCP) at ′ from the aspect of . From the aspect of P , exactly one of them was realized at ′.
9LCP fixes the elements of ′ also when > P. In contrast, when > P in BCP, denotes several mutually disconnected T s. Such cannot function as an aspect time, because the aspect time must be a single T . However, ′ where > P can be considered to have the same members as P ′. For, as P is the ultimate viewpoint, ′ where e.g. P < < ′, can be interptered to be equivalent with P ′, which is in turn equivalent with P ′. Definition 9. PA operator schema. Length 1 PA (PA-1) operator schema M ′ applies a PA-1 chain ′. M ′ is read as: It (is, was, will be) M from the aspect of that (is, was, will be) realized at ′, where M is a modality, is the aspect time, ′ is the target time, and is a property or a disjunction of properties, or in von Wright’s [3, pp. 96-8] terms “a grammatically complete sentence [such as “It rains in Helsinki.”] which, however, does not express a true of false proposition unless it is qualified with respect to time.”
A PA-1 operator is an instance of a PA-1 operator schema where M is assigned a modality: p o s s i b l e (p o s ), c o n t i n g e n t (c o n ), n e c e s s a r y (n e c ), i m p o s s i b l e (i m p ), or n e u t r a l (n e u ); see defs. 10-11.10 A PA-1 proposition is an instance of a PA-1 operator schema where , ′, and M are assigned. In LCP a PA-1 proposition is either true or false, with any , ′ combination. In BCP a PA-1 proposition is either true, false or indeterminate with any , ′ combination where ≤ P.11 Formally, a PA-1 proposition states that a specific number of elements of the set ′ conform to , i.e., modalities are considered as quantifiers over ′.12 p o s ′ is true if at least one element of ′ conforms to . n e c ′ is true if every element of ′ conforms to . c o n ′ is true if at least one but not every element of ′ conforms to . i m p ′ is true if no element of ′ conforms to . n e u ′ is true if n e c ′ is true, false if i m p ′ is true, and indeterminate if c o n ′ is true. The following rules hold for PA-1 propositions: M ′ ∧ M ″ ≡ M ′∧ ″.
M ′ ∨ M ″ ≡ M ′∨ ″.
M ′ ∨ M′ ′ ≡ M ∨ M′ ′. ′
Length PA (PA- ) operator schema M 0 … M −1 applies a PA- chain: It (is, was, will be) M from the aspect of 0 that … it (is, was, will be) M′ from the aspect of −1 that (is, was, will be) realized at . PA-n propositions are PA-n operator schemas where , M, … , M′ and 0, … , are assigned. In LCP a PA-n proposition is either true or false. In BCP a PA-n proposition where 0 ≤ P is either true, false or indeterminate.
′
A PA proposition of the type M 0 … M −1 is a single-chain proposition as it applies a single chain of accessibility 0 … −1 . Exactly one T sufices in making a single-chain proposition true, false or indeterminate. It is the earliest of 0, … , ; as 0 ≤ P, the earliest of 0, … , is earlier than or equal to P. This is intelligible as in CP the past and P are fixed, and the earliest of 0, … , causes all possibilities that are relevant to the focal proposition. A multi-chain proposition has two or more chains of accessibility; accordingly, more than one T may be required in making a multi-chain proposition true, false or indeterminate. Definition 10. Forward-directed PA-1 propositions. The direction of a PA-1 proposition is the direction of its accessibility relation ′. In forward-directed PA-1 propositions < ′. Forward-directed PA-1 propositions of the type MP >P are present propositions about the 10The modalities are written in natural language instead of the traditional one-character symbols to improve readability. Note that there is no standard symbol for neutrality.
11Analogously to def. 8, in BCP e.g. pos ′ where P < < ′ is not a PA-1 proposition. Its genuine accessibility chain can be interpreted as P ′, but M in the corresponding PA operator schema MPpos ′ is unknown. pos ′ where P < < ′ could be interpreted as the PA-2 proposition necPpos ′, which is read as “It is necessary from the aspect of P that it will be possible from the aspect of that is realizable at ′.”
12PA operators can be considered to deploy hybrid temporal logic (Goranko and Rumberg [13, ch. 7.1]), as they express propositions that have a specific truth value at exactly one instant of time. ′.” True if it rains in Helsinki in every element of P realizable at . r a i n s is an abbreviation of “It rains in Helsinki.” future, and P is a set of one T that is (LCP) or several T s that are (BCP) from the aspect of ′.” True if it rains in Helsinki in at least one element of
A: p o s s i b l e P r a i n s ′>P ≡ “It is possible from the aspect of P that it will rain in Helsinki at
B: n e c e s s a r y P r a i n s ′>P ≡ “It is necessary from the aspect of P that it will rain in Helsinki at at ′.” True if it rains in Helsinki in no element of
C: i m p o s s i b l e P r a i n s ′>P ≡ “It is impossible from the aspect of P that it will rain in Helsinki
n e c P r a i n s ′ is true. at ′.” True if it rains in Helsinki in at least one but not in every element of D: c o n t i n g e n t P r a i n s ′>P ≡ “It is contingent from the aspect of P that it will rain in Helsinki
false. In other words, true if i m p P r a i n s ′ and n e c P r a i n s ′ are false, and false if i m p P r a i n s ′ or ′” ≡ “It will rain in Helsinki at ′.” True if it rains in Helsinki in every element of
E: n e u t r a l P r a i n s ′>P ≡ “It is neutral from the aspect of P that it will rain in Helsinki at i.e., if n e c P r a i n s ′ is true. False if it rains in no element of c o n P r a i n s ′ is true. E is thereby a future contingent when D is true.13 Indeterminate if it rains in Helsinki in at least one but not in every element of P ′, i.e., if Each row below represents a consistent combination of the truth values of A-E. P ′, i.e., if i m p P r a i n s ′ is true.
P ′, ⟨A true⟩ ⟨A false⟩ ⟨A true⟩ ⟨B true⟩ ⟨B false⟩ ⟨B false⟩ ⟨C false⟩ ⟨D false⟩ ⟨C true⟩ ⟨C false⟩ ⟨D true⟩ ⟨D false⟩ ⟨E true⟩ ⟨E false⟩ ⟨E indeterminate⟩ Definition 11.
Backward-directed and synchronic PA-1 propositions. PA-1 propositions i.e., in its only element.
A: p o s s i b l e P r a i n s ′≤P ≡ ′≤P . True if it rains in Helsinki in at least one element of P ′, B: n e c e s s a r y P r a i n s ′≤P ≡ ′≤P . True if it rains in Helsinki in every element of P ′, i.e., < are backward-directed. In synchronic PA-1 propositions = ′. Backwardare present propositions about the past. Synare present propositions about the present. In MP ′ where ′ directed PA-1 propositions of the type MP ′<P chronic PA-1 propositions of the type MP
P as ¬ , and read as was/is not the case at t’. backward-directed and synchronic PA-1 propositions possibility, necessity and neutrality are equivalent, and contingency statements are false. Von Wright [17, p. 25] calls this “a modal logic of a universe of propositions which has no room for contingent propositions but in which every truth is a necessity and every falsehood is an impossibility.” The past and P are unchanging from the aspect of P, even if they could have been realized diferently. Therefore, propositions of the types p o s P ′≤P , n e c P ′≤P
and n e u P ′≤P case at t’. Backward-directed and synchronic propositions of the type i m p P ′≤P can be written as ′, and read as was/is the can be written in its only element. not in its only element.
C: i m p o s s i b l e P r a i n s ′≤P ≡ ¬ ′≤P . True if it rains in Helsinki in no element of P ′, i.e.,
13Compare to Briggs and Forbes [14, ch. 2] who analyze proposition (
D: c o n t i n g e n t r a i n s ′≤P . True if it rains in Helsinki in at least one but not in every element
P of P ′, i.e., never true.
E: n e u t r a l P r a i n s ′≤P ≡ ′<P . True if it rains in Helsinki in every element of P ′. False if it rains in Helsinki in no element of P ′. Indeterminate if it rains in Helsinki in at least one but not in every element of P ′, i.e., never indeterminate.
Each row below represents a consistent combination of the truth values of A-E. The truth values of A, B, E are equivalent and contrary to C; D is always false.
⟨A true⟩ ⟨B true⟩ ⟨C false⟩ ⟨D false⟩ ⟨E true⟩ ⟨A false⟩ ⟨B false⟩ ⟨C true⟩ ⟨D false⟩ ⟨E false⟩ Definition 12. Quantified PA-1 operators . Table 1 represents PA-1 operators that quantify over intervals of time. Henceforth, operators 1-10 are referred to as TB1.1-10. The clause “From the aspect of ” is to be added in front of the natural language definitions of TB 1.1-10. TB1.1 is expressed also as a conjunction and TB1.2 also as a disjunction of unquantified PA-1 operators. TB1.1’ transforms TB1.1 into a version that quantifies over a finite interval of time. Similarly for all operators in the table. TB1.11-12 are examples from von Wright [3, pp. 96-8]. Von Wright’s notation ∃ ′ < (M ′) is modified into M ∃ ′< .
p o s ∃ ′> p o s ∃ ′> p o s ∃ ″( < ″≤ ′) p o s ∀ ′> p o s ∀ ′> n e u ∃ ′> n e u ∀ ′> n e c ∃ ′> n e c ∀ ′> i m p ∀ ′> c o n ∃ ′> n e c ∃ ′< n e c ∀ ′< p o s ∃ ′< n e c ∀ ′<
Definition 13. Asymptotic determinism was recognized by Aristotle in Metaphysics 1027b1014: “it is necessary that he who lives shall one day die…But whether he dies by disease or by violence, is not yet determined.” That P asymptotically determines is written as p a - a s d P .14 The ‘event of death of an individual’ may be interpreted to last for exactly one instant, or for a longer finite period of time. Yet, we could contemplate a property such as being dead that lasts for a boundless period of time. In the below formulation may have any of these durations. The basic idea of p a - a s d can be stated as follows: when P < < ′ holds, P determines the
P 14pa-asdP is always false in LCP. pa-asdP is an open game quantifier , which states that a game ends after a ifnite number of steps, but it is not known at which step (cf. Kolaitis [ 18, p. 368]). interval [ ′] where will be instantiated for the first time. p a - a s d P can be formalized as the conjunction of propositions (a-d).
(a) From the aspect of P, it is necessary that from the aspect of every ″ ≥ ′ it will be necessary that is/was instantiated at least once in the interval [ ′]: n e c P n e c ∀ ″≥ ′ ∃ ‴(≤ ‴≤ ′). (b) From the aspect of P, the instantiation of is contingent at and ′: c o n P ∧ ′. (c) From the aspect of P, the instantiation of is contingent or impossible at each time in the interval ] ′[: ( c o n ∨ i m p ) P ∀ ″( < ″< ′).
(d) From the aspect of P, the instantiation of is impossible before : i m p P ∀ ″< .
PA operators save the functionality of standard temporal operators for linear and branching systems. For linear systems, Prior [19, ch. 2] originally formulated the pair of operators F and P, and later the pair of G and H (Prior [20, ch. 10]). F, P, G, H are defined and their PA analogs (§ 3) are given in table 2.15
One may start with F and P , and define G as ¬F¬ ≡ “not sometimes after P not ”, and H as ¬P¬ ≡ “not sometimes before P not ”. Alternatively, one may start with G and H , and define F as ¬G¬ , i.e., “not always after P not ”, and P as ¬H¬ , i.e., “not always before P not ”. The backward-directed P and H are applicable also in forward-branching and backward-linear systems such as BCP, whereas the forward-directed F and G need to be reinterpreted in branching systems (§5). All PA operators are applicable in linear and branching systems.
The study of temporal operators for branching systems has been centered on details of Prior’s [24, ch. VII] Peircean and Ockhamist operators (cf. Müller [25] and Rumberg [26]). The Priorian operators are infeasible from the aspect of computability, as they quantify over maximal linear subsets (defs. 14-15) of . Complete future operators (def. 16) quantify over maximal linear subsets of the set ⃗ of causal successors of , and thus do the job of the Priorian operators in a simpler way. It is shown that partial future operators (def. 17) do the job of the complete future operators. Thereby, it is also shown that the partial future operators do the job of the 15The formal definitions are from Hodkinson and Reynolds [ 21, p. 672]. The informal definitions are from Gabbay et al. [22, p. 24]. F, G, P, H appear as statistical modalities, complemented by a point and a direction of evaluation. Knuuttila [23, p. 163] characterizes the statistical modalities, that were familiar in the antiquity and to the scholastics: “a temporally indefinite sentence is necessarily true if it is true whenever uttered, possibly true if it is true sometimes, and impossible if it is always false.” Priorian operators. In efect, it sufices to explain the basic idea of Peircean operators (def. 18).
It is notable that the partial future operators are first-order PA operators, whereas the complete future operators and the Priorian operators are second-order, as they quantify over transfinite sets. , ∈ Definition 14.
Linear subset. (, ) ≔ ⊆ ∧ ∀, (, ∈ → > ∨ < ∨ = ), where . When is a linear subset of , is a subset of , and for every and that are elements of , is a causal successor or a causal predecessor of , or = .
Definition 15. where , ∈
Maximal linear subset. (, ) ≔ (, ) ∧ ∄ ( ⊆ ∧ (, ) ∧ ≠ ), . When is a maximal linear subset of , is a linear subset of , and is not a subset of any other linear subset of .
Definition 16.
Complete future operators and their PA analogs are represented in table 3.16 Complete future operators quantify over futures of the point of evaluation , i.e., over maximal linear subsets of ⃗. E.g. a s d is read as: in all futures of , there is a T Note that p a - a s d P (def. 13) is not equivalent with a s d P , and that ¬TB1.5 entails ¬TB1.6.17 that instantiates . Complete future operators and their PA analogs.
complete future op. PA pos ≔ asd ≔ con ≔ nec ≔ imp ≔ ∃ ∃ ∈ ( ) ∀ ∃ ∈ ( ) pos ∧ ¬asd ∀ ∀ ∈ ( ) ∀ ∄ ∈ ( ) pos ∃ ′> (TB1.1) pa-asd (def. 13) nec ∀ ′> (TB1-6) imp ∀ ′> (TB1-7) pos ∃ ′> ∧ ¬pa-asd ∧ ¬nec ∃ ′> (TB1-5) Definition 17.
Partial future operators. Complete future operators can be transformed into operators that quantify over partial futures ′], i.e., over maximal linear subsets of a finite ] stretch of future possibilities ⃖⃖⃗′ ≔ { ∣ ∈ ″ ∧ < ″ ≤ ′}. ⃖⃖⃗′ is the set of all T s that are accessible from at + 1 ∨ + 2 ∨ … ∨ ′. E.g. p o s can be formulated as a partial future operator as ∃ ′]∃ ∈ ] ′]( ), and as TB1.1’. Similarly for the other complete future operators.
] a causal successor of that instantiates .
Definition 18.
Peircean operators quantify over histories, i.e., maximal linear subsets of , viz., complete world-lines or complete courses of events. In LCP is a single history. In BCP consists of several histories. History ℎ that passes through point of evaluation is defined as a maximal linear subset of that contains (in BCP ≤ P). The Peircean version of a s d may be formulated as: ∀ℎ ∃ ∈ ℎ ( < ∧
). It is read as: In all histories ℎ that pass through , there is [25, p. 361] and Rumberg’s [26, p. 91] versions. depends on the nature of .
16The complete future operators conform to Galton’s [11, p. 202] informal definitions. asdP is close to Müller’s
17TB1.5&6 entail asdP . TB1.6 is mutually exclusive with pa-asdP . The compatibility of TB1.5 and pa-asdP
5. Interaction Theorems
In standard tense logic, interaction-, connection- or converse axioms GP, FH, PG, HF govern
interaction of the past operators P, H and the future operators F, G.18 The interaction axioms
are implications. They are derived as theorems by showing that CP and an antecedent of an
implication entail its consequent. The interaction axioms were originally applied in linear
systems where “will be” has a deterministic meaning. To avoid falsity and indeterminacy in
BCP, “will be” in GP, FH and PG is interpreted as PA necessity, and in HF as PA possibility.
Theorem 5. GP. Garson [27] writes GP as → : “that what is the case ( ), will at all
future times, be in the past ( ).” In PA format, GP is written as P → n e c ∀ >P ∃ ′< : If is
the case at P, then it will be necessary from the aspect of every > P that was the case at
least once before .19 It is proved that CP and P entail n e c ∀ >P ∃ ′< . (
19Recall that in BCP the initial aspect time must be P or earlier. Therefore, P → nec∀ >P ∃ ′< can be seen as an abbreviation of P → necPnec∀ >P ∃ ′< .
20nec∃ >P ∀ ′< → P is an abbreviation of necPnec∃ >P ∀ ′< → P. indeterminate in the systems of Lukasiewicz and Kleene (Akama et al. [29]). For instance, if particle goes through slit at P, and it has always been contingent that will go through , the proposition “It has always been neutral that will go through ” is indeterminate (def. 10). Consequently, Surowik [30, p. 93] suggests that F in HF should be replaced by ‘will possibly be’ (TB1.1). This reading is applied below.
Corollary 3. p o s ∃≤ P
will be realized at a
′
> , then it was possible from the aspect of every ″
∃ ′> → p o s ∀ ″ ′: If it is/was possible from the aspect of a ≤ P that
<
< that will be
realized at ′.21 It is proved that CP and p o s ∃≤ P
entail that there is such ≤ P and such ′ >
∃ ′> entail p o s ∀ ″ ′. (
< that at least one element of ′ instantiates .
∃ ′>
(
) ′ ⊂ ( − 3) ′ ⊂ … holds, i.e., is an element of ( − ) ′,
In PA format, HF is written as for all ≥ 0 , and thus p o s ∀ ″ ′ is true. ∎
< from the aspect of every < P that will be the case at least once after . It is proved that CP and
entail p o s ∀ <P
true. (
P entail that
P is made possible by P, i.e., that p o s P P is P → p o s ∀ <P ∃ ′> : If is the case at P, then it was possible
The central primitives, concepts and semantics of tense logic have been founded on a commonsense ontology of time. The firm connection between tense logic and ontology of time shows that the two disciplines can be seen as a unified whole and studied as one rather than as two separate lines of inquiry. The given fusion sets a precedent for more thorough or diferent fusions. For instance, it would be interesting to see a comprehensive fusion of tense logic and a relativistic ontology of time.
Point-accessibility operators compose a more comprehensive and comprehensible toolset than standard modal operators. They provide ontologists, philosophers, knowledge engineers and programmers a better basis for formulating and programming temporal propositions, and for dealing with time-related issues. For instance, point-accessibility operators provide naturalist philosophers better chances of explicating truthmakers and assessing truth values of propositions about this world.
I thank Aapo Halko for proofreading the article.
21Von Wright [3, p. 98] gives an analogous characterization: “Assume now that at some time ′ it is antecedently possible that at a . Then, regardless of whether this proposition comes true or not at , it must have been antecedently possible already at any time before ′.” (Eds.), Handbook of Modal Logic, Elsevier, 2007, pp. 655–720. [22] D. M. Gabbay, I. Hodkinson, M. Reynolds, Temporal Logic: Mathematical Foundations and
Computational Aspects, Oxford: Clarendon Press, 1994. [23] S. Knuuttila, Time and modality in scholasticism, in: S. Knuuttila (Ed.), Reforging the Great Chain of Being. Studies in the History of Modal Theories, Dordrecht: Reidel, 1981, pp. 163–257. [24] A. N. Prior, Past, Present and Future, Oxford: Clarendon Press, 1967. [25] T. Müller, Alternatives to histories? employing a local notion of modal consistency in branching theories, Erkenntnis 79 (2014) 1–22. doi:1 0 . 1 0 0 7 / s 1 0 6 7 0 - 0 1 3 - 9 4 5 3 - 4 . [26] A. Rumberg, Transition semantics for branching time, Journal of Logic, Language and
Information 25 (2016) 77–108. doi:1 0 . 1 0 0 7 / s 1 0 8 4 9 - 0 1 5 - 9 2 3 1 - 6 . [27] J. W. Garson, Modal logic, in: E. N. Zalta (Ed.), The Stanford Encyclopedia of Philosophy, spring 2016 ed., Metaphysics Research Lab, Stanford University, 2016. [28] R. Girle, Modal Logics and Philosophy, Acumen, 2000. [29] S. Akama, Y. Nagata, C. Yamada, Three-valued temporal logic and future contingents,
Studia Logica 88 (2008) 215–231. [30] D. Surowik, Tense logics and the thesis of determinism, Studies in Logic, Grammar and Rhetoric 7 (2001) 87–95.