David Baelde Lsv

Anthony Lick
email: lick@lsv.fr

Sylvain Schmitz
email: schmitz@lsv.fr

A Hypersequent Calculus with Clusters for Tense Logic over Ordinals

Keywords: 2012 ACM Subject Classification Theory of computation → Proof theory, Theory of computation modal logic, proof system, hypersequent

Prior's tense logic forms the core of linear temporal logic, with both past-and future-looking modalities. We present a sound and complete proof system for tense logic over ordinals. Technically, this is a hypersequent system, enriched with an ordering, clusters, and annotations. The system is designed with proof search algorithms in mind, and yields an optimal coNP complexity for the validity problem. It entails a small model property for tense logic over ordinals: every satisfiable formula has a model of order type at most ω 2 . It also allows to answer the validity problem for ordinals below or exactly equal to a given one.

Introduction

Linear temporal logic has become a staple specification language in verification since its introduction by Pnueli [START_REF] Pnueli | The temporal logic of programs[END_REF]. In its most common form, the logic features an 'until' temporal modality and ranges over linear time flows of order type ω, i.e. over infinite words, where it enjoys a PSPACE-complete satisfiability problem [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]. A large number of variants with the same complexity has been motivated and introduced in the literature, notably temporal logics with past modalities [START_REF] Lichtenstein | The glory of the past[END_REF][START_REF] Laroussinie | Temporal logic with forgettable past[END_REF], ranging over arbitrary ordinals [START_REF] Gareth | Alternating Automata and the Temporal Logic of Ordinals[END_REF][START_REF] Demri | The complexity of linear-time temporal logic over the class of ordinals[END_REF], or even-with the Stavi modalities added-over arbitrary linear time flows [START_REF] Cristau | Automata and temporal logic over arbitrary linear time[END_REF][START_REF] Rabinovich | Temporal logics over linear time domains are in PSPACE[END_REF].

Linear temporal logic finds its roots in Prior's tense logic [START_REF] Prior | Time and Modality[END_REF][START_REF] Nino | Tense and Modal Logic: a Study in the Topology of Temporal Reference[END_REF], which only featured the strict 'past' P and 'future' F modalities. This set of modalities is still interesting in its own right, as it is sufficient for many modelling tasks [START_REF] Sistla | Reasoning in a restricted temporal logic[END_REF], and is known to lead to a slightly easier NP-complete satisfiability problem both over ω [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF] and over arbitrary linear time flows [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF]. While linear tense logic is less expressive than FO(<), the first-order logic over linear orders with unary predicates, it has nevertheless nice characterisations as it captures instead its two-variable fragment FO 2 (<) [START_REF] Etessami | First-order logic with two variables and unary temporal logic[END_REF].

In this paper, we investigate tense logic over well-founded linear time flows, i.e. over ordinals, which can be denoted as K t L .3 in the taxonomy of modal logics from [START_REF] Blackburn | Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science[END_REF]. We show in particular that 1. the satisfiability problem for K t L .3 over the class of ordinals is NP-complete, and that 2. a formula ϕ of K t L .3 has a well-founded linear model if and only if it has a model of order type α for some α < ω • (|ϕ| + 2); this should be contrasted with the corresponding ω |ϕ|+2 bound proven in [START_REF] Demri | The complexity of linear-time temporal logic over the class of ordinals[END_REF]Cor. 3.3] for linear temporal logic.

These two results are however just byproducts of our main contribution, which is a sound and complete proof system for K t L .3 in which proof search runs in coNP.

All the algorithmic results for tense logic mentioned earlier in this introduction have been obtained via model-theoretic techniques, by showing that if a formula has a model, then it has a 'small' one, and it is actually possible to proceed similarly for K t L .3. However, as the resulting algorithms consist essentially in guessing a model, they are impractical as they are unlikely to avoid the (high) worst case complexity of the problem. In the case of the full linear temporal logic, this has motivated the use of automata-theoretic techniques [START_REF] Moshe | An automata-theoretic approach to automatic program verification[END_REF][START_REF] Gareth | Alternating Automata and the Temporal Logic of Ordinals[END_REF][START_REF] Bruyère | Automata on linear orderings[END_REF][START_REF] Demri | The complexity of linear-time temporal logic over the class of ordinals[END_REF], typically by building an at most exponential-sized automaton recognising the set of models of the formula: checking the language non-emptiness of the automaton can then be performed on-the-fly in PSPACE and can rely in practice on a rich algorithmic toolset. However, in the case of tense logic, it is not immediate how to tailor this approach to recover the above NP upper bound, because the automata for tense logic may require exponential-size-over ω, this is a consequence of the proof of [START_REF] Etessami | First-order logic with two variables and unary temporal logic[END_REF]Thm. 3]. Finally, if one's interest is to check that a formula ϕ is valid, neither the model-theoretic nor the automata-theoretic approach yields a 'natural' certificate that could be checked by simple independent means.

All these considerations motivate our use of proof-theoretic techniques. In their simplest form, those can be Hilbert-style axiomatisations which, in the context of modal logic, allow to characterise valid formulas in a way that is modular with respect to the considered classes of models-incidentally, the name K t L .3 refers to its axiomatisation (see Appendix A). However, these systems are not directly amenable to automated reasoning, which is rather achieved through more structured proof systems, the seminal example being Gentzen's sequent calculus. As the latter is often too limited for modal logics, it has been enriched in various ways, using e.g. labelled sequents [START_REF] Negri | Proof analysis in modal logic[END_REF], display calculus [START_REF] Nuel | Display logic[END_REF][START_REF] Kracht | Power and weakness of the modal display calculus[END_REF], nested sequents [START_REF] Kashima | Cut-free sequent calculi for some tense logics[END_REF][START_REF] Brünnler | Deep sequent systems for modal logic[END_REF][START_REF] Poggiolesi | The method of tree-hypersequents for modal propositional logic[END_REF][START_REF] Poggiolesi | A purely syntactic and cut-free sequent calculus for the modal logic of provability[END_REF][START_REF] Lellmann | Linear nested sequents, 2-sequents and hypersequents[END_REF], or hypersequents [START_REF] Arnon Avron | Hypersequents, logical consequence and intermediate logics for concurrency[END_REF][START_REF] Indrzejczak | Cut-free hypersequent calculus for S4.3[END_REF][START_REF] Kurokawa | Hypersequent calculi for modal logics extending S4[END_REF][START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF]. These enriched formalisms remain quite modular and sustain extensions simply by adding a few rules. They can be exploited to provide optimal complexity solutions to the validity problem directly by proof search [START_REF] Kanovich | The multiplicative fragment of linear logic is NP-complete[END_REF][START_REF] Lincoln | Decision problems for propositional linear logic[END_REF][START_REF] Baelde | A sequent calculus for a modal logic on finite data trees[END_REF][START_REF] Das | A cut-free cyclic proof system for Kleene algebra[END_REF][START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF], which may sometimes avoid the worst-case complexity of the problem and rely in practice on various heuristics. Finally, this approach obviously yields a proof of validity as a certificate in case of success.

Our proof system for K t L .3 is obtained as a natural extension of our earlier work on K t 4.3 [START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF], using additional insights from Avron's sequent calculus for KL [START_REF] Arnon Avron | On modal systems having arithmetical interpretations[END_REF]. This is satisfying since K t L .3 is simply obtained from K t 4.3-the tense logic of arbitrary linear time flows-by adding well-foundation to the left, i.e. towards the past (see Section 2), and completes the picture as K t Q the tense logic of dense linear time flows was also handled in [START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF]. Specifically, we use the framework of ordered hypersequents with clusters introduced in [START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF] as an elaboration, with terminating proof search, of Indrzejczak's ordered hypersequent calculus for K t 4.3 [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF][START_REF] Indrzejczak | Cut elimination theorem for non-commutative hypersequent calculus[END_REF]. Conceptually, re-using the framework required to generalise its semantics. The new semantics is more uniform, and allows us to provide purely proof-theoretic soundness, completeness, and complexity arguments in Section 3, unlike in [START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF] where soundness builds on a model-theoretic result from [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF].

Furthermore, our proof system is easily shown in Section 4 to also address the more precise problems of validity over all the well-founded linear time flows of order type β < α + 1 for a given α, and of order type exactly α < ω 2 . Such a result seems out of reach of axiomatisations, and yields for instance a coNP decision procedure for validity over ω-words. Finally, using the exponential translation of FO 2 (<) into tense logic given in [START_REF] Etessami | First-order logic with two variables and unary temporal logic[END_REF]Thm. 2], our results yield an optimal NEXP upper bound for satisfiability of the former over ordinals, which was already known from [START_REF] Otto | Two variable first-order logic over ordered domains[END_REF]. But more importantly they yield a proof system for FO 2 (<) over ordinals, which would be challenging to construct directly, because eigenvariables cannot be handled in the usual fashion.

2

Tense Logic over Ordinals

Syntax

Tense logic features two unary temporal operators, over a countable set Φ of propositional variables, with the following syntax:

ϕ ::= ⊥| p | ϕ ⊃ ϕ | G ϕ | H ϕ (where p ∈ Φ)
Formulae G ϕ and H ϕ are called modal formulae. Intuitively, G ϕ expresses that ϕ holds 'globally' in all future worlds, while H ϕ expresses that ϕ holds 'historically' in all past worlds. Other Boolean connectives may be encoded from ⊥ and ⊃, and as usual F ϕ = ¬G ¬ϕ expresses that ϕ will hold 'in the future' and P ϕ = ¬H ¬ϕ that it held 'in the past.'

Ordinal Semantics

In the case of K t L .3, our formulae shall be evaluated on Kripke structures M = (α, V ), where α is an ordinal and V : Φ → ℘(α) is a valuation of the propositional variables. Recall that an ordinal α is seen set-theoretically as {β ∈ Ord | β < α}. An ordinal is either 0 (the empty linear order), a limit ordinal λ (such that for all β < λ there exists γ with β < γ < λ), or a successor ordinal α + 1.

Given a structure M = (α, V ), we define the satisfaction relation M, β |= ϕ, where β < α and ϕ is a formula, by structural induction on ϕ:

M, β |= ⊥ M, β |= p iff β ∈ V (p) M, β |= ϕ ⊃ ψ iff if M, β |= ϕ then M, β |= ψ M, β |= G ϕ iff M, γ |= ϕ for all β < γ < α M, β |= H ϕ iff M, γ |= ϕ for all γ < β When M, β |= ϕ, we say that (M, β) is a model of ϕ.
Example 2.1. The satisfiable formulae of K t L .3 are strictly contained in the set of formulae satisfiable in K t 4.3, i.e. over arbitrary linear orders. For instance, the formula ϕ 0 = P p ∧ H (p ⊃ P p) is satisfiable in K t 4.3 but not in K t L .3, because all its models must contain an infinite decreasing sequence of worlds where p is true. Moreover, K t L .3 can force models to be of order type greater than ω: for instance, the formula

ϕ 1 = G (p ⊃ F p) ∧ G (¬p ⊃ F ¬p) ∧ F ¬p ∧ F (p ∧ G p)
forces to have a first infinite sequence of worlds not satisfying p, followed by a second infinite sequence of worlds satisfying p, and all its models (α, V ) must have α ≥ ω • 2.

Hypersequents with Clusters

As is often the case with modal logics, Gentzen's sequent calculus does not provide a rich enough framework to obtain complete proof systems. The extension we consider is to use hypersequents [START_REF] Arnon Avron | Hypersequents, logical consequence and intermediate logics for concurrency[END_REF], which are essentially sets of sequents logically interpreted as a disjunction. Indrzejczak has moved to ordered hypersequents [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF][START_REF] Indrzejczak | Cut elimination theorem for non-commutative hypersequent calculus[END_REF] (which are lists of hypersequents) to obtain a sound and complete calculus for K t 4.3. We have further enriched the structure of his ordered hypersequents with clusters and annotations [START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF] to obtain a calculus for K t 4.3 for which proof search terminates and, in fact, yields an optimal complexity decision procedure. We keep the same structure in the present work, but significantly adapt the proof rules, annotation mechanism, and even the semantics of hypersequents; we discuss these differences in more depth when concluding in Section 5. It should be noted that, unlike simple hypersequents, hypersequents with clusters do not have a translation as formulae.

Annotated Hypersequents with Clusters

A sequent (denoted S) is a pair of two finite sets of formulae, written Γ ∆. It is satisfied in a world γ of a structure M if, in that world, the conjunction of the formulae of Γ implies the disjunction of the formulae of ∆. In that case, we write M, γ |= Γ ∆. We define next the basic structure of our hypersequents, then enrich it with annotations to obtain the hypersequents that we shall work with.

Definition 3.1 (hypersequent).

A hypersequent is a list of cells, each cell being either a sequent or a non-empty list of sequents called a (syntactic) cluster. We shall use the following abstract syntax, where both operators ';' and ' ' are associative with unit '•':

H ::= C | H ; H (hypersequents) C ::= • | S | {Cl} (cells) Cl ::= S | Cl Cl (cluster contents)
Note that this definition allows for empty cells and hypersequents '•', but these notational conveniences will never arise in actual proofs-and should not be confused with the empty sequent ' '. We will see that the order of cells in a hypersequent is semantically relevant, but the order of sequents inside a cluster is not. Nevertheless, assuming an ordering as part of the syntactic structure of clusters is useful in order to refer to specific sequents or positions. Definition 3.2. An annotated sequent is a sequent that may be annotated with G formulae. We simply write Γ ∆ for a sequent carrying no annotation, otherwise we write, e.g., Γ ∆ (G ϕ, G ψ, . . .). Then, annotated hypersequents are hypersequents whose sequents are annotated, with the constraint that an annotation may only occur once in an annotated hypersequent, and that ϕ occurs on the right-hand side of sequents carrying the annotation G ϕ. Formally, we can see annotations as partial functions from the set of G formulae to the set of positions of the hypersequent.

Example 3.3. For instance, Γ ∆, ϕ (G ϕ);{Π Σ, ψ (G ψ)} is an annotated hypersequent but Γ ∆, ϕ, ψ (G ϕ, G ψ) ; {Π Σ, ψ (G ψ)}
is not allowed due to the two occurrences of (G ψ). Finally, ⊥ (G p) is not an annotated hypersequent as it fails the second condition.

Annotations will impact the semantics of hypersequents: intuitively, counter-models should attach to sequents annotated with (G ϕ) a world or set of worlds that invalidates ϕ and is (in a sense that will be made clear below) 'rightmost' for that property.

Semantics

The semantics of an ordered hypersequent with clusters relies on a notion of embedding which we define next, building on a view of hypersequents as partially ordered structures. Definition 3.4 (partial order of a hypersequent). Let H be a hypersequent containing n sequents, counting both the sequents found directly in its cells and those in its clusters. In this context, any i ∈ [1; n] is called a position of H, and we write H(i) for the i-th sequent of H. We define a partial order on the positions of H by setting i j if and only if either the i-th and j-th sequents are in the same cluster, or the i-th sequent is in a cell that lies strictly to the left of the cell of the j-th sequent. We write i ≺ j when i j but j i, i.e. j lies strictly to the right of i in H. We write i ∼ j when i j i. Finally, the domain of H is defined as dom(H) = ([1; n], ); note that empty cells are ignored in dom(H).

While a hypersequent is syntactically a finite partial order, its semantics will refer to a linear well-founded order, obtained by 'bulldozing' its clusters into copies of ω. The resulting order type is the object of the next definition.

Definition 3.5 (order type).

Let H be a hypersequent. We define its order type o(H) by induction on its structure: for cells, o(•) = 0, o(S) = 1, and o({Cl}) = ω, and for hypersequents, o(

H 1 ; H 2 ) = o(H 1 ) + o(H 2 ). Thus, o(H) = ω • k + m
where k is the number of clusters in H and m the number of non-empty cells to the right of the rightmost cluster.

Definition 3.6 (embedding).

Let H be an annotated hypersequent and α an ordinal. We say that µ : dom(H)

→ α + 1 \ {0} is an embedding of H into α, written H → µ α, if:
for all i, j ∈ dom(H), i ≺ j implies µ(i) < µ(j) and i ∼ j implies µ(i) = µ(j); and for all i ∈ dom(H), i is in a cluster if and only if µ(i) is a limit ordinal.

Observe that, if H → µ α, then o(H) < α + 1.

Definition 3.7 (semantics)

. Let M = (α, V ) be a structure, H a hypersequent, and µ an embedding H → µ α. We say that µ is annotation-respecting if, for all ϕ and i such that H(i) carries the annotation (G ϕ) and for all γ < α such that M, γ |= ¬ϕ, we have γ < µ(i).

We say that (M, µ) is a model of H, written M, µ |= H, if µ is annotation-respecting and there exists a position i of H and an ordinal β < µ(i) such that for all γ with β ≤ γ < µ(i)

we have M, γ |= H(i).
Following this definition, we say that a hypersequent is valid if for any M = (α, V ) and annotation-respecting H → µ α, we have M, µ |= H. A formula ϕ is valid in the usual sense (i.e., satisfied in every world of every ordinal structure) if and only if the hypersequent ϕ is valid in our sense.

If a hypersequent H is not valid, then it has a counter-model, that is a structure M = (α, V ) and an annotation-respecting embedding H → µ α such that, for every i ∈ dom(H) and β < µ(i), there exists γ with β ≤ γ < µ(i) such that M, γ |= H(i). For the positions i ∈ dom(H) that are not in clusters, µ(i) is a successor ordinal γ + 1 and this amounts to asking that M, γ |= H(i). When i is in a cluster, the condition implies the existence of an infinite increasing sequence (γ j ) j of ordinals with limit µ(i) = sup j γ j such that M, γ j |= H(i) for all j.

(ax)

H [ϕ, Γ ∆, ϕ] H [ϕ ⊃ ψ, Γ ∆, ϕ] H [ϕ ⊃ ψ, ψ, Γ ∆] H [ϕ ⊃ ψ, Γ ∆] (⊃ ) (⊥) H [Γ, ⊥ ∆] H [ϕ, Γ ∆, ψ, ϕ ⊃ ψ] H [Γ ∆, ϕ ⊃ ψ] ( ⊃)
Figure 1 Propositional rules of HKtL .3.

Proof System

We now present our proof system for K t L .3, called HK t L .3. This system deals with annotated hypersequents; from now on, we simply call sequents and hypersequents their annotated versions. The rules of HK t L .3 are given in figures 1 to 3: the first group includes the usual propositional rules, the second deals with modalities, and the last one with annotations. The figures make use of some notations which we explain next, before commenting on the rule definitions themselves.

Notations. First, we use hypersequents with holes. One-placeholder hypersequents, cells, and clusters are defined by the following syntax:

H [] ::= H ; C [] ; H C [] ::= | { Cl[] } Cl[] ::= Cl • Cl • Cl • ::= • | Cl
Two-placeholder cells and hypersequents have two holes identified by 1 and 2 :

H [] [] ::= H ; C [] [] ; H | H[ 1 ] ; H[ 2 ] C [] [] ::= { Cl[ 1 ] Cl[ 2 ] } | { Cl[ 2 ] Cl[ 1 ] } As usual, C [S] (resp. C [Cl]
) denotes the same cell with S (resp. Cl) substituted for ; two-placeholder cells and hypersequents with holes behave similarly. In terms of the partial orders underlying hypersequents with two holes, observe that the positions i and j associated resp. to 1 and 2 are such that i j. Second, we do not write explicitly the annotations that sequents may carry in rule applications. These annotations are implicitly the same in a conclusion sequent and the corresponding sequents in premises, or updated by adding the explicit annotation; freshly created sequents always have an explicit annotation. Annotations can prevent a rule application if the addition of an annotation would break the single-annotation constraint.

Third, we use a convenient notation for enriching a sequent: if S is a sequent Γ ∆ (A), then S (Γ ∆ (A )) is the sequent Γ, Γ ∆, ∆ (A, A ). Moreover, we sometimes need to enrich an arbitrary sequent of a cluster {Cl} with a sequent S; then {Cl} S denotes the cluster with its leftmost sequent enriched.

Rules. We now comment on the definition of our rules. The propositional rules of Figure 1 are straightforward: they are the usual ones applied to an arbitrary sequent of the hypersequent. The left modal rules of Figure 2 should not be surprising. For instance, in (G ), if the conclusion has a counter-model, then G ϕ holds at some ordinal and thus both ϕ and G ϕ must also hold at strictly greater ordinals. The rule also applies to two distinct sequents inside the same cluster; the soundness proof below shows how this is covered in detail. The ({G }) rule allows to proceed in the same way inside a cluster when the sequent 'further to the right' is the original sequent itself, something that our notations do not allow in (G ). Finally, (H ) and ({H }) are symmetric to the two previous rules. The rules ( G) and ( H) are the most complex ones. We shall not try to justify their soundness at this point, but simply make a few remarks that are important to understand their definition. First, these rules are the only ones that may introduce new cells in hypersequents. In the case of ( G), new cells are annotated with the principal formula G ϕ, which prevents another application of ( G) on G ϕ (otherwise a premise would carry this annotation at two positions). Second, the principal cell C [Γ ∆, G ϕ] in ( G) may be the rightmost cell of the conclusion hypersequent, in which case both C and H 2 are empty, and the rule has two or three premises depending on whether the principal cell is a cluster or not. When the principal cell is not rightmost, then C is not allowed to be empty, and the rule has one or two extra premises depending on whether C is a cluster or not. The situation is symmetric for ( H).

(G ) H [G ϕ, Γ ∆] [ϕ, G ϕ, Π Σ] H [G ϕ, Γ ∆] [Π Σ] H 1 ; Cl • ϕ, G ϕ, Γ ∆ Cl • ; H 2 H 1 ; Cl • G ϕ, Γ ∆ Cl • ; H 2 ({G }) (H ) H [ϕ, H ϕ, Π Σ] [H ϕ, Γ ∆] H [Π Σ] [H ϕ, Γ ∆] H 1 ; Cl • ϕ, H ϕ, Γ ∆ Cl • ; H 2 H 1 ; Cl • H ϕ, Γ ∆ Cl • ; H 2 ({H }) H 1 ; C [Γ ∆, G ϕ] ; ϕ (G ϕ) ; C ; H 2 H 1 ; C [Γ ∆, G ϕ] ; { ϕ (G ϕ)} ; C ; H 2 H 1 ; C [Γ ∆, G ϕ ϕ (G ϕ)] ; C ; H 2 if C = H 1 ; C [Γ ∆, G ϕ] ; C ( G ϕ) ; H 2 if C = • H 1 ; C [Γ ∆, G ϕ] ; C ( ϕ (G ϕ)) ; H 2 if C = • and C = {Cl} H 1 ; C [Γ ∆, G ϕ] ; C ; H 2 ( G) H 2 ; C ; H ϕ ϕ ; C [Γ ∆, H ϕ] ; H 1 H 2 ; C ( H ϕ) ; C [Γ ∆, H ϕ] ; H 1 if C = • H 2 ; C (H ϕ ϕ) ; C [Γ ∆, H ϕ] ; H 1 if C = • and C = {Cl} H 2 ; C ; C [Γ ∆, H ϕ] ; H 1 ( H)
((G)) H 1 [Γ ∆ (G ϕ)] ; H 2 [Π Σ, G ϕ] H 1 ; Γ ∆, G ϕ (G ϕ) ; H 2 ({(G)}) (( Ḡ)) H 1 [Γ ∆ (G ϕ)] ; H 2 [Π, ϕ Σ] H 1 [Γ ∆ (G ϕ)] ; H 2 [Π Σ]
Finally, the special rules of Figure 3 are, again, best explained through the soundness proof: they correspond to situations that can be ruled out or simplified by taking into account the annotation-respecting nature of our semantics. These rules are important to be able to extract counter-models from proof search failures (i.e., sequents on which no rule applies).

Examples. We have designed our rules so that they are all invertible: by keeping in premises all the formulae from the conclusion, we ensure that validity is never lost by applying a rule; this will be shown formally in Proposition 3.11. In practice, keeping all formulae can be unnecessarily heavy. Fortunately, it is easy to see that the following weakening rules are admissible:

(weak ) H [Γ ∆] H [Γ, ϕ ∆] H [Γ ∆] H [Γ ϕ, ∆] ( weak) Example 3.8. The formula ϕ 0 = P p ∧ H (p ⊃ P p) from Example 2.1 is not satisfiable in K t L .3, so the dual sequent S 0 = H (p ⊃ (H (p ⊃ ⊥) ⊃ ⊥)) H (p ⊃ ⊥) is valid.
Here is indeed a proof tree, with implicit uses of propositional and weakening rules, and principal formulae shown in orange.

(ax)

H (p ⊃ ⊥), p p ; S 0 H (p ⊃ ⊥), p H (p ⊃ ⊥) ; S 0 (ax) p ⊃ (H (p ⊃ ⊥) ⊃ ⊥), H (p ⊃ ⊥), p ; S 0 (⊃ ) H (p ⊃ ⊥), p ; H (p ⊃ (H (p ⊃ ⊥) ⊃ ⊥)) H (p ⊃ ⊥) (H ) H (p ⊃ (H (p ⊃ ⊥) ⊃ ⊥)) H (p ⊃ ⊥) ( H) Example 3.9. Since ϕ 1 = G (p ⊃ F p) ∧ G (¬p ⊃ F ¬p) ∧ F ¬p ∧ F (p ∧ G p) from Example 2.1 is satisfiable, its dual sequent S 1 = G (G p ⊃ p), G (p ⊃ (G (p ⊃ ⊥) ⊃ ⊥)) G p, G ϕ where ϕ = p ⊃ ⊥ ∨ (G p ⊃ ⊥) is invalid, although with no counter-models below ω • 2.
In our calculus, proof search for S 1 will succeed on branches not considering at least two clusters; we show below in Figure 4 one such branch, with implicit uses of propositional and weakening rules, and principal formulae shown in orange.

. . . . . . (ax) S1 ; p p (G p) ; {G p, p (G ϕ)} S1; p, G p (G p) ; {G p, p (G ϕ)} ({(G)}) S1 ; G p ⊃ p p (G p) ; {G p, p (G ϕ)} (⊃ ) G (G p ⊃ p), G (p ⊃ (G (p ⊃ ⊥) ⊃ ⊥)) G p, G ϕ ; p (G p) ; {G p, p (G ϕ)} (G ) . . . G (G p ⊃ p), G (p ⊃ (G (p ⊃ ⊥) ⊃ ⊥)) G p, G ϕ ; {G p, p (G ϕ)} ( G) G (G p ⊃ p), G (p ⊃ (G (p ⊃ ⊥) ⊃ ⊥)) G p, G (p ⊃ ⊥ ∨ (G p ⊃ ⊥)) ( G)
Figure 4 In a proof of S1 (Example 3.9) branches with a non-cluster cell for (G p) are provable.

However, proof search will fail on the branch shown in Figure 5, which corresponds to the counter-model described in Section 2.

. . . . . . . . . S1 ; { G p, p (G p)} ; {G p, p (G ϕ) p G (p ⊃ ⊥) (G (p ⊃ ⊥))} S1 ; { G p, p (G p)} ; {G p, p (G ϕ) p, p ⊃ (G (p ⊃ ⊥) ⊃ ⊥) (G (p ⊃ ⊥))} (⊃ ) S1 ; { G p, p (G p)} ; {G p, p (G ϕ) p (G (p ⊃ ⊥))} (G ) . . . S1 ; { G p, p (G p)} ; {G p, p G (p ⊃ ⊥) (G ϕ)} ( G) S1 ; {G p ⊃ p p (G p)} ; {p ⊃ (G (p ⊃ ⊥) ⊃ ⊥), G p, p (G ϕ)} (⊃ )×2 G (G p ⊃ p), G (p ⊃ (G (p ⊃ ⊥) ⊃ ⊥)) G p, G ϕ ; { p (G p)} ; {G p, p (G ϕ)} (G )×2 . . . G (G p ⊃ p), G (p ⊃ (G (p ⊃ ⊥) ⊃ ⊥)) G p, G ϕ ; {G p, p (G ϕ)} ( G) G (G p ⊃ p), G (p ⊃ (G (p ⊃ ⊥) ⊃ ⊥)) G p, G (p ⊃ ⊥ ∨ (G p ⊃ ⊥)) ( G)
Figure 5 A failed branch in the proof of S1 (Example 3.9).

Soundness

Proposition 3.10. The rules of HK t L .3 are sound: if the premises of a rule instance are valid, then so is its conclusion.

Proof. We show the contrapositive: considering an application of a rule with a conclusion hypersequent H and a counter-model (M, µ) of H with M = (α, V ) and H → µ α, we provide a counter-model of one of the premises (or a contradiction when there is no premise).

Since we will often have to extend an embedding with a value for a new position, we define µ + (i → α) as the mapping µ such that µ (i) = α, µ (k) = µ(k) for k < i and µ (k + 1) = µ(k) for k ≥ i in the domain of µ.

A full proof is given in Appendix B, and we cover here only a few key cases. Consider first an application of ( G) with Γ ∆, G ϕ at position i, when C ; H 2 is empty. For any β i < µ(i) there exists γ i with β i ≤ γ i < µ(i) such that M, γ i |= H(i), hence there also exists γ i > γ i such that M, γ i |= ϕ. Let γ be the least ordinal that contains all such γ i . We have that µ(i) ≤ γ.

If µ(i) = γ, then µ(i) must be a limit ordinal. Hence C = and the third premise H 3 is available. We construct a counter-model (M, µ ) for it by taking µ = µ + (k → γ),

where k = i + 1 is the new position in H 3 . Indeed, we have that for any β < µ (k) there exists γ with β ≤ γ < µ (k) and M, γ |= ϕ (the inequality can even be made strict). Moreover, the annotation is respected by definition of γ: there cannot be any λ ≥ γ such that M, λ |= ϕ. Otherwise we conclude by observing that (M, µ ) is a counter-model of one of the first two premises with µ = µ + (k → γ) where k is the newly created position. We check that µ is monotone, because µ(i) < γ. If γ is a successor ordinal, (M, µ ) is a counter-model of the first premise simply because the predecessor of γ invalidates ϕ and the annotation is respected; both hold by construction. If γ is a limit ordinal we have a counter-model (M, µ ) of the second premise: we do have that for any β < µ (k) there exists γ with β ≤ γ < µ (k) that invalidates ϕ, and the annotation is respected by construction.

When C ; H 2 is not empty, we need to consider whether γ is less than the ordinal to which the positions of C are mapped by µ, and use the last two premises when it is not the case.

The case of ( H) is similar, but simpler in that we can take γ = λ + 1 where λ is the least ordinal such that M, λ |= ϕ. Finally, annotation rules (Figure 3) rely on the annotation-respecting condition on µ: informally, ϕ cannot be falsified at an ordinal beyond µ(i) when i carries the annotation (G ϕ), thus the conclusions of ((G)) and ({(G)}) cannot have counter-models, and ϕ must be satisfied at ordinals corresponding to Π Σ for (( Ḡ)).

Completeness and Complexity

As in [START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF], completeness is a by-product of the very simple proof-search behaviour of our calculus. As we shall see, all the rules are invertible and proof search branches are polynomially bounded, as long as obvious pitfalls are avoided in the search strategy. Thus it is useless to backtrack during proof-search. Moreover, proof attempts result in finite (polynomial depth) partial proofs, whose unjustified leaves yield counter-models that amount (by invertibility) to counter-models of the conclusion. Hence the completeness of our calculus. We detail this argument below, and its corollary: proof-search yields an optimal coNP procedure for validity.

Proposition 3.11 (invertibility). In any rule instance, if a premise has a counter-model, then so does its conclusion.

Proof. Considering a rule instance with a counter-model (M, µ) of a premise H, we build a counter-model (M, µ ) of the conclusion H . Depending on the rule that is applied, H and H will either have exactly the same structure, or H will have a new cell. Accordingly, we take µ to be the restriction of µ to the positions of H (and adapt it accordingly for the positions

(H ) (ax) H a, a a ; H b b ; H a a ; H a, H b H a a ; H b b ; H a a ; H a, H b b, H a a ; H b b, H a ; H a, H b H a a ; H b b, H a ; H a, H b (H ) • • • H a a ; H b b ; H a, H b • • • ( H) H a a ; H a, H b ( H) H a, H b ( H) Figure 6
Proof search with a failure hypersequent and an immediately provable hypersequent.

that have been shifted). It is indeed a proper annotation-respecting embedding of H into M. It is then easy to see that (M, µ ) is a counter-model of H , since any sequent

H (i) is contained in the corresponding sequent H(j): M, µ(j) |= H(j) implies M, µ (i) |= H (i).
We characterise next the proof attempts that we consider for proof search, and show how to extract counter-models when such attempts fail. Definition 3.12. We say that a sequent is immediately provable if it is provable by an application of (H ) or ({H }) followed by (ax). We call partial proof a finite derivation tree whose internal nodes correspond to rule applications, but whose leaves may be unjustified hypersequents, and that satisfies two conditions: any rule application should be such that all premises differ from the conclusion; immediately provable sequents must be proven through (ax) and (H ) or ({H }). Finally, we call failure hypersequent a hypersequent that can only be the conclusion of a rule instance when it is also one of its premises.

Obviously, a hypersequent has a proof if and only if it has a partial proof without unjustified leaves. The two conditions on partial proofs amount to a simple proof search strategy that avoids loops. The second one addresses specifically loops arising from repeated applications of ( H), in branches where several new cells are created for the same H ϕ formula: this results in two cells of the form Γ, H ϕ ϕ, ∆ and thus in an immediately provable hypersequent. This is seen, for example, in the first premise of the third application of rule ( H) in Figure 6. Finally, failure hypersequents correspond to points where proof search is stuck, as with the unjustified hypersequent of Figure 6. We show next that such hypersequents are invalid.

Proposition 3.13. Any failure hypersequent H has a counter-model.

Proof sketch, details in Appendix B. We construct a counter-model over α = o(H), taking µ as the only possible embedding, notably satisfying µ(i) = ω • k if i belongs to the k-th cluster of H and µ(i) = ω • k + m if i is the m-th cell between the k-th and the next cluster (if any). We can then take a function pos : α → dom(H) which maps worlds β < α to positions of H in a way that respects the partial order induced by H. For a position i that does not belong to a cluster, pos(β) = i if and only if β is the predecessor of µ(i). A position i appearing in a cluster must correspond to an infinite sequence of ordinals of limit µ(i), so that for all i ∼ j and β, if pos(β) = i then there exists γ with β < γ < µ(i) = µ(j) such that pos(γ) = j; informally, this ensures that positions i and j inside a cluster are 'infinitely interleaved' within µ(i) = µ(j). For example, for the unjustified hypersequent of Figure 5, we could set pos(0) = 1, pos(i) = 2 for all other i < ω, pos(ω + 2j) = 3 and pos(ω + 2j + 1) = 4 for all j ≥ 0. We finally define the valuation

V : Φ → ℘(α) by V (p) = {β < α | ∃Γ, ∆ . H(pos(β)) = (p, Γ ∆)} and let M = (α, V ).
We claim that M, γ |= H(pos(γ)) for all γ < α: we prove by induction on ψ that, if ψ appears in the left-hand (resp. right-hand) side of H(pos(γ)), then M, γ ψ (resp. M, γ ψ). Most cases follow a standard argument, we only detail the one where ψ = G ϕ occurs on the right of H(pos(γ)). Since ( G) does not apply, an annotation must already exist for G ϕ. By rules ((G)) and ({(G)}) this annotation must be on a position i such that pos(γ) i. By definition of annotations, ϕ occurs on the right of H(i). Hence, there exists γ > γ such that i = pos(γ ), and M, γ ϕ, thus M, γ G ϕ. From there we can check that H → µ α, and the rule (( Ḡ)) enforces that µ is annotationrespecting. It is then easy to conclude that (M, µ) is a counter-model of H.

We now turn to establishing that proof search terminates, and always produces branches of polynomial length. For a hypersequent H, let len(H) be its number of sequents (i.e., the size of dom(H)), and |H| the number of distinct subformulae occurring in H.

Lemma 3.14 (small branch property). For any partial proof of a hypersequent H, any branch of the proof is of length at most 2(|H| + len(H) + 1) • |H|.

Proof. Let H be a hypersequent, P a partial proof of it, and B a branch of P. Remark that the number of positions in hypersequents of β is bounded by |H| + len(H) + 1: we have at most len(H) positions initially, and a new position may only be created once per modal formula among at most |H| formulae plus possibly one more (overall) to create an immediately provable hypersequent. This is by definition of the annotation system for G formulae, and because a second cell created by ( H) on the same H ϕ would belong to an immediately provable sequent. Any rule application adds some subformulae among |H| to the left or to the right of the turnstile at a position among |H| + len(H) + 1, hence with 2(|H| + len(H) + 1)

• |H| choices. Thus B is of length at most 2(|H| + len(H) + 1) • |H|.
We conclude that HK t L .3 is complete, and also enjoys optimal complexity proof search.

Theorem 3.15 (completeness). Every valid hypersequent H has a proof in HK t L .3.

Proof. Assume that H is not provable. Consider a partial proof P of H that cannot be expanded any more: its leaves cannot be obtained as the conclusion of a rule instance. Such a partial proof exists by Lemma 3.14. Any unjustified leaf of that partial proof has a counter-model by Proposition 3.13, and by invertibility it is also a counter-model of H. Proof. Proof search can be implemented in an alternating Turing machine maintaining the current hypersequent on its tape, where existential states choose which rule to apply (and how) and universal states choose a premise of the rule. By Lemma 3.14, the computation branches are of length bounded by a polynomial. By Proposition 3.11, the non-deterministic choices in existential states can be replaced by arbitrary deterministic choices, thus the resulting Turing machine has only universal states, hence is in coNP.

Logic on Given Ordinals

We have designed a proof system that is sound and complete for K t L .3, and enjoys optimal complexity proof search. We now show that this system can easily be enriched to obtain decision procedures not only for tense logic over arbitrary ordinals, but also for tense logic over specific ordinals. We first observe that the logic can only distinguish ordinals up to ω 2 , which should be contrasted with [START_REF] Demri | The complexity of linear-time temporal logic over the class of ordinals[END_REF]. Then we show how to capture validity over ordinals below some ω • k + m, and finally how to reason over a specific ordinal of this form.

Proposition 4.1 (small model property). If a hypersequent H has a counter-model, then it has a counter-model of order type α < ω • (|H| + len(H) + 1).

Proof. This is a corollary of Theorem 3.15. By the proof of Lemma 3.14, the hypersequents in a failure hypersequent-which are not immediately provable-have at most |H| + len(H) nonempty cells. The counter-model extracted in Proposition 3.13 from a failure hypersequent H is over o(H ) < ω • (|H| + len(H) + 1). A counter-model for H is then obtained by Proposition 3.11, with a different embedding but the same structure.

In particular, for a formula ϕ, the hypersequent H = ϕ has |H| = |ϕ| and len(H) = 1, hence the ω • (|ϕ| + 2) bound announced in the introduction.

Next we observe that we can easily enrich our calculus to obtain a proof system for tense logic over ordinals below a certain type α. Proposition 4.2. Let α be an ordinal. The proof system HK t L .3 enriched with the following axiom is sound and complete for tense logic over ordinals β ≤ α:

H (ordα) if o(H) > α
Proof. The soundness argument for the rules of HK t L .3 (Proposition 3.10) carries over to the restricted semantics, since the underlying structure (and ordinal) is never modified in the argument. Conversely, the completeness argument of Theorem 3.15 can be strengthened because, thanks to the new rule, we can guarantee that any failure hypersequent H is such that o(H) ≤ α, hence the extracted counter-model is also below this bound.

{ } k1 ; ϕ ; { } k2 ; ( ) m and { } k ; ( ) m1 ; ϕ ; ( ) m2
where

k 1 + k 2 = k, k 2 > 0 and m 1 + m 2 = m -1.
In other words, one must consider all hypersequents H containing one sequent ϕ and otherwise only empty sequents, and such

that o(H) = ω • k + m.
For instance, when k = m = 0, ϕ vacuously holds in all worlds of (0, V ). When k = 0 and m = 1 we are checking ϕ only, and (ord α ) closes any branch where a new cell is created, rendering modal formulae trivially true. When k = 1 and m = 0 we are checking ϕ ; { }.

Proof. If ϕ holds in all worlds of all structures of the form (α, V ) for some V , the hypersequents are valid and thus provable in HK t L .3 with (ord α ). We prove the converse by contradiction. Assume that all the hypersequents hold and M, β |= ϕ for some M = (α, V ) and

β < α. If ω • k 1 ≤ β < ω • (k 1 + 1) with k 1 + 1 ≤ k
we can build an embedding to obtain a counter-model of the first kind of sequent. Otherwise, ω • k ≤ β < ω • k + m and we derive a counter-model of the second kind of sequent.

Example 4.5. Consider the formula G ϕ for ϕ = G ⊥ ⊃ ⊥. We cannot prove G ϕ in general, since this formula is not satisfied over finite ordinals, as witnessed by the following partial proof and its failure hypersequent (in the left branch) corresponding to a counter-model over the ordinal 2:

( ⊃) G ϕ ; G ⊥ ⊥, ϕ (G ϕ) G ϕ; ϕ (G ϕ) G ϕ ; { G ⊥, ⊥ ⊥, ϕ (G ϕ)} (⊥) G ϕ ; { G ⊥ ⊥, ϕ (G ϕ)} ({G }) G ϕ ; { ϕ (G ϕ)} ( ⊃) G ϕ ( G)
According to Proposition 4.4, over α = ω, i.e., k = 1 and m = 0, we need to prove G ϕ ; { } in HK t L .3 extended with (ord ω ), for which the presence of the cluster will be crucial. The extra rule (ord ω ) is actually not necessary in this case, but simplifies the proof. We start with an application of ( G), this time with three premises:

G ϕ; ϕ (G ϕ) ; { } G ϕ ; { ϕ (G ϕ)} ; { } G ϕ ; { G ϕ} G ϕ ; { } ( G)
The first premise is derived as follows:

G ϕ ; G ⊥ ⊥, ϕ (G ϕ) ; {⊥ } (⊥) G ϕ ; G ⊥ ⊥, ϕ (G ϕ) ; { } (G ) G ϕ; ϕ (G ϕ) ; { } ( ⊃)
The middle premise can simply be discharged by (ord ω ). For the last premise, we use ( G) inside the cluster, which yields three premises: G ϕ ; { G ϕ} ; ϕ (G ϕ) and G ϕ ; { G ϕ} ; { ϕ (G ϕ)} are discharged by (ord ω ), while the last one is derived as follows:

G ϕ ; {⊥ G ϕ G ⊥ ⊥, ϕ (G ϕ)} (⊥) G ϕ ; { G ϕ G ⊥ ⊥, ϕ (G ϕ)} (G ) G ϕ ; { G ϕ ϕ (G ϕ)} ( ⊃)

Related Work and Conclusion

We have designed the first proof system for K t L .3, i.e. tense logic over ordinals. Thanks to Indrzejczak's ordered hypersequents [START_REF] Indrzejczak | Linear time in hypersequent framework[END_REF], enriched with clusters and annotations as in [START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF], our system enjoys optimal complexity proof search, allows to derive small model properties, and can be extended into a proof system for variants of the logic over bounded or fixed ordinals. Our ( H) rule is broadly related to the rule that Avron uses in his system for KL [START_REF] Arnon Avron | On modal systems having arithmetical interpretations[END_REF]. Unlike Avron, we cannot work with standard sequents due to the presence of converse modalities. In turn, this allows us to consider a somewhat simpler right introduction rule for H , which does not have to take into account H Γ antecedents as they will remain available in the principal cell when a new one is created.

The system most closely related to HK t L .3 is obviously the calculus for K t 4.3 [START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF] in which we introduced the notions of clusters and annotations. These were inspired by the small model property of K t 4.3 [START_REF] Ono | On the size of refutation Kripke models for some linear modal and tense logics[END_REF], and it is notable that we could put them to work in the considerably richer setting of K t L .3; it is the main technical contribution of the present paper. In retrospect, we believe that it is possible to present the semantics of HK t L .3 hypersequents as a particular case of HK t 4.3 hypersequents: the semantics µ(i) of a position in a cluster would be infinite to the left and right for HK t 4.3, but only infinite to the right for HK t L .3. This shift of perspective, together with the addition of rule (( Ḡ)), allows to get rid of the somewhat awkward use of different semantics for the soundness and completeness of HK t 4.3. It also frees the proof-theoretic development from the small model property; in fact, proof theory then allows to derive the small model property just as precisely. Of course, there are also fundamental differences between HK t L .3 and HK t 4.3: well-foundedness allows us to take H ϕ assumptions in rule ( H), which renders (H ϕ) annotations useless; this benefit of well-foundedness for proof search is usual [START_REF] Arnon Avron | On modal systems having arithmetical interpretations[END_REF][START_REF] Baelde | A sequent calculus for a modal logic on finite data trees[END_REF].

A Axiomatisation

For reference, the logic K t L .3 can also be defined as the set of theorems generated by necessitation, modus ponens and substitution from classical tautologies and the following axioms [START_REF] Blackburn | Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science[END_REF]Ch. 4]:

G (p ⊃ q) ⊃ (G p ⊃ G q) (K r ) H (p ⊃ q) ⊃ (H p ⊃ H q) (K ) p ⊃ G P p (t r ) p ⊃ H F p (t ) F p ∧ F q ⊃ F (p ∧ F q) ∨ F (p ∧ q) ∨ F (q ∧ F p) (.3 r )
P p ∧ P q ⊃ P (p ∧ P q) ∨ P (p ∧ q) ∨ P (q ∧ P p) (. 3)

H (H φ ⊃ φ) ⊃ H φ (L )
The first two axioms are simply the Kripke schema, given for each modality. Next we find the t axioms, which force the two modalities to be converses of each other. The canonical models of the trichotomy axioms .3 have accessibility relationships that are non-branching to the left and to the right. Finally, the axiom (L ) of Gödel-Löb ensures that the models are transitive and well-founded to the left.

B Detailed Proofs

Proposition 3.10. The rules of HK t L .3 are sound: if the premises of a rule instance are valid, then so is its conclusion.

Proof. We show the contrapositive: considering an application of a rule with a conclusion hypersequent H and a counter-model (M, µ) of H with M = (α, V ) and H → µ α an annotation-respecting embedding, we provide a counter-model of one of the premises (or a contradiction when there is no premise).

Since we will often have to extend an embedding with a value for a new position, we define µ + (i → α) as the mapping µ such that µ (i) = α, µ (k) = µ(k) for k < i and µ (k + 1) = µ(k) for k ≥ i in the domain of µ.

The case of propositional rules (Figure 1) is immediate: The usual reasoning applies to the principal sequent, and the same embedding is used to obtain a counter-model of one of the premises.

Next we turn to the modal rules of Figure 2:

Consider the case of (G ), applied with G ϕ, Γ ∆ at position i and Π Σ at position j such that i j. Remark that the rule ensures that i = j, but we do not need this assumption to justify it. We show that (M, µ) is an annotation-respecting counter-model of the premise H , concentrating on the only difference with H, at position j. For clarity we distinguish two cases:

When i ≺ j, we also have µ(i) < µ(j). Since (M, µ) is a counter-model of H, by taking an arbitrary β i < µ(i) we obtain γ i such that

β i ≤ γ i < µ(i) such that M, γ i |= H(i).
In particular, M, γ i |= G ϕ. Now, considering an arbitrary β < µ(j) we need to exhibit γ such that β ≤ γ < µ(j) and M, γ |= H (j). By taking β j = max(β, µ(i)) < µ(j) we obtain γ j such that β j ≤ γ j < µ(j) and M, γ j |= H(j). Furthermore, since γ i < µ(i) ≤ β j ≤ γ j , we also have M, γ j |= ϕ and M, γ j |= G ϕ, hence M, γ j |= H (j).

When i ∼ j we have that µ(i) = µ(j) and it is a limit ordinal because we are considering positions in a cluster. Consider an arbitrary β < µ(i). There exists γ i such that β ≤ γ i < µ(i) and M, γ i |= H(i). Because µ(i) is a limit ordinal, γ i + 1 < µ(i) = µ(j). Again, there exists γ j such that γ i + 1 ≤ γ j < µ(j) and M, γ j |= H(j). But, since γ i < γ j we also have that γ j satisfies ϕ and G ϕ, hence M, γ j |= H (j).

The case of rule ({G }) is covered by the second part of the previous argument, by taking i = j. Indeed, we have i ∼ i when ({G }) applies at position i.

Consider now an application of rule (H ) with Π Σ at position i and H ϕ, Γ ∆ at j. We have i j, hence µ(i) ≤ µ(j). Consider an arbitrary β < µ(i). There exists γ i such that β ≤ γ i < µ(i) and M, γ i |= H(i). We claim, as before, that there exists γ j such that γ i < γ j < µ(j) and M, γ j |= H(j). Indeed, if µ(i) < µ(j) then there exists γ j with µ(i) ≤ γ j < µ(j) that falsifies H(j). Otherwise µ(i) = µ(j) but then this must be a limit ordinal and, by considering We now distinguish several cases regarding γ. When C ; H 2 is not empty let j be the first position of the conclusion hypersequent that is in C .

γ i + 1 < µ(i) = µ(j) we obtain γ i < γ j < µ(j)
If µ(i) = γ, then µ(i) must be a limit ordinal. Hence C = and the third premise H 3 is available. We construct a counter-model (M, µ ) for it by taking µ = µ + (k → γ),

where k = i + 1 is the new position in H 3 . Indeed, we have that for any β < µ (k) there exists γ with β ≤ γ < µ (k) and M, γ |= ϕ (the inequality can even be made strict). Moreover, the annotation is respected by definition of γ: there cannot be any λ ≥ γ such that M, λ |= ϕ.

If C ; H 2 is empty, or γ < µ(j), we conclude by observing that (M, µ ) is a countermodel of one of the first two premises with µ = µ + (k → γ) where k is the position of the new cell in these premises. We check that µ is monotone, because µ(i) < γ, and γ < µ(j) when it is defined. If γ is a successor ordinal, (M, µ ) is a counter-model of the first premise simply because the predecessor of γ invalidates ϕ and the annotation is respected; both hold by construction. If γ is a limit ordinal we have a counter-model (M, µ ) of the second premise: we do have that for any β < µ (k) there exists γ with β ≤ γ < µ (k) that invalidates ϕ, and the annotation is respected by construction. Otherwise µ(j) ≤ γ. * If µ(j) < γ, we obtain a counter-model (M, µ) of the fourth premise H 4 . We check it for the only position whose sequent has changed between H and H 4 , that is position j. Take any β j < µ(j). We know that there exists γ j with β j ≤ γ j < µ(j) such that M, γ j |= H(j). But, since γ j < µ(j) < γ, there exists δ such that γ j < δ < γ and M, δ |= ϕ. Thus M, γ j |= G ϕ, and M, γ j |= H 4 (j). * If µ(j) = γ and is a limit ordinal, we also obtain a counter-model (M, µ) of the fourth premise. This time, for any β j < µ(j), we know that there exists γ j with β j ≤ γ j < µ(j) such that M, γ j |= H(j). But, since γ j < γ and γ is a limit ordinal, there still exists δ such that γ j < δ < γ and M, δ |= ϕ. Thus M, γ j |= G ϕ, and M, γ j |= H 4 (j).

there exists γ with β < γ < µ(i) = µ(j) such that pos(γ) = j; informally, this ensures that positions i and j inside a cluster are 'infinitely interleaved' within µ(i) = µ(j).

We finally define a valuation V : Φ → ℘(α) by V (p) = {β < α | ∃Γ, ∆ . H(pos(β)) = (p, Γ ∆)} and let M = (α, V ). We now claim that M, γ |= H(pos(γ)) for all γ < α: we prove by induction on ψ that, if ψ appears in the left-hand (resp. right-hand) side of the turnstile in H(pos(γ)), then M, γ ψ (resp. M, γ ψ).

If ψ is an atom p ∈ Φ the results follow by definition of V , and because (ax) does not apply to H. The propositional cases are obtained by induction hypothesis, because the corresponding rules of Figure 1 have already been applied. The cases of modal formulae on the left-hand side are similar, we only detail that of H . If ψ = H ϕ occurs on the left-hand side of H(pos(γ)) then by (H ) and ({H }), the formula ϕ must occur on the left-hand side of any H(i) with i Moreover, for all γ < γ, we have pos(γ ) pos(γ) by (a), so M, γ ϕ, and thus M, γ ψ. Assume that ψ = G ϕ occurs on the right of H(pos(γ)). Since ( G) does not apply, an annotation must already exist for G ϕ. By rules ((G)) and ({(G)}) this annotation must be on a position i such that pos(γ) i. By definition of annotations, ϕ occurs on the right of H(i). By (c), there exists γ > γ such that i = pos(γ ). We then have M, γ ϕ, thus M, γ G ϕ. Assume finally that ψ = H ϕ occurs on the right of H(pos(γ)). We prove by a subinduction on pos(γ) that M, γ |= H ϕ. Since ( H) does not apply, and since the first premise necessarily differs from the conclusion, it must be that there is a cell C preceding the cell that contains pos(γ), and that the last two premises (if available) would coincide with H. Let i be the first position in C . Take an arbitrary λ < µ(i) such that pos(λ) = i (such a λ always exists, thanks to (b) and (c) instantiated with β = 0). Since i ≺ pos(γ) it must be that λ < γ. As noted above, we have either that H ϕ belongs to the right-hand side of H(i), or that ϕ belongs to its left-hand side. In the first case, we obtain M, λ |= H ϕ by induction hypothesis on i < pos(γ). In the second case we directly have M, λ |= ϕ. We conclude either way that M, γ |= H ϕ.

We can check that H → µ α: the conditions of Definition 3.6 hold by construction. We must also check that µ is annotation-respecting. Assume that H(i) carries the annotation (G ϕ), and that there is a world M, β |= ϕ. Let j = pos(β). If j i, then by (c) there exists γ with β < γ < µ(i) such that i = pos(γ), so β < µ(i) as expected. If i ≺ j, then by the rule (( Ḡ)) ϕ occurs on the left of H(j), contradicting M, β |= ϕ. Otherwise, i = j and by (b) we have β < µ(pos(β)) = µ(i) as expected.

Finally, (M, µ) is a counter-model of H. Indeed, for all i ∈ dom(H) and β < µ(i) there exists γ with β ≤ γ < µ(i) such that pos(γ) = i, and hence M, γ |= H(i): if pos(β) = i, we can take γ = β, else (b) enforces pos(β) i, and (c) provides one such γ.

Figure 2

 2 Figure 2 Modal rules of HKtL .3. In ( G) and ( H), we allow C = • only when H2 = •.

Figure 3

 3 Figure 3 Annotation rules of HKtL .3.

Proposition 3 . 16 .

 316 Proof search in HK t L .3 is in coNP.

Example 4 . 3 .Proposition 4 . 4 .

 4344 When extending HK t L .[START_REF] Baelde | A hypersequent calculus with clusters for linear frames[END_REF] to check for validity below ω, the failing branch of Figure5can be completed, as well as the other failing branches since they all involve hypersequents of order type ω • 2, and S 1 becomes provable.We finally show how to capture validity at a fixed ordinal α < ω 2 . The basic idea is to start with a hypersequent H such that o(H) = α = ω • k + m for some finite k and m, and take rule (ord α ) to forbid larger ordinals. The only catch is that we should check that the formula of interest in valid in all possible positions. Let us write { } k for { }; • • • ; { } with k clusters containing the empty sequent, and ( ) m for ; • • • ; with m cells containing the empty sequent. The formula ϕ is valid in all structures of order type exactly α = ω •k +m if and only if HK t L .3 extended with (ord α ) proves all hypersequents of the form

  that invalidates H(j). Having M, γ j |= H(j), we also have M, γ j |= H ϕ. Thus γ i satisfies ϕ and H ϕ, and M, γ i |= H (i) as needed. The case of ({H }) is covered by the previous argument.

Consider an application of ( G) with Γ ∆, G ϕ at position i. For any β i < µ(i) there exists γ i with β i ≤ γ i < µ(i) such that M, γ i |= H(i), and thus M, γ i |= G ϕ. Hence there also exists γ i > γ i such that M, γ i |= ϕ. Let γ be the least ordinal that contains all such γ i . We have that µ(i) ≤ γ.

* Finally, if µ(j) = γ and is not a limit ordinal, then the position j is not in a cluster, so the fifth premise is available. We claim that it admits (M, µ) as a counter-model. Let θ be the predecessor of γ = θ + 1, which satisfies M, θ |= ϕ by definition of γ. Since (M, µ) is a counter-model of H we also have M, θ |= H(j). This allows us to conclude, together with the fact that, as before, the new annotation is respected by definition of γ (there cannot be any λ ≥ γ such that M, λ |= ϕ).

Finally we consider an application of rule ( H) with Γ ∆, H ϕ at position i. Let j be the first position of C , if it exists. For any β i < µ(i) there exists γ i with β i ≤ γ i < µ(i) that invalidates H(i), thus there exists γ i < γ i < µ(i) such that M, γ i |= ϕ. Let γ be the successor of the least ordinal among all such γ i . We have γ < µ(i).

where k is the new position in that premise. We do have that the predecessor of γ satisfies H ϕ (by minimality) but not ϕ (by definition). Moreover, µ is indeed annotation-respecting. If µ(j) = γ then C cannot be a cluster, because γ is a successor. In that case (M, µ) directly yields a counter-model of the third premise. Otherwise γ < µ(j) and (M, µ) is a counter-model of the second premise.

We finally consider the case of annotation rules (Figure 3): Consider an application of ((G)), with H(i) = Γ ∆ (G ϕ) and H(j) = Π Σ, G ϕ, and i ≺ j. By definition of an embedding, we have µ(i) < µ(j). Since (M, µ) is a counter-model of H, there exists γ j such that µ(i) ≤ γ j < µ(j) and M, γ j |= H(j). There also exists γ i < µ(i) such that M, γ i |= H(i). Hence there exists γ > γ j such that M, γ |= ϕ. A fortiori, γ > γ i , so µ does not respect the annotation on i, contradiction. Consider an application of ({(G)}) with H(i) = Γ ∆, G ϕ (G ϕ). For any β < µ(i) there exists γ with β < γ such that M, γ |= ϕ. Because µ is annotation-respecting, we must have γ < µ(i), thus µ(i) is a limit ordinal. This contradicts the fact that i is not in a cluster. Consider an application of (( Ḡ)) with Γ ∆ (G ϕ) at position i and Π Σ at position j, with i ≺ j. Since µ is annotation-respecting we have that, for all λ ≥ µ(i), M, λ |= ϕ. Hence (M, µ) is a counter-model of the premise. Proposition 3.13. Any failure hypersequent H has a counter-model.

Proof. Let α = o(H).

We define µ : dom(H) → α + 1 \ {0} as follows:

if i is the m-th cell of H and appears before its first cluster;

is the m-th cell between the k-th and the next cluster (if any). Now let pos : α → dom(H) be a function such that:

There always exists one such function. Its choice is quite constrained due to the definitions of α and µ. Positions i that are not in a cluster will be such that i = pos(β) for a single β, typically the predecessor of µ(i). A position i appearing in a cluster must correspond to an infinite sequence of ordinals of limit µ(i), so that for all i ∼ j and β, if pos(β) = i then


Agnès Helmstetter

Yan Y Kagan

David D Jackson

High-resolution time-independent grid-based forecast for m ≥ 5 earthquakes in California

INTRODUCTION

We have developed time-independent forecasts for California assuming that small earthquakes can be used to map the distribution of large damaging earthquakes, as suggested by [START_REF] Kafka | Does the spatial distribution of smaller earthquakes delineate areas where larger earthquakes are likely to occur?[END_REF]. Indeed, large earthquakes often nucleate in areas that have a large density of small events.

We have first declustered the catalog to remove large fluctuations of seismic activity which do no represent the long-term average. We have then estimated the spatial density of seismicity using a kernel method to smooth the location of magnitude m ≥ 2 earthquakes. Note that our model only predicts hypocenters, not rupture areas. Clearly, large earthquakes sometime propagate in areas with little seismicity, as observed for the 1857 earthquake that ruptured the southern section of the San Andreas fault, which is now mostly devoid of small earthquakes. Our model should thus be coupled with a fault model to forecast rupture areas for large earthquakes.

Our model is very similar to the time-independent forecasts of [START_REF] Helmstetter | Comparison of short-term and timeindependent earthquake forecast models for southern California[END_REF], which is in its turn an adaptation of the program by [START_REF] Kagan | Long-term probabilistic forecasting of earthquakes[END_REF] to local modern catalogs. Compared with [START_REF] Helmstetter | Comparison of short-term and timeindependent earthquake forecast models for southern California[END_REF], we have extended our forecasts to all California, and done small changes in the method. We have slightly modified the declustering method. We have modified the estimation of the smoothing distance d i used to estimate the spatial density of seismicity. Our new method is simpler and computationally more efficient, but gives very similar results. We have also estimated the completeness magnitude m 0 in each cell, and corrected our model to account for spatial variations of m 0 .

We have developed two time-independent models for the RELM earthquake forecast testing [START_REF] Kagan | Testing hypotheses of earthquake occurrence[END_REF][START_REF] Schorlemmer | Earthquake likelihood model testing[END_REF]. The first one evaluates the expected rate of all m ≥ 5 earthquakes, while the other one estimates the probability of independent events only. The two models have the same spatial distribution, but different total number of predicted events, and slightly different magnitude distributions.

Instead of the Gutenberg-Richter law [START_REF] Gutenberg | Frequency of earthquakes in California[END_REF] with a uniform b-value of 1 used by [START_REF] Helmstetter | Comparison of short-term and timeindependent earthquake forecast models for southern California[END_REF], we use a tapered Gutenberg-Richter law with a corner magnitude m c = 8, with b = 0.95 for the first model (all events) and b = 0.89 for the second model (estimated from independent events). We modify the magnitude distribution in the Geysers geothermal area, which has a much larger value b ≈ 2 for m ≥ 3.3.

EARTHQUAKE CATALOG AND DECLUSTERING

We use earthquakes of magnitude m ≥ 2 in the Advanced National Seismic System (ANSS) catalog, in the time period from 1981/1/1 to 2005/8/23. We selected earthquakes within a rectangular area 30.55 In order to measure the time-independent earthquake rate, we need to decluster the catalog to remove large fluctuations of seismicity rate in space and time due to aftershock sequences. For that we used [START_REF] Reasenberg | Second-order moment of Central California seismicity, 1969-1982[END_REF] declustering algorithm. The program CLUSTER2000 is available at http://quake.wr.usgs.gov/research/software. [START_REF] Reasenberg | Second-order moment of Central California seismicity, 1969-1982[END_REF] identified aftershocks by modeling an interaction zone around each earthquake. The spatial size of the interaction zone is based on an estimate of the stress redistribution following each earthquake. The temporal extent of the interaction zone is based on an Omori law decay of earthquake frequency following an event of a given magnitude. Two earthquakes are associated if their hypocentral and origin time difference are respectively less than the spatial and temporal extent of the dynamically modeled interaction zone for the first event [START_REF] Reasenberg | Second-order moment of Central California seismicity, 1969-1982[END_REF]. We used the following parameters:

• r fact = 8 (number of crack radii surrounding each earthquake within which to consider linking a new event into cluster)

• x meff = 2.00 ("effective" lower magnitude cutoff for catalog)

• x k = 0.50 (increase of the lower magnitude cutoff during clusters:

x meff = x meff + x k m,
where m is the magnitude of the largest event of the cluster)

• p 1 = 0.95 (probability of detecting the next clustered event, used to compute the look-ahead time τ )

• τ min = 1.0 day (minimum value of the lookahead time for building clusters, when the first event is not clustered)

• τ max = 5.0 days (maximum value of look-ahead time for building clusters)

• minimum cluster size of 5 events.

We modified the expression of the interaction distance in Reasenberg's code. We use r = 0.01 × 10 0.5m km, as suggested by [START_REF] Wells | New empirical relationships among magnitude, rupture length, rupture width, rupture area, and surface displacement[END_REF] for the scaling of rupture length with magnitude in California, instead of r = 0.011 × 10 0.4m and r < 30 km in Reasenberg's algorithm.

The resulting declustered catalog has 81659 "independent events" ("mainshocks" and "background" events), and 75545 "dependent events" ("foreshocks" and "aftershocks"). The parameters of the declustering algorithm were adjusted to remove large fluctuations of seismic activity in space and time. Clearly, the resulting declustered catalog is still clustered in space and time, as can be seen from the distribution of interevent times, which presents a deviation from an exponential distribution at short times. However, this residual clustering occurs at small space and time scales. Therefore, the density measured from this declustered catalog over large scales gives a good estimation of the long-term spatial distribution of seismicity. The declustered catalog is shown in Figure 1.

SPATIAL DISTRIBUTION OF SEISMICITY

We estimate the density of seismicity in each cell by smoothing the location of each earthquake i with an isotropic adaptive kernel K di ( r). We tested two choices for K d ( r), either a power-law

K d ( r) = C(d) (| r | 2 + d 2 ) 1.5 , (1)
or a Gaussian

K d ( r) = C ′ (d) exp - | r | 2 2 d 2 , ( 2
)
where d is the smoothing distance, and C(d) and C ′ (d) are normalizing factors, so that the integral of K d ( r) over an infinite area equals 1. We measure the smoothing distance d i associated with earthquake i as the horizontal distance between event i and the n th v closest neighbor. The number of neighbors, n v , is an adjustable parameter, estimated by optimizing the forecasts. We impose d i > 0.5 km to account for location accuracy. The kernel bandwidth d i thus decreases if the density of seismicity at the location r i of this earthquake increases, so that we have a better resolution (smaller d i ) where the density is higher.

The density at any point r is then estimated by

µ( r ) = N i=1 K di ( r -r i ) . (3)
Our forecasts are given as an average number of events in each cell of 0.1 • . The density defined by ( 3) has fluctuations at scales smaller than the grid resolution. Therefore, we need to integrate µ( r ) defined by (3) over each cell to obtain the seismicity rate in this cell.

CORRECTING FOR CATALOG INCOMPLETENESS

We have used events with m ≥ 2 to estimate the spatial distribution of seismicity. Unfortunately, the catalog is not complete everywhere at this magnitude level. Moreover, two regions, one south of 32 • N (Mexico), and one west of 124.5 • W (Mendocino area), have a much larger completeness magnitude (up to ≈ 4), and have also a high rate of large earthquakes. In order to correct for catalog incompleteness, we have estimated the completeness magnitude m 0 in each cell from the magnitude distribution.

We can estimate the magnitude distribution P m ( r , m) at point r using the same kernel method as described above to estimate the density µ( r ). We now smooth both the locations and magnitudes of all earthquakes using

P m ( r , m) = N i=1 K di ( r -r i ) G h (m -m i ) , (4)
where G h (m) is a Gaussian function of mean m and width h. The kernel width h is fixed to 15 km. We then integrate P m ( r , m) over each cell to get the magnitude distribution in this cell.

The simplest method to estimate the completeness magnitude is to define m 0 as the maxima of the smoothed magnitude distribution in each cell. Using this method, we obtain large small-scale fluctuations of m 0 , which are probably non-physical. The completeness magnitude should be relatively smooth at scales smaller than the typical distance between seismic stations. Therefore we smooth the completeness magnitude m 0 using a Gaussian filter with a standard deviation of 15 km. The result is shown in Figure 2. The central part of the testing area has m 0 ≈ 2. The completeness magnitude is much larger, up to m 0 = 4, close to the boundaries of the testing areas, especially in the Mendocino area and in Mexico. Note that a completely different method to estimate m 0 has been proposed by [START_REF] Bachmann | Probabilistic estimates of monitoring completeness of seismic networks[END_REF]. Instead of using the magnitude distribution to estimate m 0 , they use the spatial distribution of seismic stations and the detection characteristics of each station to map m 0 .

The forecasted rate of events with m ≥ m min in each cell can then be corrected from spatial variations of m 0 assuming that the magnitudes obey the Gutenberg-Richter law [START_REF] Gutenberg | Frequency of earthquakes in California[END_REF]

with b = 1 µ ′ ( r ) = µ( r ) 10 m0( r )-mmin .
(5)

LIKELIHOOD, PROBABILITY GAIN, AND MODEL OPTIMIZATION

We estimate the parameter n v (the number of neighbors, used to compute the smoothing distance d i in (3)) by optimizing the likelihood of the model. We use two different data sets to build the model µ ′ (i x , i y ) and to test it. We evaluate the performance of the forecasts by computing the likelihood of the model. In this section, we are interested only in the spatial distribution of seismicity. We do not consider the magnitude distribution of target events, or the expected number of events. Therefore, we compute the normalized density µ * (i x , i y ) in each cell (i x , i y ) using

µ * (i x , i y ) = µ ′ (i x , i y ) N t Nx i ′ x =1 Ny i ′ y =1 µ(i ′ x , i ′ y ) , (6)
where N x and N y are the total numbers of columns and rows, and N t is the number of target events. The expected number of events for the model µ * thus equals the observed number N t .

The log-likelihood of the model is given by

L = Nx ix=1 Ny iy=1 log p [ µ * (i x , i y ), n ] , ( 7
)
where n is the number of events that occurred in the cell (i x , i y ). Assuming a Poisson process, the probability p[µ * (i x , i y ), n] of having n events in the cell (i x , i y ) is given by

p[µ * (i x , i y ), n] = [µ * (i x , i y )] n exp[-µ * (i x , i y )] n! , (8)
We have tried different values of the minimum magnitude, both for the input catalog (used to measure µ) and for the target events (used to test the model). We use the same catalog for the input and target events, but different time intervals or magnitude intervals, so that earthquakes used to estimate µ are not used as target events to test the model. We evaluate the performance of our forecasts using the probability gain per earthquake of the model relative to a model with a uniform density

G = exp L -L unif N t , (9)
where L unif is the log-likelihood for a uniform model.

The results are summarized in Table 1. Figure 3 shows the density for model #2 in Table 1. The power-law kernel (2) gives a slightly larger likelihood than the Gaussian (1) (see models #1 and #2 in Table 1).

The probability gain does not change significantly with the minimum magnitude of target events for 3 ≤ m min ≤ 5.5 (see models #2-7). This suggests that small and large earthquakes have about the same spatial distribution, i.e., that the magnitude distribution is relatively uniform in space, at scales larger than the cell size of ≈ 10 km.

In contrast, the probability gain decreases continuously with the minimum magnitude of input data, as shown in models #8-20 in Table 1. The probability gain per earthquake, for target earthquakes with m ≥ 5, decreases from G = 3.0 for m min = 2, to G = 1.2 for m min = 5. G decreases with m min because the number of events used to compute µ decreases, thus the resolution of the model decreases.

Model #21 in Table 1 uses all the available input data, from 1981/1/1 to 2005/8/23, in order to estimate µ. When tested on m ≥ 3 target earthquakes since 1996, this model gives a larger gain than model #2, which used only 1981-1996 data to build the model. The increase of G between G = 4.8 for model #2 and G = 7.1 for model #21 may be partly due to the increase of the number of input events. But it's mainly due to the fact that we use (in part) the same data to build the model and to test it. Our final model (our forecast for the next 5 yrs) is model #21 in Table 1, which uses all available data.

CONCENTRATION PLOT

Another tool to test a model is the "concentration plot", which compares the observed and expected number of events as a function of the modeled density µ. The concentration plot for model #2 is shown in Figure 4. The upper plot shows the cumulative number of events as a function of the value of µ in the cells where these events occur. The lower plot shows the probability density function (obtained by taking the derivative of the curves in Figure 4a): the observed and expected number of events within each interval of µ-values. A model is incorrect if there is a significant deviation between the observed and modeled distributions. If the observed distribution is shifted to the right compared to the expected one, the model is too smooth. In our case, the observed curves are slightly to the left of the model, which means that our model is too "localized": there are more observed events in the regions of low modeled probability µ that expected.

A model is better than another one if the observed distribution in the concentration plot is shifted toward larger values of µ. The µ values in Figure 4 have been normalized so that the sum over the testing area equals 1. For comparison, a uniform model would have a density µ unif = 1/N c = 1.3 × 10 -4 (where N c = 7642 is the number of cells in the testing area). As shown in Figure 4, most events (79%) occur within cells where the modeled density is larger than the average µ unif . For this model, the average value of the density at the location of a target earthquake is 18 times larger than the average value.

MAGNITUDE DISTRIBUTION

We assume for simplicity that the magnitude distribution obeys a tapered Gutenberg-Richter law (Gutenberg and Richter, 1944) with a uniform b-value and corner magnitude m c . Specifically, we assume that the cumulative magnitude distribution has the form P (m) = 10 -b(m-mmin) exp 10 1.5(mmin-mc) ] -10 1.5(m-mc) , (10) with a minimum magnitude m min = 4.95, and a corner magnitude m c = 8, as suggested by [START_REF] Bird | Plate-tectonic analysis of shallow seismicity: Apparent boundary width, beta, corner magnitude, coupled lithosphere thickness, and coupling in seven tectonic settings[END_REF] for continental transform fault boundaries. The exponential factor in (10) describes a falloff of the distribution of seismic moments M ∼ 10 1.5m .

We use the catalog provided by RELM (available at http://proto-testing.ethz.ch/downloads/ANSS.catalog.dat), because it uses the same magnitude type and declustering method as will be used for the RELM tests. This catalog contains all events in the ANSS catalog in California with m ≥ 3, between 1984 and 2004, and gives the independence probability p i for each earthquake.

We have measured the b-value using the likelihood method [START_REF] Aki | Maximum likelihood estimate of b in the formula logN = a -bM and its confidence limits[END_REF]

b = 1 log(10)(< m > -m min ) . ( 11
)
For the non-declustered catalog, this gives b = 0.95. In order to estimate the b-value of independent events, we have measured the average magnitude < m > in ( 11) by selecting all events in the RELM catalog within the testing area, with m ≥ 4.95, and weighting each earthquake by its independence probability. This gives b = 0.89, with a number of independent events of 93. The declustering procedure slightly decreases the b-value, because it removes preferentially small events. The cumulative magnitude distribution for the non-declustered catalog is shown in Figure 5.

There is however a region, the Geysers in Northern California (lat ≈ 38.8 • N, and lon ≈ 128.8 0 W), which has an unusual magnitude distribution. It has many small m ≥ 2 events and a very large b-value. These earthquakes are induced by the geothermal activity in this area. If we assume that the magnitude distribution in this region obeys the Gutenberg-Richter law with b = 0.89, this gives a very large expected rate of m ≥ 5 earthquakes, close to the largest value in all California, while the largest event has m = 4.7 (see Figure 3).

We have thus modified the magnitude distribution in this area (for -128.9 • < lon < -128.7 • , and 38.7 • < lat < 38.9 • ). We have fitted the magnitude distribution by the Gutenberg-Richter law, selecting all events with m ≥ 3.3 in the RELM declustered catalog. The maximum likelihood method gives b = 1.94. We use the same corner magnitude m c = 8 in this region as everywhere else. For smaller events with m < 3, the magnitude distribution has a more usual b-value close to 1.

The cumulative magnitude distribution for the Geysers is shown in Figure 5. We have used this fit to estimate the expected rate of m ≥ 5 earthquakes at the Geysers, from the modeled density of m ≥ 2 events. This correction decreases the expected rate of m ≥ 5 events by a factor 80 at the Geysers compared to the model with a uniform magnitude distribution with b = 0.89 (see Figure 5). The difference further increases for larger target events. We checked that other geothermal or volcanic areas (Mammoth Lakes, Coso, Salton Sea) have a magnitude distribution close to the global distribution for California. Geothermal activity is thus not the sole cause of anomalous magnitude distribution at the Geysers.

The corrected density of m ≥ 5 events is shown in Figure 6. Compared to Figure 3, the dark spot at the Geysers has disappeared. The differences between Figures 3 and6 are the change in P (m) for the Geysers and the time window used to select input events. Figure 3

EXPECTED NUMBER OF EVENTS

We have estimated the total expected number of target events by counting the number of m > 4.95 earthquakes in the RELM catalog, which occurred within the testing area, during the time window 1984-2004. We have removed 9 m ≥ 5 events from this catalog that are explosions. This gives a total number of 7.38 earthquakes per year.

In order to estimate the rate of independent events, we have weighted each earthquake by its independence probability. This gives an average number of 4.41 events per year. We then estimate the expected number of events per year within each space-timemagnitude bin according to

E(i x , i y , i m ) = N 0 µ 0 (i x , i y ) P (i m ) , (12)
where N 0 is the expected number of target events per year in the testing area, µ 0 is equal to the spatial distribution µ, normalized so that the sum of µ 0 in the testing area equals 1, and P (i m ) is the expected number of events within the magnitude bin i m , estimated from (10). For the first model, we use N 0 = 7.38 and b = 0.95. For the second model (to forecast independent m ≥ 5 events), we use N 0 = 4.41 and b = 0.89.

CONCLUSION

We have developed a time-independent forecast for California, by smoothing seismicity. We have shown that including small m ≥ 2 events to predict larger m ≥ 5 earthquakes significantly improves the performance of the model. In contrast, the performance of our model does not depend on the minimum magnitude of target events: our model predicts as well m ≥ 3 and m ≥ 5.5 events. This suggests that large earthquakes have the same spatial distribution as smaller ones, and justifies our use of small earthquakes to estimate the probability of larger ones.

We have taken into account spatial variations of the completeness magnitude. We have also modified the magnitude distribution in the Geysers geothermal area, which has a very unusually large b-value. This correction is rather artificial, and in the future we would like to use a more systematic approach to estimate the magnitude distribution in each cell.

Because there are not enough large historical earthquakes in California, we cannot measure the corner magnitude m c (magnitude at which the magnitude distribution deviates from a pure Gutenberg-Richter law). We thus use a uniform value m c = 8, as suggested by [START_REF] Bird | Plate-tectonic analysis of shallow seismicity: Apparent boundary width, beta, corner magnitude, coupled lithosphere thickness, and coupling in seven tectonic settings[END_REF] for continental transform fault boundaries.

Some would argue that this corner magnitude may not hold for all of California, because there are few long enough faults in California which could produce a m = 8 earthquake. However, it is becoming increasingly apparent that fault length is not a reliable barrier to earthquake growth: [START_REF] Gabrielov | Geometric incompatibility in a fault system[END_REF] show that plate geometry cannot be stable on a deforming Earth, and of course the faults we see today were not always there. [START_REF] Black | Maximum Magnitude in Relation to Mapped Fault Length and Fault Rupture[END_REF] present evidence that southern California earthquakes commonly break the boundaries of geologically mapped faults. Also, the Denali 2002 M7.9 earthquake in Alaska started at a small unknown thrust fault and then proceeded to rupture strike-slip Denali fault, then rupturing Totschunda fault [START_REF] Rowe | Preface to the issue dedicated to the 2002 Denali fault earthquake sequence[END_REF].

In addition to the epicenter, seismic hazard estimation also requires the specification of the fault plane. [START_REF] Kagan | Long-term probabilistic forecasting of earthquakes[END_REF] have developed a method to forecast the orientation of the fault plane, by smoothing the focal mechanisms of past m ≥ 5.5 earthquakes. As for forecasting epicenters, it may be useful to include small earthquakes in the forecasts, in order to improve the resolution. Alternatively, our model could be coupled with fault models to predict the rupture geometry of very large earthquakes, which are likely to break a known fault.

ifornia Earthquake Center (SCEC), by the James S. Mc-Donnell Foundation 21st century scientist award/studying complex system, and by the Brinson Foundation. SCEC is funded by NSF Cooperative Agreement EAR-0106924 and USGS Cooperative Agreement 02HQAG0008. The SCEC contribution number for this paper is 983.

Table 1. Time interval [t 1 t 2 ] and minimum magnitude m min used to select input events and target earthquakes. Input events are used to compute µ. Target events are used to evaluate the log-likelihood L (7) and the probability gain per earthquake G (9). The smoothing parameter n v is adjusted to maximize L. The second column specifies the kernel function used to smooth earthquake locations, either a power-law ('pl') or a Gaussian ('gs'). -125-124-123-122-121-120-119-118-117-116-115-114

  compares forecasted rate using 1981-1996 data with earthquakes that occurred since 1996. It is thus a pseudo-real time test of the model. Figure 6 is our final forecast, which uses all available data between 1981/1/1 and 2005/8/23. The fact that the 2 models are very similar is encouraging. This shows that the spatial density does not change significantly with time.

Figure 2 .Figure 3 .

 23 Figure 2. Completeness magnitude m 0 , estimated by the maxima of the magnitude distribution in each cell, using declustered m ≥ 2 earthquakes from 1981/1/1 to 2005/8/23.

Figure 4 .

 4 Figure 4. Concentration plot for model #2 in Table 1, shown in Figure 3. The solid line is the expected number of events as a function of the modeled density µ, and the dashed line is the observed number. (a) Cumulative distribution: number of earthquakes that occur in a cell with µ * (i x , i y ) < µ. (b) Probability density function.

Figure 5 .

 5 Figure 5. Cumulative magnitude distribution, for all earthquakes within the testing area between 1984 and 2004 (solid line with dots), and fit by (10) (dashed line) with b = 0.93 for m ≥ 5. The lower curves are for the Geysers geothermal area. The dashed line is a fit by (10) with b = 1.99 for m ≥ 3.3.

Figure 6 .

 6 Figure 6. Forecasted seismicity rate (expected number of m > 4.95 events per year in each cell) for model #21 in Table 1, using a power-law kernel to smooth the location of m ≥ 2 earthquakes from 1981 to 2005. Circles are m ≥ 5 earthquakes that occurred between 1996/1/1 and 2005/8/23.

  • < latitude < 43.95 • and -126.35 • < longitude < -112.15 • , larger by 1 • than the RELM testing area, to avoid finite region size effects.

Acknowledgments. We acknowledge the Advanced National Seismic System for the earthquake catalog. Part of this work was done while one of the authors (AH) was at the KITP in Santa Barbara. This work is partially supported by NSF-EAR02-30429, NSF-PHY99-0794, NSF-EAR03-37226, NSF-EAR-0409890, by the Southern Cal-