Actual Futures in Peircean Branching-Time Logic

Bruno Barcellan - Alberto Zanardo

Abstract

In the paper Indeterminsm and the Thin Red Line, Belnap and Green show that the notion of actual future seriously clashes with Objective Indeterminism. However, there are some Computer Science and Artificial Intelligence applications of the formal structure which arises from the actual future point of view. Of course, these applications have nothing to do with the ontology of objective indeterminism, and so the objections by Belnap and Green do not apply to them. We consider an extension of Peircean branching-time logic, which contains a new future operator, f_{A}, to be read as ‘it will happen, in the future that will actually take place’. According to this reading of the new operator, Time is pictured as a tree in which each moment has one marked possible future that represents the actual future of that moment. This allows one to define a semantics for the extended language. We will provide a finite deductive system which is sound and strongly complete for the corresponding notion of validity.

Contents

1 Introduction 2

2 Actual futures - Belnap and Green’s Thin Red Line 4

3 Axioms 7

4 Chronicles 9

5 Completeness 12

1 Introduction

In Peircean branching-time logic ([Pri67] VII.6,7, [Bur80], [ØH95] 2.2,8), future tenses are viewed as involving all possible future courses of affairs; thus, we have two kinds of future-tense assertions: ‘on each course of affairs, it will be always the case that’ and ‘on each course of affairs, sooner or later, it will be the case that’. The (propositional) language L_{P} for this logic consists of denumerably many propositional variables p_{0}, p_{1}, …, of the usual boolean connectives, of the past operator H (it has always been the case that), and of two future operators, G and F, corresponding to the two kinds of future assertions considered above.

In the semantics for branching-time logics, Time is pictured as a tree, namely, as a pair T = ⟨T, <⟩ in which T is a set (of moments) and <, the earlier-later relation between moments, is an irreflexive order on T and fulfils the tree condition:

∀t, t′, t′′ ∈ T (t′ < t and t′′ < t ⇒ t′ < t′′ or t′′ < t′ or t′ = t′′)

Moreover, in this paper we also assume that Time is endless (∀t ∈ T, ∃t′ : t < t′) and connected (∀t, t′ ∃t′′ (t′′ < t and t′′ < t′)).

For every moment t, the sets {t′ : t′ < t} and {t′ : t′ > t} will be called, respectively, the past and the future of possibilities (or, briefly, the future) of t; the past of t is a linear order, while t and its future constitute a tree. A history in T is a maximal linearly ordered subset of T . We will say that the history h passes through the moment t to mean that t ∈ h. The set of all histories in T will be denoted by H(T ).

An evaluation of the propositional variables in the tree T = ⟨T, <⟩ is a function assigning to each propositional variable a subset of T. Arbitrary L_{P} - formulas are true or false at moments of a tree, under a given evaluation. We will write T , V ⊧_{t} α to mean that α is true at t in T , under the evaluation V. The recursive definition of truth is given by the following evaluation rules.

E1 T , V ⊧_{t} p_{i}  iff t ∈ V (p_{i})
E2 T , V ⊧_{t} ¬α iff T , V |̸=_{t} α
E3 T , V ⊧_{t} α ∧ β iff T , V ⊧_{t} α and T , V ⊧_{t} β
E4 T , V ⊧_{t} Hα iff ∀t′ < t, T , V ⊧_{t′} α
E5 T , V ⊧_{t} Gα iff ∀h ∈ H(T ) [t ∈ h ⇒ ∀t′ (t′ ∈ h and t < t′ ⇒
T , V ⊧_{t′} α)]
E6 T , V ⊧_{t} F α iff ∀h ∈ H(T ) [t ∈ h ⇒ ∃t′ (t′ ∈ h and
t < t′ and T , V ⊧_{t′} α)]

Truth in a tree, validity, satisfiability and other semantical notions are defined in the usual way; in particular, the formula α is satisfiable whenever there exist T , V, and t such that T , V ⊧_{t} α and α is valid (⊧ α) iff ¬α is not satisfiable.

Rules E5 and E6 correspond to the two kinds of (Peircean) future assertions considered at the beginning of this section. It is worth noticing that the quantification over histories involved in E5 is not essential; this rule is equivalent to

E5′ T , V ⊧_{t} Gα iff ∀t′ > t, T , V ⊧_{t′} α

The dual operators of H, G, and F are defined by: P = ¬H¬, f = ¬G¬, and g = ¬F ¬. Thus, P and f mean, respectively, ‘at some past moment’ and ‘at some future moment (in some possible course of affairs)’. The operator g is to be read as ‘always in the future, on some possible course of affairs’.

A bundle B on the tree T is a set of histories such that, for every moment t, there exists an element of B which passes through t. Pairs ⟨T , B⟩ in which B is a bundle on T will be called bundled trees. Truth at a moment t in the bundled tree ⟨T , B⟩, under the evaluation V (⟨T , B⟩, V ⊧_{t}) is defined in the same way as truth in a tree, except that the quantification over H(T ) in E5 and E6 is replaced by a quantification over B. Thus, E6 becomes

E6^{∗} ⟨T , B⟩, V ⊧_{t} F α iff ∀h ∈ B [t ∈ h ⇒ ∃t′ ∈ h (t < t′ and ⟨T , B⟩, V ⊧_{t′} α)]

while E5 can still be expressed by E5′.

The (existential) future-tense assertions F α and fα can be read as: it is possible that α will happen and it is necessary that α will happen. So, in Peircean branching-time logic, there is no room for the formal translation of

α will happen  (1.1)

Assertions like this one seem to refer to the course of affairs which is actually going to take place; that is, they seem to be readable as

α will happen, in the actual future  (1.2)

In other words, the sentence ‘α will happen’ seems to refer to a particular history, the actual history, and this leads to picture Time as a tree with a marked branch which represents that history (see Figure 1).

[figure] Figure 1

In the present paper we will first discuss the representation of Time as in Figure 1 and we will consider an extension L_{AP} of Peircean language, obtained by adding an actual future operator f_{A}. The formula f_{A}α is true at the moment t of the marked history whenever α is true at some point of that history in the future of t.

Of course, the definition of the formal properties of the operator f_{A} requires something more than marking a history; for instance, an obvious problem arises when defining the truth value, if any, of f_{A}α at moments that do not belong to the marked history. This and other connected issues will be discussed in the next section where a semantics for L_{AP} will be defined. In particular, we will consider Belnap and Green’s point of view ([BG94]) according to which picturing Time as in Figure 1 clashes with Objective Indeterminism. We will show, however, that an enriched version of the picture Figure 2 is suitable for dealing with Time in applications of branching-time logic. In Sections 3 to 5 we will provide an axiomatic theory sound and complete for L_{AP} -validity.

2 Actual futures - Belnap and Green’s Thin Red Line

In [BG94], Belnap and Green call Thin Red Line (TRL) the marked history of Figure 1 and show that, if objective indeterminism holds, the reading of (1.1) as (1.2) leads to unacceptable consequences^{1}. Their discussion about the TRL is a part of the Historical Openness Thesis (Sections 5,6 in [BG94]) according to which sentences of the form (1.1) are historically open, in the same sense as ‘x is brindle’ is an open sentence ^{2}.

The first part of the Historical Openness Thesis is that assertions of the form (1.1) are not closed by constancy: given any moment t_{0}, the truth value of ‘The coin will come up heads’ at t_{0} depends in an essential way on the history passing through t_{0} that we consider and there is no constant truth value as the history varies (thus, the quantification over histories involved by the Peircean operators F and G makes both inadequate for representing the future tense ‘will’ in (1.1)).

The arguments against the TRL point of view constitute the second part of the Historical Openness Thesis, which holds that assertions of the form (1.1) are not closed by context. This means that the context of use does not supply any particular (actual) history at which the sentence (1.1) is to be evaluated. In order to prove this, Belnap and Green assume that (1.2) is a correct reading of (1.1) and they first wonder whether there is only one TRL. The uniqueness of the TRL is apparently negated by the meaningfulness of the sentence

The coin will come up heads. It is possible, though, that it will come up tails, and then later it will come up tails (though at that moment it could come up heads).

in which the two occurrences of ‘will’ cannot refer to the same actual history.

Afterwards, Belnap and Green consider, instead of a single TRL, a function TRL(·) which assigns a history to each moment: TRL(t) is the actual history of t. Of course, they assume that each moment belongs to its own actual history.

1Other shocking consequences of the TRL point of view are shown in [BG93].

2The other main thesis of [BG94] is the Assertability Thesis: “In contrast to the senselessness of asserting an assignment open sentence such as ‘x is brindle,’ there is no radical defect in asserting a typical future-tensed sentence such as ‘The coin will come up heads,’ even under conditions, even known to the speaker, of radical indeterminism” (p. 377).

Even this picture of Time, however, turns out to be unacceptable. In order to prove this, they have only to consider the implications

(α will happen) will happen ⇒ α will happen  (2.1)
α ⇒ (α will happen) happened  (2.2)

which can be hardly negated in any theory for temporal truth^{3}.

If (2.1) and (2.2) are assumed to be true for every sentence α, in fact, the function TRL(·) must have the property that

for all t_{1}, t_{2}, t_{1} < t_{2} ⇒ TRL(t_{1}) = TRL(t_{2})  (2.3)

but, since every TRL(t) is a linear order, this property excludes, against objective indeterminism, that moments with diverging futures can exist.

In the semantics for L_{AP} considered in the present paper, each moment has its own actual history, but, instead of (2.3), we will assume a weaker property, so that Time will still be pictured as a tree. A consequence of this weakening is that the formal counterpart of (2.2) above is not a validity. Below, we will show how to make sense of this. In the following definition, and in the next technical sections, we will write A(t), instead of TRL(t) to denote the actual history of t.

Definition 2.1 An actualizing function A on the tree T [resp. bundle tree ⟨T , B⟩] is any function which assigns a history [resp. an element of B] to each moment in T and such that, for all moments t, t′

(1) t ∈ A(t),

(2) if t < t′ and t′ ∈ A(t), then A(t) = A(t′),^{4}

(3) there exists a moment t^{∗}, such that, for any t < t^{∗}, A(t) = A(t^{∗}).

Pairs ⟨T , A⟩ and triples ⟨T , B, A⟩ in which A is an actualizing function on T or on ⟨T , B⟩ will be called actualized trees (a.t.’s) and actualized bundled trees (a.b.t.’s), respectively. The actual future of t is the intersection between A(t) and the future of t. By Condition (2) in the definition above, if t′ is in the actual future of t, then t and t′ share the same actual history. If the moments t^{∗} and t^{∗∗} fulfil Condition (3), then, since we are assuming that trees are connected, A(t^{∗}) = A(t^{∗∗}). Thus, we can call A(t^{∗}) the real history, or the TRL, and real moments its elements^{5}.

On the basis of Definition 2.1, the picture of Time is that of Figure 2 (where only the TRL and the actual future of the moment t are marked).

The language L_{AP} can be interpreted in a.t.’s. Formulas of L_{P} can be evaluated in the obvious way and the evaluation rule for f_{A}α is

3According to [BG94] (p. 380), the negation of (2.2) would lead to assert something very odd like “The coin came up tails, but this is not what was going to happen. The coin was going to come up heads. It’s just that it didn’t”.

4This weakening of (2.3) is also considered in [Bar96] and in [BHØ98].

5No condition equivalent to (3) is assumed in [TG80] and [BHØ98].

[figure: TRL; t; A(t)] Figure 2
E7 ⟨T , A⟩, V ⊧_{t} f_{A}α iff ∃t′ ∈ A(t) (t < t′ and ⟨T , A⟩, V ⊧_{t′} α)

Actualized trees could have been defined otherwise, using the relation “to be in the actual future of” (>_{A}) as primitive notion and by defining suitable properties for this relation ([Bar96]). Starting with the actualizing function A of Definition 2.1, <_{A} can be defined by

t <_{A} t′ ≡^{def} t < t′ and t′ ∈ A(t)  (2.4)

and the evaluation rule E7 can be written as

E7′ ⟨T , B, A⟩, V ⊧_{t} f_{A}α iff ∃t′ >_{A} t : ⟨T , A⟩, V ⊧_{t′} α

On the basis of E7 or of E7′, f_{A} turns out to be a linear time future operator and in fact the following formulas are L_{AP} -validities:

f_{A}f_{A}α → f_{A}α
f_{A}α ∧ f_{A}β → f_{A}(α ∧ f_{A}β) ∨ f_{A}(β ∧ f_{A}α) ∨ f_{A}(α ∧ β)

In particular, the first of these formulas corresponds to (2.1) above. As for the translation of (2.2) in L_{AP}, the formula α → P f_{A}α is not a validity. For the stronger formula α → Hf_{A}α, however, we have that, for every a.t. ⟨T , A⟩,

t ∈ TRL iff for every evaluation V, ⟨T , A⟩, V ⊧_{t} p → Hf_{A}p  (2.5)

Thus, the truth of p → Hf_{A}p at a point t can be viewed as a test to check whether t belongs to the TRL or not.

In [Bar96], the first author shows that Computer Science offers an interpretation of L_{AP} in which it makes sense to consider counterexamples to (2.2). Other examples of ‘actual future’ readings of (1.1) can be found in [BHØ98], where an Ockhamist ([Pri67], [Bur79]) branching-time logic is considered.

Artificial Intelligence too has recently paid some attention to the notion of ‘actual line’, e.g., in the Situation Calculus ([PR95], [Pin98]). We believe that, in this area, the picture of Time provided by Definition 2.1 is particularly significant in connection with Partial Information Reasoning. When information is partial, there are many future developments of the present state of affairs that are compatible with our knowledge and this leads to a tree-like representation of the world. Works in this area are aimed at providing methods for determining, or choosing, a particular future course of events, the one which best fits suitable criteria like minimal change principles, probability, typicality and others. In all cases, the efforts are meant to provide a picture of the world like that of Figure 2, where the marked future of a state of affairs is the most suitable from the point of view of the criterion under consideration.

According to this point of view, the satisfiability of the negation of p → Hf_{A}p has a quite reasonable reading: if this formula can be falsified at a given moment t, then, somewhere in the past of t, the world did not develop according to our ‘preferred developments’ criteria.

3 Axioms

We will call Actualized Peircean Logic (briefly, AP-logic) the logic of L_{AP} with the actualized tree or actualized bundled tree semantics. A consequence of a result by John Burgess ([Bur80]) discussed below, is that the two logics coincide. The axioms and rules for AP-logic are A0-11 and R0-4 below, where p and q denote arbitrary propositional variables and α is an arbitrary formula; moreover, we will write g_{A} ( =^{def} ¬f_{A}¬) to denote the dual operator of f_{A}.

A0  All truth-functional tautologies
A1 1,2. H(p → q) → (Hp → Hq), G(p → q) → (Gp → Gq)
3.  G(p → q) → (F p → F q)
A2 1,2. Gp → F p, Gp → gp
A3 1,2,3. Hp → HHp, Gp → GGp, F F p → F p
A4 1,2. p → GP p, p → Hfp
A5 1,2. (Hp ∧ p ∧ Gp) → GHp, (Hp ∧ p ∧ gp) → gHp
A6  F Gp → GF p
A7  g_{A}(p → q) → (g_{A}p → g_{A}q)
A8 1.  f_{A}p ∧ f_{A}q → [f_{A}(p ∧ f_{A}q) ∨ f_{A}(q ∧ f_{A}p) ∨ f_{A}(p ∧ q)]
2.  f_{A}f_{A}p → f_{A}p
A9 1,2,3. f_{A}p → fp, g_{A}p → gp, Gp → g_{A}p
A10 1. f_{A}(p ∧ P q) ∧ ¬q ∧ H¬q → f_{A}(q ∧ f_{A}p)
2. f_{A}(¬α ∧ g¬α ∧ δ) ∧ F α → f_{A}(α ∧ f_{A}δ)
A11  P (q ∨ ¬q) → P H(p → Hf_{A}p)
R0,1 Substitution, Modus Ponens
R2 Generalization: to infer Gα and Hα from α
R3 To infer α from ¬p ∧ H¬p ∧ Gp → α, if p does not occur in α

It is straightforward to check that these axioms and rules are sound^{6}. Axioms A0-6 constitute the Peircean fragment of AP-logic. In [Bur80], this fragment is proved to be complete for Peircean validity. Many of the results proved in that paper are applicable here without any modification. For the proofs of these results we will refer to the corresponding proofs in [Bur80].

6Rule R3 is an instance of the Irreflexivity Rule ([Gab81]). In [Zan90], an infinite set of

The f_{A}-fragment of AP-logic consists of axioms A7,8 and of the rule ⊢ α ⇒ ⊢ g_{A}α which follows from R2 and A9.3; this fragment is well known to be complete for validity in temporal structures which are linear towards the future (in a language containing f_{A} as the only temporal operator). This completeness result will be used freely in the paper.

We will adopt the standard definitions of theoremhood (⊢), deducibility from the set X of formulas (X ⊢). The notions of consistency, and of maximal consistent set (m.c.s.) are defined in the usual way. Capital Greek letters will range over m.c.s.’s. The set of m.c.s.’s can be endowed with the relation ≺ defined by

Γ ≺ Δ ≡^{def} {α : Gα ∈ Γ} ⊆ Δ  (3.1)

Standard arguments show that Γ ≺ Δ is equivalent to each of the inclusions: {α : Hα ∈ Δ} ⊆ Γ, Γ ⊆ {α : P α ∈ Δ}, and Δ ⊆ {α : fα ∈ Γ}. The relation ≺ can have reflexive clusters, that is, there could be m.c.s.’s Δ and Γ such that Γ ≺ Δ and Δ ≺ Γ. We will write Γ ≺≺ Δ (or Δ ≻≻ Γ) to mean that Γ ≺ Δ and Δ ⊀ Γ. The following Lemmas 3.1-4 are trivial consequences of Lemmas 3.2-7 in [Bur80].

Lemma 3.1 The relation ≺ is transitive and left-connected (that is, if Δ ≺ Γ and Θ ≺ Γ, then either Δ ≺ Θ, or Θ ≺ Δ, or Θ = Δ).

Lemma 3.2 If P α ∈ Γ, then there exists a Δ such that Δ ≺ Γ and α ∈ Δ. If fα ∈ Γ, then there exists a Δ such that Δ ≻ Γ and α ∈ Δ.

Lemma 3.3 Assume P α ∈ Δ, Γ ≺ Δ and ¬p ∧ H¬p ∈ Γ. Then there exists a Θ such that Γ ≺ Θ ≺ Δ and α ∈ Θ.

Lemma 3.4 Assume ¬α ∧ ¬F α ∈ Δ, Γ ≺ Δ and F α ∈ Γ. Then there exists a Θ such that Γ ≺ Θ ≺ Δ and α ∈ Θ.

In this paper, we will consider a new relation, ≺_{A}, which is defined on the basis of the operator g_{A} in the same way as ≺ was defined by means of the operator G. This new relation corresponds to the relation <_{A} considered in Section 2.

Γ ≺_{A} Δ ≡^{def} {α : g_{A}α ∈ Γ} ⊆ Δ (≡ Δ ⊆ {α : f_{A}α ∈ Γ})  (3.2)

Axioms A8 and A9.1, and compactness arguments prove the following lemma.

axioms is provided which can replace rule R3 from Burgess’ axiomatization of Peircean logic.

This holds also for the axiomatization of AP-logic considered herein because the completeness proof uses R3 only in the Peircean fragment.

Lemma 3.5 1. The relation ≺_{A} is transitive and right-connected. 2. Γ ≺_{A} Δ ⇒ Γ ≺ Δ. 3. If f_{A}α ∈ Δ, then there exists a m.c.s. Γ such that Δ ≺_{A} Γ and α ∈ Γ.

Lemma 3.6 1. If F α ∧ g_{A}δ ∈ Γ, then there exists a Δ such that Γ ≺_{A} Δ and α ∧ δ ∈ Δ. 2. If f_{A}α ∈ Γ, ¬α ∧ g_{A}¬α ∈ Δ, and Γ ≺_{A} Δ, then there exists a Σ such that Γ ≺_{A} Σ ≺_{A} Δ and α ∈ Σ.

Proof. 1. By axiom A9.2, ⊢ F α → f_{A}α and hence f_{A}α ∧ g_{A}δ ∈ Γ which implies f_{A}(α ∧ δ) ∈ Γ by temporal logic validities. Then, Lemma 3.5 can be applied to prove the thesis.

2. By Lemma 3.5, we can consider a m.c.s. Σ ≻_{A} Γ such that α ∈ Σ. Since ¬α ∧ g_{A}¬α ∈ Δ, Σ ≠ Δ and Δ ⊀_{A} Σ and hence, by the right connectedness of ≺_{A}, we can conclude Σ ≺_{A} Δ. □

Lemma 3.7 If Γ ≺≺ Δ ≺ Σ and Γ ≺_{A} Σ, then Γ ≺_{A} Δ ≺_{A} Σ

Proof. Since Γ ≺≺ Δ, we can consider a formula α_{1} ∈ Δ such that H¬α_{1} ∈ Γ. Moreover, Γ ≺≺ Δ implies Γ ≠ Δ and hence there exists a formula α_{2} such that α_{2} ∈ Δ and ¬α_{2} ∈ Γ. Given any finite subset {δ_{1}, …, δ_{n}} of Δ, call δ the conjunction α_{1} ∧ α_{2} ∧ δ_{1} ∧ … ∧ δ_{n}; by truth functional tautologies, we have δ ∈ Δ and ¬δ ∧ H¬δ ∈ Γ.

Since Δ ≺ Σ and Γ ≺_{A} Σ, f_{A}(σ ∧ P δ) belongs to Γ for every conjunction σ = σ_{1} ∧ … ∧ σ_{m} of formulas in Σ. By axiom A10.1, f_{A}(δ ∧ f_{A}σ) is in Γ for all δ and σ as above and hence the thesis follows by compactness. □

Lemma 3.8 For every m.c.s. Γ, there exists a m.c.s. Γ^{∗} ⪯ Γ such that, for every Δ′ ≺ Δ ⪯ Γ^{∗}, Δ′ ≺_{A} Δ ≺_{A} Γ^{∗}.

Proof. If there is a m.c.s. Σ^{∗} ⪯ Γ such that {Σ : Σ ≺ Σ^{∗}} = ∅, then we can let Γ^{∗} be Σ^{∗}. Otherwise, P (q ∨¬q) ∈ Γ and hence, by Axiom A11, P H(α → Hf_{A}α) ∈ Γ for every formula α. The implication P Hβ_{1} ∧…∧P Hβ_{n} → P H(β_{1} ∧…∧β_{n}) is a Peircean validity and hence, by compactness, there exists a m.c.s. Γ′ ≺ Γ such that H(α → Hf_{A}α) ∈ Γ′ for every formula α. Since {Σ : Σ ≺ Γ′} ≠ ∅, we can consider a m.c.s. Γ^{∗} ≺ Γ′. The set Γ^{∗} and every Δ ≺ Γ^{∗} contain all formulas of the form α → Hf_{A}α.

This implies that, if Δ′ ≺ Δ ⪯ Γ^{∗}, then, for every α ∈ Γ^{∗} and β ∈ Δ, f_{A}α ∈ Δ and f_{A}β ∈ Δ′, and hence Δ′ ≺_{A} Δ ≺_{A} Γ^{∗}. □

4 Chronicles

The first definitions and results of this section concern the Peircean fragment of AP-logic and are borrowed from [Bur80]. Lemmas 4.3-6 below are Lemmas 3.9-12 in Burgess’ paper.

Definition 4.1 A chronicle on the tree T = ⟨T, <⟩ is a function C which assigns a m.c.s. to each element of T and such that, for all x, y ∈ T, x < y implies C(x) ≺ C(y).

We will be interested in the chronicles having some of the following five properties. Some of them are significant when the tree T is a linear order.

C1 ∀α, ∀x, y [x < y & P α ∈ C(y) & ¬α ∧ H¬α ∈ C(x) ⇒
∃z(x < z < y & α ∈ C(z))]
C2 ∀α, ∀x, y [x < y & F α ∈ C(x) & ¬α ∧ g¬α ∈ C(y) ⇒
∃z(x < z < y & α ∈ C(z))]
C3 ∀α, ∀x [P α ∈ C(x) ⇒ ∃y(y < x & α ∈ C(y))]
C4 ∀α, ∀x [F α ∈ C(x) ⇒ ∃y(x < y & α ∈ C(y))]
C5 ∀α, ∀x [fα ∈ C(x) ⇒ ∃y(x < y & α ∈ C(y))]

Definition 4.2 The chronicle C will be said: (1) gapless if C1,2 above hold,

(2) historic if C1-3 hold, (3) full if C1-3,5 hold. The chronicle C on the linear order T will be said: (4) prophetic if C1,2,4 hold, (5) perfect if C1-4 hold.

Lemma 4.3 For any Γ there exists a historic chronicle C on a denumerable linear order T such that T has a last element x_{0} with C(x_{0}) = Γ.

Lemma 4.4 For any Γ and any fα ∈ Γ there exists a prophetic chronicle C on a denumerable linear order T such that T has a first element x_{0} with C(x_{0}) = Γ and a later element x with α ∈ C(x).

Lemma 4.5 Let C be a historic chronicle on a linear order T . There exists an extension C′ of C to a perfect chronicle on a denumerable linear order T′ which is an extension of T .

Lemma 4.6 For any Γ and any gα ∈ Γ there exists a prophetic chronicle C on a denumerable linear order T such that T has a first element x_{0} with C(x_{0}) = Γ and, for every later element x, α ∈ C(x).

These results are used in [Bur80] to provide a Henkin construction which shows that the f_{A}-free fragment of PA-logic is complete for Peircean validity w.r.t. bundled trees. The results proved below will allow us to turn Burgess’ construction into a construction of an actualized bundled tree.

Definition 4.7 The function C is an A-chronicle on the a.t. ⟨T , A⟩ if it is a chronicle on T and, for all x, y ∈ T, x <_{A} y implies C(x) ≺_{A} C(y). An A-chronicle on the linear order T is an A-chronicle on ⟨T , A⟩, where A is the unique actualizing function on T .

Properties C6 and C7 below are the f_{A}-counterparts of properties C2 and C4 above.

\begin{matrix}C6 & \begin{matrix}∀α, ∀x, y [x <_{A} y & f_{A}α ∈ C(x) & ¬α ∧ g_{A}¬α ∈ C(y) ⇒ \\ ⇒ ∃z(x <_{A} z <_{A} y & α ∈ C(z))] \end{matrix} \\ C7 & ∀α, ∀x [f_{A}α ∈ C(x) ⇒ ∃y(x <_{A} y & α ∈ C(y))] \end{matrix}

Definition 4.8 The chronicle C will be said A-sound if it is an A-chronicle and C6,7 hold.

Lemma 4.9 For every Γ, there exists a linear order T = ⟨T, <⟩ and a prophetic A-sound chronicle C on it, such that ⟨T, <⟩ has a first element x_{0} with C(x_{0}) = Γ. This implies in particular that, for all g_{A}γ ∈ Γ and all x > x_{0}, γ ∈ C(x).

Proof. We will define T and C as unions ⋃_{i∈ω} T_{i} and ⋃_{i∈ω} C_{i}, where each T_{i} is a finite linear order ⟨T_{i}, <_{i}⟩ and each C_{i} is an A-chronicle on it. We let T_{0} be the linear order ⟨{x_{0}}, ∅⟩, in which x_{0} is an arbitrary object, and we let C_{0}(x_{0}) be Γ.

Consider any enumeration α_{0}, α_{1}, …, α_{n}, … of all formulas of the form F α, or P α, or f_{A}α, in which each formula occurs infinitely often. Assume that T_{n} and C_{n} have already been defined and that T_{n} consists of the points x_{0} <_{n} x_{1} <_{n} … <_{n} x_{N}. We assume, as inductive hypothesis, that C_{n}(x_{0}) ≺_{A} … ≺_{A} C_{n}(x_{N}). The linear order T_{n+1} and the A-chronicle C_{n+1} are defined according to the following three cases. Case 1: α_{n} is F α. If C_{n} and T_{n} do not contain any counterexample to C2 or to C4, we do nothing and let T_{n+1} and C_{n+1} be respectively T_{n} and C_{n}.

Otherwise, we consider the pairs (x_{i}, x_{i+1}), if any, such that F α ∈ C_{n}(x_{i}) and ¬α ∧ ¬F α ∈ C_{n}(x_{i+1}). Since C_{n}(x_{i}) ≺_{A} C_{n}(x_{i+1}), for every finite conjunction δ of formulas in C_{n}(x_{i+1}), f_{A}(¬α∧g¬α∧δ) belongs to C_{n}(x_{i}) and hence, by A10.2, this set contains also f_{A}(α ∧ f_{A}δ). By compactness, there exists a m.c.s. Σ such that C_{n}(x_{i}) ≺_{A} Σ_{i} ≺_{A} C_{n}(x_{i+1}) and α ∈ Σ_{i}. We consider a new object x′_{i} for each of these pairs and we extend <_{n} and C_{n} by letting x_{i} <_{n} x′_{i} <_{n} x_{i+1} and C_{n}(x′_{i}) = Σ_{i}.

If F α ∈ C_{n}(x_{N}), by Lemma 3.6 there exists a m.c.s. Σ such that C_{n}(x_{N}) ≺_{A} Σ and α ∈ Σ. We consider a new object x′_{N} and we extend <_{n} and C_{n} as above.

We let T_{n+1} and C_{n+1} be the linear order and the A-chronicle on it obtained in this way. Case 2: α_{n} is f_{A}α. We do nothing if C_{n} and T_{n} do not contain any counterexample to C6 or to C7. Otherwise, we consider the maximum index i such that f_{A}α ∈ C_{n}(x_{i}); then either i = N or C_{n}(x_{i+1}) contains ¬α∧g_{A}¬α. In both cases, by Lemma 3.5, we can consider a m.c.s. Σ such that α ∈ Σ and C_{n}(x_{i}) ≺_{A} Σ; in the second case, Lemma 3.6 yields also Σ ≺_{A} C_{n}(x_{i+1}). We add a new point x′_{i} to T_{n} and we extend <_{n} by setting x_{N} <_{n} x′_{i} or x_{i} <_{n} x′_{i} <_{n} x_{i+1} according to whether i = N or not. We set C_{n}(x′_{i}) = Σ and we let T_{n+1} and C_{n+1} be the linear order and the A-chronicle on it obtained in this way. Case 3: α_{n} is P α. If α ∨ P α ∈ C(x_{0}) (= Γ), we do nothing and we let T_{n+1} and C_{n+1} be respectively T_{n} and C_{n}. Otherwise, we consider the smallest index i such that P α ∈ C_{n}(x_{i+1}) and ¬α ∧ H¬α ∈ C_{n}(x_{i}).

By Lemma 3.3, there exists a m.c.s. Σ such that α ∈ Σ and Σ ≺ C_{n}(x_{i+1}). Since ¬α∧H¬α ∈ C_{n}(x_{i}), we have also C_{n}(x_{i}) ≺≺ Σ and hence, by Lemma 3.8, C_{n}(x_{i}) ≺_{A} Σ ≺_{A} C_{n}(x_{i+1}). Thus, we can consider a new object x′_{i} and extend <_{n} and C_{n} by letting x_{i} <_{n} x′_{i} <_{n} x_{i+1} and C_{n}(x′_{i}) = Σ.

This concludes the proof. Since the sequence α_{0}, α_{1}, …, α_{n}, … contains infinitely many occurrences of each α_{i}, no counterexample to C1,2,4,6,7 can be found in the linear order T with the chronicle C. □

Lemma 4.10 If Γ ≺ Δ, then there exists a denumerable linear order T and a gapless chronicle C on it such that T has a first element x_{0} with C(x_{0}) = Γ and a last element y_{0} with C(y_{0}) = Δ.

Proof. We start with a two-point tree x_{0} <_{0} y_{0} and the chronicle C_{0} defined by C_{0}(x_{0}) = Γ and C_{0}(y_{0}) = Δ. Then we use the techniques of the previous lemma. □

Lemma 4.11 Let Γ^{∗} be as in Lemma 3.9. Then there exists a denumerable linear order T and a perfect chronicle C on it such that (1) C is A-sound, and (2) C(x_{0}) = Γ^{∗} for some x_{0} in T .

Proof. We start with a one-point linear order ⟨{x_{0}}, ∅⟩ and the chronicle C_{0} defined by C_{0}(x_{0}) = Γ^{∗}. Then, we use the techniques of Lemma 4.9 in order to eliminate every counterexample to C1-4,6,7. The case in which α_{n} is P α and P α ∈ C_{n}(z_{0}), where z_{0} is the first element of T_{n}, is dealt with by extending T_{n} with a new element x <_{n} z_{0} and by letting C_{n}(x) be any Δ ≺ C_{n}(z_{0}) such that α ∈ Δ. Since z_{0} ≤_{n} x_{0} and C_{n}(x_{0}) = Γ^{∗}, Lemma 3.9 can be applied. □

5 Completeness

Lemma 5.1 Assume that: (1) C is a full A-sound chronicle on the actualized bundled tree ⟨T , B, A⟩, (2) for every h ∈ B, the restriction of C to h is prophetic, and (3) the evaluation V on T is defined by V (p) = {t : p ∈ C(t)}. Then, for every moment x and every L_{AP} -formula α,

⟨T , B, A⟩, V ⊧_{x} α iff α ∈ C(x)  (5.1)

Proof. By induction on the complexity of α. □

Theorem 5.2 Every m.c.s. Γ is satisfiable in an actualized bundled tree.

Proof. The construction of the a.b.t. in which Γ turns out to be satisfiable consists of ω stages. At Stage 0 we first consider the two-history tree T_{−1} of Figure 3 and a chronicle C_{−1} on it such that: 1) C_{−1}(y_{0}) = Γ, 2) C_{−1}(x_{0}) is any Γ^{∗} ≺ Γ fulfilling the condition of Lemma 3.9, 3) the marked history h^{∗} and the restriction of C_{−1} to it are, respectively, the linear order T and the perfect Aprophetic A-chronicle C constructed in Lemma 4.11, and 4) the interval [x_{0}, y_{0}] and the restriction of C_{−1} to it are, respectively the linear order T and the gapless chronicle C constructed in Lemma 4.10.

Then, for each y in the left-open interval ]x_{0}, y_{0}] we consider a linear order T_{y}^{A} having y as first element and a chronicle C_{y}^{A} on it having the same properties as T and C in Lemma 4.9 with Γ = C_{−1}(y); we assume also that the linear

[figure: h^{∗}; x_{0}; T_{−1}; y_{0}; h^{∗}; x_{0}; T_{0}; y_{0}] Figure 3

orders T_{y}^{A} are pairwise disjoint and that y is the only moment which belongs to both T_{−1} and T_{y}^{A}.

We let T_{0} be the smallest tree which has T_{−1} and each T_{y}^{A} as subtrees (see Figure 3) and we let C_{0} be the union of C_{−1} and of all C_{y}^{A}’s. For every x ∈ h^{∗}, we set A_{0}(x) = h^{∗} and, for any y in ]x_{0}, y_{0}] and every z in T_{y}^{A} we let A_{0}(z) be the history in T_{0} which contains T_{y}^{A}. Thus, A_{0} is an actualizing function on T_{0} and C_{0} is a gapless A-sound chronicle on ⟨T_{0}, A_{0}⟩. The chronicle C_{0} is also historic. In fact, the restriction of C_{0} to h^{∗} is historic and, for every x ∉ h^{∗}, if P α ∈ C_{0}(x) and ¬(α ∨ P α) ∈ C_{0}(x_{0}), then we can use the gaplessness of C_{0} to conclude that α ∈ C_{0}(z) for some z <_{0} x.

The next stages are dealt with on the basis of a sequence α_{0}, …, α_{n}, … of all formulas of the form fα, or gα in which each formula occurs infinitely often. Call T_{n} = ⟨T_{n}, <_{n}⟩ and C_{n} the tree and the A-chronicle on it defined at the n-th stage. We assume that C_{n} is gapless and A-sound. Case 1: α_{n} is fα. We consider the set X of moments x in T_{n} such that fα ∈ C_{n}(x) and α ∉ C_{n}(y) for every y >_{n} x. By Lemma 4.4, for each x ∈ X we can consider a linear order T_{x} = ⟨T_{x}, <_{x}⟩ and a prophetic chronicle C_{x} on it such that x is the first element of T_{x}, C_{x}(x) = C_{n}(x), and α ∈ C_{x}(y) for some y >_{x} x. We assume also that the sets T_{x} are pairwise disjoint and that T_{x} ∩ T_{n} = {x}. We set

T′_{n} = T_{n} ∪ ⋃_{x∈X} T_{x} and C′_{n} = C_{n} ∪ ⋃_{x∈X} C_{x}

and we let <′_{n} be the smallest order relation which contains <_{n} and each <_{x}. Call T′_{n} the tree defined in this way.

For every y ∈ T′_{n} − T_{n}, we now consider a linear order T_{y}^{A} and a chronicle C_{y}^{A} on T_{y}^{A} like at Stage 0. We let T_{n+1} be the smallest tree which contains T′_{n} and each T_{y}^{A} as subtrees and we let C_{n+1} be the union of C′_{n} and all C_{y}^{A}’s. For each y ∈ T′_{n} − T_{n} and every z in T_{y}^{A}, we let A′_{n}(z) be the history in T_{n+1} which contains T_{y}^{A}; this implies in particular z ∈ A′_{n}(z). Finally, we let A_{n+1} be A_{n} ∪ A′_{n}.

On the basis of this construction, we can observe that:

(a) Every history in T_{n} is also a history in T_{n+1} and the domain of A′_{n} is T_{n+1} − T_{n}. Thus, A_{n+1} is a function from moments to histories in T_{n+1}.

(b) If z <_{n+1} z′ are moments T_{n+1} − T_{n} and z′ ∈ A′_{n}(z), then there is a y ∈ T′_{n} − T_{n} such that z and z′ belong T_{y}^{A}, and hence A′_{n}(z) = A′_{n}(z′).

(c) A_{n+1} contains A_{0} and hence, for every t^{∗} ∈ h^{∗} and every t < t^{∗}, A_{n+1}(t) = A_{n+1}(t^{∗}).

Thus, A_{n+1} is an actualizing function on T_{n+1}, and C_{n+1} is a gapless Asound chronicle on the actualized tree ⟨T_{n+1}, A_{n+1}⟩. Case 2: α_{n} is gα. We proceed like in Case 1, using Lemma 4.6 instead of Lemma 4.4. The set X considered in this case is the set of all moments x, in T_{n}, such that gα ∈ C_{n}(x) and every history passing through x in T_{n} contains a point y such that α ∉ C_{n}(y).

Call T the tree in which T and < are respectively the union of all T_{n} and of all <_{n}. By (a) above, every history in some T_{n} is also a history in T ; thus, the set B = ∪_{n∈ω}H(T_{n}) is a bundle on T .

Every finite set of moments in T is contained in some T_{n}. Thus: (i) A = ∪_{n∈ω}A_{n} is actualizing function on ⟨T , B⟩, (ii) C = ∪_{n∈ω}C_{n} is an A-chronicle on ⟨T , B, A⟩, and (iii) the A-chronicle C is gapless and A-sound.

Moreover, the construction above shows that: (iv) for every moment x in T and every fα ∈ C(x), there is moment x′ such that α ∈ C(x′), (v) for every moment x, there is a x′ ∈ h^{∗} such that x′ ≤ x, and (vi) the restriction of C to every element of B is prophetic.

Then, (v) implies that the proof that C_{0} is historic applies to C too, and hence, by (iv), C is full. By Lemma 5.1 and (vi), this concludes the proof. □

In general, the bundle B of the previous proof is different from the set H(T ) of all histories in T . Example 4.3 in [Bur80] shows that, for suitable choices of Γ, (5.1) fails if T and C are constructed as above and B = H(T ): it can happen that, for some h ∈ H(T ) and x ∈ h, F α ∈ C(x), but α ∉ C(y) for every y > x in h. Then, Theorem 5.2 does not answer the question of the satisfiability of m.c.s.’s in actualized trees.

As far as Peircean logic is concerned, though, this question is answered by Theorem 4.5 in [Bur80], and the proof of this theorem can be easily turned into a proof for Actualized Peircean logic. Roughly, we can start with the tree T and the A-chronicle C of Theorem 5.2, and consider the histories in H(T ) on which the restriction of C is not prophetic. We extend these histories and C with new points in order to eliminate the corresponding counterexamples to C4. Of course, having new points requires new constructions like that of Theorem 5.2 and this generates new histories. The proof of Theorem 4.5 in [Bur80], however, shows that ω_{1} applications of this procedure lead to a tree T^{∗} with a full Asound chronicle C^{∗} such that the restriction of C^{∗} to any history in H(T^{∗}) is prophetic. Thus,

Theorem 5.3 Every m.c.s. Γ is satisfiable in an actualized tree.

Acknowledgements

Part of this work was written while the second author held a grant from the Portuguese FCT in the Centro de Matemática Aplicada of the Instituto Superior Tećnico of Lisbon. The authors wish also to thank Maria Concetta Di Maio, Javier Pinto, and Jaime Ramos for helpful suggestions and observations.

References

[Bar96] B. Barcellan. Risultati di completezza e definibilità in logiche del tempo ramificato. ‘Laurea’ dissertation, Facoltà di Scienze MM.FF.NN., Università di Padova, July 1996.

[BG93] N. Belnap and M. Green. Wagering on the future. Manuscript, 1993.

[BG94] N. Belnap and M. Green. Indeterminism and the Thin Red Line. Philosophical Perspectives, 8: Logic and Language:365–388, 1994.

[BHØ98] T. Braüner, P. Hasle, and P. Øhrstrøm. Ockhamistic logics and true futures of counterfactual moments. In L. Khatib and R. Morris, editors, Proceedings of Fifth International Workshop on Temporal Representation and Reasoning, pages 132–139. IEEE Press, 1998. Affiliated to 11th Annual Florida Artificial Intelligence Research Symposium.

[Bur79] J. Burgess. Logic and time. J. of Symbolic Logic, 44:556–582, 1979.

[Bur80] J. Burgess. Decidability for branching time. Studia Logica, 39:203– 218, 1980.

[Gab81] D. Gabbay. An irreflexivity lemma with applications to axiomatizations of conditions on tense frames. In U. Mönnich, editor, Aspects of Philosophical Logic, pages 67–89. Reidel, Dordrecht, 1981.

[ØH95] P. Øhrstrøm and P. F. V. Hasle. Temporal Logic: From Ancient Ideas to Artificial Intelligence. Studies in Linguistic and Philosophy. Reidel, Dordrecht, 1995.

[Pin98] J. Pinto. Occurrences and narratives as constraints in the branching structure of the situation calculus. J. of Logic and Computation, 8(6):777–808, 1998.

[PR95] J. Pinto and R. Reiter. Reasoning about time in the situation calculus. Annals of Mathematics and Artificial Intelligence, 14:251–268, 1995.

[Pri67] A. Prior. Past, Present and Future. Clarendon, Oxford, 1967.

[TG80] R. Thomason and A. Gupta. A theory of conditionals in the context of branching time. In W. L. Harper, R. Stalnaker, and G. Pearse, editors, Ifs: Conditionals, Belief, Decision, Chance and Time, pages 299–322. Reidel, Dordrecht, 1980.

[Zan90] A. Zanardo. Axiomatization of ‘Peircean’ Branching-Time Logic. Studia Logica, 49(2):183–195, 1990.