Axiomatization of a Branching Time Logic with Indistinguishability Relations

Branching-time logics have traditionally played a major role in modelling non-deterministic theories about time. Since [12], two main semantics for logics of branching-time have been considered. Prior called Peircean and Ockhamist these semantics. The essential difference between them is the interpretation of the future operator F in a tree-like representation of time.

In Peircean semantics, F φ is read as “eventually in the future, on every history passing through the moment under consideration, φ will happen”. Peircean language has also a future operator G, whose interpretation is “always in the future, on every history passing through the moment under consideration”. The Ockhamist interpretation of F φ, instead, is relative to pairs (m o m e n t, h i s t o r y), and F φ is read as “eventually in the future, on the history under consideration, φ will happen”. The Ockhamist language counterpart of the branching aspect of time is a modal operator L that quantifies over the set of histories passing through the moment under consideration.

Various works on logics of agency consider a partition of this set into undividedness classes, e.g. [3]: two histories are undivided at t whenever their intersection contains a moment in the future of t.

In [22], a generalization of the notion of undividedness is considered: at any moment t, an equivalence relation I _t (indistinguishability at t) between the histories passing through t is given. The only property of the indistinguishability relations is that, if two histories are indistinguishable at a moment t, they are also indistinguishable at every moment in the past of t (indistinguishability condition). This implies, in particular, that undividedness is a particular case of indistinguishability.

Trees with indistinguishability relations (I-trees) provide a semantics for a temporal language with tense and modal operators [22]. In this semantics, truth is relative to pairs (t, π), where t is a moment and π is an indistinguishability class at t, and the modal operator quantifies over indistinguishability classes. The tense operators have a Peircean reading, but the implicit quantification over histories is restricted to the indistinguishability class under consideration.

As it is pointed out in [22], Ockhamist and Peircean semantics correspond to the limit cases of the I-tree semantics in which each (respectively, no) history passing through t is distinguishable at t from any other.

In this paper, a finite axiomatization with a non standard rule for such a language interpreted over bundled I-trees with indistinguishability relations is given. This axiomatization is proved to be sound and strongly complete.

The syntax and the semantics are presented in Section 2. The language considered has, as tense operators, F and G for the future and H for the past, and, as modal operator, L. F, G and L are interpreted as explained above. H is interpreted as “always in the past, on every history passing through the class under consideration”. The semantics is given with respect to the class of bundled I-trees, instead of with respect to trees. A bundle on a tree is a selection of the histories of the tree such that every moment occurs in at least one history of the bundle. Moreover, trees are required to be upward endless. The indistinguishability relations and the quantification of the tense operators are restricted to the histories selected by the bundle.

There are two main reasons why we consider bundled I-trees instead of I-trees. A technical one: the Soundness and Strong Completeness Theorem is achieved by a particular construction in which only histories of a particular kind are desired and the bundle let us select these histories (cf. Section 4 Question 2). And a conceptual one: it has been argued, e.g. in [10, 11], that bundled validity is a more correct formalization of human intuition about time and possibility (nonetheless, we cannot avoid to report that, e.g. in [14], doubts about preferring bundled validity have been raised).

In Section 2, the Hilbert system is also presented. This Hilbert system is a “mix” of the Hilbert system for Peircean semantics presented in [2] and the Hilbert system for Ockhamist semantics presented in [7, Section 7.7, pp. 299–306].

Among the deduction rules of the system, a form of the IRR rule occurs. IRR rules have been introduced in [6], where it is shown that they can characterize irreflexivity, a property that, as it is well known, cannot be characterized by modal axioms.

A version of this rule is employed here because it yields important properties of the structure built to prove the Soundness and Strong Completeness Theorem (cf. Section 3.2, in particular Remark 15).

The completeness theorem is achieved in Section 3 by a construction adapted from [2], mostly for what concerns the Peircean aspects of the logic, and from [7, Section 7.7, pp. 299–306], mostly for what concerns the Ockhamist aspects of the logic.

1.1 Historical Background

As mentioned, Peircean and Ockhamist semantics have been introduced in [12]. Peircean logic has been axiomatized in [2] with a form of the IRR rule and in [20] without. The bundled version of Ockhamist logic has been axiomatized in [19] without IRR rule (an axiomatization with a form of the IRR rule due to Gabbay is cited in [18]). An axiomatization of the unbundled Ockhamist logic and a brief sketch of the completeness proof have been presented in [15].

Many other logics of branching time have been introduced. All of them are some kind of variation of either Peircean or Ockhamist logic. E.g., in [19] and [20], the temporal operators G and H are replaced by the more expressive ‘Since’ and ‘Until’ operators from [8]. Branching time logics are often used in computer science. Here, since time simulates the steps of a computation, time is assumed discrete. Example of such logics are the Peircean logics UB of [1], CTL of [4], the Ockhamist version CTL* of [5] and the P-extension of CTL*, PCTL*, of [9, 21]. Also many of these logics have been axiomatized. E.g., bundled CTL* in [17], CTL* in [13] and PCTL* in [16].

As for the notion of ‘indistinguishability’, the semantics with ‘indistinguishability’ relations has been defined in [22] as a generalization of the semantics with ‘undividedness’ relations of [3].

In this section the syntax, the semantics and the Hilbert system are given.

2.1 Syntax

Here, the language and what a formula is are defined.

Definition 1

Let PV be a countably infinite set. The elements of PV are called atoms. The set \(\mathcal {L}=PV\cup \{(,), \neg ,\wedge ,G,F,H,L\}\) is called language. Formulas are strings of language elements built up recursively according to the following rules:

1. 1.

   p ∈ P V is a formula.

2. 2.

   If φ and ψ are formulas, (¬φ), (φ ∧ ψ), (G φ), (F φ), (H φ) and (L φ) are formulas.

∨, → and ↔ are the usual abbreviations. P abbreviates ¬H¬, f abbreviates ¬G¬, g abbreviates ¬F¬, and M abbreviates ¬L¬. The usual precedence rules among operators are assumed. Call theory any set of formulas.

2.2 Semantics

Here, a number of definitions are given in order to define the semantics. After them, satisfiability and validity for a formula, and semantical entailment of a formula from a theory are defined.

Definition 2

A binary relation R over a set A is called downward linear if, for each a, b, c ∈ A such that b R a and c R a, b = c or b R c or c R b. A binary relation R over a set A is called linear if, for each a, b ∈ A, a = b or a R b or b R a. A binary relation R over a set A is called upward endless if, for each a ∈ A, there is b ∈ A such that a R b.

Definition 3

A tree is a 2-tuple (T, <), where T is a set and < is an irreflexive, transitive and downward linear binary relation on T.

Definition 4

Given a tree \(\mathcal {T}=(T,< )\), we call history any ⊆-maximal <-linear h ⊆ T. \(H_{\mathcal {T}}\) denotes the set of histories in \(\mathcal {T}\). Given t ∈ T, \(H_{\mathcal {T},t}\) denotes the set of histories h in \(\mathcal {T}\) passing through t, that is with t ∈ h.

Remark 5

Given a tree \(\mathcal {T}=(T,< )\), and a non empty linear subset S ⊆ T, by Zorn’s Lemma, it is possible to extend S to a history.

Definition 6

Given a tree \(\mathcal {T}=(T,< )\), a subset \(B\subseteq H_{\mathcal {T}}\) is called bundle if it fulfils \(T=\bigcup _{h\in B}h\). Given a tree (T, <) and a bundle B, the 3-tuple (T, <, B) is called bundled tree. Given a bundled tree (T, <, B) and t ∈ T, B _t denotes the set of histories h ∈ B passing through t.

Definition 7

Given a bundled tree (T, <, B), a function \(I:T\rightarrow \mathcal {P}(B\times B)\), t ↦ I _t , is called indistinguishability function if it fulfils the following condition:

1. 1.

   I _t is an equivalence relation over B _t .

2. 2.

   For every h, k ∈ B and every t, s ∈ h ∩ k, with t < s, if h I _s k then h I _t k.

Given a bundled tree (T, <, B) and an indistinguishability function \(I:T\rightarrow \mathcal {P}(B\times B)\), the 4-tuple (T, <, B, I) is called bundled I-tree. Given a bundled I-tree \(\mathcal {T}=(T,<,B,I)\) and t ∈ T, \({\Pi }_{\mathcal {T},t}\) denotes the set of the equivalence classes of I _t .

The suffixes will be forgotten when there is no case of confusion.

Definition 8

A 4-tuple \(\mathcal {F}= (T,<,B,I )\) is called frame if (T, <, B, I) is a bundled I-tree and < is upward endless. A 5-tuple \(\mathcal {M}= (T,<,B,I,V )\) is called model if (T, <, B, I) is a frame for \(\mathcal {L}\) and \(V:PV\rightarrow \mathcal {P} (\bigcup _{t\in T}(\{t\}\times {\Pi }_{\mathcal {T},t}))\) is a function, called evaluation.

Definition 9

Given any model \(\mathcal {M}= (T,<,B,I,V )\), any atom p, any two formulas φ and ψ, define

1. 1.

   \(\mathcal {M},(t,\pi )\models p\) if (t, π) ∈ V(p).

2. 2.

   \(\mathcal {M},(t,\pi )\models \neg \varphi \) if \(\mathcal {M},(t,\pi )\not \models \varphi \).

3. 3.

   \(\mathcal {M},(t,\pi )\models \varphi \wedge \psi \) if \(\mathcal {M},(t,\pi )\models \varphi \) and \(\mathcal {M},(t,\pi )\models \psi \).

4. 4.

   \(\mathcal {M},(t,\pi )\models G\varphi \) if, for each h ∈ π and each s ∈ h with \(t<s,\mathcal {M},(s,[h]_{I_{s}})\models \varphi \).

5. 5.

   \(\mathcal {M},(t,\pi )\models F\varphi \) if, for each h ∈ π, there is s ∈ h with t < s such that \(\mathcal {M},(s,[h]_{I_{s}})\models \varphi \).

6. 6.

   \(\mathcal {M},(t,\pi )\models H\varphi \) if, for each h ∈ π and each s ∈ h with s < t, \(\mathcal {M},(s,[h]_{I_{s}})\models \varphi \).

7. 7.

   \(\mathcal {M},(t,\pi )\models L\varphi \) if, for each ρ ∈ π _t , \(\mathcal {M},(t,\rho )\models \varphi \).

If \(\mathcal {M},(t,\pi )\models \varphi \), we say that \(\mathcal {M},(t,\pi )\) satisfies φ. If φ is satisfied at each (t, π) in \(\mathcal {M}\), we say that \(\mathcal {M}\) satisfies φ, written \(\mathcal {M}\models \varphi \). If φ is satisfied in every \(\mathcal {M}\), we say that φ is valid, written ⊧φ. Finally, given a set of formulas Δ and a formula φ, we say that Δsemantically entails φ, written Δ ⊧ φ, if, for each model \(\mathcal {M}=(T,{<,}B,I,h)\), each t ∈ T and each π ∈ π _t such that \(\mathcal {M},(t,\pi )\models \psi \) for all ψ ∈ Δ, \(\mathcal {M}, (t,\pi )\models \varphi \).

2.3 Hilbert System

Here, the Hilbert system is given, and provability for a formula and syntactical entailment of a formula from a theory are defined.

The Hilbert system is a “mix” of the Hilbert system for Peircean semantics presented in [2] and the Hilbert system for Ockhamist semantics presented in [7, Section 7.7, pp. 299–306]. In particular, axioms 1b – 1n come from [2]. Axioms 1o – 1r are S 5 for L, exactly as in [7, Section 7.7, pp. 299–306], while axioms 1s and 1t are adapted from [7, Section 7.7, pp. 299–306] to the present context. Among the deduction rules of the system, a form of the IRR rule occurs. A form of the IRR rule also occurs in both [2] and [7, Section 7.7, pp. 299–306].

Definition 10

Here is the Hilbert system:

1. 1.

   Axioms: let p, q be any two distinct atoms

   1. (a)

      All propositional logic tautologies.

   2. (b)

      H(p → q) → (H p → H q).

   3. (c)

      G(p → q) → (G p → G q).

   4. (d)

      G(p → q) → (F p → F q).

   5. (e)

      p → H f p.

   6. (f)

      p → G P p.

   7. (g)

      H p → H H p.

   8. (h)

      G p → G G p.

   9. (i)

      F F p → F p

   10. (j)

       G p → F p.

   11. (k)

       G p → g p.

   12. (l)

       H p ∧ p ∧ G p → G H p.

   13. (m)

       H p ∧ p ∧ g p → g H p.

   14. (n)

       F G p → G F p.

   15. (o)

       L(p → q) → (L p → L q).

   16. (p)

       L p → L L p.

   17. (q)

       L p → p.

   18. (r)

       p → L M p.

   19. (s)

       M P p → P M p.

   20. (t)

       H p ∧ ¬p ∧ L q → G L H(M(H p ∧ ¬p) → q).

2. 2.

   Inference rules: let p be any atom, φ and ψ any two distinct formulas

   1. (a)

      Substitution \(\frac {\varphi }{\varphi (\psi /p)}\).

   2. (b)

      Generalization \(\frac {\varphi }{G\varphi }\); \(\frac {\varphi }{H\varphi }\); \(\frac {\varphi }{ L\varphi }\).

   3. (c)

      Modus Ponens \(\frac {\varphi , \varphi \rightarrow \psi }{\psi }\).

   4. (d)

      IRR rule \(\frac {Hp\wedge L\neg p\rightarrow \varphi }{\varphi }\) where p is an atom not occurring in φ.

We say that φ is provable, written ⊢ φ, if, for some sequence of formulas ψ ₁, ... , ψ _m = φ, we have that, for each i = 1, ... , m, ψ _i is either an axiom or is obtained from some formulas in {ψ ₁, ... , ψ _{i − 1}} by the application of an inference rule. A set of formulas Δsyntactically entails φ, written Δ ⊢ φ, if there are formulas ψ ₁, ... , ψ _m ∈ Δ such that ⊢ ψ ₁ ∧ ... ∧ ψ _m → φ.

In this section the Soundness and Strong Completeness Theorem is proved. In Section 3.1 a number of preliminary results are given. In Section 3.2 the notion of IRR theory is defined and studied. In Section 3.3, for each IRR complete consistent theory Δ, a Kripke frame associated to Δ is defined. This Kripke frame is obtained through a selective filtration over the canonical model associated with the Hilbert System. This filtration is adapted from [2]. In Section 3.4, given an arbitrary IRR complete consistent theory Δ, the associated Kripke frame is turned into a model (over a bundled I-tree) for Δ. This model is defined through a filtration adapted from [7]. These results are then used in Section 3.5 to prove the Soundness and Strong Completeness Theorem.

3.1 Preliminary Results

In this Section a number of preliminary results are introduced. They will be used to study IRR theories in Sections 3.2 and 3.3.

Proposition 11

The following are provable results:

1. 1.

   if ⊢ p → q then ⊢ Gp → Gq.

2. 2.

   if ⊢ p → q then ⊢ Fp → Fq.

3. 3.

   if ⊢ p → q then ⊢ gp → gq.

4. 4.

   if ⊢ p → q then ⊢ fp → fq.

5. 5.

   if ⊢ p → q then ⊢ Hp → Hq.

6. 6.

   if ⊢ p → q then ⊢ Pp → Pq.

7. 7.

   ⊢ G(p ∧ q) ↔ Gp ∧ Gq.

8. 8.

   ⊢ f(p ∧ q) → fp ∧ fq.

9. 9.

   ⊢ P(p ∧ q) → Pp ∧ Pq.

10. 10.

    ⊢ Gp → fp.

11. 11.

    ⊢ fgp → fp.

12. 12.

    ⊢ Gp ∧ fq → f(p ∧ q).

13. 13.

    ⊢ Gp ∧ Fq → F(p ∧ q).

14. 14.

    ⊢ Fp ∧ gq → f(p ∧ q).

15. 15.

    ⊢ Hp ∧ Pq → P(p ∧ q).

16. 16.

    ⊢ gHp → p.

17. 17.

    If ⊢ p → q, then ⊢ Lp → Lq.

18. 18.

    If ⊢ p → q, then ⊢ Mp → Mq.

19. 19.

    ⊢ Lp ∧ Mq → M(p ∧ q)

20. 20.

    ⊢ Hp ∧ p ∧ gp → Hgp.

21. 21.

    ⊢ Hp ∧ gq → gH(P¬p → q).

Proof

Here is a sketch of the proofs.

1. 1.

   Straight from axiom 1c (G(p → q) → (G p → G q)).

2. 2.

   Straight from axiom 1d (G(p → q) → (F p → F q)).

3. 3.

   By axiom 1d (G(p → q) → (F p → F q)), ⊢ F¬q → F¬p.

4. 4.

   By axiom 1c (G(p → q) → (G p → G q)), ⊢ G¬q → G¬p.

5. 5.

   Straight from axiom 1b (H(p → q) → (H p → H q)).

6. 6.

   By axiom 1b (H(p → q) → (H p → H q)), ⊢ H¬q → H¬p.

7. 7.

   ( → ): ⊢ G(p ∧ q) → G p and ⊢ G(p ∧ q) → G q. (←): G p → (G q → G(p ∧ q)).

8. 8.

   By Proposition 11.4, ⊢ f(p ∧ q) → f p and ⊢ f(p ∧ q) → f q.

9. 9.

   By Proposition 11.6, ⊢ P(p ∧ q) → P p and ⊢ P(p ∧ q) → P q.

10. 10.

    Straight from axioms 1j (G p → F p) and 1k (G p → g p).

11. 11.

    By axiom 1j (G p → F p), ⊢ f g p → f f p. Thus, by axiom 1h (G p → G G p), ⊢ f g p → f p.

12. 12.

    ⊢ G p → (G¬(p ∧ q) → G¬q). Thus, ⊢ G p → (¬G¬q → ¬G¬(p ∧ q)).

13. 13.

    ⊢ G p → (F q → F(p ∧ q)).

14. 14.

    By axiom 1d (G(p → q) → (F p → F q)), ⊢ G¬(p ∧ q) → (F p → F¬q). Thus, F p ∧ ¬F¬q → ¬G¬(p ∧ q).

15. 15.

    ⊢ H p → (H¬(p ∧ q) → H¬q). Thus, ⊢ H p → (¬H¬q → ¬H¬(p ∧ q)).

16. 16.

    Straight from axioms 1f (p → G P p) and 1j (G p → F p).

17. 17.

    Straight from axiom 1o (L(p → q) → (L p → L q)).

18. 18.

    By axiom 1o (L(p → q) → (L p → L q)), ⊢ L¬q → L¬p.

19. 19.

    ⊢ L p → (L¬(p ∧ q) → L¬q). Thus, ⊢ L p → (¬L¬q → ¬L¬(p ∧ q)).

20. 20.

    By axiom 1f (p → G P p), ⊢ P F p → P F G P p. By axiom 1n (F G p → G F p), P F G P p → P G F P p. Thus, ⊢ P F p → P G F P p. Thus, by axiom 1e (p → H f p), ⊢ P F p → F P p. Thus, ⊢ g H p → H g p. Thus, by axiom 1m (H p ∧ p ∧ g p → g H p), H p ∧ p ∧ g p → H g p.

21. 21.

    ⊢ H p → ¬P¬p ∨ q. Thus, by axiom 1g (H p → H H p), H p → H(¬P¬p ∨ q). Moreover, g q → g(¬P¬p ∨q). Thus, H p ∧ g q → H(¬P¬p ∨ q) ∧ (¬P¬p ∨ q) ∧ g(¬P¬p ∨ q). Thus, by axiom 1m (H p ∧ p ∧ g p → g H p), H p ∧ g q → g H(¬P¬p ∨ q).

□

Proposition 12

⊢ P(p ∧ Fq) → P(Pp ∧ q) ∨ q ∨ Fq.

Proof

Let φ stand for P p ∧ q. Easily, ⊢ P(p ∧ F q) → P(G P p ∧ F q), ⊢ P(G P p ∧ F q) → P F(P p ∧ q). Thus

Moreover ⊢¬P(P p ∧ q) → H¬(P p ∧ q), ⊢¬q → ¬(P p ∧ q), ¬F q → g¬(P p ∧ q). This yields ⊢ ¬P(P p ∧ q) ∧ ¬q ∧ ¬F q → H¬φ ∧ ¬φ ∧ g¬φ. Proposition 11.20 (H p ∧ p ∧ g p → H g p) gives

Combining Eqs. 1 and 2, we obtain

Therefore, ⊢¬(P(p ∧ F q) ∧ ¬P(P p ∧ q) ∧ ¬q ∧ ¬F q). □

Definition 13

□ is a variable ranging over {H, G, L}. ◊ abbreviates ¬□¬. H ⁻ stands for G, G ⁻ stands for H, L ⁻ stands for L.

Proposition 14

Let φ, ψ, χ ₁, χ ₂, ... , χ _n be formulas. If

then

Proof

First, we prove by induction on j = 0, 1, ... , n, that

From (3), we obtain

Hence,

Axioms 1f (p → G P p), 1e (p → H f p), 1r (p → L M p) and Modus Ponens entail

This is (5) for j = 0.

Consider a natural number m such that 0 ≤ m < n, and assume (5) for j = m. Proceeding as before we get

With a little bit of propositional work, this gives (5) for j = m + 1.

Therefore

The same procedure yields (4). □

3.2 IRR Complete Consistent Theories

IRR theories are introduced in order to obtain a number of properties for the Kripke frame defined in Section 3.3. In particular, points 3 and 4 of Proposition 38, which are consequences of respectively Propositions 25 and 26. The peculiarity of the IRR theories is that they contain a “name” (a formula of the form H p ∧ L¬p, for some atom p) for themselves and for each theory finitely reachable by a sequence of R ∪ R ⁻¹ ∪ S-steps. This fact immediately yields Proposition 25, and allow the use of axiom 1t to prove Proposition 26.

Remark 15

The use of IRR complete consistent theories is allowed by Propositions 18 and 19. In proving these propositions, the IRR rule is crucial.

Definition 16

A theory Δ is consistent if, for every n ∈ ℕ, every φ ₁, φ ₂,...φ _n ∈ Δ, \(\not \vdash \neg \bigwedge _{i=1}^{n} \varphi _{i}\). It is complete if, for all formulas φ, φ ∈ Δ or ¬φ ∈ Δ. It is IRR if the following conditions hold:

1. 1.

   For some atom p, H p ∧ L¬p ∈ Δ.

2. 2.

   For each formula φ ∈ Δ, for each n ∈ ℕ, if φ can be read as ◊₁(ψ ₁ ∧ ◊₂(ψ ₂ ∧ ... ∧ ◊ _n ψ _n ))...), then for some q not occurring in φ, ◊₁(ψ ₁ ∧ ◊₂(ψ ₂ ∧ ... ∧ ◊ _n (H q ∧ L¬q ∧ ψ _n ))...) ∈ Δ.

Remark 17

It is easily provable that, for each n ∈ ℕ, if a formula φ can be read as ◊₀(ψ ₀ ∧ ◊₁(ψ ₁ ∧ ... ∧ ◊ _n ψ _n ))...) and as \(\Diamond _{0}^{\prime }(\psi _{0}^{\prime }\wedge \Diamond _{1}^{\prime }(\psi _{1}^{\prime }\wedge ... \wedge \Diamond _{n}^{\prime } \psi _{n}^{\prime }))...)\), then, for all i = 0, 1, ... , n, \(\Diamond _{i}=\Diamond ^{\prime }_{i}\) and \(\psi _{i}=\psi ^{\prime }_{i}\).

Proposition 18

If Δ is a consistent theory and p an atom not occurring in any φ ∈ Δ, then Δ ∪ {Hp ∧ L¬p} is consistent.

Proof

Suppose Δ ∪ {H p ∧ L¬p} is inconsistent. Then, there is n ∈ ℕ and δ ₀, δ ₁, ... , δ _n ∈ Δ such that

By propositional logic, this is equivalent to

By IRR rule, this yields

which is against the consistency of Δ. □

Proposition 19

Let Δ′ be a consistent theory such that the number of atoms not occurring in any φ ∈ Δ′ is infinite. Then, there is an IRR complete consistent theory Δ such that Δ′ ⊆ Δ.

Proof

Define Δ₀ = Δ′ ∪ {H p ∧ L¬p}, for some atom p not occurring in any φ ∈ Δ′. By Proposition 18, Δ₀ is consistent.

Let (ψ ₀, m ₀), (ψ ₁, m ₁), ... be an enumeration of all pair (ψ _i , m _i ), where ψ _i is a formula, and, if m _i = 0, then ψ _i cannot be read as ◊₁(ψ ₁ ∧ ◊₂(ψ ₂ ∧ ... ∧ ◊ _n ψ _n ))...), if m _i ≠ 0, then ψ _i can be read as \(\Diamond _{1} (\psi _{1}\wedge \Diamond _{2}(\psi _{2}\wedge ... \wedge \Diamond _{m_{i}} \psi _{m_{i}}))...)\). Moreover, we can assume that φ _i is readable as ◊₁(ψ ₁ ∧ ◊₂(ψ ₂ ∧ ... ∧ ◊ _n ψ _n ))...) if and only if i is odd.

Assume Δ _n was defined. Either Δ _n ∪ {ψ _n } or Δ _n ∪ {¬ψ _n } is consistent. If Δ _n ∪ {¬ψ _n } is consistent, set Δ _{n + 1} = Δ _n ∪ {¬ψ _n }. Otherwise, if n is even set Δ _{n + 1} = Δ _n ∪ {ψ _n }. If n is odd, ψ _n can be read as \(\Diamond _{1} (\psi _{1}\wedge \Diamond _{2}(\psi _{2}\wedge ... \wedge \Diamond _{m_{n}} \psi _{m_{n}}))...)\). Since the number of atoms not occurring in any φ ∈ Δ is infinite, we can pick an atom q not occurring in any φ ∈ Δ _n ∪ {ψ _n }. Denote \(\Diamond _{1}(\psi _{1}\wedge \Diamond _{2}(\psi _{2}\wedge ... \wedge \Diamond _{m_{n}}(Hq\wedge L\neg q\wedge \psi _{m_{n}}))...)\) with ψ _n (q). We claim that Δ _n ∪ {ψ _n (q)} is consistent. If not, there is m ∈ N and δ ₀, δ ₁, ... , δ _m ∈ Δ _n such that \( \vdash \neg (\bigwedge _{i=0}^{m} \delta _{i}\wedge \psi _{n}(q))\). By propositional logic, that is

Thus, by Proposition 14,

Hence, by propositional logic,

Thus, by IRR rule,

Hence, by Proposition 14,

By propositional logic, that is \( \vdash \neg (\bigwedge _{i=0}^{m} \delta _{i}\wedge \psi _{n})\). This contradicts the consistency of Δ _n ∪ {ψ _n } and the claim is proved. Easily, ⊢ ψ _n (q) → ψ _n . Hence, Δ _n ∪ {ψ _n (q)} ∪ {ψ _n } is consistent as well. Define Δ _{n + 1} = Δ _n ∪ {ψ _n (q)} ∪ {ψ _n }. Easily, \({\Delta }=\bigcup _{n\in \mathbf {N}}{\Delta }_{n}\) is as desired. □

Proposition 20

Let Δ, Γ be complete consistent theories. The following conditions are equivalent:

1. 1.

   For every formula φ, Gφ ∈ Δ implies φ ∈ Γ.

2. 2.

   For every formula φ, φ ∈ Γ implies fφ ∈ Δ.

3. 3.

   For every formula φ, Hφ ∈ Γ implies φ ∈ Δ.

4. 4.

   For every formula φ, φ ∈ Δ implies Pφ ∈ Γ.

Proof

From 1. to 2. Assume 1. and that φ ∈ Γ and f φ ∉ Δ. Then, by completeness of Δ, G¬φ ∈ Δ whence, by 1., ¬φ ∈ Γ, against the consistency of Γ.

From 2. to 3. Assume 2. and that G φ ∈ Γ and ¬φ ∉ Δ. Then, by 2., f H φ ∈ Δ and, by completeness of Δ, ¬φ ∈ Δ. Then, by axiom 1f (p → G P p), G P¬φ ∈ Δ, against the consistency of Δ.

From 3. to 4. Similarly to from 1. to 2. From 4. to 1., similarly to from 2. to 3., using axiom 1e (p → H f p). □

Definition 21

Let Δ, Γ be IRR complete consistent theories. Define Δ ≺ Γ if one of the previous conditions holds. Define Δ ≼ Γ if Δ = Γ or Δ ≺ Γ. Γ ≻ Δ stands for Δ ≺ Γ. Γ ≽ Δ stands for Δ ≼ Γ.

Proposition 22

Let Δ, Γ be complete consistent theories. The following conditions are equivalent:

1. 1.

   For every formula φ, Lφ ∈ Δ implies φ ∈ Γ.

2. 2.

   For every formula φ, φ ∈ Γ implies Mφ ∈ Δ.

Proof

Similarly to proof of Proposition 20, from 1. to 2. □

Definition 23

Let Δ, Γ be two IRR complete consistent theories. Define Δ ∼ Γ if one of the previous conditions holds.

Proposition 24

Let φ be a formula and Δ an IRR complete consistent theory such that fφ ∈ Δ (respectively Pφ ∈ Δ, Mφ ∈ Δ). Then there is an IRR maximal consistent theory Γ such that Δ ≺ Γ (respectively Δ ≻ Γ, Δ ∼ Γ) and φ ∈ Γ.

Proof

By definition of IRR theory, we have

for some atom p. {H p ∧ L¬p ∧ φ} ∪ {ψ|G ψ ∈ Δ} is consistent. Otherwise

Define Γ₀ = {H p ∧ L¬p ∧ φ} ∪ {ψ|G ψ ∈ Δ}.

For the n + 1 case proceed as in Proposition 19, but, if Γ _n ∪ {¬ψ _n } is not consistent and n is odd, make sure that there is an atom q such that q does not occur in ψ _n and Γ _n ∪ {ψ _n (q)} is consistent. We claim that

Suppose not, then,

Thus,

This is against the consistency of Γ _n ∪ {ψ _n }. Therefore,

for q such as in Definition 16.2, i.e. not occurring in

and, thus, not occurring in ψ _n . Suppose Γ _n ∪ {ψ _n (q)} is inconsistent. Then, for ψ with G ψ ∈ Δ such that

Hence,

Thus,

However,

and

Then, Proposition 11.12 (⊢ G p ∧ f q → f(p ∧ q)) yields

This is a contradiction. Therefore Γ _n ∪ {ψ _n (q)} is consistent and q as desired. Define \({\Gamma }=\bigcup _{n\in \mathbf {N}}{\Gamma }_{n}\).

The cases in which P φ ∈ Δ or M φ ∈ Δ are similar. □

Proposition 25

≺ ∩ ∼= ∅.

Proof

Suppose not. Then, there are two IRR complete consistent theories Δ, Γ such that Δ ≺ Γ and Δ ∼ Γ. However, for some atom p, H p ∧ L¬p ∈ Γ. Thus, p ∈ Δ and ¬p ∈ Δ. □

Proposition 26

Let Δ, Γ, Γ′ be IRR complete consistent theories. If Δ ≺ Γ and Γ ∼ Γ′ then there is an IRR complete consistent theory Δ′ such that Δ ∼ Δ′ and Δ′ ≺ Γ′.

Proof

For some atom p, H p ∧ ¬p ∈ Δ. Thus, M P(H p ∧ ¬p) ∈ Γ′. Hence, by axiom 1s (M P p → P M p), P M(H p ∧ ¬p) ∈ Γ′. So there is Δ′ < Γ′ with M(H p ∧ ¬p) ∈ Δ′. We claim that Δ ∼ Δ′. Assume L φ ∈ Δ. Axiom 1t (H p ∧ ¬p ∧ L q → G L H(M(H p ∧ ¬p) → q)) entails φ ∈ Δ′. □

Remark 27

We also proved that for every Δ′ ≺ Γ′ with M(H p ∧ ¬p) ∈ Δ′, Δ ∼ Δ′.

Proposition 28

≺ is a transitive, upward endless and downward linear relation over the set of IRR complete consistent theories.

Proof

Transitivity easily follows from axiom 1h (G p → G G p). Upward endlessness easily follows from Proposition 11.10 (⊢ G p → f p) (which is obtained combining axioms 1j (G p → F p) and 1k (G p → g p) and yields ⊢ f⊤).

Let us show downward linearity. Suppose we have Δ, Γ₁ and Γ₂ with Γ₁, Γ₂ ≺ Δ, Γ₁ ≠ Γ₂, Γ₁ ⊀ Γ₂ and Γ₂ ⊀ Γ₁. Hence, there are χ ₁, χ ₂ and χ ₃ such that χ ₁ ∈ Γ₁, χ ₁ ∉ Γ₂, χ ₂ ∈ Γ₁, f χ ₂ ∉ Γ₂, χ ₃ ∈ Γ₁ and P χ ₃ ∉ Γ₂. Thus, P(χ ₁ ∧ χ ₂ ∧ χ ₃) ∈ Δ and f P(χ ₁ ∧ χ ₂ ∧ χ ₃) ∈ Γ₂. Applying axiom 1l (H p ∧ p ∧ G p → G H p) and Proposition 118 (⊢ f(p ∧ q) → f p ∧ f q) and 119 (⊢ P(p ∧ q) → P p ∧ P q), we obtain a contradiction. □

Proposition 29

∼ is an equivalence relation over the set of IRR complete consistent theories.

Proof

Easy using axiom 1q (L p → p) for reflexivity, 1r (p → L M p) for symmetry, 1p (L p → L L p) for transitivity. □

Proposition 30

Let φ be a formula, and Γ, Δ IRR complete consistent theories. Suppose Γ ≺ Δ, Fφ ∈ Γ and ¬(φ ∨ Fφ) ∈ Δ. Then there exists an IRR complete consistent theory Θ such that Γ ≺ Θ ≺ Δ and φ ∈ Θ.

Proof

By definition of IRR theory, for some atom p, H p ∧ L¬p ∈ Γ. Thus, P(H p ∧ L¬p ∧ F φ) ∈ Δ. Proposition 12 (⊢ P(p ∧ F q) → P(P p ∧ q) ∨ q ∨ F q)) entails P(P(H p ∧ L¬p) ∧ φ) ∈ Δ. Hence, for some q such as in Definition 16.2,

Let ψ _p be H p ∧ ¬p, ψ _q be H q ∧ ¬q.

Define Θ₀ = {ψ _q ∧ φ} ∪ {P γ|γ ∈ Γ} ∪ {δ|H δ ∈ Δ}. We claim that Θ₀ is consistent. Otherwise, for γ ∈ Γ, δ such that H δ ∈ Δ,

Thus,

However,

For, suppose not, P(ψ _p ∧ ¬γ) ∈ Δ. Thus, there is Γ′ such that Γ′ ≺ Δ and ψ _p ∧ ¬γ ∈ Γ′. Then, by downward linearity, Γ ≺ Γ′ or Γ = Γ′ or Γ ≻ Γ′ and this is against ψ _p ∧ γ ∈ Γ. Hence, because of axiom 1g (H → H H p),

Then, by (6) and Proposition 11.15 (⊢ H p ∧ P q → P(p ∧ q)),

Thus,

This is a contradiction and the claim is proved.

For the n + 1 case we proceed as in Proposition19, but, if Θ _n ∪ {¬ψ _n } is not consistent and n is odd, we make sure that there is an atom r such that r does not occur in ψ _n and Θ _n ∪ {ψ _m (r)} is consistent. We claim that

Suppose not, then

Thus,

However, since, being ψ _p ∈ Γ, P ψ _p ∈ Θ₀, this is against the consistency of Γ _n ∪ {ψ _n }. Therefore,

for r such as in Definition 16.2, i.e. not occurring in \(P(\psi _{q}\wedge P\psi _{p}\wedge \varphi \wedge \bigwedge ({\Theta }_{n}-{\Theta }_{0})\wedge \psi _{n}(r))\) and, thus, not occurring in ψ _n (r). Suppose Γ _n ∪ {ψ(r)} is inconsistent, then, for γ ∈ Γ and δ with H δ ∈ Δ,

However,

Observe that, as before, H(ψ _p → γ) ∈ Δ. Then, reasoning as before,

Finally, since H δ ∈ Δ, by Proposition 11.15 (⊢ H p ∧ P q → P(p ∧ q)),

This is a contradiction and r is as desired. Define \({\Theta }=\bigcup _{m\in \mathbf {N}}{\Theta }_{m}\). □

3.3 Kripke Frame

In this section, for each IRR complete consistent theory Δ, a particular Kripke frame is defined. It has, as domain, a set of arbitrary points and, as relations, a relation R and a relation S. It is related to the canonical model associated to the Hilbert System by means of a function C, named, as in [2], chronicle. More precisely, C associates each point to an IRR complete consistent theory, and for every couple of points x, y, if x R y (respectively, x S y) then C(x) ≺ C(y) (respectively, C(x) ∼ C(y)).

The reason why this Kripke frame, instead of the canonical model restricted to the set of the IRR complete consistent theories, is considered is that the structure needed to perform the filtration of Section 3.4 is “slightly” different from the structure of the canonical model restricted to the set of the IRR complete consistent theories. In particular, we want no history to be completely S-related to any other history. This property will be crucial in defining the indistinguishability relations over the frame of the model built in Section 3.4.

This Kripke frame is built following the construction provided in [2]. There, Peircean logic was considered. Here, the Ockhamist operator L is also present. Therefore, here, in addition to the G, F and H cases (Propositions 34, 35 and 36), treated also in [2, cf Lemmas 3.9, 3.10, 3.12], the L case is also treated (Proposition 37).

Definition 31

A Kripke-frame is a 3-tuple (W, R, S) where W is a set and R and S are binary relations on W.

Definition 32

A chronicle on a Kripke-frame \(\mathcal {F}=(W,R,S)\) is a function C assigning to each w ∈ W an IRR complete consistent theory in such a way that w R v implies C(w) ≺ C(v) and w S v implies C(w) ∼ C(v).

Definition 33

Consider the following conditions over a chronicle C on a linear order \(\mathcal {I}=(I,R)\) (a linear order (I, R) can be viewed as a Kripke frame \((I,R,\varnothing )\)):

1. 1.

   For each formula ψ, each i, j ∈ I such that i R j, P ψ ∈ C(j) and ψ, P ψ ∉ C(i), there is k ∈ I such that i R k, k R j and ψ ∈ C(k).

2. 2.

   For each formula ψ, each i, j ∈ I such that i R j, F ψ ∈ C(i) and ψ, F ψ ∉ C(j), there is k ∈ I such that i R k, k R j and ψ ∈ C(k).

3. 3.

   For each formula ψ, each i ∈ I such that P ψ ∈ C(i), there is j ∈ I such that j R i and ψ ∈ C(j).

4. 4.

   For each formula ψ, each i ∈ I such that F ψ ∈ C(i), there is j ∈ I such that i R j and ψ ∈ C(j).

If C satisfies 1, 2, 3, it is called historic. If C satisfies 1, 2, 4, it is called prophetic. If C satisfies 1, 2, 3, 4, it is called perfect.

All of the following propositions, from Proposition 34 to Proposition 36, follow a similar pattern. A linear order \(\mathcal {I}\) and a chronicle C on \(\mathcal {I}\) satisfying some of the requirements of Definition 33 must be defined. Note that these requirements are existential. \(\mathcal {I}\) and C are defined inductively. At step 0, a linear order \(\mathcal {I}_{0}\) and a chronicle C ₀ on \(\mathcal {I}_{0}\) is defined. At step n + 1, the satisfaction by \(\mathcal {I}_{n}\) and C _n of a particular instance of the desired requirements is checked. If such an instance is not satisfied, the missing elements are added and the chronicle on these new elements defined. The resulting linear order and chronicle define \(\mathcal {I}_{n+1}\) and C _{n + 1}. \(\mathcal {I}\) is then defined as the union of the \(\mathcal {I}_{n}\) and C as the union of the C _n .

Proposition 34

For every IRR complete consistent theory Δ, there is a linear order \(\mathcal {I}=(I,R)\) and a historic chronicle C on \(\mathcal {I}\) such that \(\mathcal {I}\) has a last element i, with C(i) = Δ.

Proof

Step 0. Consider a new object i and define \(\mathcal {I}_{0}=(I_{0},R_{0})\), where I ₀ = {i}, \(R_{0}=\varnothing \), and C ₀ = {(i, Δ)}.

Let φ ₁, φ ₂,... be an enumeration of all the formulas of the form P ψ or F ψ such that every φ occurs infinitely many times.

Step n+1. Suppose φ _{n + 1} is P ψ. List the elements of I _n in R _n order: i _m , i _{m − 1}, ... , i ₁( = i). Consider i ₁. If P ψ ∉ C _n (i ₁) or P ψ ∨ ψ ∈ C _n (i ₂), go to i ₂. Otherwise, by Proposition 24, there is an IRR complete consistent theory Γ, with C _n (i ₂) ≺ Γ ≺ C _n (i ₁) and ψ ∈ Γ. Add an element \(i^{\prime }_{1}\) between i ₁ and i ₂ to I _n , and \((i^{\prime }_{1},{\Gamma })\) to C _n . Go to i ₂. Proceed in this way till i _m is reached. If P ψ ∉ C _n (i _m ), stop. Otherwise, by Proposition 24, there is an IRR complete consistent theory Γ, with Γ ≺ C _n (i _m ) and ψ ∈ Γ. Add an element \(i^{\prime }_{m}\) before i _m to I _n , and \((i^{\prime }_{m},{\Gamma })\) to C _n . Call the resulting structure \(\mathcal {I}_{n+1}=(I_{n+1},R_{n+1})\), and the resulting chronicle C _{n + 1}.

Suppose φ _{n + 1} is F ψ. List the elements of I _n in R _n order: i _m , i _{m − 1}, ... , i ₁( = i). Consider i _m . If F ψ ∉ C _n (i _m ) or F ψ ∨ ψ ∈ C _n (i _{m − 1}), go to i _{m − 1}. Otherwise, by Proposition 30, there is an IRR complete consistent theory Θ, with C _n (i _m ) ≺ Θ ≺ C _n (i _{m − 1}) and ψ ∈ Θ. Add an element \(i^{\prime }_{1}\) between i _m and i _{m − 1} to I _n and \((i^{\prime }_{m},{\Theta })\) to C _n . Go to i _{m − 1}. Proceed in this way till i ₁ is reached and stop, without adding any new object after i ₁. Call the resulting structure \(\mathcal {I}_{n+1}=(I_{n+1},R_{n+1})\), and the resulting chronicle C _{n + 1}.

Define \(\mathcal {I}=(I,R)\) as the union of all the \(\mathcal {I}_{n}\), and C as the union of all the C _n . □

Proposition 35

For every formula ψ, for every IRR complete consistent theory Δ, with fψ ∈ Δ, there exists a linear order \(\mathcal {I}=(I,R)\) and a prophetic chronicle C on \(\mathcal {I}\) such that \(\mathcal {I}\) has a first element i, with C(i) = Δ, and there is j, with iRj and ψ ∈ C(j).

Proof

Step 0. Proposition 24 assures that there exists Γ with Δ ≺ Γ and ψ ∈ Γ. Consider new objects i, j and define \(\mathcal {I}_{0}=(I_{0},R_{0})\), where I ₀ = {i, j}, R ₀ = {(i, j)}, and C ₀ = {(i, Δ), (j,Γ)}.

Let φ ₁, φ ₂,... be an enumeration of all the formulas of the form P ψ or F ψ such that every φ occurs infinitely many times.

Step n+1. Suppose φ _{n + 1} is F ψ. List the elements of I _n in R _n order: (i = )i ₁, i ₂, ... , i _M . Consider i ₁. If F ψ ∉ C _n (i ₁) or F ψ ∨ ψ ∈ C _n (i ₂), go to i ₂. Otherwise, there is an IRR complete consistent theory Θ, with C _n (i ₁) ≺ Θ ≺ C _n (i ₂) and ψ ∈ Θ. Add an element \(i^{\prime }_{1}\) between i ₁ and i ₂ to I _n , and \((i^{\prime }_{1},{\Theta })\) to C _n . Go to i ₂. Proceed in this way till i _M is reached. If F ψ ∉ C _n (i _M ), stop. Otherwise, by axiom 1k (G p → g p) and Proposition 24, there is an IRR complete consistent theory Γ, with C _n (i _M ) ≺ Γ and ψ ∈ Γ. Add an element \(i^{\prime }_{m}\) after i _M to I _n , and \((i^{\prime }_{m},{\Gamma })\) to C _n . Call the resulting structure \(\mathcal {I}_{n+1}=(I_{n+1},R_{n+1})\), and the resulting chronicle C _{n + 1}.

Suppose φ _{n + 1} is P ψ. List the elements of I _n in R _n order: (i = )i ₁, i ₂, ... , i _M . Consider i _M . If P ψ ∉ C _n (i _M ) or P ψ ∨ ψ ∈ C _n (i _{M − 1}), go to i _{M − 1}. Otherwise, there is an IRR complete consistent theory Γ with C _n (i _{M − 1}) ≺ Γ ≺ C _n (i _M ) and ψ ∈ Γ. Add an element \(i^{\prime }_{m}\) between i _M and i _{M − 1} to I _n , and \((i^{\prime }_{m},{\Gamma })\) to C _n . Go to i _{M − 1}. Proceed in this way till i ₁ is reached and stop, without adding any new object after i ₁. Call the resulting structure \(\mathcal {I}_{n+1}=(I_{n+1},R_{n+1})\), and the resulting chronicle C _{n + 1}.

Define \(\mathcal {I}=(I,R)\) as the union of all the \(\mathcal {I}_{n}\), and C as the union of all the C _n . □

Proposition 36

For every formula ψ, every IRR complete consistent theory Δ, with gψ ∈ Δ, there exists a linear order \(\mathcal {I}=(I,R)\) and a prophetic chronicle C on \(\mathcal {I}\) such that \(\mathcal {I}\) has a first element i, with C(i) = Δ, and for all j, with iRj, ψ ∈ C(j).

Proof

Consider the case in which ψ is H χ, for some formula χ. Proceed as in Proposition 35, with only the following modifications:

1. 1.

   At step 0, use axioms 1i (F F p → F p) and 1j (G p → F p) to find an IRR complete consistent theory Γ, with Δ ≺ Γ and g H χ ∈ Δ.

2. 2.

   At each step n > 0, if z _{M, n} is the last element of \(\mathcal {I}_{n}\), assure that g H χ ∈ C _n (z _{M, n} ), proceeding as follows:

   1. (a)

      According to the proof of Proposition 35, the last element of \(\mathcal {I}_{n+1}\) is different from the last element of \(\mathcal {I}_{n}\) only when φ _n is F 𝜗, for some formula 𝜗, and F 𝜗 ∈ C _n (z _{M, n} ). Now, if F 𝜗 ∧ g H χ ∈ C _n (z _{M, n} ), by axiom 1i (F F p → F p) and Proposition 11.14 (⊢ F p ∧ g q → f(p ∧ q)), f(𝜗 ∧ g H χ) ∈ C _n (z _{M, n} ). Therefore, we can assure that g H χ ∈ C _{n + 1}(z _{M, n + 1}) as well.

At the end, by axiom 1j (G p → F p), for every i ∈ I, there is j ∈ I, with i R j and g H χ ∈ C(j). Hence, f g H χ ∈ C(i). Applying Proposition 11.11 (⊢ f g p → f p) and and axiom 1f (p → G P p), χ ∈ C(i).

Suppose ψ is an arbitrary formula. For some atom p, H p ∧ ¬p ∈ Δ. Thus, using Proposition 11.21 (⊢ H p ∧ g q → g H(P¬p → q)), g H(P¬p → ψ) ∈ Δ. Therefore, there exists a linear order \(\mathcal {I}=(I,R)\) and a prophetic chronicle C on \(\mathcal {I}\) such that \(\mathcal {I}\) has a first element i, with C(i) = Δ, and, for every element j ∈ I P¬p → ψ ∈ C(j). Therefore, for every j ∈ I, with i R j, ψ ∈ C(j). □

Proposition 37

For every formula ψ, every linear order \(\mathcal {I}=(I,R)\) with a first element i, every historic chronicle C on \(\mathcal {I}\) , with Mψ ∈ C(i), there exists a linear order \(\mathcal {I}^{\prime }=(I^{\prime },R^{\prime })\) , with a first element i′, and a historic chronicle C′ on \(\mathcal {I}^{\prime }\) such that ψ ∈ C′(i′) and, for all j ∈ I there is j′ ∈ I′, with C(j) ∼ C′(j′), and for all j′ ∈ I′ there is j ∈ I, with C′(j′) ∼ C(j).

Proof

Proposition 24 assures that there is Γ with C(i) ∼ Γ and ψ ∈ Γ. Consider a new object i′ and define I′={i′} and C′(i′) = Γ. For all j ∈ I, with j R i, by Proposition 26, there is Γ _j such that C(j) ∼ Γ _j and Γ _j ≺ Γ. Thus, for all j ∈ I, with j R i, add a new object j′ to I′ and define C′(j′) = Γ _j . Finally, for every j′, k′ ∈ I′, define j′R′k′ if and only if C′(j′) ≺ C′(k′).

Consider any formula ψ and any j′ ∈ I′, with P ψ ∈ C′(j′). Then, by Proposition 24, there is Γ′, with Γ′ ≺ C(j′) and ψ ∈ Γ′. Thus, by Proposition 26, there is Γ, with Γ ≺ C(j) and Γ ∼ Γ′. For some p, H p ∧ L¬p ∈ Γ. Hence, P(H p ∧ L¬p) ∈ C(j). Then, there is k ∈ I, with k R j and H p ∧ L¬p ∈ C(k). Therefore, by downward linearity of ≺, Γ = C(k). Thus, there is k′ ∈ I′, with Γ ∼ C(k′). Therefore, by downward linearity of ≺ and \(\prec \cap \sim =\varnothing \), Γ′ = C′(k′).

Similarly, given any ψ and any j′, l′ ∈ I′ with l′R′j′, P ψ ∈ C′(j′) and ¬ψ ∧ ¬P ψ ∈ C′(l′), there is k′ ∈ I′, with l′R′k′, k′R′j′ and ψ ∈ C′(k′); given any formula ψ and any j′, l′ ∈ I′, with j′R′l′, F ψ ∈ C′(j′) and ¬ψ ∧ ¬F ψ ∈ C′(l′), there is k′ ∈ I′, with j′R′k′, k′R′l′ and ψ ∈ C′(k′). □

The following proposition shows how to build, for each IRR complete consistent theory Δ, the desired Kripke frame. Again, some existential requirements must be satisfied, an inductive construction will be performed, and, at each step, the missing part of the frame and the associated part of the chronicle will be added by means of Propositions from 34 to 37.

Proposition 38

For every IRR complete consistent theory Δ, there is a Kripke-frame \(\mathcal {F}=(W,R,S)\) and a chronicle C on \(\mathcal {F}\) such that there is w ∈ W with C(w) = Δ, and for each w ∈ W, each formula ψ:

1. 1.

   R is transitive, downward linear and upward endless.

2. 2.

   S is an equivalence relation.

3. 3.

   \(R\cap S=\varnothing \).

4. 4.

   For each v, v′ ∈ W, if wRv and vSv′, there is w′ such that wSw′ and w′Rv′.

5. 5.

   There is h ∈ H _w such that C↾h (where C↾h means C restricted to h) is a perfect chronicle.

6. 6.

   If fψ ∈ C(w), there is h ∈ H _w such that C↾h is a perfect chronicle, and there is v ∈ h, with wRv and ψ ∈ C(v).

7. 7.

   If gψ ∈ C(w), there is h ∈ H _w such that C↾h is a perfect chronicle, and for all v ∈ h, with wRv, ψ ∈ C(v).

8. 8.

   If Mψ ∈ C(w), there is v ∈ W, with wSv and ψ ∈ C(v).

Proof

Let Δ be an arbitrary IRR complete consistent theory.

Step 0. By Proposition 34, there exists a Kripke-frame \(\mathcal {F}=(I,R,S)\) and a historic chronicle C on \(\mathcal {F}\) such that S = {(i, i)|i ∈ I}, (I, R) is a linear order with a last element i, and C(i) = Δ. Define \(\mathcal {F}_{0}=\mathcal {F}\) and C ₀ = C.

Step n+1. Consider every pair (w, φ), where w ∈ W _n −W _{n − 1} and φ is a formula in C _n (w) of the form f ψ, g ψ or M ψ.

Suppose φ is f ψ. By Proposition 35, there exists a Kripke-frame \(\mathcal {F}_{(w,\varphi )}=(I,R,S)\) and a prophetic chronicle C _{(w, φ)} on \(\mathcal {F}_{(w,\varphi )}\) such that S = {(i, i)|i ∈ I}, (I, R) is a linear order with a first element i, C _{(w, φ)}(i) = C _n (w), and there is j ∈ I with i R j and ψ ∈ C _{(w, φ)}(j). We can assume i = w and I − {i} disjoint from W _n .

Suppose φ is g ψ. By Proposition 36, there exists a Kripke-frame \(\mathcal {F}_{(w,\varphi )}=(I,R,S)\) and a prophetic chronicle C _{(w, φ)} on \(\mathcal {F}_{(w,\varphi )}\) such that S = {(i, i)|i ∈ I}, (I, R) is a linear order with a first element i, C _{(w, φ)}(i) = C _n (w), and for all j with i R j, ψ ∈ C _{(w, φ)}(j). We can assume i = w and I − {i} disjoint from W _n .

Suppose φ is M ψ. Assume that, if I _w denote {v ∈ W _n |v R _n ∪ = w}, C _n ↾I _w is historic on I _w (*). Thus, by Proposition 37, there exists a Kripke-frame \(\mathcal {F}_{(w,\varphi )}=(I,R,S)\) and a historic chronicle C _{(w, φ)} on \(\mathcal {F}_{(w,\varphi )}\) such that S = {(i, i)|i ∈ I}, (I, R) is a linear order such that it has a first element i with ψ ∈ C _{(w, φ)}(i) and for all v ∈ I _w , there is j ∈ I, with C _n (v) ∼ C _{(w, φ)}(j), and for all j ∈ I, there is v ∈ I _w , with C _n (v) ∼ C _{(w, φ)}(j). We can assume I disjoint from W _n .

All the \(\mathcal {F}_{(w,\varphi )}-\{w\}\) can be assumed disjoint. Let \(\mathcal {F}_{n+1}\) be the union of \(\mathcal {F}_{n}\) and all the \(\mathcal {F}_{(w,\varphi )}\), and C _{n + 1} the union of C _n and all the C _{(w, φ)}. For every \(\mathcal {F}_{(w,\varphi )}=(I,R,S)\), with φ of the form M ψ, for every i ∈ I, for every i′ ∈ I _w with C _{(w, φ)}(i′) ∼ C _n (i), add (i′, i) and (i, i′) to S _n , obtaining \(S^{0}_{n+1}\). Close \(S^{0}_{n+1}\) under transitivity, obtaining S _{n + 1}. Let \(\mathcal {F}\) be the union of all the \(\mathcal {F}_{n}\) and C the union of all the C _n .

It is easy to prove that assumption (∗) holds at step 0 and that, if assumption (∗) holds at step n, then it holds at the step n + 1. Properties 1-8 easily follow. □

3.4 Model (Over a Bundled I-Tree)

In the previous section, for each IRR complete consistent theory Δ, a Kripke frame associated to Δ has been defined. In this section, given an arbitrary IRR complete consistent theory Δ, following [7, Section 7.7, pp. 299–306], the associated Kripke frame \(\mathcal {F}=(W,R,S)\) is turned into a model (over a bundled I tree) for Δ. This is done by quotienting over S (S is an equivalence relation). The idea underlying this filtration is the following. The points of the Kripke-frame \(\mathcal {F}\) are meant to represent equivalence classes modulo indistinguishability and the equivalence relation S represents the property that two classes are relative to the same moment in time.

Indistinguishability relations and an evaluation are then defined over the resulting frame and the resulting model is proved to satisfy Δ.

Let Δ be an arbitrary IRR complete consistent theory and \(\mathcal {F}=(W,R,S)\) and C, respectively, the Kripke frame and the chronicle associated to Δ provided by Proposition 38.

Definition 39

For all w ∈ W, define w = {v ∈ W|w S v}, and W = {w|w ∈ W}. For all w, v ∈ W, define w R v if and only if there are w′ ∈ w and v′ ∈ v such that w′R v′.

Remark 40

By Proposition 38.4, given w, v ∈ W, with w R v, there is w′ ∈ w such that w′R v.

Proposition 41

R is an irreflexive, transitive, downward linear and upward endless binary relation over W.

Proof

Given any w ∈ W, suppose w R w. Then, by Remark 40, there is w′ ∈ w with w′R w. This contradicts \(R\cap S=\varnothing \). Therefore, R is irreflexive. Transitivity and downward linearity easily follow from Remark 40 and the same properties for R. Upward endlessness for R easily follows from upward endlessness for R. □

Definition 42

For each \(h\in H_{\mathcal {F}}\), define h = {w|w ∈ h}.

Definition 43

Given w ∈ W, define the date of birth of w, DOB(w), as the natural number n such that w has been introduced at step n. Given w, w′ ∈ W such that w S w′, define the date of birth of the relation S between w and w′, DOB(S, w, w′) as the natural number n such that w and w′ have been S-related at step n.

Definition 44

Define the reflexive closure of R as \(\underline {R}=\{(w,v)\in W\times W | wRv \text { or }w=v\}\).

Proposition 45

For every distinct w, w′ ∈ W, if wSw′ and DOB(S,w,w′) = n, then:

1. 1.

   Either for each v ∈ W such that \(v \underline {R} w\) , DOB(v) = n;

2. 2.

   Or for each v′ ∈ W such that \(v^{\prime } \underline {R} w^{\prime }\) , DOB(v′) = n.

Proof

According to the construction, there are three ways in which w and w′ may have been S-related:

1. 1.

   There is v such that: \(w\underline {R}v\), DOB(v) = n − 1, M ψ ∈ C(v) for some formula ψ. Therefore, a new element v′, together with a new element w′, has been introduced at step n to answer (v, M ψ). In this case, thesis is easily fulfilled.

2. 2.

   There is v′ such that: \(w^{\prime }\underline {R}v^{\prime }\), DOB(v′) = n − 1, M ψ ∈ C(v′) for some formula ψ. Therefore, a new element v, together with a new element w, has been introduced at step n to answer (v′, M ψ). In this case, thesis is easily fulfilled.

3. 3.

   w and w′ has been S-related by performing the transitive closure of \({S^{0}_{n}}\). By definition of transitive closure, there is \(m\in \mathbb {N}\) and x ₁, x ₂, ... , x _m ∈ W _n such that \(w=x_{0}{S^{0}_{n}} x_{1}{S^{0}_{n}}...{S^{0}_{n}} x_{m+1}=w^{\prime }\) and such that, for each i, j = 0, 1, ... , m + 1 with i ≠ j, x _i ≠ x _j . Observe that \({S^{0}_{n}}\setminus S_{n-1}\) always relates an element whose DOB is n − 1 with an element whose DOB is n. Thus, there must be i = 0, 1, ... , m + 1 such that DOB(x _i ) = n. Observe that, by construction, such an x _i has been \({S^{0}_{n}}\)-related to one and only one element v and such a v ∈ W _{n − 1}. Therefore, either w or w′ must be x _i . Assume, without loss of generality, w is x _i . Then DOB(w) = n. Observe that w has been S-related to an object different than w, namely w′, at the same step w has been introduced. Therefore, by construction, there must be v ∈ W _n such that \(w \underline {R}v\) and such that v has been introduced at step n to answer (v′, M ψ) for some v′ ∈ W _{n − 1} and formula ψ. Thesis easily follows.

□

Corollary 46

Consider distinct w,w′ ∈ W such that wSw′ and DOB(S,w,w′) = n. Then, for each v ∈ W such that wRv and such that there is v′ ∈ W with w′Rv′ and vSv′, we have DOB(v) ≤ n.

Proof

Consider such a v. Assume DOB(v) > n. Then, DOB(S, v, v′) > n. Thus, by Proposition 45, either DOB(w) > n or DOB(w′) > n. However, this contradicts DOB(S, w, w′) = n. □

Proposition 47

For each \(n\in \mathbb {N}\) , for each upward endless \(h_{1}\in H_{\mathcal {F}_{n}}\) , there is no \(h_{2}\in H_{\mathcal {F}}\setminus {h_{1}}\) such that, for each w ₁ ∈ h ₁ , there is w ₂ ∈ h ₂ with w ₁ S _n w ₂.

Proof

By induction on \(n\in \mathbb {N}\). If n = 0, easy since there is no upward endless \(h_{1}\in H_{\mathcal {F}_{0}}\). Consider n > 0 and assume thesis for every k < n. Suppose thesis fails for n. Consider an upward endless \(h_{1}\in H_{\mathcal {F}_{n}}\) such that there is \(h_{2}\in H_{\mathcal {F}}\setminus {h_{1}}\) such that, for each w ₁ ∈ h ₁, there is w ₂ ∈ h ₂ with w ₁ S _n w ₂. If \(h_{1}\in H_{\mathcal {F}_{n-1}}\), contradiction by i.h. If \(h_{1}\in H_{\mathcal {F}_{n}}\setminus H_{\mathcal {F}_{n-1}}\), since h ₁ is upward endless, there is w ₁ ∈ h ₁ such that \(\{v_{1}\in h_{1} | w_{1}\underline {R}v_{1}\}\) has been introduced at step n answering (w ₁, φ) for some formula φ of the form either f ψ or g ψ. Thus, since, for each \(v\in \{v_{1}\in h_{1} | w_{1}\underline {R}v_{1}\}\), S _n (v) = {v}, a contradiction follows. □

Corollary 48

For every \(h_{1},\in H_{\mathcal {F}}\) , there is no \(h_{2}\in H_{\mathcal {F}}\setminus \{h_{1}\}\) such that for every w ₁ ∈ h ₁ there is w ₂ ∈ h ₂ , with w ₁ Sw ₂ . Therefore, h ↦ h, for \(h\in H_{\mathcal {F}}\) , is injective.

Proof

Suppose not. Consider \(h_{1}\in H_{\mathcal {F}}\) and \(h_{2}\in H_{\mathcal {F}}\setminus \{h_{1}\}\) such that for every w ₁ ∈ h ₁ there is w ₂ ∈ h ₂, with w ₁ S w ₂. Consider w ₁ ∈ h ₁ and w ₂ ∈ h ₂ such that w ₁ S w ₂. Let DOB(S, w ₁, w ₂) = n. Consider any v ₁ ∈ h ₁ with w ₁ R v ₁. By assumptions, there is v ₂ ∈ h ₂ such that w ₂ R v ₂ and v ₁ S v ₂. Thus, by Corollary 46, DOB(v ₁), DOB(v ₂) and DOB(S, v ₁, v ₂) ≤ n. Thus, \(h_{1}\in H_{\mathcal {F}_{n}}\) and for all w ₁ ∈ h ₁ there is w ₂ ∈ h ₂ such that w ₁ S _n w ₂. This contradicts Proposition 47. □

Definition 49

Define B as the set of all h such that C↾h is perfect.

Proposition 50

B is a bundle over (W, R).

Proof

It follows from Proposition 38.5. □

Definition 51

Given w ∈ W, h ₁, h ₂ ∈ B _w , define h ₁ I _w h ₂ if and only if h ₁ ∩ w = h ₂ ∩ w. Define I(w) = I _w .

Proposition 52

I is an indistinguishability function over (W, R, B).

Proof

Easily I is a function and for each w ∈ W, I _w is an equivalence relation on B _w . Given any v, w ∈ W, with v R w, and any h ₁, h ₂ ∈ B _w , with h ₁ I _w h ₂, consider any w′ ∈ h ₁ ∩ w, and any v′ ∈ h ₁ ∩ v. By linearity of h ₁, v′ and w′ must be comparable. If w′ ≤ v′, possibly applying Proposition 38.4, we would contradict \(R\cap S=\varnothing \). Hence v′ ∈ h ₂. In the same way, h ₂ ∩ v ⊆ h ₁ ∩ v. Therefore h ₁ I _v h ₂. □

Definition 53

For each w ∈ W, define π _w = {h ∈ B|h ∩ w = {w}}.

Remark 54

Since \(R\cap S=\varnothing \), for every w ∈ W, for every h ∈ B _w , there is (one and only one) w′ ∈ w such that h ∩ w = {w′}.

Proposition 55

For every w ∈ W, for every π ∈ π _w , there is a unique w′ ∈ w such that \(\pi =\pi _{w^{\prime }}\).

Proof

Consider any h ∈ π. Let h ∩ w = {w′}. Then, \(\pi =\pi _{w^{\prime }}\). Uniqueness easily follows. □

Definition 56

Given p ∈ P V, define

Proposition 57

\(\mathcal {N}=(\mathbf {W},\mathbf {R},B,I,V^{\prime })\) is a model.

Proof

It follows from the previous results. □

Proposition 58

For each w ∈ W, π _w is an equivalence class of I _w .

Proof

From Proposition 38.5, it follows that there is h ∈ H _w such that h ∈ B _w . By Remark 54, h ∈ π _w . Let π = {h′ ∈ B|h I _w h′}. Plainly, π _w = π. □

Proposition 59

For every formula φ, for every w ∈ W, φ ∈ C(w) if and only if \(\mathcal {N},(\mathbf {w},\pi _{w})\models \varphi \).

Proof

By induction on the complexity of φ. Easy, if φ is p, ¬ψ or ψ ∧ χ for some atom p and formulas ψ and χ.

Suppose φ is H ψ and H ψ ∈ C(w). Take any h ∈ π _w , any v ∈ h such that v < w. Then, there is v′ ∈ v such that v′ ∈ h and v′R w. Thus, ψ ∈ C(v′). Hence, by inductive hypothesis, \(\mathcal {N},(\mathbf {v},\pi _{v^{\prime }})\models \psi \). Therefore, since \(\pi _{v^{\prime }}=[\mathbf {h}]_{I_{\mathbf {v}}}\), \(\mathcal {N},(\mathbf {v},[\mathbf {h}]_{I_{\mathbf {v}}})\models \psi \). In conclusion, \(\mathcal {N},(\mathbf {w},\pi _{w})\models H\psi \). Suppose H ψ ∉ C(w). Then, by Proposition 38.5, there is h ∈ H _w such that C↾h is perfect. Hence, there is v ∈ h such that v R w and ψ ∉ C v. Thus, by inductive hypothesis, \(\mathcal {N},(\mathbf {v},\pi _{v})\not \models \psi \). Therefore, since \(\pi _{v}=[\mathbf {h}]_{I_{\mathbf {v}}}\), \(\mathcal {N},(\mathbf {v},[\mathbf {h}]_{I_{\mathbf {v}}})\not \models \psi \). In conclusion, \(\mathcal {N},(\mathbf {w},\pi _{w})\not \models H\psi \).

Suppose φ is G ψ and G ψ ∈ C(w). Take any h ∈ π _w , any v ∈ h such that w R v. Then, there is v′ ∈ v such that v′ ∈ h and w R v′. Thus, ψ ∈ C(v′). Hence, by inductive hypothesis, \(\mathcal {N},(\mathbf {v},\pi _{v^{\prime }})\models \psi \). Therefore, since \(\pi _{v^{\prime }}=[\mathbf {h}]_{I_{\mathbf {v}}}\), \(\mathcal {N},(\mathbf {v},[\mathbf {h}]_{I_{\mathbf {v}}})\models \psi \). In conclusion, \(\mathcal {N},(\mathbf {w},\pi _{w})\models G\psi \). Suppose G ψ ∉ C(w). Then, 38.6, there is h ∈ H _w such that C↾h is perfect and there is v ∈ h such that w R v and ψ ∉ C(v). Thus, by inductive hypothesis, \(\mathcal {N},(\mathbf {v},\pi _{v})\not \models \psi \). Therefore, since \(\pi _{v}=[\mathbf {h}]_{I_{\mathbf {v}}}\), \(\mathcal {N},(\mathbf {v},[\mathbf {h}]_{I_{\mathbf {v}}})\not \models \psi \). In conclusion, \(\mathcal {N},(\mathbf {w},\pi _{w})\not \models G\psi \).

Suppose φ is F ψ and F ψ ∈ C(w). Consider any h ∈ π _w . By, definition, C↾h is perfect. Hence, there is v ∈ h such that ψ ∈ C(v). Thus, by inductive hypothesis, \(\mathcal {N},(\mathbf {v},\pi _{v})\models \psi \). Therefore, since \(\pi _{v}=[\mathbf {h}]_{I_{\mathbf {v}}}\), \(\mathcal {N},(\mathbf {v},[\mathbf {h}]_{I_{\mathbf {v}}})\models \psi \). In conclusion, \(\mathcal {N},(\mathbf {w},\pi _{w})\models F\psi \). Suppose F ψ ∉ C(w). Then, by Proposition 38.7, there is h ∈ H _w such that C↾h is perfect and for all v ∈ h with w R v, ψ ∉ C v. Hence, by inductive hypothesis, \(\mathcal {N},(\mathbf {v},\pi _{v})\not \models \psi \). Therefore, since \(\pi _{v}=[\mathbf {h}]_{I_{v}}\), \(\mathcal {N},(\mathbf {v},[\mathbf {h}]_{I_{\mathbf {v}}})\not \models \psi \). In conclusion, \(\mathcal {N},(\mathbf {w},\pi _{w})\not \models F\psi \).

Suppose φ is L ψ and L ψ ∈ C(w). Take any π ∈ π _w . \(\pi =\pi _{w^{\prime }}\), for some w′ ∈ w. Then, ψ ∈ C(w′). Thus, by inductive hypothesis, \(\mathcal {N},(\mathbf {w},\pi _{w^{\prime }})\models \psi \). Therefore, \(\mathcal {N},(\mathbf {w},\pi )\models \psi \). In conclusion, \(\mathcal {N},(\mathbf {w},\pi _{w})\models L\psi \). Suppose L ψ ∉ C(w). Then, by Proposition 38.8, there is w′ ∈ w such that ψ ∉ C(w′). Thus, by inductive hypothesis, \(\mathcal {N},(\mathbf {w},\pi _{w^{\prime }})\not \models \psi \). Therefore, \(\mathcal {N},(\mathbf {w},\pi _{w})\not \models L\psi \). □

3.5 Soundness and Strong Completeness Theorem

At this point, for every IRR complete consistent theory we are able to exhibit a model that satisfies it. Nonetheless, to prove the Soundness and Strong Completeness Theorem, we want to be able to do it for every consistent theory. The problem is that not every consistent theory can be extended to an IRR complete consistent theory. Therefore we cannot apply the construction introduced above.

A consistent theory Δ can be extended to a maximal consistent IRR theory only if the number of atoms not occurring among the formulas in Δ is infinite. If we index the set PV of atoms and we double (p _i ↦ p _2i ) the atoms p _i ∈ Δ, the resulting theory #Δ is such that the number of atoms not occurring among the formulas in #Δ is infinite. It can be proved that, if Δ is consistent, then #Δ is consistent as well. Therefore, #Δ can be extended to a maximal consistent IRR theory Δ^∗. We are then able to build a model for Δ^∗. This model, by a slight modification of the evaluation function, can be turned into a model for Δ. The Sound and Strong Completeness Theorem then follows.

Definition 60

Let p ₁, p ₂,... be an enumeration without repetition of PV. Given a formula φ, let # φ denote the formula obtained from φ by replacing every occurrence of every atom p _i with p _2i . Given a theory Δ, let #Δ be the theory obtained from Δ by replacing every φ ∈ Δ with #φ. Given a theory Δ, call Δ⁻¹ the theory obtained from Δ as follows: first discard every φ ∈ Δ wherein some atom indexed with an odd number occurs; then replace every remaining #φ with φ.

Proposition 61

Given a constant theory Δ, if Δ is consistent, #Δ is consistent. Hence, by Proposition 16, there is an IRR complete consistent theory Δ^∗, with #Δ ⊆ Δ^∗.

Proof

Suppose #Δ is inconsistent. Therefore, there are #δ ₁, #δ ₂, ... , #δ _n ∈ # Δ such that \(\vdash \neg \bigwedge _{i=1}^{n}\#\delta _{i}\). Consider any proof of \(\neg \bigwedge _{i=1}^{n}\#\delta _{i}\). Since such a proof is finite, there is a one-one function s:P V → P V such that, for every atom p with odd index occurring in the proof, s(p) has an even index and it does not occur in the proof. Consider the sequence obtained from the considered proof of \(\neg \bigwedge _{i=1}^{n}\#\delta _{i}\) by replacing every atom p with odd index by s(q). Then, this sequence is of the form # φ ₁, # φ ₂, ... , # φ _n . Moreover, # φ ₁, # φ ₂, ... , # φ _n is a proof of \(\neg \bigwedge _{i=1}^{n}\#\delta _{i}\) as well. Hence, φ ₁, φ ₂, ... , φ _n is a proof \(\neg \bigwedge _{i=1}^{n}\delta _{i}\). Thus, since δ ₁, δ ₂, ... , δ _n ∈ Δ, Δ is inconsistent. □

Fix an arbitrary consistent theory Δ from Definition 62 to Proposition 64.

Definition 62

Let \(\mathcal {N}=(\mathbf {W},\mathbf {R},B,I,V^{\prime })\) be the model of Definition 39 for Δ^∗. For each p ∈ P V, define

Define the model \(\mathcal {M}=(\mathbf {W},\mathbf {R},B,I,V)\) and call it model for Δ.

Proposition 63

For every formula φ, w ∈ W, π ∈ π _w , \(\mathcal {M},(\mathbf {w},\pi )\models \varphi \) if and only if \(\mathcal {N},(\mathbf {w},\pi )\models \#\varphi \).

Proof

Easy induction on the complexity of φ. □

Proposition 64

For every formula φ, for every w ∈ W, if φ ∈ C(w) ⁻¹ then \(\mathcal {M},(\mathbf {w},\pi _{w})\models \varphi \).

Proof

# φ ∈ C(w). Therefore, Propositions 63 and 59 implies \(\mathcal {M},(\mathbf {w}, \pi _{w})\models \varphi \). □

Proposition 65

For every consistent theory Δ, there is a model \(\mathcal {T}=(T,<,B,I,V)\) and a pair \((t,\pi )\in \bigcup _{t\in T}(\{t\}\times {\Pi }_{t})\) such that \(\mathcal {T},(t,\pi )\models {\Delta }\).

Proof

Consider the model \(\mathcal {M}=(\mathbf {W},\mathbf {R},B,I,V)\) for Δ. According to the construction, there is w ∈ W such that Δ ⊆ C ⁻¹(w). Therefore, Proposition 64 yields \(\mathcal {M},(\mathbf {w},\pi _{w})\models {\Delta }\). □

Theorem 66 (Soundness and Strong Completeness Theorem)

For every consistent theory Δ, every formula φ, Δ ⊢ φ if and only if Δ ⊧ φ.

Proof

Left-to-right direction is easily provable. We use upward endlessness to prove validity of axiom 1j (G p → F p), the indistinguishability condition to prove validity of axioms 1g (H p → H H p), 1h (G p → G G p), 1l (H p ∧ p ∧ G p → G H p) and 1m (H p ∧ p ∧ g p → g H p), both of them to prove validity of axiom 1n (F G p → G F p), and irreflexivity to prove that the IRR rule preserves validity. For right-to-left direction, suppose Δ⊯φ. Then, Δ ∪ {¬φ} is consistent. Thus, there is a model \(\mathcal {T}=(T,<,B,I,V)\) and a pair \((t,\pi )\in \bigcup _{t\in T}(\{t\}\times {\Pi }_{t})\) such that \(\mathcal {T},(t,\pi )\models {\Delta }\cup \{\neg \varphi \}\). Therefore, Δ ⊮φ. □

Along the paper two questions have been implicitly raised:

1. 1.

   Is there an axiomatization of the considered logic without a form of the IRR rule?

   As Section 3.2 and in particular Remark 15 show, the IRR rule is used to get structural properties of the Kripke Frames of Section 3.3, namely Propositions 25 and 26. These properties seem unavoidable, as they guarantee that what we obtain, by quotienting over S, in Section 3.4 is a tree. An axiomatization without a form of the IRR rule seems then to need additional axioms to get these properties. As the axiomatization of this paper is a mix of the axiomatizations with IRR rule of the Peircean and bundled Ockhamist logics, would it be useful to mix the axiomatizations without IRR rule for Peircean and bundled Ockhamist logics of, respectively, [20] and [19]?

2. 2.

   Is there an axiomatization of the logic of (unbundled) I-trees? First consider the following example showing the crucial role of bundles in our construction. Let V _{B T} denote the set of all validities of the class of all bundled I-trees. Consider the formula γ = L G(L p → M f L p) → M g(L p → f L p). With a bit of work, one can show that γ ∉ V _{B T} . Consider a formula equivalent to ¬γ such as L G(L p → M f L p) ∧ L F(L p ∧ G M¬p). Since we proved that the Hilbert system of Section 2.3 is sound and strongly complete with respect to V _{B T} , we know that such a formula is consistent, whence that there is an IRR complete consistent theory Δ containing L G(L p → M f L p) ∧ L F(L p ∧ G M¬p).

   Then, the construction of Section 3.3 produces the following situation, where straight lines denote R and waved lines S:

   

   with C(w) = Δ. When quotienting over S, we obtain a new history, say \(\mathbb {h}_{\infty }\) (straight lines denoting R):

   

   Without a bundle we would have to consider \(\mathbb {h}_{\infty }\) as well. Surely, for all v and \(\mathbb {h}\in H_{\mathbf {v}}\), if L p ∈ v, then we would define \((\mathbf {v},[\mathbb {h}]_{\mathbf {v}})\in V(p)\). Then, \(\mathcal {N},(\mathbf {w},[\mathbb {h}_{\infty }])\models g(Lp\rightarrow fLp)\).

   

   Then \(\mathcal {N},(\mathbf {w},\pi _{w})\models Mg(Lp\rightarrow fLp)\). However, since L F(L p ∧ G M¬p) ∈ C(w), we would contradict Proposition 59.

   Now, let V _T be the set of all validities of the class of all (unbundled) I-trees. With a bit of work one can show that γ ∈ V _T . Moreover, since an (unbundled) I-tree can be seen as a bundled I-tree where the bundle select all the histories, V _{B T} ⊆ V _T . Therefore, \(V_{BT}\subsetneq V_{T}\). This suggests the need of new axioms and rules to get the ‘missing validities’ (e.g. γ). But what are these new axioms and rules? In [14, 15], formulas similar to γ have been used to highlight similar issues concerning the axiomatization of the Ockhamist logic of unbundled trees. In [15], adding an axiom schema to obtain certain validities on the flavor of γ yields an axiomatization of the Ockhamist logic of unbundled trees. This suggests to try adding a similar axiom schema.