Kaustuv Chaudhuri
email: kaustuv.chaudhuri@inria.fr

Damien Doligez
email: damien.doligez@inria.fr

Leslie Lamport

Stephan Merz
email: stephan.merz@inria.fr

Verifying Safety Properties With the TLA+ Proof System

Overview

TLAPS, the TLA + proof system, is a platform for the development and mechanical verification of TLA + proofs. The TLA + proof language is declarative, and understanding proofs requires little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. Proofs are written in the same language as specifications; engineers do not have to translate their high-level designs into the language of a particular verification tool. A proof manager interprets a TLA + proof as a collection of proof obligations to be verified, which it sends to backend verifiers that include theorem provers, proof assistants, SMT solvers, and decision procedures.

The first public release of TLAPS is available from [START_REF]TLAPS web-site[END_REF], distributed with a BSD-like license. It handles almost all the non-temporal part of TLA + as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties. Intuitively, a safety property asserts what is permitted to happen; a liveness property asserts what must happen; for a more formal overview, see [START_REF] Alpern | Defining liveness[END_REF][START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF].

Foundations

TLA + is a formal language based on TLA (the Temporal Logic of Actions) [START_REF] Lamport | Specifying Systems[END_REF]. It was designed for specifying the high-level behavior of concurrent and distributed systems, but it can be used to specify safety and liveness properties of any discrete system or algorithm. A behavior is a sequence of states, where a state is an assignment of values to state variables. Safety properties are expressed by describing the allowed steps (state transitions) in terms of actions, which are first-order formulas involving two copies v and v ′ of each state variable, where v denotes the value of the variable at the current state and v ′ its value at the next state. These properties are proved by reasoning about actions, using a small and restricted amount of temporal reasoning. Proving liveness properties requires propositional linear-time temporal logic reasoning plus a few TLA proof rules.

It has always been possible to assert correctness properties of systems in TLA + , but not to write their proofs. We have added proof constructs based on a hierarchical style for writing informal proofs [START_REF] Lamport | How to write a proof[END_REF]. The current version of the language is essentially the same as the version described elsewhere [START_REF] Chaudhuri | A TLA + Proof System[END_REF]. Here, we describe only the TLAPS proof system. Hierarchical proofs are a stylistic variant of natural deduction with lemmas and have been used in other declarative proof languages [START_REF] Corbineau | A declarative proof language for the Coq proof assistant[END_REF][START_REF] Rudnicki | An overview of the Mizar project[END_REF][START_REF] Wenzel | The Isabelle/Isar reference manual[END_REF]. A hierarchical proof is either a sequence of steps together with their proofs, or a leaf (lowest-level) proof that simply states the known facts (previous steps and theorems) and definitions from which the desired conclusion follows. The human reader or a backend verifier must ensure that the leaf proofs are correct in their interpretation of TLA + to believe the entire proof.

The TLAPS proof manager, TLAPM, reads a (possibly incomplete) hierarchical proof and invokes the backend verifiers to verify the leaf proofs. One important backend is Isabelle/TLA + , which is an implementation of TLA + as an Isabelle object logic (see Section 4.1). Isabelle/TLA + can be used directly with Isabelle's generic proof methods, or other certifying backend verifiers can produce proofs that are checked by Isabelle/TLA + . Currently, the only certifying backend is the Zenon theorem prover [START_REF] Bonichon | Zenon : An extensible automated theorem prover producing checkable proofs[END_REF]. Among the non-certifying backends is a generic SMT-LIB-based backend for SMT solvers, and a decision procedure for Presburger arithmetic. We plan to replace these with certifying implementations such as the SMT solver veriT [START_REF] Bouton | veriT: An open, trustable and efficient SMT-solver[END_REF] and certifying implementations of decision procedures [START_REF] Chaieb | Proof synthesis and reflection for linear arithmetic[END_REF].

TLAPS is intended for avoiding high-level errors in systems, not for providing a formal foundation for mathematics. It is far more likely for a system error to be caused by an incomplete or incorrect specification than by an incorrect proof inadvertently accepted as correct due to bugs in TLAPS. Although we prefer certifying backends whenever possible, we include non-certifying backends for automated reasoning in important theories such as arithmetic.

Proof management

A TLA + specification consists of a root module that can (transitively) import other modules by extension and parametric instantiation. Each module consists of a number of parameters (state variables and uninterpreted constants), definitions, and theorems that may have proofs. TLAPS is run by invoking the Proof Manager (TLAPM) on the root module and telling it which proofs to check. In the current version, we use pragmas to indicate the proofs that are not to be checked, but this will change when TLAPS is integrated into the TLA + Toolbox IDE [START_REF]TLA + Toolbox[END_REF]. The design of TLAPM for the simple constant expressions of TLA + was described in [START_REF] Chaudhuri | A TLA + Proof System[END_REF]; this section explains the further processing required to support more of the features of TLA + . TLAPM first flattens the module structure, since the module language of TLA + is not supported by backend verifiers, which will likely remain so in the future.

Non-constant reasoning: A TLA + module parameter is either a constant or a (state) variable. Constants are independent of behaviors and have the same value in each state of the behavior, while a variable can have different values in different states. Following the tradition of modal and temporal logics, TLA + formulas do not explicitly refer to states. Instead, action formulas are built from two copies v and v ′ of variables that refer to the values before and after the transition. More generally, the prime operator ′ can be applied to an entire expression e, with e ′ representing the value of e at the state after a step. A constant expression e is one that does not involve any state variables, and is therefore equal to e ′ . (Double priming is not allowed in TLA + ; the TLA + syntactic analyzer catches such errors.)

Currently, all TLAPS backends support logical reasoning only on constant expressions. The semantics of the prime operator is therefore syntactically approximated as follows: it is commuted with all ordinary operators of mathematics and is absorbed by constant parameters. Thus, if e is the expression (u = v + 2 * c) where u and v are variables and c a constant, then e ′ equals u ′ = v ′ + 2 * c. TLAPM currently performs such rewrites and its rewrite engine is trusted.

Operators and substitutivity: At any point in the scope of its definition, a user-defined operator is in one of two states: usable or hidden. A usable operator is one whose definition may be expanded in a proof; for example, if the operator P defined by P(x, y) ∆ = x + 2 * y is usable, then TLAPM may replace P(2, 20) with 2 + 2 * 20 (but not with 42, which requires proving that 2 + 2 * 20 = 42). A user-defined operator is hidden by default; it is made usable in a particular leaf proof by explicitly citing its definition, or for the rest of the current subproof by a use step (see [START_REF] Chaudhuri | A TLA + Proof System[END_REF] for the semantics of use).

Because TLA + is a modal logic, it contains operators that do not obey substitutivity, which underlies Leibniz's principle of equality. For example, from (u

= 42) = true one cannot deduce (u = 42) ′ = true ′ , i.e., u ′ = 42. A unary operator O( ) is substitutive if e = f implies O(e) = O( f ),
for all expressions e and f . This definition is extended in the obvious way to operators with multiple arguments. Most of the modal primitive operators of TLA + are not substitutive; and an operator defined in terms of non-substitutive operators can be non-substitutive. If a non-substitutive operator is usable, then TLAPM expands its definition during preprocessing, as described in the previous paragraph; if it is hidden, then TLAPM replaces its applications by cryptographic hashes of its text to prevent unsound inferences by backend verifiers. This is a conservative approximation: for example, it prevents proving O(e ∧ f ) = O( f ∧ e) for a hidden non-substitutive operator O. Users rarely define non-substitutive operators, so there seems to be no urgent need for a more sophisticated treatment.

Subexpression references:

A fairly novel feature of the TLA + proof language is the ability to refer to arbitrary subexpressions and instances of operators, theorems, and proof steps that appear earlier in the module or in imported modules, reducing the verbosity and increasing the maintainability of TLA + proofs. Positional references denote a path through the abstract syntax; for example, for the definition, O(x, y) Verifying obligations: Once an obligation is produced and processed as described before, TLAPM invokes backend verifiers on the proof obligations corresponding to the leaf proofs. The default procedure is to invoke the Zenon theorem prover first. If Zenon succeeds in verifying the obligation, it produces an Isabelle/Isar proof script that can be checked by Isabelle/TLA + . If Zenon fails to prove an obligation, then Isabelle/TLA + is instructed to use one of its automated proof methods. The default procedure can be modified through pragmas that instruct TLAPM to bypass Zenon, use particular Isabelle tactics, or use other backends. Most users will invoke the pragmas indirectly by using particular theorems from the standard TLAPS module. For instance, using the theorem named SimpleArithmetic in a leaf proof causes TLAPM to invoke a decision procedure for Presburger arithmetic for that proof. The user can learn what standard theorems can prove what kinds of assertions by reading the documentation, but she does not need to know how such standard theorems are interpreted by TLAPM.

Backend verifiers 4.1 Isabelle/TLA +

Isabelle/TLA + is an axiomatization of TLA + in the generic proof assistant Isabelle [START_REF] Paulson | Isabelle: A Generic Theorem Prover[END_REF]. It embodies the semantics of the constant fragment of TLA + in TLAPS; as mentioned in Section 2, it is used to certify proofs found by automatic backend verifiers. We initially considered encoding TLA + in one of the existing object logics that come with the Isabelle distribution, such as Isabelle/ZF or Isabelle/HOL. However, this turned out to be inconvenient, mainly because TLA + is untyped. (Indeed, TLA + does not even distinguish between propositions and terms.) We would have had to define a type of TLA + values inside an existing object logic and build TLA + -specific theories for sets, functions, arithmetic etc., essentially precluding reuse of the existing infrastructure.

Isabelle/TLA + defines classical first-order logic based on equality, conditionals, and Hilbert's choice operator. All operators take arguments and return values of the single type c representing TLA + values. Set theory is based on the uninterpreted predicate symbol ∈ and standard Zermelo-Fränkel axioms. Unlike most presentations of ZF, TLA + considers functions to be primitive objects rather than sets of ordered pairs. Natural numbers with zero and successor are introduced using Hilbert's choice as some set satisfying the Peano axioms; the existence of such a set is established from the ZF axioms. Basic arithmetic operators over natural numbers such as ≤, +, and * are defined by primitive recursion, and division and modulus are defined in terms of + and * . Tuples and sequences are defined as functions whose domains are initial intervals of the natural numbers. Characters are introduced as pairs of hexadecimal digits, and strings as sequences of characters. Records are functions whose domains are finite sets of strings. Isabelle's flexible parser and pretty-printer transparently converts between the surface syntax and the internal representation. The standard library introduces basic operations for these data structures and proves elementary lemmas about them. It currently provides more than 1400 lemmas and theorems, corresponding to about 200 pages of pretty-printed Isar text. Isabelle/TLA + sets up Isabelle's generic automated proof methods (rewriting, tableau and resolution provers, and their combinations).

It is a testimony to the genericity of Isabelle that setting up a new object logic was mostly a matter of perseverance and engineering. Because TLA + is untyped, many theorems come with hypotheses that express "typing conditions". For example, proving n + 0 = n requires proving that n is a number. When the semantics of TLA + allowed us to do so, we set up operators so that they return the expected "type"; for example, p ∧ q is guaranteed to be a Boolean value whatever its arguments p and q are. In other cases, typechecking is left to Isabelle's automatic proof methods; support for conditional rewrite rules in Isabelle's simplifier was essential to make this work.

Zenon

Zenon is a theorem prover for first-order logic with Hilbert's choice operator and equality. It is a proof-producing theorem prover: it outputs formal proof scripts for the theorems it proves. Zenon was extended with a backend that produces proofs in Isar syntax; these proofs use lemmas based on the Isabelle/TLA + object logic and are passed to Isabelle for verification. Zenon is therefore not part of the trusted code base of TLAPS.

Zenon had to be extended with deduction rules specific to TLA + : rules for reasoning about set-theoretic operators, for the case operator of TLA + , for set extensionality and function extensionality, for reasoning directly on bounded quantifiers (which is not needed in theory but is quite important for efficiency), and for reasoning about functions, strings, etc. Interestingly, Hilbert's choice operator was already used in Zenon for Skolemization, so we were easily able to support the choose operator of TLA + .

Future work includes adding rules to deal with tuples, sequences, records, and arithmetic, and improving the handling of equality. While there is some overlap between Zenon and Isabelle's automatic methods as they are instantiated in Isabelle/TLA + , in practice they have different strong points and there are many obligations where one succeeds while the other fails. Zenon uses Isabelle's automatic proof tactics for some of the elementary steps when it knows they will succeed, in effect using these tactics as high-level inference rules.

Other backends

The first release of TLAPS comes with some additional non-certifying backends. For arithmetic reasoning we have:

-An SMT-LIB based backend that can be linked to any SMT solver. Obligations are rewritten into the AUFLIRA theory of SMT-LIB, which generally requires omitting assumptions that lie outside this theory. This backend is needed for reasoning about real numbers. We have successfully used Yices, CVC3, Z3, veriT and Alt-Ergo in our examples. In future work we might specialize this generic backend for particular solvers that can reason about larger theories. -A Presburger arithmetic backend, for which we have implemented Cooper's algorithm. Our implementation is tailored to certain elements of TLA + that are not normally part of the Presburger fragment, but can be (conservatively) injected.

For both these backends, TLAPM performs a simple and highly conservative sort detection pass for bound identifiers. Both backends are currently non-certifying, but we plan to replace them with certifying backends in the future. In particular, we are integrating the proof-producing SMT solver veriT [START_REF] Bouton | veriT: An open, trustable and efficient SMT-solver[END_REF], with the goal of tailoring it for discharging TLA + proof obligations.

Proof development

Writing proofs is hard and error-prone. Before attempting to prove correctness of a TLA + specification, we first check finite instances with the TLC model checker [START_REF] Lamport | Specifying Systems[END_REF]. This usually catches numerous errors quickly -much more quickly than by trying to prove it correct. Only after TLC can find no more errors do we try to write a proof. The TLA + language supports a hierarchical, non-linear proof development process that we find indispensable for larger proofs [START_REF] Gafni | Disk Paxos[END_REF]. The highest-level proof steps are derived almost without thinking from the structure of the theorem to be proved. For example, a step of the form P 1 ∨ . . .∨ P n ⇒ Q is proved by the sequence of steps asserting P i ⇒ Q, for each i. When the user reaches a simple enough step, she first tries a fully automatic proof using a leaf directive citing the facts and definitions that appear relevant. If that fails, she begins a new level with a sequence of proof-less assertion steps that simplify the assertion, and a final qed step asserting that the goal follows from these steps. These new lower-level steps are tuned until the qed step is successfully verified. Then, the steps are proved in any order. (The user can ask TLAPM what steps have no proofs.) The most common reason that leaf proofs fail to verify is that the user has forgotten to use some fact or definition. When a proof fails, TLAPM prints the usable hypotheses and the goal, with usable definitions expanded. Examining this output often reveals the omission.

This kind of hierarchical development cries for a user interface that allows one to see what has been proved, hide irrelevant parts of the proof, and easily tell TLAPM what it should try to prove next. Eventually, these functions will be provided by the TLA + Toolbox. (It now performs only the hiding.) When TLAPS is integrated into the Toolbox, writing the specification, model-checking it, and writing a proof will be one seamless process. Meanwhile, we have written an Emacs mode that allows hierarchical viewing of proofs and choosing which parts to prove.

We expect most users to assume simple facts about data structures such as sequences rather than spending time proving them -especially at the beginning, before we have developed libraries of such facts for common data structures. Relying on unchecked assumptions would be a likely source of errors; it is easy to make a mistake when writing an "obviously true" assumption. Such assumptions should therefore be modelchecked with TLC.

Example developments

We have written a number of proofs, mainly to find bugs and see how well the prover works. Most of them are in the examples sub-directory of the TLAPS distribution. Here are the most noteworthy: -Peterson's Mutual Exclusion Algorithm. This is a standard shared memory mutual exclusion algorithm. The algorithm (in its 2-process version) is described in a dozen lines of PlusCal, an algorithm language that is automatically translated to TLA + . The proof of mutual exclusion is about 130 lines long. -The Bakery Algorithm with Atomic Reads and Writes. This is a more complicated standard mutual exclusion example; its proof (for the N-process version) is 800 lines long.

-Paxos. We have specified a high-level version of the well-known Paxos consensus algorithm as a trivial specification of consensus and two refinement steps-a total of 100 lines of TLA + . We have completed the proof of the first refinement and most of the proof of the second. The first refinement proof is 550 lines long; we estimate that the second will be somewhat over 1000 lines.

Tuning the back-end provers has made them more powerful, making proofs easier to write. While writing machine-checked proofs remains tiresome and more time consuming than we would like, it has not turned out to be difficult once the proof idea has been understood.

∆=

  x = 20 * y + 2, the reference O(3, 4)!2!1 resolves to the first subexpression of the second subexpression of O(3, 4), i.e., 20 * 4. Subexpressions can also be labelled and accessed via labelled references. For example, for O(x, y) ∆ = x = l::(y * 20) + 2, the reference O(3, 4)!l refers to 4 * 20 and will continue to refer to this expression even if the definition of O is later modified to O(x, y) ∆ = x = 7 * y 2 + l::(20 * y) + 2. TLAPM replaces all subexpression references with the expressions they resolve to prior to further processing.

Acknowledgements Georges Gonthier helped design the TLA + proof language. Jean-Baptiste Tristan wrote the (incomplete) Paxos proof.


Kaustuv Chaudhuri
email: kaustuv.chaudhuri@inria.fr

Classical and Intuitionistic Subexponential Logics are Equally Expressive

It is standard to regard the intuitionistic restriction of a classical logic as increasing the expressivity of the logic because the classical logic can be adequately represented in the intuitionistic logic by double-negation, while the other direction has no truth-preserving propositional encodings. We show here that subexponential logic, which is a family of substructural refinements of classical logic, each parametric over a preorder over the subexponential connectives, does not suffer from this asymmetry if the preorder is systematically modified as part of the encoding. Precisely, we show a bijection between synthetic (i.e., focused) partial sequent derivations modulo a given encoding. Particular instances of our encoding for particular subexponential preorders give rise to both known and novel adequacy theorems for substructural logics.

Introduction

In [START_REF] Miller | Finding unity in computational logic[END_REF], Miller writes: "While there is some recognition that logic is a unifying and universal discipline underlying computer science, it is far more accurate to say that its universal character has been badly fractured . . . one wonders if there is any sense to insisting that there is a core notion of 'logic'."

Possibly the oldest such split is along the classical/intuitionistic seam, and each side can be seen as more universal than the other. Classical logics, the domain of traditional mathematics, generally have an elegant symmetry in the connectives that can often be exploited to create sophisticated proof search and model checking algorithms. On the other hand, intuitionistic logics, which introduce an asymmetry between multiple hypotheses and single conclusions, can express the computational notion of function directly, making it the preferred choice for programming languages and logical frameworks. Can the rift between these two sides be bridged?

Miller proposes one approach: to use structural proof theory, particularly the proof theory of focused sequent calculi, as a unifying language for logical formalisms. There is an important proof theoretic difference between a given classical logic and its intuitionistic restriction (see defn. 8): the classical formulas can be encoded using the intuitionistic connectives in such a way that classical provability is preserved, i.e., a formula is classically provable if and only if its encoding is intuitionistically provable. In the other direction, however, there are no such general encodings. The classical logic will either have to be extended (for example, with terms and quantifiers) or refined with substructural or modal operators. For this reason, intuitionistic logics are sometimes considered to be more expressive than their classical counterparts.

In this paper, we compare logical calculi for "universality" using the specific technical apparatus of adequate propositional encodings. That is, given a formula in a source logic O, we must be able to encode it in a target logic M that must preserve the atomic predicates and must reuse the reasoning principles of M, particularly its notion of provability. An example of such an encoding would be ordinary classical logic encoded in ordinary intuitionistic logic where each classical formula A is encoded as the intuitionistic formula ¬¬A. We can go further and also reuse the proofs of the target calculus; in fact, there are at least the following levels of adequacy: Local adequacy is an ideal for encodings because it is a strong justification for seeing the target calculus as more universal: (partial) proofs in the source calculus can be recovered at any level of detail. However, it is unachievable except in trivial situations. Indeed, even adequacy is often difficult; for instance, the linear formula !a ⊸ !b ⊸ !a has three sequent proofs, differing in the order in which the second ⊸ and the two !s are introduced, but there is only a single sequent proof of a ⊃ b ⊃ a.

It is nevertheless possible to define a kind of local adequacy that is more flexible: adequacy up to permutations of inference rules entirely inside one of the phases of focusing. A focused proof [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF] is a proof that makes large synthetic rules that are maximal chains of positive or negative inference rules. An inference rule is positive, sometimes called synchronous, if it involves an essential choice, while it is negative or asynchronous if the choices it presents (if any) are inessential. The term "focus" describes the way positive inferences are chained to form synthetic steps: each inference is applied (read from conclusion to premises) to a single formula under focus, and the operands of this connective remain under focus in the premises.

Definition 2 (focal adequacy) An encoding of sequents from a source to a target focused calculus is focally adequate if they have the same synthetic inference rules.

Since focusing abstracts away the inessential permutations of inference rules, a focally adequate encoding can be used to compare logics for "essential universality". Surprisingly, there are very few known focal adequacy results (see [START_REF] Chaudhuri | The Focused Inverse Method for Linear Logic[END_REF][START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF] for practically all such known results). This paper fills in many of the gaps for existing (substructural) logics by proving a pair of general encodings (see theorems 12 and 17) about subexponential logics [START_REF] Danos | The structure of exponentials: Uncovering the dynamics of linear logic proofs[END_REF][START_REF] Nigam | Algorithmic specifications in linear logic with subexponentials[END_REF]. It is well known that the exponentials of linear logic are non-canonical. If a pre-order is imposed upon them with suitable conditions, then the resulting logic is well-behaved, satisfying identity, admitting cuts, and allowing focusing. Moreover, classical, intuitionistic, and linear logics can be seen as instances of subexponential logic for particular collections of subexponentials. Our encodings are generic, parametric on the subexponential signature of the source and target logics. As particular instances, we obtain focal adequacy results for: classical logic (CL) in intuitionistic logic (IL), IL in classical linear logic (CLL), CLL in intuitionistic linear logic (ILL), and an indefinite bidirectional chain between classical and intuitionistic subexponential logics, all of which are novel. Moreover, our encodings show that any analysis (such as cut-elimination) or algorithm (such as proof search) that is generic on the subexponential signature cannot (and need not) distinguish between classical and intuitionistic logics.

The rest of this paper is organized as follows: in sec. 2 classical subexponential logic is introduced, together with its focused sequent calculus and well known instances; in sec. 3 its intuitionistic restriction is presented; then in sec. 4 the bidirectional encoding between classical and intuitionistic subexponential logic is constructed. Details omitted here for space reasons can be found in the accompanying technical report [START_REF] Chaudhuri | Classical and intuitionistic subexponential logics are equally expressive[END_REF].

Classical subexponential logic

Subexponential logic borrows most of its syntax from linear logic [START_REF] Girard | Linear logic[END_REF]. As we are comparing focused systems, we adopt a polarised syntax from the beginning. Polarised formulas will have exactly one of two polarities: positive (P, Q, . . .) constructed out of the positive atoms and connectives, and negative (N, M, . . .) constructed out of the negative atoms and connectives. These two classes of formulas are mutually recursive, mediated by the indexed subexponential operators ! z and ? z . Notation 3 (syntax) Positive formulas (P, Q) and negative formulas (N, M) have the following grammar:

P, Q p P ⊗ Q 1 P ⊕ Q 0 ! z N + (positive) N, M n N & M ⊤ N M ⊥ P ⊸ N ? z P - (negative)
Atomic formulas are written in lower case (a, b, . . .), with p and q reserved for positive and n and m reserved for negative atomic formulas. P -denotes either a positive formula or a negative atom, and likewise N + denotes a negative formula or a positive atom. We write A, B, . . . for any arbitrary formula (positive or negative).

Because we will eventually consider its intuitionistic restriction, we retain implication ⊸ as a primitive even though it is classically definable. However, we exclude the nonlinear implication (⊃) because the unrestricted zones are non-canonical; i.e., there are many such implications, each defined using a suitable subexponential (or compositions thereof). The subscript z in exponential connectives denotes zones drawn from a subexponential signature (using the terminology of [START_REF] Nigam | Algorithmic specifications in linear logic with subexponentials[END_REF]).

Definition 4 A subexponential signature Σ is a structure Z, ≤, l, U where:

-Z, ≤ is a non-empty pre-ordered set (the "zones"); l ∈ Z is a "working" zone;

-U ⊆ Z is a set of unrestricted zones that is ≤-closed, i.e., for every z 1 , z 2 ∈ Z, if z 1 ≤ z 2 , then z 1 ∈ U implies z 2 ∈ U.
Z \ U will be called the restricted zones.

We use u, v, w to denote unrestricted zones and r, s, t to denote restricted zones.

Unrestricted zones admit both weakening and contraction, while restricted zones are linear. The logic is parametric on the signature. (Particular mentions of the signature will be omitted unless necessary to disambiguate, in which case they will be written in a subscript.) We use use a two-sided sequent calculus formulation of the logic in order to avoid appeals to De Morgan duality. This will not only simplify the definition of the intuitionistic restriction (sec. 3), but will also be crucial to the main adequacy result. Formulas in contexts are annotated with their subexponential zones as follows: z : A will stand for A occurring in zone denoted by z, and z : (A 1 , . . . , A k ) for z : A 1 , . . . , z : A k . Sequents are of the following kinds:

Γ

Notation 5

We write Γ u or ∆ u for those contexts containing only unrestricted elements, i.e., each element is of the form u : A with u ∈ U. Likewise, we write Γ r or ∆ r for contexts containing only restricted elements.

The rules of the calculus are presented in fig. 1. Focused sequent calculi presented in this style, which is a stylistic variant of Andreoli's original formulation [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF], have an intensional reading in terms of phases. At the boundaries of phases are sequents of the form Γ ; • ⊢ • ; ∆, which are known as neutral sequents. Proofs of neutral sequents proceed (reading from conclusion to premises) as follows:

1. Decision: a focus is selected from a neutral sequent, either from the left or the right context. This focused formula is moved to its corresponding focused zone using one of the rules rdr, udr, rdl and udl (u/r = "unrestricted"/"restricted", d = "decision", and r/l = "right"/"left"). These decision rules copy the focused formula iff it occurs in an unrestricted zone.

(right focus) of the focused formula. For binary rules, the restricted portions of the contexts are separated and distributed to the two premises. This much should be familiar from focusing for linear logic [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF][START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF].

Γ u , z : p ⊢ p ; ∆ u pr Γ u , Γ r 1 ⊢ [P] ; ∆ u , ∆ r 1 Γ u , Γ r 2 ⊢ [Q] ; ∆ u , ∆ r
The two unusual rules for subexponential logic are ! z r and ? z l, which are generalizations of rules for the single exponential in ordinary linear logic. These rules have a side condition that no formulas in a strictly ≤-smaller zone may be present in the conclusion. If the working zone l is ≤-minimal (which is not necessarily the case), then this side condition is trivial and the rules amount to a pure change of polarities, similar to the ↑ and ↓ connectives of polarised linear logic [START_REF] Laurent | Etude de la polarisation en logique[END_REF]. For the other zones, this rule tests for the emptiness of some of the zones. It is this selective emptiness test that gives subexponential logic its expressive power [START_REF] Nigam | Algorithmic specifications in linear logic with subexponentials[END_REF][START_REF] Nigam | Exploiting non-canonicity in the sequent calculus[END_REF].

3. Active phase: once the exponential rules ! z r and ? z l are applied, the sequents become active and left and right active rules are applied. The order of the active rules is immaterial as all orderings will produce the same list of neutral sequent premises. In Andreoli's system the irrelevant non-determinism in the order of these rules was removed by treating the active contexts Ξ and Ω as ordered contexts; however, we do not fix any particular ordering.

In the traditional model of focusing, the above three steps repeat, in that order, in the entire proof. The focused system can therefore be seen as a system of synthetic inference rules (sometimes known as bipoles) for neutral sequents. It is possible to give a very general presentation of such synthetic inference systems, for which we can prove completeness and cut-elimination in a very general fashion [START_REF] Chaudhuri | Focusing strategies in the sequent calculus of synthetic connectives[END_REF]. It is also possible, with some non-trivial effort, to show completeness of the focused calculus without appealing to synthetic rules [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF][START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF]. We do not delve into such proofs in this paper because this ground is well trodden. Indeed, a focused completeness theorem for a very similar (but more general) formulation of subexponential logic can be found in [14, chapter 6]. The synthetic soundness and completeness theorems are as follows, proof omitted: Fact 6 (synthetic soundness and completeness) Write for the sequent arrow for an unfocused variant of the calculus of fig. 1, obtained by placing the focused and active formulas in the l zone and relaxing the focusing discipline. 1

If

Γ ; • ⊢ • ; ∆, then Γ ∆ (synthetic soundness). 2. If Γ, l : Ω l : Ξ, ∆ then Γ ; Ω ⊢ Ξ ; ∆ (synthetic completeness). ⊓ ⊔
Despite its somewhat esoteric formulation, it is easy to see how subexponential logic generalizes classical substructural logics. -Polarised classical linear logic (CLL) is determined by ll = {l, u}, l ≤ u, l, {u} . In addition to the injections of mall, we also have the exponentials ! = ! u and ? = ? u . -Polarised classical logic (CL) is given by the signature l = {l}, •, l, {l} .

⊓ ⊔

In addition to such instances produced by instantiating the subexponential signature, it is also possible to get the unpolarised versions of these logics by applying ! l and ? l to immediate negative (resp. positive) subformulas of positive (resp. negative) formulas.

Intuitionistic subexponential logic

One direct way of defining intuitionistic fragments of classical logics is as follows: Definition 8 (intuitionistic restriction) Given a two-sided sequent calculus, its intuitionistic restriction is that fragment where all inference rules are constrained to have exactly a single formula on the right hand sides of sequents.

The practical import of this restriction is that the connectives and ⊥ disappear, because their right rules require two and zero conclusions, respectively. As a result, ⊸ becomes a primitive because its classical definition requires (and De Morgan duals, which are also missing with the intuitioistic restriction). In a slight break from tradition [9,16,2], we retain ? z in the intuitionistic syntax. The intuitionistic restriction produces the following kinds of sequents:

Γ ⊢ [P] right focus on P Γ ; [N] ⊢ z : Q - left focus on N Γ ; Ω ⊢ N + ; • active on Ω and N + Γ ; Ω ⊢ • ; z : Q -
active on Ω We shall use γ to stand for the right hand forms-either N + ; • or • ; z : Q --for active sequents above. The full collection of rules is given in fig. 2. As before, we use Q - (resp. N + ) to refer to a positive formula or negative atom (resp. negative formula or positive atom).

The nature of subexponential signatures does not change in moving from classical to intuitionistic logic. The decision rule udr obviously cannot copy the right formula in the intuitionistic case. Thus, both the right decision rules collapse; ? z takes on an additional modal aspect and is no longer the perfect dual of ! z . The standard explanation of this loss of symmetry in the exponentials is the creation of a new possibility judgement that is weaker than linear truth; see [START_REF] Chang | A judgmental analysis of linear logic[END_REF] for such a reconstruction of the intuitionistic ?.

The proof of completeness for focused intuitionistic subexponential logic has never been published. However, any similar proof for intuitionistic linear logic, such as [START_REF] Chaudhuri | A logical characterization of forward and backward chaining in the inverse method[END_REF][START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF], can be adapted. Again, we simply state the synthetic version of the theorems here without proof.

Fact 9 (synthetic soundness and completeness) Write for the sequent arrow for an unfocused variant of the calculus of fig. 2, obtained by placing the focused and active

formulas in the l zone and relaxing the focusing discipline.

If

Γ ; • ⊢ • ; z : Q -, then Γ z : Q -. (right focus) Γ u , z : p ⊢ p pr Γ u , Γ r (decision) Γ ⊢ [P] Γ ; • ⊢ • ; z : P dr Γ ; [N] ⊢ z : Q - Γ, r : N ; • ⊢ • ; z : Q -rdl Γ, u : N ; [N] ⊢ z : Q - Γ, u : N ; • ⊢ • ; z : Q -udl Fig. 2. Focused sequent calculus for intuitionstic subexponential logic 2. If Γ, l : Ω z : Q -then Γ ; Ω ⊢ • ; z : Q -. 3. If Γ, l : Ω l : N then Γ ; Ω ⊢ N ; •. ⊓ ⊔
The intuitionstic restrictions of the familiar instances from defn. 7 simply use the same subexponential signatures.

Focally adequate encodings

This section contains the main technical contribution of this paper: focally adequate encodings (defn. 2) that are generic on subexponential signatures. At the level of focal adequacy, therefore, the asymmetry in the expressive power of classical and intuitionistic logics disappears.

Classical in intuitionistic

To introduce the mechanisms of encoding, we first look at the unsurprising direction: a classical logic in its own intuitionistic restriction. The well known double negation translation, if performed clumsily, can break even full adequacy. For example, if N M is translated as

¬(! l ¬! l N ⊗ ! l ¬! l M)
where ¬P P ⊸ k where k is some fixed negative atom that is not used in classical logic. In the rule r under this encoding, there are instances of ! l that have no counterpart in the classical side. Indeed, there is no derived rule in the classical focused calculus that allows one to conclude Γ ;

• ⊢ N M ; • from Γ ; • ⊢ • ; ! l N, ! l M,
which is what would result if the active phase could be suspended arbitrarily and the subformula property were discarded. Such a rule is certainly admissible, but admissibile rules do not preserve bijections between proofs, and are only definable for full proofs in any case. How does one encode classical logic in its intuitionistic restriction such that polarities are respected? The above example suggests an obvious answer: when translating N M as if it were right-active, do not also translate the subformulas M and N as if they were right-active, for they will be sent to the left. Instead, translate them as if they were left-active. 2

Definition 10 (encoding classical formulas)

-The encoding (-) = from classical positive (resp. negative) formulas to intuitionistic positive (resp. negative) formulas is as follows:

(p) = = p (! z N) = = ! z (N) = (P ⊗ Q) = = (P) = ⊗ (Q) = (1) = = 1 (P ⊕ Q) = = (P) = ⊕ (Q) = (0) = = 0 (N) = = ¬ (N)
-The encoding (-) from classical negative (resp. positive) formulas to intuitionstic positive (resp. negative) formulas is as follows:

(n) = n ⊥ (? z P) = ! z (P) (N N) = (N) ⊗ (M) (⊥) = 1 (N & M) = (N) ⊕ (M) (⊤) = 0 (P ⊸ N) = (P) = ⊗ (N) (P) = ¬ (P) =
where for every negative atom n, there is a positive atom n ⊥ in the encoding.

This rule has no intuitionistic counterpart. Therefore, the encoding of ⊸ must prevent the right formula Q -from being sent to the left branch, i.e., to test that the rest of the right context in a right focus is empty. MALL itself cannot perform this test because it lacks any truly modal operators. Exactly the same problem exists for the encoding of IL in CL, which also lacks any true modal operators.

Quite obviously, the encoding of ⊸ requires some means of testing the emptiness of contexts. CLL (defn. 7) has an additional zone u that is greater than l, and therefore ! u can test for the absence of any l-formulas. It turns out that this is enough to get a focally adequate encoding of IL as follows: the sole zone l of IL is split into two, l r (restricted) and l u (unrestricted), and the right hand side of IL sequents is encoded with l r . Then, whenever P is of the form ! l N, the translation of it on the right is of the form ! l u M. In the rest of this subsection, we will systematically extend this observation to an arbitrary subexponential signature. Definition 14 (signature splitting) Let a subexponential signature Σ = Z, ≤, l, U be given. Write:

-Ẑ for the zone set (Z × {l}) ∪ (Z × {r}), where l and r are distinct labels for the left and the right of the sequents, respectively, and × is the Cartesian product. Z × {l} will be called the left form of Ẑ, and Z × {r} will be called its right form. -Û for the unrestricted zone set U × {l}.

-ˆl for the working zone (l, l).

-≤ for the smallest relation on Ẑ × Ẑ for which:

-(x, l) ≤ (y, l) if x ≤ y; -(x, r) ≤ (y, r) if x ≤ y; and -(x, r) ≤ (x, l) and (x, l) ˆ (x, r).

The subexponential signature Σ = Ẑ, ≤, ˆl, Û will be called the split form of Σ.

We intend to treat the right form specially. The zones in the right form are restricted, which encodes the linearity of the right hand side inherent in the intuitionistic restriction (defn. 8). Our encoding will guarantee that the right hand sides of sequents in the encoding contain no zones in the left form. Thus, when ! (z,l) N is under right focus, the side condition on the !r rule will ensure that there are no other formulas on the right hand side, because the right forms are made pointwise smaller than their left forms. Dually, on the left we shall use ? (z,r) to encode ? z ; since the right form zones are pointwise smaller than the left form zones, but retain the pre-split ordering inside their own zone, the side conditions enforce the same occurrences as in the source calculus.

Definition 15 (encoding intuitionistic contexts)

-The left-passive context Γ is encoded pointwise using the translation (-) lp :

z : N + lp = (z, l) : N + lp (p) lp = p (N) lp = (N) lf -A left-focused formula N is encoded using the translation (-) lf : (n) lf = n ? z P -lf = ? (z,r) P -la (N & M) lf = (N) lf & (M) lf (⊤) lf = ⊤ (P ⊸ N) lf = (P) rf ⊸ (N) lf
-A right-focused formula P is encoded using the translation (-) rf :

(p) rf = p ! z N + rf = ! (z,l) N + ra (P ⊗ Q) rf = (P) rf ⊗ (Q) rf (1) rf = 1 (P ⊕ Q) rf = (P) rf ⊕ (Q) rf (0) rf = 0
-A left-active context Ω is encoded pointwise using the translation (-) la :

(a) la = ! (l,l) a ! z N + la = ! (z,l) N + lp (P ⊗ Q) la = (P) la ⊗ (Q) la (1) la = 1 The cases for (! z N + ) rf and (? z P -) lf will be crucial for the proof of thm. 17. Most of the remaining cases can be seen as an abstract interpretation of the focused rules (fig. 2) on the various contexts. The definition of the encoding of intuitionistic sequents is now completely systematic.

(P ⊕ Q) la = (P) la ⊕ (Q) la (

Definition 16 (encoding intuitionistic sequents)

The encoding -?! of intuitionistic sequents as classical sequents is as follows:

Γ ⊢ [P] ?! = (Γ) lp ⊢ (P) rf ; • Γ ; [N] ⊢ z : Q -?! = (Γ) lp ; (N) lf ⊢ z : Q -rp Γ ; Ω ⊢ N + ; • ?! = (Γ) lp ; (Ξ) la ⊢ N + ra ; • Γ ; Ω ⊢ • ; z : Q -?! = (Γ) lp ; (Ξ) la ⊢ • ; z : Q -rp
Observe that the right hand sides of the encoding have the intuitionistic restriction (defn. 8). This restriction will be enforced at every transtion from a focused to an active phase, which is enough because the active rules cannot increase the size of the right contexts.

Theorem 17 The encoding of defn. 16 is focally adequate (defn. 2).

Proof. As before for thm. 12, we shall prove this by inventorying the intuitionistic rules of fig. 2, encode the conclusions of each of these rules, and observe whether the neutral premises of the derived inference rules are in bijection with those of the fig. 2. All but the following important cases are omitted here for space reasons. 4-cases of i/pr and i/! z r :

(Γ u ) lp , z : p ⊢ p c/pr (Γ u ) lp , (z : p) lp ⊢ (p) rf Γ u , z : p ⊢ p ?! Γ ; • ⊢ N + ; • ?! (Γ) lp ; • ⊢ (N + ) la ; • (Γ) lp ⊢ ! (z,l) (N + ) la ; • c/!r (Γ) lp ⊢ (! z N + ) rf ; • Γ ⊢ ! z N + ?!
The boxed instance of c/!r is valid because all the zoned formulas in (Γ) lp are in the left form zones, as is the zone of the ! itself, so the comparison ≤ is the same as ≤ on the intuitionistic zones (defn. 14).

The boxed instance of c/⊸l contains the only split of the right context that can succeed in the same focused phase, i.e., reach an initial sequent or a phase transition, becaue that (P) rf eventually produces either a positive atom (which must finish the proof with c/pr and since right form zones are restricted (z : Q -) rp cannot be present) or a ! (z,l) which guarantees that the rest of the right context is empty. -cases of i/? z l and dr :

Γ ; P -⊢ • ; y : Q -?! (Γ) lp ; (P -) la ⊢ • ; (y : Q -) rp (Γ) lp ; ? (z,r) (P -) la ⊢ (y : Q -) rp c/?l (Γ) lp ; (? z P -) lf ⊢ (y : Q -) rp Γ ; ? z P -⊢ y : Q -?! Γ ⊢ [P] (Γ) lp ⊢ (P) rf ; • (Γ) lp ; • ⊢ • ; (z, r) : (P) rf c/rdr (Γ) lp ; • ⊢ • ; (z : P) rp Γ ; • ⊢ • ; z : P ?!
The boxed instance of c/?l is justified because the subscript zone (z, r) is of the right form (in order to compare with (y, r)) which is ≤-smaller than its corresponding left-form zone (defn. [START_REF] Nigam | Exploiting non-canonicity in the sequent calculus[END_REF]. Note that it is crucial for soundness to have (z, r) not be smaller than all left form zones. Since right form zones are restricted, there is no copying in the boxed instance of c/rdr. The other decision cases are similar.

⊓ ⊔

We note one important direct corollary of thm. 17.

Corollary 18 (intuitionistic logic in classical linear logic)

There is a focally adequate encoding of intuitiontistic logic in classical linear logic.

It is well known [START_REF] Girard | Linear logic[END_REF] that (classical) linear logic can encode the intuitionistic implication ⊃ as follows: A ⊃ B !A ⊸ B. However, this encoding is only globally adequate [START_REF] Schellinx | Some syntactical observations on linear logic[END_REF]. It is possible to refine this encoding to obtain a fully adequate encoding [START_REF] Liang | A unified sequent calculus for focused proofs[END_REF] in an enriched classical linear logic which is not apparently an instance of classical subexponential logic. Corollary 18 further improves our undertanding of encodings of intuitionistic implicication by permuting ! into the antecedent of the implication until there is a phase change, which removes the bureaucratic polarity switch inherent in this implication. 5Proof (of cor. 18). The split of the signature l (defn. 7) is isomorphic to the signature ll, so apply thm. 17. ⊓ ⊔

Conclusions

Section 4 shows that any given classical (resp. intuitionistic) subexponential logic can be encoded in a related intuitionistic (resp. classical) subexponential logic such that partial synthetic derivations are preserved. This is a technical result, with at least one of the directions of encoding being novel. It strongly suggests that one of the fractures in logic identified by Miller in [START_REF] Miller | Finding unity in computational logic[END_REF]-the classical/intuitionistic divide-might be healed by analyses and algorithms that are generic on subexponential signatures. One might still favour "classical" or "intuitionistic" dialects for proofs, but neither format is more fundamental. The results of this paper have two caveats. First, we only consider the "restricted" or the "unrestricted" flavours of subexponentials; in [START_REF] Danos | The structure of exponentials: Uncovering the dynamics of linear logic proofs[END_REF] there were also subexponentials of the "strict" and "affine" flavours for which our results here do not extend directly. Second, we do not consider encodings involving non-propositional kinds, such as terms or frames. Subexponentials are still useful for such stronger encodings, but representational adequacy may not be as straightforward.

  ⊢ [P] ; ∆ right focus on P Γ ; [N] ⊢ ∆ left focus on N Γ ; Ω ⊢ Ξ ; ∆ active on Ω and Ξ The contexts in these sequents have the following restrictions: -All elements of the left passive context Γ are of the form z : N + . -All elements of the right passive context ∆ are of the form z : P -. -All elements of the left active context Ω are of the form P -. -All elements of the right active context Ξ are of the form N + .

Fig. 1 .

 1 Fig. 1. Focused sequent calculus for classical subexponential logic

Fact 7 (-

 7 familiar instances) Polarised classical multiplicative additive linear logic (MALL) is determined by mall = {l}, •, l, ∅ . The injections between the two polarised classes, sometimes known as shifts, are as follows: ↓= ! l and ↑= ? l .

0) la = 0 -

 0 A right-active formula N + is encoded using the translation (-) ra :(a) ra = ! (l,r) a ? z P -ra = ? (z,r) P -rp (N & M) ra = (N) ra & (M) ra (⊤) ra = ⊤ (P ⊸ N) ra = (P) la ⊸ (N) ra-A right-passive zoned formula z : P -is encoded using the translation (-) rp : z : P -rp = (z, r) : P -rp (n) rp = n (P) rp = (P) rf

Focused phase: for a left or a right focused sequent, left or right focus rules are applied to the formula under focus. These focused rules are all non-invertible in the (unfocused) sequent calculus and therefore depend on essential choices made in the proof. In all cases except ! z r and ? z l the focus persists to the subformulas (if any)

Γ u , Γ r 1 , Γ r 2 ⊢ [P ⊗ Q] ; ∆ u , ∆ r 1 , ∆ r 2 ⊗r Γ u ⊢ [1] ; ∆ u 1r Γ ⊢ [P i ] ; ∆ Γ ⊢ [P 1 ⊕ P 2 ] ; ∆ ⊕r i Γ ; • ⊢ N + ; ∆ ∀x : A ∈ Γ, ∆. z ≤ x Γ ⊢ ! z N + ; ∆ ! z r (left focus) Γ u ; [n] ⊢ ∆ u , z : n nl Γ ; [P i ] ⊢ ∆ Γ ; [P 1 & P 2 ] ⊢ ∆ &l i Γ u , Γ r 1 ; [N] ⊢ ∆ u , ∆ r 1 Γ u , Γ r 2 ; [M] ⊢ ∆ u , ∆ r 2 Γ u , Γ r 1 , Γ r 2 ; [N M] ⊢ ∆ u , ∆ r 1 , ∆ r 2 l Γ u ; [⊥] ⊢ ∆ u ⊥l Γ u , Γ r 1 ⊢ [P] ; ∆ u , ∆ r1

Γ u , Γ r 1 , Γ r 2 ; [P ⊸ M] ⊢ ∆ u , ∆ r 1 , ∆ r 2 ⊸l Γ ; P -⊢ • ; ∆ ∀x : A ∈ Γ, ∆. z ≤ x Γ ; ? z P -⊢ ∆ ? z l (right active) Γ ; Ω ⊢ Ξ ; ∆, l : a Γ ; Ω ⊢ Ξ, a ; ∆ ar Γ ; Ω ⊢ Ξ, N ; ∆ Γ ; Ω ⊢ Ξ, M ; ∆ Γ ; Ω ⊢ Ξ, N & M ; ∆ &r Γ ; Ω ⊢ Ξ, ⊤ ; ∆ ⊤r Γ ; Ω ⊢ Ξ, N, M ; ∆ Γ ; Ω ⊢ Ξ, N M ; ∆ r Γ ; Ω ⊢ Ξ ; ∆ Γ ; Ω ⊢ Ξ, ⊥ ; ∆ ⊥r Γ ; Ω, P ⊢ Ξ, N ; ∆ Γ ; Ω ⊢ Ξ, P ⊸ N ; ∆ ⊸r Γ ; Ω ⊢ Ξ ; ∆, z : P - Γ ; Ω ⊢ Ξ, ? z P -; ∆ ? z r (left active) Γ, l : a ; Ω ⊢ Ξ ; ∆ Γ ; Ω, a ⊢ Ξ ; ∆ al Γ ; Ω, P, Q ⊢ Ξ ; ∆ Γ ; Ω, P ⊗ Q ⊢ Ξ ; ∆ ⊗l Γ ; Ω ⊢ Ξ ; ∆ Γ ; Ω, 1 ⊢ Ξ ; ∆ 1l Γ ; Ω, P ⊢ Ξ ; ∆ Γ ; Ω, Q ⊢ Ξ ; ∆ Γ ; Ω, P ⊕ Q ⊢ Ξ ; ∆ ⊕l Γ ; Ω, 0 ⊢ Ξ ; ∆ 0l Γ, z : N + ; Ω ⊢ Ξ ; ∆ Γ ; Ω, ! z N + ⊢ Ξ ; ∆ ! z l(decision) Γ ⊢ [P] ; ∆ Γ ; • ⊢ • ; ∆, r : P rdr Γ ⊢ [P] ; ∆, u : P Γ ; • ⊢ • ; ∆, u : P udr Γ ; [N] ⊢ ∆ Γ, r : N ; • ⊢ • ; ∆ rdl Γ, u : N ; [N] ⊢ ∆ Γ, u : N ; • ⊢ • ; ∆ udl

This is basically Gentzen's LK in two-sided form for subexponential logic.

⊢ [P] Γ u , Γ r

⊢ [Q] Γ u , Γ r 1 , Γ r 2 ⊢ [P ⊗ Q] ⊗r Γ u ⊢ [1] 1r Γ ⊢ [P i ] Γ ⊢ [P 1 ⊕ P 2 ] ⊕r i Γ ; • ⊢ N + ; • ∀x : A ∈ Γ. z ≤ x Γ ⊢ ! z N + ! z r (left focus) Γ u ; [n] ⊢ z : n nl Γ ; [P i ] ⊢ z : Q - Γ ; [P 1 & P 2 ] ⊢ z : Q -&l i Γ u , Γ r 1 ⊢ [P] Γ u , Γ r 2 ; [M] ⊢ z : Q - Γ u , Γ r 1 , Γ r 2 ; [P ⊸ M] ⊢ z : Q -⊸l Γ ; P -⊢ • ; y : Q - ∀x : A ∈ Γ, y : Q -. z ≤ x Γ ; ? z P -⊢ y : Q - ? z l right active Γ ; Ω ⊢ • ; l : a Γ ; Ω ⊢ a ; • ar Γ ; Ω ⊢ N ; • Γ ; Ω ⊢ M ; • Γ ; Ω ⊢ N & M ; • &r Γ ; Ω ⊢ ⊤ ; • ⊤r Γ ; Ω, P ⊢ N ; • Γ ; Ω ⊢ P ⊸ N ; • ⊸r Γ ; Ω ⊢ • ; z : P Γ ; Ω ⊢ ? z P ; • ? z r (left active) Γ, l : a ; Ω ⊢ γ Γ ; Ω, a ⊢ γ al Γ ; Ω, P, Q ⊢ γ Γ ; Ω, P ⊗ Q ⊢ γ ⊗l Γ ; Ω ⊢ γ Γ ; Ω, 1 ⊢ γ 1l Γ ; Ω, P ⊢ γ Γ ; Ω, Q ⊢ γ Γ ; Ω, P ⊕ Q ⊢ γ ⊕l Γ ; Ω, 0 ⊢ γ 0l Γ, z : N ; Ω ⊢ γ Γ ; Ω, ! z N ⊢ γ ! z l

adequately encode the classical logic itself. This is not the case in the other direction without further modifications to the subexponential signature. It is easy to see this: consider just the MALL fragment and the problem of encoding the i/⊸l rule. If ⊸ is encoded as itself, then in the classical side we have the following derived rule (all the zones are l, and elided):Γ ⊢ [P] ; Q -Γ ; [N] ⊢ • Γ ; [P ⊸ N] ⊢ Q -

See[START_REF] Chaudhuri | Classical and intuitionistic subexponential logics are equally expressive[END_REF].

Note that the polarised intuitionistic implication P ⊸ N, if encoded using Girard's encoding, would be !↑P ⊸ N, which breaks the polarisation of the antecedent.

Contexts are translated element-wise.

Definition 11 (encoding classical sequents)

The encoding (-) ⊥⊥ of classical sequents as intuitionistic sequents is as follows: In other words, focused sequents are translated to right-focused sequents, and active sequents to left-active sequents. The right contexts are dualised and sent to the left where the intuitionistic restriction does not apply, while the left focus on negative formulas is turned into a right focus because of the lack of a multiplicative left-focused rule (except ⊸l which would cause an inadvertent polarity switch).

Theorem 12

The encoding of defn. 11 is focally adequate (defn. 2).

Proof. We will inventory the classical rules in fig. 1, and in each case compute the intuitionistic synthetic derivations of the encoding of the conclusion of the classical rules. Here are the interesting 3 cases, with the double inference lines denoting (un)folding of defns. 10 and 11, and the rule names written with the prefix c/ or i/ to distinguish between classical and intuitionistic respectively.

-cases of c/pr and c/!r :

All the logical rules used are invertible. The boxed instance of i/? l r requires some explanation: obviously a left active rule on (N) can be applied before this rule. However, since they are both active rules, the choice of which to perform first is immaterial as they will produce the same neutral premises. If we want local-not focal-adequacy, we will have to impose a right-to-left ordering on the active rules. The case of c/nl and c/?l is similar. -case of c/ r :

The cases of c/⊥r, c/! z l and c/? z r are similar.

3 See [START_REF] Chaudhuri | Classical and intuitionistic subexponential logics are equally expressive[END_REF] for the remaining cases.

-case of c/rdr :

Note that the right premise is forced to terminate in the same phase. This would not be possible if, instead of k, we were to use some other negative formula such as ? l 0. In the presence of some unrestricted subexponential u, we might have used ? u 0 instead (note that, classically, ? u 0 ≡ ⊥).

⊓ ⊔

Corollary 13

-There is a focally adequate encoding of classical MALL in intuitionistic MALL.

-There is a focally adequate encoding of CLL in ILL.

-There is a focally adequate encoding of CL in IL.

Proof. Instantiate thm. 12 on the subexponential signatures from defn. 7.

⊓ ⊔

These instances are all apparently novel, partly because focal adequacy of classical logics in their own intuitionistic restrictions has not been deeply investigated. In the work on LJF [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF] there is a focally adequate encoding of classical logic in intuitionistic linear logic, which can be seen as a combination of the second and third of the above instances.

Intuitionistic in classical

The previous subsection showed that the intuitionistic restriction of a classical logic can


A Youssef
email: ahmed.youssef@apc.univ-paris7.fr

Infrared behavior and gauge artifacts in de Sitter spacetime I. The photon field

We study the infrared (long distance) behavior of the free photon field in de Sitter spacetime. Using a two-parameter family of gauge fixing terms, we show that the infrared (IR) behavior of the two-point function is highly gauge-dependent and ranges from vanishing to growing. This situation is in disagreement with its counterpart in flat spacetime, where the two-point function vanishes in the IR for any choice of the gauge fixing parameters. A criterion to isolate the "physical" part of the two-point function is given and is shown to lead to a well-behaved two-point function in the IR.

INTRODUCTION

The study of quantum field theory in the de Sitter background is of paramount importance to the understanding of the early universe as well as its present accelerated expansion. One of the most striking, yet poorly understood, aspects of de Sitter QFT is the so called infrared problem. The simplest and most serious manifestation of this problem being the non-vanishing of the correlation functions for largely -spacelike and timelike -separated points. This is for instance a well-known fact for the massless minimally coupled (mmc) scalar and the graviton fields. In this letter we study the IR behavior of the photon field in de Sitter space and show that it exhibits similar IR pathologies. More importantly we are able to show that these are purely gauge artifacts.

The organization of the letter is as follows. First we compute the correlation function using the R λ gauges λ(∇ a A a ) 2 /2. Then we generalize the computation to the larger family of higher derivative gauge fixing terms λ(∇ a A a ) 2 /2 + ξR 2 (∇ a A a ) (∇ a A a )/2. Finally we propose a decomposition of the two-point function into a physical and a gauge part and we show that the physical part is vanishing in the IR.

The d-dimensional de Sitter spacetime X d of "radius" R can be identified with the real one-sheeted hyperboloid in the d + 1 Minkowski spacetime M d+1

X d = x ∈ R d+1 , η µν x µ x ν = R 2
where η µν is the "mostly plus" flat metric diag(-1, +1, • • • , +1). Let µ(x, x ′ ) denote the geodesic distance between the points x and x ′ and g ab be the d-dimensional de Sitter (or d-dimensional Minkowski if R → ∞) metric. We will compute the Wightman two-point function W aa ′ (x, x ′ ) = Ω|A(x)A(x ′ )|Ω in different gauges. In the previous formula |Ω designates the Euclidean (Bunch-Davies) vacuum state. This vacuum being de Sitter invariant, W aa ′ (x, x ′ ) is a maximally symmetric bi-tensor. As shown in detail in [START_REF] Allen | Vector Two-Point Functions in Maximally Symmetric Spaces[END_REF], all such bi-tensors can be expressed in terms of the parallel propagator g aa ′ (x, x ′ ) between x and x ′ , and the two vectors n a = ∇ a µ and n a ′ = ∇ a ′ µ. Our two-point function is thus written as

W aa ′ (x, x ′ ) = α 1 (µ)g aa ′ + α 2 (µ)n a n a ′
where, for spacelike separations (µ 2 > 0), α 1 and α 2 are scalar functions of the geodesic distance µ only. We will frequently use the following formulas [START_REF] Allen | Vector Two-Point Functions in Maximally Symmetric Spaces[END_REF]:

g b ′ a n b ′ = -n a ′ , g ab = g c ′ a g c ′ b ∇ a n b = A(g ab -n a n b ), ∇ a n b ′ = C(g ab ′ + n a n b ′ ) ∇ a g bc ′ = -(A + C)(g ab n c ′ + g ac ′ n b )
where

A = cot(µ/R) R , and C = - csc(µ/R) R .
It is also useful to introduce the quantity z given for spacelike separations (µ 2 > 0 or 0 < z < 1) by

z = cos 2 µ 2R . (1)
All of our calculations are performed in the spacelike region 0 < z < 1. They can be extended further by analytic continuation in the z variable to the cut complex plane C \ (1, ∞). Finally, the Feynman propagator

G F aa ′ = i Ω|T A a (x)A a ′ (x ′
)|Ω , can be obtained as the limiting value of W aa ′ when approaching the branch cut z > 1 from above.

We end our introduction by noting that several, quite interesting, recent works (see [START_REF] Polyakov | De Sitter space and Eternity[END_REF] among many others) were devoted to the study of infrared effects in de Sitter. In these articles however, only massive (although interacting) fields are considered. IR pathologies are of course much stronger for massless fields and they appear already at the linear level.

THE R λ GAUGES

The gauge fixed action describing the massless vector field A a is

S λ = d 4 x √ -g 1 4 F ab F ab + λ 2 (∇ a A a ) 2 (2)
where

F ab = ∇ a A b -∇ b A a .
The resulting equation of motion is D ab A b = 0 where

D ab = g ab - (d -1) R 2 g ab + (λ -1)∇ a ∇ b . (3)
Flat space. In flat space (R → ∞), the Fourier transform of the Feynman propagator reads

G F aa ′ (k) = 1 k 2 -iǫ g aa ′ + 1 -λ λ 1 (k 2 -iǫ) 2 k a k a ′ .
Using the (massless limit) of the scalar Feynman propagator (given, as always, for spacelike separations)

G F (x, x ′ ) = d 4 k (2π) 4 e ik(x-x ′ ) k 2 + m 2 -iǫ = im (2π) 2 K 1 (mµ) µ (4)
(where K is the modified Bessel function of the second kind) and its derivatives with respect to x and x ′ we get the coordinate-space two-point function

W aa ′ = λ + 1 8π 2 λµ 2 g aa ′ - λ -1 4π 2 λµ 2 n a n a ′ . (5)
For all values of λ, this expression vanishes for large timelike and spacelike separations as expected.

De Sitter space. Following [START_REF] Allen | Vector Two-Point Functions in Maximally Symmetric Spaces[END_REF], we write the twopoint function in de Sitter space as

W [λ] aa ′ (x, x ′ ) = α [λ] 1 (z) g aa ′ + α [λ] 2 (z) n a n a ′ . ( 6
)
where α 1 , α 2 are scalar functions of the invariant quantity z defined in [START_REF] Strocchi | Selected topics on the general properties of quantum field theory[END_REF]. The equation of motion D ab W b a ′ = 0 implies two independent equations on α 1 and α 2 . These equations are most easily solved in the Feynman gauge λ = 1 and the result is found in [START_REF] Allen | Vector Two-Point Functions in Maximally Symmetric Spaces[END_REF] to be

α [λ=1] 1 (z) = 1 48π 2 R 2 3 1 -z + 1 z + 2 z + 1 z 2 ln(1 -z) α [λ=1] 2 (z) = 1 24π 2 R 2 1 - 1 z + 1 z - 1 z 2 ln(1 -z)
Instead of vanishing for largely separated points, the correlation goes to a non-zero constant function

lim z→∞ W [λ=1] aa ′ (x, x ′ ) = 1 24π 2 R 2 n a n a ′ . (7)
This constant vanishes in the flat spacetime limit (R → ∞) as expected. The non-vanishing of the correlator in de Sitter space seems to contradict our experience with the more familiar flat space QFT. It is indeed a general result of the latter, sometimes referred to as the cluster decomposition principle [START_REF] Strocchi | Selected topics on the general properties of quantum field theory[END_REF], that the correlation functions must decay in the IR. To our knowledge, only very special QFT models, e.g confinement models like the massless scalar in two-dimensional flat space, seem to escape this result.

As explained in the introduction, it turns out that this IR pathological behavior of the photon field is typical of de Sitter massless fields. The most notable examples are the mmc scalar and the graviton fields. The correlation functions of these fields exhibit even stronger pathologies as they grow in the IR (see for instance [START_REF] Bros | Scalar tachyons in the de Sitter universe[END_REF][START_REF] Starobinsky | Spectrum of relict gravitational radiation and the early state of the universe[END_REF][START_REF] Antoniadis | Graviton fluctuations in de Sitter space[END_REF][START_REF] Higuchi | The covariant graviton propagator in de Sitter spacetime[END_REF]).

This "IR problem" is at the heart of an open discussion in the community. It led some authors [START_REF] Antoniadis | Cosmological dark energy: prospects for a dynamical theory[END_REF] to speak of a "striking violation of cluster decomposition properties of the de Sitter invariant vacuum state". It has also been shown that this growing of the graviton two-point function render scattering amplitudes divergent [START_REF] Floratos | Tree-level scatering amplitudes in de Sitter space diverge[END_REF]. As a consequence, the authors of [START_REF] Antoniadis | Cosmological dark energy: prospects for a dynamical theory[END_REF], among many others, suspect a quantum instability of de Sitter space, meaning that the de Sitter geometry is not a stable ground state of quantum gravity with a cosmological constant.

Other workers in the field, mainly motivated by the fact that the correlations of some gauge invariant quantities fall-off in the IR limit, claim that the non-vanishing of the two-point functions in the IR is nothing but a gauge artifact. For instance, the electromagnetic field correlation function is well-behaved in the IR [START_REF] Allen | Vector Two-Point Functions in Maximally Symmetric Spaces[END_REF]:

F ab F a ′ b ′ = 1 8π 2 R 4 1 (1 -z) 2 g [a ′ [a g b ′ ] b] + 4 n [a g [b ′ b] n a ′ ] .
The same is true for the graviton field as there is no growing terms in the correlation function of the Riemann tensor

R abcd (x)R a ′ b ′ c ′ d ′ (x ′ ) .
In the following we will study in detail the IR problem in the case of the photon field in de Sitter. The IR behavior of this field received considerably less attention in the literature than its counterpart for the mmc and the graviton field. This is certainly due to the importance of these two-fields in inflation theory. It is also probably due to the fact that in actual QED calculations, the non vanishing term [START_REF] Antoniadis | Graviton fluctuations in de Sitter space[END_REF] will not contribute to scattering processes (see last section). This model will however prove to be precious in realizing that -at least for some situations -serious IR pathologies in de Sitter space arewithout doubt -gauge artifacts.

The equation of motion (3) applied to the two-point function [START_REF] Antoniadis | Cosmological dark energy: prospects for a dynamical theory[END_REF] leads after some algebra to a coupled system of differential equations. Hereafter we will only need one of these equations, namely:

H 1, d -2, 1 2 + 1 -λ 2 α 1 + λ -1 2 α ′ 2 + λ -λ d λ d -1 α 1 z + 1 2 1 1 -z - 1 z α 2 = 0 ( 8
)
where the prime denote derivation with respect to the variable z,

λ d = d -3 d -1
and H is the hypergeometric operator defined by

H[a, b, c] = z(1 -z) d 2 dz 2 + [c -(a + b + 1)z] d dz -ab
Another, moreover first order, relation between α 1 and α 2 is obtained by considering the two-point function of the field strength

F ab F a ′ b ′ = β 1 g [a ′ [a g b ′ ] b] + β 2 n [a g [b ′ b] n a ′ ] .
In fact, the equation of motion (in vacuum) ∇ a F ab = 0 implies the relation [START_REF] Allen | Vector Two-Point Functions in Maximally Symmetric Spaces[END_REF]

α 2 = z 8π 2 R 2 (z -1) + 2(1 -z) (zα ′ 1 + α 1 ) (9)
We now specialize our results to the d = 4 case for simplicity. The general solution in the Euclidean vacuum is found to be

α [λ] 1 (z) = 1 48π 2 R 2 λ 3(λ + 1) 2(1 -z) + 3λ -1 2z + (3λ -1) 1 z + 1 2z 2 ln(1 -z) α [λ] 2 (z) = 1 24π 2 R 2 λ 1 - 3(λ -1) 2(1 -z) - 3λ -1 2z + (3λ -1) 1 2z - 1 2z 2 ln(1 -z)
and the IR behavior is given by

lim z→±∞ W [λ] aa ′ (x, x ′ ) = 1 24π 2 R 2 λ n a n a ′ . (10)
This result means that one can cure any IR bad behavior by going to the Landau gauge λ → ∞. More importantly, we see that the IR behavior of the correlation function is pure gauge, thus asking whether or not the two-point function is well or ill-behaved in the IR is in itself -at least partially-a misleading question. Finally we note that there exists a special choice of the gauge fixing parameter, namely λ = 1 3 (more generally λ d in d dimensions), that cancels logarithmic terms and gives a particularly simple two-point function. We note, perhaps as a curiosity for the time being, that for large dimensions d, λ d goes to the Feynman gauge λ = 1, which is the simplest gauge in flat space.

MORE PATHOLOGICAL GAUGES

We now consider a larger family of gauge fixing terms. Our motivation is that the IR pathology we exhibited in the last section, namely that the correlation function tends to a constant, might seem -I believe mistakenlymild enough not to worry about. We will show that in this more general gauge, the two-point function is actually growing in the IR, exactly like the mmc scalar or the graviton fields. We consider the action

S λ,ξ = S λ + ξ 2m 2 d 4 x √ -g(∇ a A a ) (∇ a A a ) (11)
where we have added a higher derivative gauge fixing term. Similar higher derivative gauge fixing are occasionally used in QCD and the electro-weak theories. They were also used to study flat space perturbative quantum gravity [START_REF] Antoniadis | Gauge invariance in quantum gravity[END_REF]. We note that if we want λ and ξ to be dimensionless, such higher derivative gauge fixing terms require the introduction of a mass quantity m . In flat space m is introduced by hand, while in de Sitter space the inverse of the de Sitter radius plays naturally this role:

m 2 = 1 R 2 .
This observation renders the introduction of higher derivative gauge fixing somehow more natural in the de Sitter case. The equation of motion reads

g ab + (λ -1)∇ a ∇ b + ξ m 2 ∇ a ∇ b A b = 0 (12)
Flat space. The flat space Feynman propagator is found in Fourier space to be

GF aa ′ (k) = g aa ′ k 2 -iǫ + 1 -λ λ (k 2 -iǫ) 2 + ξ m 2 λ 2 1 k 2 -iǫ - 1 k 2 -m 2 λ ξ -iǫ k a k a ′
The reader will note the relative negative sign typical of higher derivative theories in front of the last propagator. Using (4) and its derivatives the coordinate-space twopoint function is then found to be

W aa ′ = 1 2π 2 m 2 λµ 4 ν 2 + 1 2π 2 m 2 λµ 4 ν 2 + K 2 (imµν) 4π 2 λµ 2 g aa ′ + 2 π 2 m 2 λµ 4 ν 2 + 1 -λ 4π 2 λµ 2 + K 0 (imµν) π 2 λµ 2 +i mν 4π 2 λµ - 2 π 2 mλµ 3 ν K 1 (imµν) n a n a ′
where we have introduced the quantity ν = (λ/ξ) 1/2 . For all values of λ and ν, this expression vanishes for large timelike and spacelike separations as expected. The short distance singularity is given by

W aa ′ ∼ 1 8π 2 µ 2 (g aa ′ -2n a n a ′ ) .
We emphasize that the short distance singularity of the two theories (2) and [START_REF] Martin-Garcia | xAct, Efficient Tensor Computer Algebra[END_REF] are different. This is due to the non commutation of the limits ξ → 0 and µ → 0.

De Sitter space. We now consider the action (11) in de Sitter space and thus set 1/m 2 = R 2 . Following the same methods described above we obtain the following equations on α 1 :

α (4) 1 = 4(τ -2)(τ + 3) (z -1) 2 z 2 α 1 + 3(2z -1) τ 2 + τ -16 (z -1) 2 z 2 α ′ 1 - 12 -(z -1)z(τ -8)(τ + 9) (z -1) 2 z 2 α ′′ 1 -8 1 z + 1 z -1 α ′′′ 1
where we introduced the parameter τ

= √ 4λ+9ξ- √ ξ 2 √ ξ
. Obtaining this equation requires some elaborate algebraic manipulations. The calculations in this section were thus verified with the tensor algebra system xAct on Mathematica [START_REF] Martin-Garcia | xAct, Efficient Tensor Computer Algebra[END_REF]. This equation can be solved in closed form. Using the asymptotic formulas in table I the solution verifying: i)regularity at z = 0 and ii)flat space short distance singularity is found. For non integer values of τ it reads

α [λ,τ ] 1 (z) = 2Q 2 τ (2z -1) -π cot(πτ )P 2 τ (2z -1) 32π 2 R 2 λ (z -1)z (τ 2 + τ -2) + 3λ -1 96π 2 R 2 λ (2z + 1) ln(1 -z) z 2 + 1 z + 1 32π 2 R 2 λ(τ -1)(τ + 2) 1 (z -1) 2 - (λ + 1)τ (τ + 1) -2λ z -1
where P and Q are Legendre functions of the first and second kind respectively. As before, α 2 is obtained by [START_REF] Antoniadis | Gauge invariance in quantum gravity[END_REF]. The asymptotic behavior in the IR is given by (τ > 1):

α [λ,τ ] 1 (z) ∼ - 2 2τ -5 cot(πτ )Γ τ + 1 2 π 3/2 R 2 λ(τ + 2)Γ(τ ) z τ -2 α [λ,τ ] 2 (z) ∼ 2 4τ -1 (τ -1)τ cot(πτ )Γ τ + 3 2 Γ τ + 5 2 π 2 R 2 λ(2τ + 3) (2τ 2 + 5τ + 2) Γ(2τ + 2) z τ -1
Thus for τ > 2 for instance, the two-point function grows like z τ -2 in the IR. This strong IR growing is purely a gauge artifact since, as proven in the beginning of this letter, no IR pathologies arise in the Landau gauge.

z → 0 z → 1 z → ∞ P (2) τ (2z -1) - sin(πτ ) πz Γ(τ + 3) 2 Γ(τ -1) (z -1) 2 2τ Γ(τ + 1/2) √ π Γ(τ -1) z τ Q (2) τ (2z -1) - cos(πτ ) 2z 1 2(z -1) √ π Γ(τ + 3) 2 2(τ +1) Γ(τ + 3/2) 1 z τ +1

A PHYSICAL DECOMPOSITION

The previously described situation, namely that the IR behavior of the two-point function in de Sitter space contains important gauge artifacts makes it natural to look for a decomposition of the two-point function into a physical and a non-physical parts. We show now that such a decomposition exists and is given by the following rewriting of the two-point function

W [λ] aa ′ (x, x ′ ) = g aa ′ β 1 (z) + ∇ a ∇ a ′ β 2 (z). (13)
In fact, most of the physics is included in the "quantum" action W J defined by

exp i W J = D[A a ] exp i S + d 4 x √ -g A a J a
where J a is an external conserved current ∇ a J a = 0. The tree-level expression of the effective action is given by

W J = dV x dV x ′ J a (x)W aa ′ (x, x ′ )J a ′ (x ′ )
where dV x = d 4 x -g(x) is the invariant volume element. Since the current J a is conserved, integration by parts ensures that only β 1 will contribute to W J and it thus fully deserves to be referred to as the "physical" two-point function. An explicit form of the functions β 1 and β 2 can be found by solving the system

α 1 = β 1 + 1 2R 2 β ′ 2 , R 2 α 2 = (1 -z)β ′ 2 + z(1 -z)β ′′ 2 .
The solutions are unique if one requires regularity near z = 0 and we obtain

W Phys aa ′ (x, x ′ ) = 1 16π 2 R 2 1 1 -z + ln(1 -z) z g aa ′ (14)
It is a remarkable (and expected) fact that W Phys aa ′ is (λ, ξ) independent and is well behaved in the IR. In flat spacetime, the Feynman gauge (λ = 1, ξ = 0) gives precisely this physical two-point function. The situation in de Sitter is quite different and no choice of the gauge fixing parameters gives the physical two-point function. A natural question is wether a more general gauge fixing term gives directly W Phys aa ′ (x, x ′ ) in de Sitter space.

OUTLOOK

We showed that the IR pathological behavior of the photon's two-point function is nothing but a gauge artifact. We suggest that the situation is similar for the graviton field. The IR behavior of the latter is however necessarily more intricate since it has been shown that the (transverse-traceless) growing term of the two-point function does not cancel out from scattering amplitudes [START_REF] Antoniadis | Graviton fluctuations in de Sitter space[END_REF][START_REF] Floratos | Tree-level scatering amplitudes in de Sitter space diverge[END_REF]. This implies in particular that a decomposition like (14) does not lead to a well-behaved "physical" twopoint function. The IR behavior of the graviton field will be examined in [START_REF] Youssef | Infrared behavior and gauge artifacts in the de Sitter universe II. The graviton field[END_REF].

TABLE I .

 I Asymptotics of the Legendre functions near singular points.

ACKNOWLEDGMENTS

It is a pleasure to thank J.P Gazeau, A. Higuchi, K. Meissner, U. Moschella, E. Mottola, A.M. Polyakov and A. Starobinsky for stimulating discussions about de Sitter quantum field theory.