Aloïs Brunel
email: alois.brunel@ens-lyon.org

Olivier Hermant
email: olivier.hermant@isep.fr

Clément Houtmann
email: clement.houtmann@inria.fr

Orthogonality and Boolean Algebras for Deduction Modulo

Originating from automated theorem proving, deduction modulo removes computational arguments from proofs by interleaving rewriting with the deduction process. From a proof-theoretic point of view, deduction modulo defines a generic notion of cut that applies to any first-order theory presented as a rewrite system. In such a setting, one can prove cut-elimination theorems that apply to many theories, provided they verify some generic criterion. Pre-Heyting algebras are a generalization of Heyting algebras which are used by Dowek to provide a semantic intuitionistic criterion called superconsistency for generic cutelimination. This paper uses pre-Boolean algebras (generalizing Boolean algebras) and biorthogonality to prove a generic cut-elimination theorem for the classical sequent calculus modulo. It gives this way a novel application of reducibility candidates techniques, avoiding the use of proofterms and simplifying the arguments.

Introduction

In the usual models of predicate logic (Boolean algebras, Heyting algebras, Kripke models), the interpretations of logically equivalent formulae are always equal. In particular, valid formulae are all interpreted by one unique truth value representing truthness. This is adequate for the study of purely logical systems but insufficient for the study of deduction modulo [START_REF] Dowek | Theorem proving modulo[END_REF]: indeed, in order to remove irrelevant computational arguments from proofs, deduction modulo interleaves rewriting with the deduction process and therefore defines a computational equivalence which is usually strictly weaker than logical equivalence and that appeals to a distinction at the semantical level too. For example, Euclid's algorithm can be specified in deduction modulo: in particular when a < b and b mod a = 0, the gcd of a and b is equal to the gcd of (b mod a) and a. Propositions "2 is the gcd of 4 and 6" and "2 is the gcd of 2 and 4" are then computationally and logically equivalent (because 2 = 6 mod 4). These two propositions are also logically equivalent to Fermat's Last Theorem (all of them are valid), but they are not computationally equivalent to it. Indeed reducing this theorem to a trivial assertion such as "2 is the gcd of 4 and 6" involves proving the theorem. Such a proof hardly qualifies as a computation.

Introduced by Dowek [START_REF] Dowek | Truth values algebras and proof normalization[END_REF], pre-Heyting algebras are a generalization of Heyting algebras which take into account such a distinction between computational and logical equivalences. Interestingly, they provide a semantic intuitionistic criterion called superconsistency for generic cut-elimination in deduction modulo. A theory is superconsistent if it has an interpretation in any pre-Heyting algebra. Since reducibility candidates in deduction modulo [START_REF] Dowek | Proof normalization modulo[END_REF] are a remarkable example of a pre-Heyting algebra, any superconsistent theory can be interpreted in this algebra and consequently verifies the generic notion of cut-elimination provided by deduction modulo. Therefore pre-Heyting algebras are adequate for deduction modulo in intuitionistic logic.

In this paper, we propose a similar notion of model for deduction modulo in classical logic that we call pre-Boolean algebras. We show that these models lead to a classical version of superconsistency which implies cut-elimination in classical sequent calculus modulo. Our approach significantly differs on two points from the original use of reducibility candidates in deduction modulo [START_REF] Dowek | Proof normalization modulo[END_REF]. First, we do not use original Girard's reducibility candidates [START_REF] Girard | Interprétation Fonctionnelle et Élimination des Coupures de l'Arithmétique dOrdre Supérieur[END_REF] or Tait's saturated sets [START_REF] Tait | A realizability interpretation of the theory of species[END_REF], but rather orthogonality which easily adapts to classical sequent calculi: This technique has first been introduced to prove strong normalization of linear logic [START_REF] Girard | Linear logic[END_REF] and has since been used many times for various linear logic fragments [START_REF] Okada | Phase semantic cut-elimination and normalization proofs of firstand higher-order linear logic[END_REF][START_REF] Gimenez | Calculer et Raisonner avec les Réseaux de la Logique Linéaire[END_REF] but also for the classical version of system F ω [START_REF] Lengrand | Classical F [omega], orthogonality and symmetric candidates[END_REF] and is the basis of Krivine's classical realizability [START_REF] Krivine | Realizability in classical logic[END_REF]. Second, we only prove cut-elimination instead of normalization, hence our proof is considerably simplified. Our technique is related to the proofs of cut-elimination for linear logic that use phase semantics [START_REF] Okada | A uniform semantic proof for cut-elimination and completeness of various first and higher order logics[END_REF][START_REF] Abrusci | Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic[END_REF][START_REF] Ciabattoni | Towards a semantic characterization of cutelimination[END_REF], but whereas those cut-elimination models can be seen as projections of typed reducibility candidates models [START_REF] Okada | Phase semantic cut-elimination and normalization proofs of firstand higher-order linear logic[END_REF], ours is crucially designed in a untyped fashion: superconsistency forecloses the degree of freedom to choose the interpretation of atomic formulae, and the truth values must be forced to contain all the axioms, in order to be able to conclude.

This paper is organized as follows: Deduction modulo, impersonated by a classical sequent calculus, is presented in Section 2. In Section 3, we define pre-Boolean algebras, our generalization of Boolean algebra which acknowledge the distinction between computational and logical equivalences. Section 4 introduces orthogonality for classical deduction modulo using sets of pointed sequents, which allows us to construct a pre-Boolean algebra of sequents and prove adequacy (i.e. cut-elimination) in Section 5. Finally in Section 6, we extract a non-trivial Boolean algebra from the pre-Boolean algebra of sequents presented in Section 5.

Classical sequent calculus modulo

We suppose given a signature containing a set of variables (x, y, z . . . ), a set of function symbols and a set of predicate symbols. Each function symbol and each predicate symbol has a fixed arity. Terms (t, u, v . . . ) and atomic formulae (a, b, c . . . ) are constructed as usual. Formulae (A, B, C . . . ) are constructed from atomic formulae, negated atomic formulae (ā, b, c . . . ), conjunctions (∧), disjunctions (∨), universal quantification (∀) and existential quantification (∃).

A, B

::= a | ā | ⊤ | ⊥ | A ∧ B | A ∨ B | ∀x.A | ∃x.A
Negation is the involutive function (.) ⊥ recursively defined as

a ⊥ = ā ⊥ ⊥ = ⊤ (A ∧ B) ⊥ = A ⊥ ∨ B ⊥ (∀x.A) ⊥ = ∃x.A ⊥ ā⊥ = a ⊤ ⊥ = ⊥ (A ∨ B) ⊥ = A ⊥ ∧ B ⊥ (∃x.A) ⊥ = ∀x.A ⊥
Capture avoiding substitutions are denoted [t/x]. Sequents are finite multisets of formulae (denoted ⊢ A 1 , A 2 . . . ). If ≡ is a congruence relation on formulae, the (one-sided) sequent calculus LK modulo ≡ is described in Figure 1.

⊢ A, A ⊥ (Axiom) ⊢ A, ∆1 ⊢ A ⊥ , ∆2 ⊢ ∆1, ∆2 (Cut) ⊢ A, ∆ A ≡ B ⊢ B, ∆ (Conv) ⊢ A, A, ∆ ⊢ A, ∆ (Contr) ⊢ ∆ ⊢ A, ∆ (Weak) ⊢ ⊤ (⊤) (no rule for ⊥) ⊢ A, ∆1 ⊢ B, ∆2 ⊢ A ∧ B, ∆1, ∆2 (∧) ⊢ A, B, ∆ ⊢ A ∨ B, ∆ (∨) ⊢ A[t/x], ∆ ⊢ ∃x.A, ∆ (∃) ⊢ A, ∆ x fresh in ∆ ⊢ ∀x.A, ∆ (

A generalized semantics

This section introduces a generalization of Boolean algebras based on the same idea as the extension from Heyting algebras to pre-Heyting algebras (also known as Truth Values Algebras) [START_REF] Dowek | Truth values algebras and proof normalization[END_REF]: in order to make a distinction between computational and logical equivalences, the antisymmetry condition on the order is released, imposing therefore similar but weaker conditions than having distributed complemented lattice. The definition given here is stricter than the one given by Dowek in his course notes [START_REF] Dowek | Fondements des systèmes de preuve[END_REF] since we force the negation operator to be involutive. Of course, when the pre-order becomes an order, both notions boil down to Boolean algebras. 3. ⊤ (resp. ⊥) is a greatest (resp. lowest) element:

a ≤ ⊤ ⊥ ≤ a 4. ∨ is distributive over ∧ and ∧ is distributive over ∨: a ∨ (b ∧ c) ≤ (a ∨ b) ∧ (a ∨ c) and (a ∨ b) ∧ (a ∨ c) ≤ a ∨ (b ∧ c) a ∧ (b ∨ c) ≤ (a ∧ b) ∨ (a ∧ c) and (a ∧ b) ∨ (a ∧ c) ≤ a ∧ (b ∨ c)
5. a ⊥ is a complement of a: a ∧ a ⊥ ≤ ⊥ and ⊤ ≤ a ∨ a ⊥ . 6. (.) ⊥ is idempotent: a ⊥⊥ = a.

For any S ⊆ B, ∀S denotes one of its greatest lower bounds when it exists. ∃S denotes one of the lowest upper bounds of S when it exists. A pre-Boolean algebra is said complete when greatest lower bounds and lowest upper bounds exist for any arbitrary S ⊆ B.

The first points 1-3 correspond to the definition of a bounded lattice adapted to a pre-order. Point 4 imposes the lattice to be distributive and point 5 to be complemented. Points 1-5 are exactly equivalent to the pre-Boolean algebra definition of [START_REF] Dowek | Fondements des systèmes de preuve[END_REF], by defining, as usual, a ⇒ b as a ⊥ ∨ b (conversely, by defining a ⊥ to be a ⇒ ⊥). In addition, we impose the idempotency to the negation operator (.) ⊥ (point 6). Any pre-Boolean algebra whose pre-order is actually a (partial) order is a Boolean algebra. Let us also remark that the quotient set of any pre-Boolean algebra by the equivalence relation induced by the pre-order (≥ ∩ ≤) is a Boolean algebra.

Interpretations in pre-Boolean algebras are defined as usual.

Definition 2 (Interpretation). Let B, ≤, ⊤, ⊥, ∧, ∨, (.) ⊥ , ∀, ∃ be a pre-Boolean algebra and (.) * be a function from n-ary atomic predicates to functions in M n → B and from n-ary function symbols to functions in M n → M , for some chosen domain M . Let φ be a valuation assigning to each variable a value in M . If C is a formula and t is a term, then their respective interpretations C * φ and t * φ are defined inductively as:

f (t 1 , . . . , t n ) * φ = f * ((t 1 ) * φ , . . . , (t n ) * φ ) x * φ = φ(x) P (t 1 , . . . , t n ) * φ = P * ((t 1 ) * φ , . . . , (t n ) * φ ) (for n-ary predicates) (⊤) * = ⊤ (A ∧ B) * φ = A * φ ∧ B * φ (∀x.A) * φ = ∀{ (A) * φ+(d/x) | d ∈ M } (⊥) * = ⊥ (A ∨ B) * φ = A * φ ∨ B * φ (∃x.A) * φ = ((∀x.(A ⊥ )) * φ ) ⊥ where φ + (d/x
) is the valuation assigning d to x and φ(y) to any y = x.

Lemma 1 (Substitution). For any formula A, terms t and u, and valuation φ, (u

[t/x]) * φ = u * φ+(t * φ /x) and (A[t/x]) * φ = A * φ+(t * φ /x) .
Proof. By structural induction on u (resp. A).

Definition 3 (Model interpretation). Let ≡ be a congruence on terms and formulae. An interpretation (.) * is said to be a model interpretation for ≡ if and only if for any valuation φ, any terms t ≡ u and formulae

A ≡ B, t * φ = u * φ and A * φ = B * φ .
The usual definition of consistency states that a theory is consistent if it can be interpreted in a model. In particular, a congruence ≡ is consistent if there exists a model interpretation (.) * for ≡ in some model, i.e. in some pre-Boolean algebra. Such a definition is strengthened to define superconsistency [START_REF] Dowek | Truth values algebras and proof normalization[END_REF] as follows.

Definition 4 (Superconsistency). A congruence ≡ is superconsistent if for all pre-Boolean algebra D, an interpretation can be found for ≡ in D.

Behaviours

We dedicate the following sections to a proof that superconsistency is a criterion which entails cut-elimination in our one-sided classical sequent calculus: if ≡ is superconsistent, then cut-elimination holds in LK modulo ≡. To establish such a cut-elimination result, we use orthogonality to design a pre-Boolean algebra of pointed sequents and demonstrate adequacy which in turn implies cut-elimination. The technique used here to prove cut-elimination significantly differs from Dowek and Werner's approach [START_REF] Dowek | Proof normalization modulo[END_REF], mainly by the use of orthogonality instead of reducibility candidates. Another minor difference is that we do not prove strong normalization but cut-elimination (i.e. admissibility of the Cut rule). However the philosophy remains: in the process of proving cut-elimination, we demonstrate that a pre-Boolean algebra is constructed. Therefore we finally obtain a superconsistency criterion, based on our definition of pre-Boolean algebra, for cut-elimination in our classical sequent calculus modulo.

The notion of orthogonality that we will use in Section 5 relies on sets of pointed sequents. These are usual sequents where one formula is distinguished.

Definition 5 (Pointed Sequents). We define pointed sequents as sequents of the form ⊢ ∆ where at most one formula A of ∆ is distinguished. We denote this formula by A • . The set of pointed sequents is the set of sequents of the form ⊢ A • , ∆ and is noted P • . The set of usual sequents is the set of sequents of the form ⊢ ∆ with no distinguished formula and is noted P . Pointed sequents are represented by letters t, u, s . . . Moreover, the subset of P • which contains exactly all the sequents whose distinguished formula is A is denoted by P

• (A). If X ⊆ P • we pose X(A) = X ∩ P • (A).
Pointed sequents are meant to interact through cuts, and therefore define orthogonality.

Definition 6 (Cut). If t = (⊢ A • , ∆ 1 ) and u = (⊢ B • , ∆ 2 ) are pointed sequents with B ≡ A ⊥ , then the sequent t ⋆ u is defined by t ⋆ u = (⊢ ∆ 1 , ∆ 2 ). Obviously t ⋆ u ∈ P . Notice that if B ≡ A ⊥ , t ⋆ u is undefined.
We denote by Ax the set of all axioms, that is the sequents ⊢ A ⊥ , A for every A. Ax • is the set of pointed axioms.

Definition 7 (Orthogonal). In what follows, we pose

⊥ ⊥ = { ⊢ ∆ | ⊢ ∆ has a cut-free proof in LK modulo ≡ } .
We will write ⊥ ⊥ • for the set of pointed sequents which have a cut-free proof. If X ⊆ P • , then we define the orthogonal of X as

X ⊥ = B { u ∈ P • (B) | ∀t ∈ X(C) with B ≡ C ⊥ , t ⋆ u ∈ ⊥ ⊥ }
Lemma 2. The usual properties on orthogonality hold:

X ⊆ X ⊥⊥ , X ⊆ Y implies Y ⊥ ⊆ X ⊥ , X ⊥⊥⊥ = X ⊥ .
Definition 8 (Behaviour). A set of sequents X is said to be a behaviour when X ⊥⊥ = X.

Lemma 3. Behaviours are always stable by conversion through ≡.

Proof. Let us prove first that any orthogonal X ⊥ is stable by conversion:

if (⊢ A • , ∆) ∈ X ⊥ and A ≡ B, then (⊢ B • , ∆) ∈ X ⊥ . Let us assume that (⊢ C • , ∆ ′ ) ∈ X with C ≡ B ⊥ . Then C ≡ A ⊥ (since B ⊥ ≡ A ⊥ ) and since (⊢ A • , ∆) ∈ X ⊥ ,
there exists a cut-free proof of ⊢ ∆, ∆ ′ . We just proved that (⊢ B • , ∆) ∈ X ⊥ . Now, any behaviour X = X ⊥⊥ is the orthogonal of X ⊥ and therefore is stable by conversion through ≡.

⊓ ⊔ Lemma 4. The set of behaviours is closed under unrestricted intersection.

Proof. If S is a set of behaviours, then we show that

X∈S X ⊥⊥ ⊆ X∈S X .
Let us take an element t ∈ ( S) ⊥⊥ . Let X be an element of S. Let u ∈ X ⊥ . Because S ⊆ X, we have X ⊥ ⊆ ( S) ⊥ . Hence u ∈ ( S) ⊥ and so t ⋆ u ∈ ⊥ ⊥. That means t ∈ X ⊥⊥ , but X is a behaviour, so t ∈ X. This is true for every X ∈ S so finally t ∈ X∈S X. ⊓ ⊔ Definition 9 (Behaviours Operations). if X and Y are behaviours and S is a set of behaviours, then X ∧ Y and ∀S are respectively defined as

X ∧ Y = ((X.Y ) ∪ Ax • ) ⊥⊥ where X.Y is { ⊢ (A ∧ B) • , ∆ A , ∆ B | (⊢ A • , ∆ A ) ∈ X and (⊢ B • , ∆ B ) ∈ Y } and ∀S = ({ ⊢ (∀xA) • , ∆ | for any t ∈ T , X ∈ S, (⊢ (A[t/x]) • , ∆) ∈ X } ∪ Ax • ) ⊥⊥
where T is the set of open terms of the language.

By definition and by Lemma 2, X ⊥ , X ∧ Y and ∀S are always behaviours.

The pre-Boolean algebra of sequents

The next step towards cut-elimination is the construction of a pre-Boolean algebra whose elements are behaviours. The base set of our algebra is

D = { X | Ax • ⊆ X ⊆ ⊥ ⊥ • and X = X ⊥⊥ }
Let us construct a pre-Boolean algebra from D using operators (.) ⊥ , ∧ and ∀.

Lemma 5. If S ⊆ D then S is the greatest lower bound of S in D (for the inclusion order ⊆).

Proof. Since the base set D is closed under unrestricted intersection (Lemma 4),

S ∈ D. Now if C ∈ D is a lower bound of S, then C ⊆ S.
Hence S is the greatest lower bound of S in D.

⊓ ⊔ Lemma 6. For all X ∈ D, X ⊥ ∈ D.

Proof. Let us notice that (Ax

• ) ⊥ = ⊥ ⊥ • . Then Ax • ⊆ X ⊆ ⊥ ⊥ • (since X ∈ D) and Lemma 2 imply Ax • ⊆ (Ax • ) ⊥⊥ = (⊥ ⊥ • ) ⊥ ⊆ X ⊥ ⊆ (Ax • ) ⊥ = ⊥ ⊥ • . ⊓ ⊔ Lemma 7. If X, Y ∈ D, then for every C, (⊢ (C ⊥ ) • , C) ∈ (X.Y ∪ Ax • ) ⊥ .
Proof. We prove equivalently that for all

(⊢ C • , ∆) ∈ (X.Y ∪ Ax • ), the sequent ((⊢ (C ⊥ ) • , C) ⋆ (⊢ C • , ∆)) = (⊢ C, ∆) has a cut-free proof.
- -X ∧ Y is a behaviour by definition.

If (⊢ C • , ∆) ∈ Ax • , then ∆ = C ⊥ . Therefore (⊢ (C ⊥ ) • , C) ⋆ (⊢ C ⊥ , C • ) = (⊢ C ⊥ , C) has obviously a cut-free proof. -If (⊢ C • , ∆) ∈ X.Y , then C = A ∧ B, ∆ = ∆ 1 ,
-

Ax • ⊆ X ∧ Y since Ax • ⊆ (X.Y ∪ Ax • ) ⊆ (X.Y ∪ Ax • ) ⊥⊥ = X ∧ Y . -Now, let us prove that X ∧ Y ⊆ ⊥ ⊥ • . We take (⊢ C • , ∆) ∈ X ∧ Y and we
show that it has a cut-free proof. First, we can notice that (⊢ (

C ⊥ ) • , C) ∈ (X.Y ∪ Ax • ) ⊥ (Lemma 7). Hence, (⊢ C • , ∆) ⋆ (⊢ (C ⊥ ) • , C) = (⊢ C, ∆) ∈ ⊥ ⊥ and so (⊢ C, ∆) has a cut-free proof: (⊢ C • , ∆) ∈ ⊥ ⊥ • .
Finally let us prove stability under ∀: let us assume that S is a subset of D and prove that ∀S ∈ D.

-∀S is a behaviour by definition.

-The definition of ∀S shows that it is the biorthogonal

X ⊥⊥ of a set X containing Ax • . Therefore Ax • ⊆ X ⊆ X ⊥⊥ = ∀S. -Finally to prove ∀S ⊆ ⊥ ⊥ • , it suffices to show that ({ ⊢ (∀xA) • , ∆ | for any t ∈ T , X ∈ S, (⊢ (A[t/x]) • , ∆) ∈ X } ∪ Ax • ) ⊆ ⊥ ⊥ • because ⊥ ⊥ • is a behaviour. Ax • ⊆ ⊥ ⊥ •
obviously. Now, we assume that for any t ∈ T and any X ∈ S, (⊢ (D[t/x]) • , Γ ) ∈ X. Let us prove that (⊢ (∀x.D) • , Γ ) ∈ ⊥ ⊥ • . It suffices to take a fresh variable y ∈ T : then (⊢ (D[y/x] • , Γ )) is cut-free and by the ∀ rule, we obtain that (⊢ ∀x.D, Γ ) is cut-free too.

⊓ ⊔ Theorem 2. The structure D, ≤, ⊤, ⊥, ∧, ∨, (.) ⊥ , ∀, ∃ , where

-≤ be the trivial pre-order on D, -⊤ is ⊥ ⊥ • and ⊥ is ⊥ ⊥ •⊥ ,
the operators ∧, (.) ⊥ , ∀ are those defined in Definition 9 and 7 -and the operators ∨ and ∃ are the respective boolean dual of ∧ and

∀, i.e. X ∨ Y = (X ⊥ ∧ Y ⊥ ) ⊥ and ∃S = (∀S ⊥ ) ⊥ where S ⊥ = { X ⊥ | X ∈ S },
is a pre-Boolean algebra.

Proof. Since we chose a trivial pre-order, there is nothing to check but the stability of D under all the operators, that holds by the above lemmata.

⊓ ⊔

Finally we can state our main result.

Theorem 3 (Adequacy). Let ≡ be a congruence on terms and formulae and (.) * be a model interpretation for ≡ in D. Let ⊢ C 1 , ..., C k be a provable sequent in LK modulo ≡, let σ be a substitution whose domain does not contain any bounded variable in C 1 , ..., C k , φ be a valuation and let

(⊢ (σC ⊥ 1 ) • , ∆ 1 ) ∈ ((C 1 ) * φ ) ⊥ , . . . , (⊢ (σC ⊥ k ) • , ∆ k ) ∈ ((C k ) * φ ) ⊥ . Then ⊢ ∆ 1 , ..., ∆ k ∈ ⊥ ⊥. Proof.
The proof is done by induction on the last rule of the proof of ⊢ C 1 , . . . , C k .

Axiom For simplicity we suppose that the axiom is performed on

C 1 and C 2 = C ⊥ 1 . Therefore (C 2 ) * φ = ((C 1 ) * φ ) ⊥ and since (⊢ (σC ⊥ 1 ) • , ∆ 1 ) ∈ ((C 1 ) * φ ) ⊥ = (C 2 ) * φ and (⊢ (σC ⊥ 2 ) • , ∆ 2 ) ∈ ((C 2 ) * φ ) ⊥ , then ⊢ ∆ 1 , ∆ 2 ∈ ⊥ ⊥. By weakening, ⊢ ∆ 1 , . . . , ∆ k ∈ ⊥ ⊥.
Conjunction For simplicity we assume that the derivation is

⊢ A 1 , C 2 , . . . , C k ⊢ A 2 , C k+1 , . . . , C n (∧) ⊢ A 1 ∧ A 2 C1 , C 2 , . . . , C k , C k+1 , . . . , C n Let us assume (⊢ (σC ⊥ i ) • , ∆ i ) ∈ ((C i ) * φ ) ⊥ for all i > 1. By induction hypoth- esis, ⊢ σA • 1 , ∆ 2 , . . . , ∆ k is in ((A 1 ) * φ ) ⊥⊥ = (A 1 ) * φ and ⊢ σA • 2 , ∆ k+1 , . . . , ∆ n is in ((A 2 ) * φ ) ⊥⊥ = (A 2 ) * φ . Therefore ⊢ σC • 1 , ∆ 2 , . . . , ∆ n is in (A 1 ) * φ .(A 2 ) * φ ⊆ ((A 1 ) * φ .(A 2 ) * φ ) ⊥⊥ ⊆ ((A 1 ) * φ .(A 2 ) * φ ∪ Ax • ) ⊥⊥ = (C 1 ) * φ = ((C 1 ) * φ ) ⊥⊥ . Then ⊢ ∆ 1 , . . . , ∆ n ∈ ⊥ ⊥.
Disjunction For simplicity we assume that the derivation is

⊢ A 1 , A 2 , C 2 , . . . , C k (∨) ⊢ A 1 ∨ A 2 C1 , C 2 , . . . , C k Let us assume that (⊢ (σC ⊥ i ) • , ∆ i ) is in ((C i ) * φ )
⊥ for all i > 1 and let us prove that for all (⊢ (σC ⊥ 1 )

• , ∆ 1 ) ∈ ((C 1 ) * φ ) ⊥ , the sequent ⊢ ∆ 1 , . . . , ∆ k is in ⊥ ⊥. It is equivalent to prove that ⊢ σC • 1 , ∆ 2 , . . . , ∆ k is in ((C 1 ) * φ ) ⊥⊥ = ((A 1 ) * φ ∨ (A 2 ) * φ ) ⊥⊥ = (((A 1 ) * φ ) ⊥ ∧ ((A 2 ) * φ ) ⊥ ) ⊥⊥⊥ = (((A 1 ) * φ ) ⊥ ∧ ((A 2 ) * φ ) ⊥ ) ⊥ = (((A 1 ) * φ ) ⊥ .((A 2 ) * φ ) ⊥ ∪ Ax • ) ⊥⊥⊥ = (((A 1 ) * φ ) ⊥ .((A 2 ) * φ ) ⊥ ∪ Ax • ) ⊥
or equivalently to prove that for all sequent (⊢ (σC ⊥ 1 )

• , ∆ 1 ) in the set ((A 1 ) * φ ) ⊥ .((A 2 ) * φ ) ⊥ ∪ Ax • , the sequent ⊢ ∆ 1 , . . . , ∆ k is in ⊥ ⊥. -if (⊢ (σC ⊥ 1 ) • , ∆ 1 ) ∈ Ax • , then ∆ 1 = σC 1 . Since ⊢ (σA ⊥ 1 ) • , σA 1 and ⊢ (σA ⊥ 2 ) • , σA 2 are respectively in ((A 1 ) * φ ) ⊥ and ((A 2 ) * φ ) ⊥ , then by in- duction hypothesis, ⊢ σA 1 , σA 2 , ∆ 2 , . . . , ∆ k ∈ ⊥ ⊥ . Using (∨ R ), ⊢ A 1 ∨ A 2 , ∆ 2 , . . . , ∆ k = ⊢ ∆ 1 , . . . , ∆ k ∈ ⊥ ⊥ . -if (⊢ (σC ⊥ 1 ) • , ∆ 1 ) ∈ ((A 1 ) * φ ) ⊥ .((A 2 ) * φ ) ⊥ , then there exist sequents with ⊢ (σA ⊥ 1 ) • , ∆ a and ⊢ (σA ⊥ 2 ) • , ∆ b respectively in ((A 1 ) * φ ) ⊥ and ((A 2 ) * φ ) ⊥ such that ∆ 1 is ∆ a , ∆ b . Then by induction hypothesis, ⊢ ∆ a , ∆ b , ∆ 2 , . . . , ∆ k = ⊢ ∆ 1 , ∆ 2 , . . . , ∆ k ∈ ⊥ ⊥ .
Universal quantifier For simplicity we assume that the derivation is

⊢ A, C 2 , . . . , C k x is fresh in each C i (∀) ⊢ ∀x.A C1 , C 2 , . . . , C k Let us assume that (⊢ (σC ⊥ i ) • , ∆ i ) is in ((C i ) * φ ) ⊥ for all i > 1 and that the sequent (⊢ ((σ∀x.A) ⊥ ) • , Γ ) is in ((∀xA) * φ ) ⊥ . We now want to prove that the sequent (⊢ ∆ 2 , . . . , ∆ k , Γ ) is in ⊥ ⊥. It is sufficient to prove that the sequent (⊢ ∆ 2 , . . . , ∆ k , (σ(∀x.A)) • ) is in (∀x.A) * Φ .
By noticing that σ only substitutes variables that are free in ∀x.A, we get that σ(∀x.A) = ∀x.(σA). It remains to prove that if t ∈ T and d ∈ M , then (⊢ (σA

[t/x]) • , Γ ) ∈ (A * φ+[d/x] ). But, because x is fresh in C i , (⊢ ((σ + [t/x])C ⊥ i ) • , ∆ i ) = (⊢ (σC ⊥ i ) • , ∆ i ) for each i > 1. Again since x is fresh in each C i , it is easy to see that ((C i ) * φ ) ⊥ = ((C i ) * φ+[d/x] ) ⊥ for each i > 1.
Hence the induction hypothesis applies to (σ + [t/x]) and (φ + [d/x]). We then know that

⊢ ∆ 1 , . . . , ∆ k , ((σ + [t/x])A) • ∈ A * φ+[d/x]
which is what we wanted. Existential quantifier For simplicity we assume that the derivation is

⊢ A[t/x], C 2 , . . . , C k (∃) ⊢ ∃x.A C1 , C 2 , . . . , C k Let us assume that (⊢ (σC ⊥ i ) • , ∆ i ) is in ((C i ) * φ ) ⊥ for all i > 1 and that (⊢ ((σ∃x.A) ⊥ ) • , Γ ) ∈ ((∃x.A) * φ ) ⊥ = (∀x.A ⊥ ) * φ .
Since x is not in the domain of σ (because x is bounded in ∃x.A), and by definition of (.) ⊥ , we have (σ∃x.A) ⊥ = ∀x.(σA) ⊥ . Hence we know that (⊢ (∀x.(σA

) ⊥ ) • , Γ ) ∈ ∀{ (A ⊥ ) * φ+[d/x] | ∀d ∈ M }. In particular, we have (⊢ (σA[t/x]) ⊥ , Γ ) ∈ (A ⊥ ) * φ+[t * φ /x] . By Lemma 1, (A ⊥ ) * φ+[t * φ /x] = (A[t/x] ⊥ ) *
φ , so we can apply the induction hypothesis and finally obtain that

⊢ ∆ 1 , . . . , ∆ k , Γ ∈ ⊥ ⊥. Cut The derivation is ⊢ A, C 1 , . . . , C p ⊢ A ⊥ , C p+1 , . . . , C k (Cut) ⊢ C 1 , . . . , C k for some 1 p k. Let us suppose that (⊢ (σC ⊥ i ) • , ∆ i ) is in ((C i ) * φ ) ⊥ for all i. Then by induction hypothesis, -if ⊢ (σA ⊥ ) • , ∆ is in (A * φ ) ⊥ , then ⊢ ∆, ∆ 1 , . . . , ∆ p ∈ ⊥ ⊥ -and if ⊢ σA • , ∆ is in A * φ , then ⊢ ∆, ∆ p+1 , . . . , ∆ k ∈ ⊥ ⊥. Therefore ⊢ σA • , ∆ 1 , . . . , ∆ p is in A * φ and ⊢ (σA ⊥ ) • , ∆ p+1 , . . . , ∆ k is in (A ⊥ ) * φ = (A * φ ) ⊥ . Then ⊢ ∆ 1 , . . . , ∆ k , Γ 1 , . . . , Γ n ∈ ⊥ ⊥.
Weakening For simplicity we assume that the derivation is

⊢ C 2 , . . . , C k (Weak) ⊢ C 1 , C 2 . . . , C k Let us suppose that (⊢ (σC ⊥ i ) • , ∆ i ) is in ((C i ) * φ ) ⊥ for all i > 1.
Then by induction hypothesis, ⊢ ∆ 2 , . . . , ∆ k ∈ ⊥ ⊥. Therefore by weakening in cut-free proofs, ⊢ ∆ 1 , . . . , ∆ k ∈ ⊥ ⊥. Contraction For simplicity we assume that the derivation is

⊢ C 1 , C 1 , . . . , C k (Contr) ⊢ C 1 , . . . , C k Let us suppose that (⊢ (σC ⊥ i ) • , ∆ i ) is in ((C i ) * φ ) ⊥ for all i > 0. Then by induction hypothesis, ⊢ ∆ 1 , ∆ 1 , . . . , ∆ k ∈ ⊥ ⊥. Therefore by contraction in cut-free proofs, ⊢ ∆ 1 , . . . , ∆ k ∈ ⊥ ⊥.
Conversion For simplicity, we assume that the derivation is

⊢ A, C 2 , . . . , C k A ≡ C 1 (≡) ⊢ C 1 , C 2 , . . . , C k and since A ≡ C 1 , we know that A * φ = (C 1 ) * φ and (A * φ ) ⊥ = ((C 1 ) * φ ) ⊥ . Let us suppose that ⊢ (σC ⊥ i ) • , ∆ i is in ((C i ) * φ ) ⊥ for all i > 1. Then since σC ⊥ 1 ≡ σA ⊥ , the sequent ⊢ σA ⊥ , ∆ is also in ((C i ) * φ ) ⊥ = (A * φ ) ⊥ . Finally by induction hypothesis, ⊢ ∆ 1 , . . . , ∆ k ∈ ⊥ ⊥. ⊓ ⊔
Cut-elimination is a corollary of our adequacy result.

Corollary 1 (Superconsistency implies cut-elimination). If ≡ is a superconsistent theory, then cut-elimination holds for LK modulo ≡, i.e. any sequent ⊢ ∆ derivable in LK modulo ≡ has a cut-free proof in LK modulo ≡.

Proof. Superconsistency of ≡ implies that there exists a model interpretation (.) * for ≡ in the pre-Boolean algebra of sequents D (corresponding to ≡). Let ⊢ C 1 , . . . , C k be some provable sequent in LK modulo ≡. Let us remark that

(⊢ (C ⊥ i ) • , C i ) ∈ ((C i ) * φ ) ⊥ for each C i (
where φ is the empty valuation). Then by our adequacy result (Theorem 3), (⊢ C 1 , . . . , C k ) ∈ ⊥ ⊥. In other words, this sequent has a cut-free proof in LK modulo ≡.

⊓ ⊔ Remark 1. To prove cut-elimination, we crucially rely on the fact that for each formula A and whatever the model interpretation (.) * given by the superconsistency is, A * φ contains all the axioms of the form ⊢ B ⊥ , B • , including ⊢ A ⊥ , A • . This cannot be achieved using phase semantics based cut-elimination models, or any other typed framework because we do not have control on the model interpretation (.) * .

In this section, we exhibit a (non-trivial) Boolean algebra, similar but simpler to the one that can be found in [START_REF] Dowek | A simple proof that super-consistency implies cut elimination[END_REF], extracted from the pre-Boolean algebra of sequents of section 5.

Definition 10 (Context Extraction). Let A be a formula, we define ⌊A⌋ to be the set of contexts Γ = A 1 , • • • , A n such that for any valuation φ, substitution σ, and any sequence of contexts

∆ i such that ⊢ ∆ i , ((σA i ) ⊥ ) • ∈ (A i ) * φ ⊥ , ⊢ ∆ 1 , • • • , ∆ n , (σA) • ∈ A *
φ . Equivalently, one may impose that for any context ∆ such that ⊢ ∆, ((σA

) ⊥ ) • ∈ A * φ ⊥ , we have ⊢ ∆ 1 , • • • , ∆ n , ∆ ∈ ⊥ ⊥.
Definition 11 (Boolean algebra). We define B, ≤, ⊤, ⊥, ∧, ∨, . ⊥ , ∀, ∃ as follows. B is the set containing ⌊A⌋ for any A. The order is inclusion, and the operations are

⊤ = ⌊⊤⌋ ⌊A⌋ ∧ ⌊B⌋ = ⌊A ∧ B⌋ ⌊A⌋ ⊥ = ⌊A ⊥ ⌋ ⊥ = ⌊⊥⌋ ⌊A⌋ ∨ ⌊B⌋ = ⌊A ∨ B⌋
∀{ ⌊A[t/x]⌋ | t ∈ T } = ⌊∀xA⌋ ∃{ ⌊A[t/x]⌋ | t ∈ T } = ⌊∃xA⌋
Notice that ⌊A[t/x]⌋ for t ∈ T does not depend of the chosen representative of the equivalence class t since as soon as t 1 ≡ t 2 , ⌊A[t 1 /x]⌋ = ⌊A[t 2 /x]⌋. Lemma 8. Let A and B be two formulae. Then:

-A ⊥ ∈ ⌊A⌋ -if A 1 , ..., A n ∈ ⌊A⌋ then ⊢ A 1 , ..., A n , A has a cut-free proof. -⊢ A ⊥ , B has a cut-free proof if, and only if, ⌊A⌋ ⊆ ⌊B⌋ Proof. -⊢ ∆, (σA) ⊥⊥ • ∈ (A ⊥ ) * φ ⊥ and ⊢ ∆, σA • ∈ A * φ are the same statement. -⊢ (A ⊥ i ) • , A i ∈ A * i ⊥ φ
for each A i and φ. By Definition 10, ⊢ A 1 , ..., A n , A ∈ ⊥ ⊥. -the if part follows from the two previous points: A ⊥ ∈ ⌊A⌋ ⊆ ⌊B⌋ and therefore ⊢ A ⊥ , B has a proof. For the only if part, let A 1 , ..., A n ∈ ⌊A⌋, σ be a substitution and φ be a valuation.

Let ∆ i such that ⊢ ∆ i , ((σA i ) ⊥ ) • ∈ (A i ) * φ ⊥ . By hypothesis ⊢ ∆ 1 , ..., ∆ n , (σA) • ∈ A * φ , so Theorem 3 applied to the proof of ⊢ A ⊥ , B implies that ⊢ ∆ 1 , ..., ∆ n , (σB) • ∈ B * φ . Therefore A 1 , ..., A n ∈ ⌊B⌋.
Proposition 1. B, ≤, ⊤, ⊥, ∧, ∨, . ⊥ , ∀, ∃ is a boolean algebra, and ⌊.⌋ is a model interpretation in this algebra, where the domain for terms is T .

Proof. This proposition is a consequence of the adequacy Theorem 3. Let us check the points of Definition 11:

1. ⌊A⌋ ∧ ⌊B⌋ is the greatest lower bound of ⌊A⌋ and ⌊B⌋.

-⌊A ∧ B⌋ ⊆ ⌊A⌋: by Lemma 8 since ⊢ (A ∧ B) ⊥ , A has a two-step proof.

- -⌊C⌋ ⊆ ⌊⊤⌋: by Lemma 8 since ⊢ C ⊥ , ⊤ has a two-step proof.

-⌊⊥⌋ ⊆ ⌊C⌋: by Lemma 8 since ⊢ ⊥ ⊥ , C has a two-step proof. 4. distributivity of ∧ and ∨ follow from the same laws in the logic, through Lemma 8: if two formulae A and B are equivalent then ⌊A⌋ = ⌊B⌋. 5. ⌊A ⊥ ⌋ is a complement of ⌊A⌋.

-⌊⊤⌋ ⊆ ⌊A ⊥ ∨ A⌋: by Lemma 8 since ⊢ ⊤ ⊥ , A ⊥ ∨ A has a two-step proof.

-⌊A ⊥ ∧ A⌋ ⊆ ⌊⊥⌋: by Lemma 8 since ⊢ (A ⊥ ∧A) ⊥ , ⊥ has a two-step proof. 6. idempotency of (.) ⊥ : ⌊A⌋ ⊥⊥ = ⌊A ⊥⊥ ⌋ = ⌊A⌋.

Lastly, we check that the operators ∀ and ∃ define a greatest lower bound and a lowest upper bound, respectively. Notice that although the order is set inclusion, those operators are not set intersection and union1 : B is neither complete, nor closed under arbitrary union and intersection and it misses many sets.

-⌊∀xA⌋ ⊆ { ⌊A[t/x]⌋ | t ∈ T }: by Lemma 8 since for any t, ⊢ (∀xA) A direct proof of Proposition 1, bypassing Lemma 3, is possible. In this option, each of its case uses the same arguments than the corresponding case of Theorem 3. Such a proof would be made easier by considering the definition of [START_REF] Dowek | Fondements des systèmes de preuve[END_REF] for pre-Boolean algebra where one has conditions on ⇒ rather than distributivity laws.

The benefits of a direct proof would be an alternative proof of the cutelimination theorem, as it is done in [START_REF] Dowek | A simple proof that super-consistency implies cut elimination[END_REF], through the usual soundness theorem with respect to Boolean Algebras and strong completeness with respect to the particular Boolean Algebra we presented here.

Conclusion

We have generalized Boolean algebras into pre-Boolean algebras, a notion of model for classical logic which acknowledges the distinction between computational and logical equivalences. We also have demonstrated how superconsistency -a semantic criterion for generic cut-elimination in (intuitionistic) deduction modulo-adapts to classical logic: We have proposed a classical version of superconsistency based on pre-Boolean algebras. Using orthogonality, we have constructed a pre-Boolean algebra of sequents which allows to prove that our classical superconsistency criterion implies cut-elimination in classical sequent calculus modulo. In the last section, we have explained how a non-trivial Boolean algebra of contexts can be extracted from the pre-Boolean algebra of sequents, therefore relating our orthogonality cut-elimination proof with the usual semantics of classical logic (i.e. Boolean algebras). Finally we have proved that the same cut-elimination result can be obtained from this particular Boolean algebra, without going through the proof of adequacy for the pre-Boolean algebra.

Let us notice that any pre-Boolean algebra is also a pre-Heyting algebra. Therefore a theory which is superconsistent on pre-Heyting algebras is automatically superconsistent on pre-Boolean algebras. (The converse does not hold in general and pre-Heyting algebras are not always pre-Boolean algebras.) Dowek has proved [START_REF] Dowek | Truth values algebras and proof normalization[END_REF] that several theories of interest are superconsistent on pre-Heyting algebras: arithmetic, simple type theory, the theories defined by a confluent, terminating and quantifier free rewrite system, the theories defined by a confluent, terminating and positive rewrite system and the theories defined by a positive rewrite system such that each atomic formula has at most one one-step reduct. We automatically obtain that these theories are also superconsistent on pre-Boolean algebras, and therefore that cut-elimination holds in classical sequent calculus modulo these theories.

Using Pre-Boolean algebras is not the unique way of connecting the superconsistency criterion with classical logic. For instance, one can use double-negation translations and prove that superconsistency (on pre-Heyting algebras) of a theory implies superconsistency (still on pre-Heyting algebras) of its doublenegation translation which in turn implies cut-elimination in classical logic, using [START_REF] Dowek | Proof normalization modulo[END_REF]. Superconsistency of double-negated theories on pre-Heyting algebras and superconsistency on pre-Boolean algebras remain to be compared. Both are implied by superconsistency on pre-Heyting algebras, and in both cases, no counterexample of the inverse has been found yet.

∀)Fig. 1 .

 1 Fig. 1. Sequent calculus LK modulo ≡

  The structure must verify, for any a, b, c ∈ B: 1. a ∧ b is a greatest lower bound of a and b: a ∧ b ≤ a a ∧ b ≤ b c ≤ a and c ≤ b implies c ≤ a ∧ b 2. a ∨ b is a lowest upper bound of a and b: a ≤ a ∨ b b ≤ a ∨ b a ≤ c and b ≤ c implies a ∨ b ≤ c

  ∆ 2 and both ⊢ A, ∆ 1 and ⊢ B, ∆ 2 have cut-free proofs. By application of the (∧) rule, ⊢ A ∧ B, ∆ 1 , ∆ 2 has a cut-free proof.⊓ ⊔ Theorem 1. D is stable under (.) ⊥ , ∧ and ∀.Proof. First, Lemma 6 implies stability under (.) ⊥ . Let us prove stability under ∧: let us assume X, Y ∈ D and prove X ∧Y ∈ D.

∀

  and ∃ are defined only on sets of the form { ⌊A[t/x]⌋ | t ∈ T }, where T is the set of equivalence classes modulo ≡ of open terms:

  ⌊A ∧ B⌋ ⊆ ⌊B⌋: by Lemma 8 since ⊢ (A ∧ B) ⊥ , B has a two-step proof. -⌊C⌋ ⊆ ⌊A⌋ and ⌊C⌋ ⊆ ⌊B⌋ implies ⌊C⌋ ⊆ ⌊A ∧ B⌋: by hypothesis and Lemma 8, C ⊥ ∈ ⌊C⌋ ⊆ ⌊A⌋ ∩ ⌊B⌋, and we have two proofs of ⊢ C ⊥ , A and ⊢ C ⊥ , B. We combine them to form a proof of ⊢ C ⊥ , A ∧ B and conclude by Lemma 8. 2. ⌊A⌋ ∨ ⌊B⌋ is the least upper bound of ⌊A⌋ and ⌊B⌋. -⌊A⌋ ⊆ ⌊A ∨ B⌋: by Lemma 8 since ⊢ A ⊥ , A ∨ B has a two-step proof. -⌊B⌋ ⊆ ⌊A ∨ B⌋: by Lemma 8 since ⊢ B ⊥ , A ∨ B has a two-step proof. -⌊A⌋ ⊆ ⌊C⌋ and ⌊B⌋ ⊆ ⌊C⌋ implies ⌊A ∨ B⌋ ⊆ ⌊C⌋: by hypothesis and Lemma 8, A ⊥ ∈ ⌊A⌋ ⊆ ⌊C⌋ and ⊢ A ⊥ , C has a proof. By a similar argument ⊢ B ⊥ , C has also a proof. We combine them to form a proof of ⊢ (A ∨ B) ⊥ , C and conclude by Lemma 8. 3. properties of greatest and lowest elements.

  ⊥ , A[t/x] has a one-step proof. -⌊C⌋ ⊆ { ⌊A[t/x]⌋ | t ∈ T } implies C ⊆ ⌊∀xA⌋: assume without loss of generality that x does not appear freely in C. By hypothesis and Lemma 8, C ⊥ ∈ ⌊C⌋ ⊆ { ⌊A[t/x]⌋ | t ∈ T } ⊆ ⌊A[x/x]⌋ and ⊢ C ⊥ , A has a proof. Adding a (∀) rule yields a proof of ⊢ C ⊥ , ∀xA. We conclude by Lemma 8. -{ ⌊A[t/x]⌋ | t ∈ T } ⊆ ⌊∃xA⌋: by Lemma 8 since for any t, ⊢ A[t/x] ⊥ , ∃xA has a one-step proof. -{ ⌊A[t/x]⌋ | t ∈ T } ⊆ ⌊C⌋ implies ⌊∃xA⌋ ⊆ ⌊C⌋: assume without loss of generality that x does not appear freely in C. By hypothesis and Lemma 8, A ⊥ ∈ ⌊A[x/x]⌋ ⊆ C and ⊢ A ⊥ , C has a proof. Adding a (∀) rule yields a proof of ⊢ (∃xA) ⊥ , C. We conclude by Lemma 8. Definition 10 ensures that ⌊.⌋ is an interpretation (Definition 2), provided that terms are interpreted by their equivalence class modulo ≡. Lastly, if A ≡ B then they are logically equivalent and by Lemma 8 ⌊A⌋ = ⌊B⌋.

so, for instance, the greatest lower bound is allowed to be smaller than set intersection