Michael Lau
email: michael.lau@mat.ulaval.ca

Olivier Mathieu
email: mathieu@math.univ-lyon1.fr

Jordan algebras and weight modules

Keywords: weight modules, Weyl modules, Tits-Kantor-Koecher construction, Jordan algebras, highest weight categories primary 17B10; secondary 17B60, 17C05, 17C50

We consider bounded weight modules for the universal central extension sl 2 (J) of the Tits-Kantor-Koecher algebra of a unital Jordan algebra J. Universal objects called Weyl modules are introduced and studied, and a combinatorial dominance criterion is given for analogues of highest weights.

Specializing J to the free Jordan algebra J(r) of rank r, the category C f in of finite-dimensional Z-graded sl 2 (J)-modules shares many properties with the representation theory of algebraic groups. Using a deep result of Zelmanov, we show that this subcategory admits Weyl modules. By analogy, we conjecture that C f in is a highest weight category. The resulting homological properties would then imply cohomological vanishing results previously conjectured as a way of determining graded dimensions of free Jordan algebras.

Introduction

Let J be a unital Jordan algebra over an algebraically closed field k of characteristic 0. Tits defined a Lie algebra structure on the space (sl 2 (k) ⊗ k J) ⊕ Inn J, where Inn J is the Lie algebra of inner derivations [START_REF] Tits | Une classe d'algèbres de Lie en relation avec les algèbres de Jordan[END_REF]. This construction was later generalized by Kantor [9] and Koecher [START_REF] Koecher | The Minnesota Notes on Jordan Algebras and Their Applications[END_REF] and is now called the Tits-Kantor-Koecher algebra and denoted by T KK(J). The Lie algebra T KK(J) is perfect and admits a universal central extension sl 2 (J) described [START_REF] Allison | Central quotients and coverings of Steinberg unitary Lie algebras[END_REF]. See also [START_REF] Allison | Central extensions of Lie algebras graded by finite root systems[END_REF][START_REF] Neher | Lie algebras graded by 3-graded root systems[END_REF].

With the exception of r = 1 and r = 2, the structure of the free Jordan algebras J(r) is unknown. However, it was proved in [START_REF] Kashuba | On the free Jordan algebras[END_REF] that its structure is determined by the sl 2 (k)-invariants of H * (sl 2 (J(r))). The following conjecture was provided.

Conjecture A [START_REF] Kashuba | On the free Jordan algebras[END_REF]Conj. 3]. H n (sl 2 (J(r))) sl 2 (k) = 0, for all n > 0.

Verification of this conjecture would give a recursive method to compute the dimensions of the graded components of J(r). In the present paper, we will interpret this conjecture in terms of representation theory.

Let {e, f, h} be the standard basis of sl 2 (k), and let h(a) = h ⊗ a ∈ sl 2 (J) for all a ∈ J. For any sl 2 (J)-module M and integer j, let M j be the weight space M j = {m ∈ M : h(1).m = j m}. The module M is said to be bounded of level

n if M = -n≤j≤n M j
for some nonnegative integer n with M n = 0. A vector space V endowed with a linear map ρ : J → End(V ) is called a J-space if it satisfies (J1) [ρ(a), ρ(a 2 )] = 0, (J2) [[ρ(a), ρ(b)], ρ(c)] = 4ρ(∂ a,b c), for all a, b, c ∈ J, where ∂ a,b (c) = a(cb) -(ac)b. When ρ(1) acts by multiplication by n, V is called a J-space of level n. For any bounded sl 2 (J)-module M of level n, the weight space M n has a structure of J-space of level n, where ρ(a) is the action of h(a). The J-space V is said to be dominant of level n if V = M n for some bounded sl 2 (J)-module M of level n.

Our first main result characterizes dominant J-spaces of level n. For any partition σ = (σ 1 , σ 2 , . . . , σ m ) of n + 1, we write |C σ | for the cardinality of the corresponding conjugacy class in S n+1 and sgn(σ) for its signature. We write ρ σ (a) for the expression ρ(a σ 1 )ρ(a σ 2 ) • • • ρ(a σm ) for all a ∈ J. The following result appears as Theorem 2.6.

Theorem B. Let (V, ρ) be a J-space of level n. Then V is dominant if and only if it satisfies the following condition

σ n+1 sgn(σ) |C σ | ρ σ (a) = 0.
For any dominant J-space of level n, the Weyl module ∆(M ) is the bounded sl 2 (J)-module of level n defined by the following universal property:

Hom

sl 2 (J) (∆(V ), M ) = Hom J (V, M n ),
for all bounded sl 2 (J)-modules M of level n, where homomorphisms of Jspaces are defined to be linear maps commuting with the action of J.

Assume now that J = ⊕ n≥0 J n is a finitely generated Z + -graded unital Jordan algebra with J 0 = k1. The grading on J clearly induces a grading on the Lie algebra sl 2 (J). We show that the category C f in of finite-dimensional Z-graded sl 2 (J)-modules admits a Weyl module for each dominant J-space.

Theorem C. For any Z-graded finite-dimensional dominant J-space V of level n, the Weyl module ∆(V ) is finite-dimensional.
Theorem C is nontrivial and uses a deep result of Zelmanov on nil Jordan algebras. It appears as Theorem 3.1 in the paper, and shows that the category C f in shares many properties with categories of representations of reductive algebraic groups in positive characteristic. This leads to the following conjecture.

Conjecture D. The category C f in is a highest weight category, in the sense of Cline, Parshall, and Scott.

A proof of Conjecture D would also settle Conjecture A of [START_REF] Kashuba | On the free Jordan algebras[END_REF].

Theorem E. Let r ≥ 1. If C f in is a highest weight category, then Conjecture A holds.
Theorem E appears below as Theorem 3.2.

Bounded weight modules

Let J be a unital Jordan algebra over an algebraically closed field k of characteristic zero. All vector spaces, algebras, and tensor products will be taken over k. For every a, b ∈ J, let L a : J → J be the multiplication operator

L a (b) = ab. Write ∂ a,b = [L a , L b ],
and let κ be one half the Killing form on sl 2 (k). We write Inn J for the set {∂ a,b : a, b ∈ J} of inner derivations of J. The element x ⊗ a in the vector space sl 2 (k) ⊗ J will be denoted by x(a). We fix a standard basis {h, e, f } of sl 2 (k) with [h, e] = 2e, [h, f ] = -2f , and [e, f ] = h.

Tits construction

In his 1962 paper, Tits defined a Lie algebra structure on the space

T KK(J) := sl 2 (k) ⊗ J ⊕ Inn J, with Lie bracket 1. (T1) [x(a), y(b)] = [x, y](ab) + κ(x, y)∂ a,b 2. (T2) [∂, x(a)] = x(∂ a),
where x(a) = x ⊗ a for any x, y ∈ sl 2 , ∂ ∈ Inn J, and a, b ∈ J. This construction was later generalized to Jordan pairs and triple systems by Kantor and Koecher, and T KK(J) is known as the Tits-Kantor-Koecher (TKK) algebra.

Tits-Allison-Gao construction

The TKK algebra is perfect, that is, T KK(J) = [T KK(J), T KK(J)], so T KK(J) admits a universal central extension, which we denote by sl 2 (J). This Lie algebra was nicely described in the 1996 paper of Allison and Gao [START_REF] Allison | Central quotients and coverings of Steinberg unitary Lie algebras[END_REF] in the context of universal coverings of the Steinberg unitary Lie algebras stu n (J) for n ≥ 3. The case where n = 3 corresponds to T KK(J). See also [START_REF] Allison | Central extensions of Lie algebras graded by finite root systems[END_REF] for equivalent formulas written in terms of sl 2 (k).

As a vector space,

sl 2 (J) = (sl 2 (K) ⊗ J) ⊕ {J, J},
where {J, J} = (2 J)/S and S = Span{a ∧ a 2 | a ∈ J}. For any a, b ∈ J, we write {a, b} for the image of a ∧ b in {J, J}. The bracket on sl 2 (J) is given by

(R1) [x(a), y(b)] = [x, y](ab) + κ(x, y){a, b} (R2) [{a, b}, x(c)] = x(∂ a,b c) (R3) [{a, b}, {c, d}] = {∂ a,b c, d} + {c, ∂ a,b d}.
for all a, b, c, d ∈ J and x, y ∈ sl 2 (k). It is a bit tricky to show that (R3) is skew-symmetric [START_REF] Allison | Central quotients and coverings of Steinberg unitary Lie algebras[END_REF].

There is an obvious Lie algebra epimorphism sl 2 (J) → T KK(J) which is the identity on sl 2 ⊗ J and sends the symbol {a, b} to ∂ a,b . When the Jordan algebra J is associative, we have {J, J} = HC 1 (J), and the construction specializes to results of Kassel and Loday [START_REF] Kassel | Extensions centrales d'algèbres de Lie[END_REF]. 12.3 The short grading of sl 2 (J)

The Lie algebra G := sl 2 (J) decomposes with respect to the adjoint action of 1 2 h(1) as

G = G -1 ⊕ G 0 ⊕ G 1 , where G -1 = f ⊗ J, G 0 = h ⊗ J ⊕ {J, J}, and
G 1 = e ⊗ J.
This decomposition is a root grading in the sense of Berman-Moody [START_REF] Berman | Lie algebras graded by finite root systems and the intersection matrix algebras of Slodowy[END_REF], and is called the short grading of G. In fact, every root-graded Lie algebra of type A 1 has a universal central extension isomorphic to sl 2 (J) for some unital Jordan algebra J. See [START_REF] Neher | Lie algebras graded by 3-graded root systems[END_REF] or [START_REF] Allison | Central extensions of Lie algebras graded by finite root systems[END_REF] for details.

Bounded modules

For any sl 2 (J)-module V and any k ∈ Z, let

V k = {v ∈ V : h(1)v = k v}. An sl 2 (J)-module V is said to be a bounded weight module of level if V = ⊕ -≤m≤ V m , with V = 0.

J-spaces

Recall that a vector space M endowed with a linear map ρ :

J → End(M ) is called a J-space if ρ satisfies (J1) [ρ(a), ρ(a 2 )] = 0, (J2) [[ρ(a), ρ(b)], ρ(c)] = 4ρ(∂ a,b c). A J-space is said to be of level n if ρ(h(1)) = n id.
Lemma 2.1. Let (M, ρ) be a representation of the Lie algebra G 0 . Then the map ρ : a → ρ(h(a)) determines a J-space structure on M .

Conversely, if M is a J-space, then there is a unique G 0 -module structure (M, ρ) such that ρ(h(a)) = ρ(a) for any a ∈ J.

Proof. Let (M, ρ) be a G 0 -module. For a ∈ J, set ρ(a) = ρ(a). Since [h(a), h(a 2 )] = 4{a, a 2 } = 0, it follows that [ρ(a), ρ(a 2 )] = 0, proving (J1). Let a, b, c ∈ J. We have [[h(a), h(b)], h(c)] = 4h(∂ a,b c), and therefore [[ρ(a), ρ(b)], ρ(c)] = 4ρ(∂ a,b c), proving (J2).
Conversely, assume that M is a J-space. It is clear that G 0 is generated by the vector space h ⊗ J and defined by the relations (H1) [h(a), h(a 2 )] = 0, and

(H2) [[h(a), h(b)], h(c)] = 4h(∂ a,b c),
for any a, b, c ∈ J. Therefore there is a unique structure ρ of G 0 -module on M such that ρ(h(a)) = ρ(a)

A linear map σ : J → End k (M ) is a Jordan birepresentation (and M is a Jordan bimodule) if the semidirect product (a, m)(b, n) = (ab, bm + an) gives a Jordan algebra structure to the vector space direct sum J ⊕ M . This condition is equivalent to the conditions (M1) [σ(a), σ(a 2 )] = 0, and

(M2) σ(a 2 b) + 2σ(a)σ(b)σ(a) = 2σ(ab)σ(a) + σ(a 2 )σ(b),
for all a, b ∈ J. It follows from [8, II.9(47')] that (M1) and (M2) imply that ρ = 2σ satisfies (J1) and (J2). The converse is not true, however. If (M, ρ) is a J-space of level n, then setting a = b = 1 ∈ J in (M2), we see that the only possible values for n = ρ(1) are 0, 1 or 2 (Peirce decomposition), if we wish to induce a J-bimodule structure on M with action σ = 1 2 ρ. But as we will see in Example 2.10, there exist J-spaces of any level.

Dominant J-spaces

Any J-space M of level n can be induced to a generalized Verma module

V (M ) = U(G) ⊗ U (G 0 ⊕G 1 ) M,
where G 1 acts as zero on M . The main result of this section will be an analysis of which J-spaces M of level n determine G-modules V (M ) with bounded quotients V (M )/X, such that the composition of natural maps

M → V (M ) → V (M )/X
is an injection of G 0 ⊕ G 1 -modules. Such a quotient V (M )/X will be called a bounded M -quotient of V (M ) of level n, and in this case, M is said to be dominant. Note that if V (M )/X is a bounded M -quotient of level n, then n is a nonnegative integer and the weight n subspace (V (M )/X) n is precisely M . Proposition 2.2. Let M be a J-space of nonnegative integer level n, with G 0 -action given by ρ : J → End k (M ). Then the generalized Verma module V (M ) has a bounded M -quotient if and only if e(1) n+1 f (a) n+1 m = 0, for all a ∈ J and m ∈ M .

Proof. If V (M ) has a nonzero bounded M -quotient V (M )/X, then M = (V (M )/X) n = V (M ) n , so X n = 0. By sl 2 -theory, we see that (V (M )/X) m = 0 for all m < -n, so X m = V (M ) m for all m < -n. In particular, f (a) n+1 m ∈ V (M ) -n-2 = X -n-2 ⊆ X for all m ∈ M , so e(1) n+1 f (a) n+1 m ∈ X for all a ∈ J and m ∈ M . But then e(1) n+1 f (a) n+1 m ∈ V (M ) n ∩ X = 0.
Conversely, suppose that e(1) n+1 f (a) n+1 m = 0 for all a ∈ J and m ∈ M . Let Z ⊂ V (M ) be a G-submodule which is maximal with respect to the property that Z n = 0. Linearisation of the relation e(1) n+1 f (a

) n+1 m = 0 gives e(1) n+1 f (b 1 ) • • • f (b n+1 )m = 0,
for all b 1 , . . . , b n+1 ∈ J and m ∈ M . Then for any a 1 , . . . , a n+1 ∈ J, we have

h(a 1 ) . . . h(a n+1 )e(1) n+1 f (b 1 ) • • • f (b n+1 )m = 0, from which it follows that e(a 1 ) • • • e(a n+1 )f (b 1 ) • • • f (b n+1 )m = 0, for all a i , b j ∈ J and m ∈ M . In particular, this shows that f (b 1 ) • • • f (b n+1 )m ∈ Z, and V (M ) k ⊆ Z for all k ≤ -n -2. Therefore, V (M ) k = Z k for all k < -n, and V (M )/Z is a bounded M -quotient.
We now introduce some notation. Let σ = (σ 1 , . . . , σ m ) be a partition of n + 1, that is,

σ 1 ≥ • • • ≥ σ m ≥ 1, for some m ≥ 1, where σ 1 + • • • + σ m = n + 1.
We write |C σ | for the cardinality of the conjugacy class C σ of permutations in the symmetric group S n+1 with cycle structure σ. The sign of these permutations will be denoted by sgn(σ), and we write ρ σ (a) for the expression ρ(a σ 1 )ρ(a σ 2 ) • • • ρ(a σm ) for all a ∈ J and σ n + 1. It follows easily from Condition (C1) that [ρ(a i ), ρ(a j )] = 0 for all i, j, so this product is independent of the order of the factors.

The Newton polynomials

N (x) = x 1 + • • • + x n in n indeterminates x 1 , . . . , x n generate the ring of symmetric polynomials k[x 1 , . . . , x n ] Sn . We write N σ (x) = N σ 1 (x)N σ 2 (x) • • • N σm (x)
for each partition σ = (σ 1 , . . . , σ m ) of n+1. The space P n+1 ⊂ k[x 1 , . . . , x n ] Sn of symmetric polynomials of total degree n + 1 is clearly of dimension p(n + 1) -1, where p(n + 1) is the number of partitions of n + 1. The Newton polynomials N 1 (x), . . . , N n (x) are algebraically independent, so {N σ (x) : σ n + 1 such that σ = (1, 1, . . . , 1)} is a basis for P n+1 , and the set

{N σ (x) : σ n + 1}
has exactly one linear dependence relation, up to scalar multiple. We include an amusing representation-theoretic argument below, that we have not seen elsewhere in the literature.

Proposition 2.3. Up to scalar multiple, the unique linear dependence relation on the set {N σ (x) :

σ n + 1} is σ n+1 sgn(σ)|C σ |N σ (x) = 0.
Proof. By the Frobenius character formula,

N σ (x) = λ χ λ (σ)S λ ,
where the sum is taken over all partitions λ = (1, 1, . . . , 1) of n + 1. Here χ λ (σ) is the character (evaluated at any permutation of cycle structure σ) of the Specht module associated with λ, and S λ is the Schur polynomial associated to λ. See [START_REF] Fulton | Representation Theory: A First Course[END_REF] for details. Since sgn is the character of the sign representation, the Specht module associated to (1, . . . , 1), we see that

σ n+1 sgn(σ)|C σ |N σ (x) = σ∈S n+1 sgn(σ)N σ (x) = σ∈S n+1 χ (1,...,1) (σ) λ =(1,...,1) χ λ (σ)S λ = λ =(1,...,1) S λ σ∈S n+1 χ (1,...,1) (σ)χ λ (σ),
and the inner product

(χ (1,...,1) , χ λ ) = σ∈S n+1 χ (1,...,1) (σ)χ λ (σ)
is 0 whenever λ = (1, . . . , 1), by the orthogonality relations.

Remark 2.4. Proposition 2.3 can also be proved with a more standard combinatorial argument: Let V be a vector space of dimension n, with basis {e 1 , . . . , e n }. Let h : V → V be defined by h(e i ) = x i e i , and let h ⊗(n+1) : V ⊗(n+1) → V ⊗(n+1) be the induced endomorphism. For σ ∈ S n+1 , we have

Tr(h ⊗(n+1) • σ) = N σ (x).
Since σ∈S n+1 sgn(σ)σ acts as zero on V ⊗(n+1) , the dependence relation follows.

The following well-known formula, originally due to Garland [START_REF] Garland | The arithmetic theory of loop groups[END_REF] and reinterpreted by Chari and Pressley [START_REF] Chari | Weyl modules for classical and quantum affine algebras[END_REF], will be used to prove boundedness conditions.

Lemma 2.5. Let p : U(G) → U(G -1 )U(G 0 ) be the projection relative to the (vector space) decomposition

U(G) = U(G)G 1 ⊕ U(G -1 )U(G 0 ). Then p(e(1) r f (a) n+1 ) is the coefficient of u n+1 in the generating function (-1) r r!(n + 1)! (n + 1 -r)! ∞ s=1 f (a s )u s n+1-r exp - ∞ t=1 h(a t ) t u t .
Theorem 2.6. Let (M, ρ) be a J-space of level n. Then the following conditions are equivalent:

(1) M is dominant.

(2) e(1) n+1 f (a) n+1 m = 0 for all a ∈ J and m ∈ M .

(

) σ n+1 sgn(σ)|C σ |ρ σ (a) = 0. 3
Proof. By Proposition 2.2, Conditions (1) and ( 2) are equivalent, so we need only prove that (2) and (3) are equivalent. Since e(1) n+1 f (a) n+1 is homogeneous of degree 0 with respect to the grading induced by ad (h ⊗ 1), we see that its action on any highest weight vector m is given by the action of its projection p on the subspace U(G 0 ) with respect to the decomposition U(G)

0 = U(G 0 ) ⊕ (U(G)G 1 ∩ U(G) 0 ) of the space U(G) 0 of degree 0 elements of U(G).
By Lemma 2.5, p(e(1) n+1 f (a) n+1 ) is the coefficient of u n+1 in the generating series

(-1) n+1 (n + 1)!(n + 1)!exp - ∞ k=1 h(a k ) k u k .
Computing directly, the coefficient of

u n+1 in exp -∞ k=1 h(a k ) k u k is σ n+1 (-1) rσ h σ (a) ( rσ i=1 σ i ) mσ j=1 a j !
, where σ i is the length of the ith row of the Young frame T σ associated to the partition σ, r σ is the number of rows of T σ , m σ is the number of columns of T σ , a j is the number of rows of length j in T σ , and

h σ (a) = h(a σ 1 )h(a σ 2 ) • • • h(a σr σ ).
If odd(r σ ) (respectively, even(r σ ) is the number of odd-length (respectively, even-length) rows of T σ , we see that (-1) n+1 = (-1) odd(rσ) , so (-1) n+1 (-1) rσ = (-1) n+1 (-1) odd(rσ) (-1) even(rσ) = (-1) even(rσ) = sgn(σ).

By elementary counting arguments, Example 2.7. By Theorem 2.6, any dominant J-space M of level 0 is trivial, in the sense that ρ : J → End k (M ) is the zero map and M , equipped with the trivial G-action, is the unique bounded M -quotient of V (M ).

|C σ | = (n + 1)! ( rσ i=1 σ i )
Example 2.8. Dominant J-spaces (M, ρ) of level 1 satisfy ρ(a 2 ) = ρ(a) 2 for all a ∈ J, so

ρ(ab) = 1 2 (ρ(a)ρ(b) + ρ(b)ρ(a)), (2.9)
for all a, b ∈ J by linearization. Dominant J-spaces (M, ρ) of level 1 are thus precisely associative specializations, Jordan algebra homomorphisms ρ from J to special Jordan algebras of linear operators on a vector space M .

Example 2.10. For levels higher than 2, dominant J-spaces are never Jordan bimodules. See the discussion after Lemma 2.1 for details. Many such Jspaces exist. For example, it follows immediately from Proposition 2.3 and Theorem 2.6, that the map

ρ : k[t] → End k k[x 1 , . . . , x n ] Sn (2.11) t → N (x)
defines a dominant J-space of level n for the (associative) Jordan algebra J = k[t], an example we will consider in more detail in Section 3.

Weyl modules and highest weight categories

Let n be a nonnegative integer. The categories C b (M ) of bounded weight modules attached to bounded J-spaces M of level n admit universal objects ∆(M ), called Weyl modules. Every bounded M -quotient of level n is a homomorphic image of ∆(M ), and it is clear that

∆(M ) = V (M ) / U(G) <-n V (M ) = n =0 ∆(M ) n-2 ,
where ∆(M ) n-2 is the vector subspace of weight n -2 . Identifying

G -1 = {f ⊗ a : a ∈ J} ⊂ G = (sl 2 (k) ⊗ J) ⊕ {J, J}
with J, the weight space V (M ) n-2 identifies with the vector space S J ⊗ M for = 0, . . . , n.

Weyl modules for finite dimensional dominant Jspaces

Let J = ∞ =0 J be a finitely generated Z + -graded unital Jordan algebra with J 0 = k1. Let M = ∞ =0 M be a Z-graded dominant J-space of level n. We now prove one of our main results, that the category C f in of finitedimensional Z-graded sl 2 (J)-modules contains its Weyl modules. Theorem 3.1. Let M be a Z-graded dominant J-space of level n, for a Z +graded and finitely generated Jordan algebra J with J 0 = k1. Then the Weyl module ∆(M ) is finite dimensional if and only if M is finite dimensional.

Proof. If ∆(M ) is finite dimensional, then M ⊆ ∆(M ) is clearly also finite dimensional. Conversely, assume that M is finite dimensional. Up to a possible shift in grading, we may assume that M is Z + -graded. Let N be the largest nonnegative integer for which the graded component M N is nonzero. Let a ∈ J be a homogeneous element with deg a > N , and let v ∈ M . By Lemma 2.5, e(1) n f (a) n+1 v is the coefficient of u n+1 in the formal series

(-1) n n!(n + 1)! ∞ s=1 f (a s )u s exp - ∞ t=1 h(a t ) t u t v.
By degree considerations, h(a t )v = 0 for all t ≥ 1, so

e(1) n f (a) n+1 v = (-1) n n!(n + 1)!f (a n+1 )v,
and f (a n+1 )v = 0 as an element of ∆(M ).

In particular, f b (N +1)(n+1) M = 0 for all b in the (non-unital) Jordan subalgebra

J + = ∞ =1 J ⊂ J. Let I = {x ∈ J + : f (x)M = 0}. For all x ∈ J + , y ∈ I, and m ∈ M , 0 = h(x)f (y)m = f (y)h(x)m -2f (xy)m = -2f (xy)m
since h(x)M ⊆ M and f (y)M = 0. Therefore, xy ∈ I and I is an ideal of J + . Since b (N +1)(n+1) ∈ I for all b ∈ J + , the Jordan algebra J + /I is nil of bounded index, hence locally nilpotent by a result of Zelmanov [START_REF] Zelmanov | Jordan nil-algebras of bounded index[END_REF]. But J, and thus J + /I, is finitely generated, so J + /I is nilpotent and there exists N > 0 such that every product (in any association) of N elements of J + is in I. The (finitely many) generators of J may be chosen to be homogeneous and of positive degree at most r for some r > 0. In particular, J s ⊆ I for all s ≥ rN . That is, f (a)M = 0 for all a ∈ J with deg a ≥ rN .

The weight space ∆(M ) n-2 is spanned by monomials of the form

f (a 1 ) • • • f (a )w
with a 1 , . . . , a ∈ J and w ∈ M. Since the f (a i ) commute with each other, the set {f (a 1 ) • • • f (a )w : w ∈ M and a 1 , . . . , a ∈ J with deg a i < rN for all i} already spans ∆(M ) n-2 . As M and J i are finite dimensional for all i, it now follows that dim ∆(M ) n-2 < ∞ for all , and the Weyl module ∆(M ) = n =0 ∆(M ) n-2 is also finite dimensional.

Highest weight categories and character formulas for free Jordan algebras

Cline, Parshall, and Scott [START_REF] Cline | Finite dimensional algebras and highest weight categories[END_REF] introduced the notion of highest weight category as a unifying theme in representation theory, modelled after highest weight representations of semisimple algebraic groups and their Lie algebras. Their definition requires labelling simple objects by a poset Λ, and the existence of enough injectives, as well as costandard objects labelled by the same index set as the simples and satisfying various axioms. Given the similarities between the category C f in of finite-dimensional Z-graded sl 2 (J(r))-modules and the representation theory of reductive algebraic groups in positive characteristic, we conjecture that C f in is a highest weight category, with the Weyl modules and their duals (twisted by the Cartan involution) as the standard and costandard objects, respectively. In a highest weight category, the higher ext-groups Ext i (∆(λ), ∇(µ)) = 0 for all i > 0 and λ, µ ∈ Λ. If C f in is indeed a highest weight category as conjectured above, the vanishing of higher extgroups would, in fact, settle the main conjecture of [START_REF] Kashuba | On the free Jordan algebras[END_REF] and thus describe the graded dimensions of the free Jordan algebras J(r).

Theorem 3.2. If C f in is a highest weight category with Weyl modules and their duals as its standard and costandard objects, then H i (sl 2 (J(r))) contains no nonzero trivial sl 2 (k)-modules for i > 0.

Proof. Let J be the free unital Jordan algebra J(r) on r generators, and suppose that C f in is a highest weight category as in the hypotheses of the theorem. As noted above, in a highest weight category, Ext i (∆(λ), ∇(µ)) vanishes for all i > 0 and indices λ, µ of simples, where ∆(λ) and ∇(µ) are the corresponding standard and costandard objects. In C f in , the Weyl and dual Weyl modules corresponding to the trivial 1-dimensional sl 2 (J)-module k are themselves 1-dimensional, so

Ext i C f in (k, k) = 0 for all i > 0. But Ext i C f in (k, k) = H i (sl 2 (J))
, and the cohomology ring

H * (sl 2 (J)) = H * (sl 2 (k)) ⊗ H * (sl 2 (J), sl 2 (k)).
As H 0 (sl 2 (J)) = H 0 (sl 2 (k)) = k, we see that H * (sl 2 (J)) = k and the relative cohomology H i (sl 2 (J), sl 2 (k)) = 0, for all i > 0. The result now follows from the universal coefficient theorem and the interpretation of the relative cohomology as the sl 2 (k)-invariants in H i (sl 2 (J)).

Example: Weyl modules for free Jordan algebras of rank 1

For any Jordan algebra J with unit 1 and n ∈ Z + , let

T (J) = k1 ⊕ J ⊕ J ⊗2 ⊕ J ⊗3 ⊕ • • •
be its tensor algebra, and let I ⊆ T (J) be the two-sided ideal generated by the relations

1 -n1, (3.3) a ⊗ a 2 -a 2 ⊗ a, (3.4) a ⊗ b ⊗ c + c ⊗ b ⊗ a -b ⊗ a ⊗ c -c ⊗ a ⊗ b + b(ac) -a(bc), (3.5)
σ n+1 sgn(σ)|C σ |T σ (a), (3.6)
for all a, b, c ∈ J, where

T σ (a) = a σ 1 ⊗ a σ 2 ⊗ • • • ⊗ a σm for all partitions σ = (σ 1 , . . . , σ m ) n + 1.
The associative algebra U n (J) = T (J)/I is called the universal J-space envelope of level n. There is a unique associative algebra homomorphism ρ : T (J) → End k (M ) extending the action ρ : J → End k (M ) of any J-space (M, ρ) of level n, and in light of Lemma 2.1 and Theorem 2.6, the map ρ descends to the quotient U n (J). By construction, dominant J-spaces of level n and left U n (J)-modules are equivalent notions, and a J-space (M, ρ) of level n is said to be free of rank r if (M, ρ) is a free U n (J)-module.

Let F = U n (J) be the universal J-space envelope of level n for a unital Jordan algebra J. If J is finitely generated as a Jordan algebra, then F is finitely generated as an associative algebra, by Relation (3.6). For example, if J = k[t] is the free Jordan algebra of rank 1, then F = k[x 1 , . . . , x n ] Sn is the algebra of symmetric polynomials, where t corresponds to the Newton polynomial N Let L be the two-dimensional simple sl 2 (k)-module. The Jordan algebra J = k[t] is commutative and associative, and it is easy to see that {J, J} = 0 and the TKK algebra G = sl 2 (J) = sl 2 (k) ⊗ J is centrally closed. The space L[t] = L ⊗ k[t] is obviously a G-module, where (x ⊗ p(t)).(v ⊗ q(t)) = xv ⊗ p(t)q(t), for all x ∈ sl 2 (k), v ∈ L, and p(t), q(t) ∈ J. This gives a G-module structure on the space S n (L[t]) ⊂ T (L[t]) of homogeneous symmetric tensors of degree n. Proof. Let v ∈ L be a nonzero vector of weight 1 with respect to the action of h ∈ sl 2 (k). There is a natural injection ι : F -→ S n (L[t]), with ι :

(x) = x 1 + • • • + x n ∈ F . If J is free of rank m, then U 0 (J) = k and U 1 (J)
σ∈Sn x a σ(1) σ(1) • • • x a σ(n) σ(n) -→ σ∈Sn (v ⊗ t a σ(1) ) ⊗ • • • ⊗ (v ⊗ t a σ(n) ).
This maps extends uniquely to a G-module epimorphism

V (F ) → S n (L[t])
u.p → u.ι(p), for all u ∈ U (G) and p ∈ F, with kernel <-n V (F ) .

Remark 3.8. In fact, for every prime Jordan algebra J and every n ≥ 2, there is a dominant J-space of level n, on which the Lie algebra G 0 (J) = (h ⊗ J) ⊕ {J, J} acts faithfully. If J is special, then there is a faithful associative specialization ρ : J → End k (M ), and M is a J-space of level 1.

The faithfulness of the extension ρ : G 0 → End k (M ) on {J, J} follows immediately from the assumption that J is prime. We can then take the n-fold tensor product of M to obtain a faithful J-space of level n.

If J is the Albert algebra A, then we can construct a faithful G 0 -module of level n as a tensor product of copies of the level 2 and level 3 representations of the Albert algebra, obtained from representations of the exceptional Lie algebra E 6 , viewed as the subalgebra (k h ⊗ A) ⊕ {A, A} of the Lie algebra sl 2 (A).

This observation is clearly not true for arbitrary (non-prime) Jordan algebras. For example, the Lie algebra G 0 (k[t, t -1 ]) has a nontrivial centre that acts as 0 on all bounded modules.

mσ j=1 a j ! .See [ 14 ,

 !14 Proposition 1.1.1], for instance. The projection of e(1) n+1 f (a) n+1 on U(G 0 ) is thus (n + 1)! σ n+1 sgn(σ)|C σ |h σ (a), so Conditions (2) and (3) are equivalent.

  is the quotient of the free associative algebra in m generators by the ideal generated by the relation a ⊗ b ⊗ c + c ⊗ b ⊗ a = b ⊗ a ⊗ c + c ⊗ a ⊗ b for all a, b, c ∈ J.

Proposition 3 . 7 .

 37 Let F = k[x 1 , . . . , x n ] Sn be the rank 1 free U n (k[t])-module. Then the Weyl module ∆ n (F ) is isomorphic to S n (L[t]).

The notation in[START_REF] Kassel | Extensions centrales d'algèbres de Lie[END_REF] differs slightly from the modern conventions-Kassel-Loday write HC

for what is now denoted as HC 1 .

sharing not applicable to this article as no datasets were generated or analysed during the current study.


F R Éd

Éric Blanqui
email: frederic.blanqui@inria.fr

Gilles Dowek
email: gilles.dowek@inria.fr

Emilie Grienenberger
email: emilie.grienenberger@ens-paris-saclay.fr

Gabriel Hondet
email: gabriel.hondet@inria.fr

¸ois Thir

A MODULAR CONSTRUCTION OF TYPE THEORIES

Keywords: logical framework, λΠ-calculus modulo rewriting, Dedukti, logic, type theory

The λΠ-calculus modulo theory is a logical framework in which many type systems can be expressed as theories. We present such a theory, the theory U, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of U corresponding to each of these systems, and prove that, when a proof in U uses only symbols of a sub-theory, then it is a proof in that sub-theory.

Introduction

The λΠ-calculus modulo theory (λΠ/≡) [START_REF] Cousineau | Embedding pure type systems in the lambda-Pi-calculus modulo[END_REF], that is the basis of the language Dedukti [ABC + 16, HB20], is a logical framework, that is, a framework to define theories. It generalizes some previously proposed frameworks: Predicate logic [START_REF] Hilbert | Grundzüge der theoretischen Logik[END_REF], λ-Prolog [START_REF] Nadathur | An overview of lambda-prolog[END_REF], Isabelle [START_REF] Paulson | Isabelle: The next 700 theorem provers[END_REF], the Edinburgh logical framework [START_REF] Harper | A framework for defining logics[END_REF], also called the λΠ-calculus, Deduction modulo theory [START_REF] Dowek | Theorem proving modulo[END_REF][START_REF] Dowek | Proof normalization modulo[END_REF], Pure type systems [START_REF] Berardi | Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube[END_REF][START_REF] Terlouw | Een nadere bewijstheoretische analyse van GSTT's[END_REF], and Ecumenical logic [START_REF] Prawitz | Classical versus intuitionistic logic[END_REF][START_REF] Dowek | On the definition of the classical connectives and quantifiers[END_REF][START_REF] Pereira | Normalization, soundness and completeness for the propositional fragment of Prawitz'Ecumenical system[END_REF][START_REF] Grienenberger | A logical system for an Ecumenical formalization of mathematics[END_REF]. It is thus an extension of Predicate logic that provides the possibility for all symbols to bind variables, a syntax for proof-terms, a notion of computation, a notion of proof reduction for axiomatic theories, and the possibility to express both constructive and classical proofs.

λΠ/≡ enables to express all theories that can be expressed in Predicate logic, such as geometry, arithmetic, and set theory, but also Simple type theory [START_REF] Church | A formulation of the simple theory of types[END_REF] and the Calculus of constructions [START_REF] Th | The calculus of constructions[END_REF], that are less easy to define in Predicate logic.

We present a theory in λΠ/≡, the theory U, where all proofs of Minimal, Constructive, and Ecumenical predicate logic; Minimal, Constructive, and Ecumenical simple type theory; Simple type theory with predicate subtyping, prenex predicative polymorphism, or both; the Calculus of constructions, and the Calculus of constructions with prenex predicative polymorphism can be expressed. This theory is therefore a candidate for a universal theory, where proofs developed in implementations of Classical predicate logic (such as automated theorem proving systems, SMT solvers, etc.), Classical simple type theory (such as HOL 4, Isabelle/HOL, HOL Light, etc.), the Calculus of constructions (such as Coq, Matita, Lean,

Γ Σ,R t : Πx : A, B Γ Σ,R u : A Γ Σ,R t u : (u/x)B (app) Γ Σ,R t : A Γ Σ,R B : s Γ Σ,R t : B (conv) A ≡ βR B
Figure 1: Typing rules of λΠ/≡ with signature Σ and rewriting rules R

x 1 : B 1 , . . . , x m : B m is in Λ(Σ) if B 1 , . . . , B m are. It is often convenient to group constant declarations and rules into small clusters, called "axioms".

A relation → preserves typing in (Σ, R) if, for all contexts Γ and terms t, u and A of Λ(Σ), if Γ Σ,R t : A and t → u, then Γ Σ,R u : A. The relation → β preserves typing as soon as → βR is confluent (see for instance [START_REF] Blanqui | Type theory and rewriting[END_REF]) for, in this case, the product is injective modulo ≡ βR : Πx : A, B ≡ βR Πx : A , B if and only if A ≡ βR A and B ≡ βR B . The relation → R preserves typing if every rewriting rule → r preserves typing, that is: for all contexts Γ, substitutions θ and terms A of Λ(Σ), if Γ Σ,R θl : A then Γ Σ,R θr : A.

Although typing is defined with arbitrary signatures Σ and sets of rewriting rules R, we are only interested in sets R verifying some confluence and type-preservation properties.

Definition 2.1 (System, theory). A system is a pair (Σ, R) such that each rule of R is in Λ(Σ). It is a theory if → βR is confluent on Λ(Σ), and every rule of R preserves typing in (Σ, R).

Therefore, in a theory, → βR preserves typing since → β preserves typing (for → βR is confluent) and → R preserves typing (for every rule preserves typing). We recall two other basic properties of λΠ/≡ we will use in Theorem 4.5: Lemma 2.2. If Γ Σ,R t : A, then either A = KIND or Γ Σ,R A : s for some sort s.

If Γ Σ,R Πx : A, B : s, then Γ Σ,R A : TYPE.

The theory U

Let us now present the system U which is formed with axioms expressed in λΠ/≡. We will prove in Theorem 4.7 that this system is indeed a theory.

3.1. Object-terms. The notions of term, proposition, and proof are not primitive in λΠ/≡. The first axioms of the theory U introduce these notions. We first define a notion analogous to the Predicate logic notion of term, to express the objects the theory speaks about, such as the natural numbers. As all expressions in λΠ/≡ are called "terms", we shall call these expressions "object-terms", to distinguish them from the other terms.

To build the notion of object-term in λΠ/≡ we declare a constant I of type TYPE

I : TYPE (I-decl)
and constants of type I → ... → I → I for the function symbols, for instance a constant 0 of type I and a constant succ of type I → I. The object-terms, for instance (succ (succ 0)) and (succ x), are then just λΠ/≡ terms of type I and, in an object-term, the variables are λΠ/≡ variables of type I. If we wanted to have object-terms of several sorts, like in Many-sorted predicate logic, we could just declare several constants I 1 , I 2 , ..., I n of type TYPE.

3.2. Propositions. Just like λΠ/≡ does not contain a primitive notion of object-term, it does not contain a primitive notion of proposition, but tools to define this notion. To do so, in the theory U, we declare a constant Prop of type TYPE Prop : TYPE (Prop-decl) and predicate symbols, that is constants of type I → ... → I → Prop, for instance a constant positive of type I → Prop. Propositions are then λΠ/≡ terms, such as (positive (succ (succ 0))), of type Prop.

Implication.

In the theory U, we then declare a constant for implication

⇒ : Prop → Prop → Prop (written infix) (⇒-decl)
and we can then construct the term (positive (succ (succ 0))) ⇒ (positive (succ (succ 0))) of type Prop.

3.4. Proofs. Predicate logic defines a language for terms and propositions, but proofs have to be defined in a second step, for instance as derivations in natural deduction, sequent calculus, etc. These derivations, like object-terms and propositions, are trees. Therefore, they can be represented as λΠ/≡ terms.

Using the Brouwer-Heyting-Kolmogorov interpretation, a proof of the proposition A ⇒ B should be a λΠ/≡ term expressing a function mapping proofs of A to proofs of B. Then, using the Curry-de Bruijn-Howard correspondence, the type of this term should be the proposition A ⇒ B itself. But, this is not possible in the theory U yet, as the proposition A ⇒ B has the type Prop, and not the type TYPE.

A strict view on the Curry-de Bruijn-Howard correspondence leads to identify Prop and TYPE, yielding the conclusion that all types, including I, and Prop itself, are propositions. A more moderate view leads to the introduction of an embedding Prf of propositions into types, mapping each proposition A to the type Prf A of its proofs. This view is moderate in two respects. First, the propositions themselves are not the types of their proofs: if t is a proof of A, then it does not have the type A, but the type Prf A. Second, this embedding is not surjective. So not all types are types of proofs, in particular I and Prop are not.

So, in the theory U, we declare a constant Prf Prf : Prop → TYPE (Prf-decl)

When assigning the type Prop → TYPE to the constant Prf, we use the fact that λΠ/≡ supports dependent types, that is the possibility to build a family of types Prf x parameterized with a variable x of type Prop, where Prop is itself of type TYPE.

According to the Brouwer-Heyting-Kolmogorov interpretation, a proof of A ⇒ A is a λΠ/ ≡ term expressing a function mapping proofs of A to proofs of A, so that it can be both built and used as a function. In particular, the identity function λx : Prf A, x mapping each proof of A to itself is a proof of A ⇒ A. According to the Curry-de Bruijn-Howard correspondence, this term should have the type Prf (A⇒A), but it has the type Prf A → Prf A. So, the types Prf (A ⇒ A) and Prf A → Prf A must be identified. To do so, we use the fact that λΠ/≡ allows the declaration of rewriting rules, so that Prf (A ⇒ A) rewrites to Prf A → Prf A.

Prf (x ⇒ y) → Prf x → Prf y (⇒-red)
This rule expresses the meaning of the constant ⇒. It is, in λΠ/≡, the expression of the Brouwer-Heyting-Kolmogorov interpretation of proofs for implication: a proof of x ⇒ y is a function mapping proofs of x to proofs of y. So, in the theory U, the Brouwer-Heyting-Kolmogorov interpretation of proofs for implication is made explicit: it is the rule (⇒-red).

3.5. Universal quantification. Unlike implication, the universal quantifier binds a variable. Thus, we express the proposition ∀z A as the proposition ∀ (λz : I, A) [Chu40, NM88, Pau93, HHP93], yielding the type I → Prop for the argument of ∀, hence the type (I → Prop) → Prop for the constant ∀ itself.

But, in the theory U, we allow quantification, not only over the variables of type I, but over variables of any type of object-terms. We could introduce a different quantifier for each type of object-terms, for instance two quantifiers of type (I 1 → Prop) → Prop and (I 2 → Prop) → Prop if we had two types I 1 and I 2 of object-terms. But, as in some cases, we will have an infinite number of types of object-terms, this would require the introduction of an infinite number of constants.

Thus, we rather want to have a single generic quantifier. But we cannot give the type ΠX : TYPE, (X → Prop) → Prop to this quantifier, first because in λΠ/≡ there is no way to quantifiy over a variable of type TYPE, but also because this would introduce the possibility to quantify over Prop and all the types of the form Prf A, while we do not always want to consider these types as types of object-terms.

Therefore, in the theory The types of object-terms then have the form El A and are distinguished among the other terms of type TYPE.

We can now give the type Πx : Set, (El x → Prop) → Prop to the generic universal quantifier

∀ : Πx : Set, (El x → Prop) → Prop (∀-decl)
and write ∀ ι (λz : I, A) for the proposition ∀z A.

Just like for the implication, we declare a rewriting rule expressing that the type of the proofs of the proposition ∀ x p is the type of functions mapping each z of type El x to a proof of p z

Prf (∀ x p) → Πz : El x, Prf (p z) (∀-red)
Again, the Brouwer-Heyting-Kolmogorov interpretation of proofs for the universal quantifier is made explicit: it is this rule (∀-red).

3.6. Other constructive connectives and quantifiers. The other connectives and quantifiers are defined à la Russell. For the conjunction, for example, Prf (x ∧ y) is defined as Πz : Prop, (Prf x → Prf y → Prf z) → Prf z. This definition does not use the quantifier ∀ of the theory U (so far, in the theory U, we can quantify over the type I, but not over the type Prop), but the quantifier Π of the logical framework λΠ/≡ itself.

Remark that, per se, the quantification on the variable z of type Prop is predicative, as the term Πz : Prop, (Prf x → Prf y → Prf z) → Prf z has type TYPE and not Prop. But, the rule rewriting Prf (x ∧ y) to Πz : Prop, (Prf x → Prf y → Prf z) → Prf z introduces some impredicativity, as the term x ∧ y of type Prop is "defined" as the inverse image, for the embedding Prf, of the type Πz : Prop, (Prf x → Prf y → Prf z) → Prf z, that contains a quantification on a variable of type Prop

: Prop ( -decl) Prf → Πz : Prop, Prf z → Prf z ( -red) ⊥ : Prop (⊥-decl) Prf ⊥ → Πz : Prop, Prf z (⊥-red) ¬ : Prop → Prop (¬-decl) Prf (¬ x) → Prf x → Πz : Prop, Prf z (¬-red) ∧ : Prop → Prop → Prop (written infix) (∧-decl) Prf (x ∧ y) → Πz : Prop, (Prf x → Prf y → Prf z) → Prf z (∧-red) ∨ : Prop → Prop → Prop (written infix) (∨-decl) Prf (x ∨ y) → Πz : Prop, (Prf x → Prf z) → (Prf y → Prf z) → Prf z (∨-red) ∃ : Πa : Set, (El a → Prop) → Prop (∃-decl) Prf (∃ a p) → Πz : Prop, (Πx : El a, Prf (p x) → Prf z) → Prf z
(∃-red) 12:7 3.7. Infinity. Now that we have the symbols and ⊥, we can express that the type I is infinite, that is, that there exists a non-surjective injection from this type to itself. We call this non-surjective injection succ. To express its injectivity, we introduce its left inverse pred.

To express its non-surjectivity, we introduce an element 0, that is not in its image positive [START_REF] Dowek | Arithmetic as a theory modulo[END_REF]. This choice of notation enables the definition of natural numbers as some elements of type I

0 : I (0-decl) succ : I → I (succ-decl) pred : I → I (pred-decl) pred 0 → 0 (pred-red1) pred (succ x) → x (pred-red2) positive : I → Prop (positive-decl) positive 0 → ⊥ (positive-red1) positive (succ x) → (positive-red2)
3.8. Classical connectives and quantifiers. The disjunction in constructive logic and in classical logic are governed by different deduction rules. As the deduction rules express the meaning of the connectives and quantifiers, we can conclude that the disjunction in constructive logic and in classical logic have different meanings. If these disjunctions have different meanings, they should be expressed with different symbols, for instance ∨ for the constructive disjunction and ∨ c for the classical one, just like, in classical logic, we use two different symbols for the inclusive disjunction and the exclusive one.

The constructive and the classical disjunction need not belong to different languages, but they can coexist in the same. Ecumenical logics [Pra15, Dow15, PR17, Gri19] are logics where the constructive and classical connectives and quantifiers coexist. A proposition whose connectors and quantifiers are all constructive, is said to be "purely constructive", and one whose connectors and quantifiers are all classical, is said to be "purely classical". The others are said to be "mixed propositions". Any deductive system, where a purely constructive proposition is provable if and only if it is provable in Constructive predicate logic, and where a purely classical proposition is provable if and only if it is provable in Classical predicate logic, is Ecumenical. Ecumenical logics may of course differ on mixed propositions.

Many Ecumenical logics consider the constructive connectives and quantifiers as primitive and attempt to define the classical ones from them, using the negative translation as a definition. There are several options: the classical disjunction, for instance, can be defined in any of the following ways:

(1)

A ∨ c B = ¬¬(A ∨ B) (2) A ∨ c B = (¬¬A) ∨ (¬¬B) (3) A ∨ c B = ¬¬((¬¬A) ∨ (¬¬B))
and similarly for the other connectives and quantifiers.

Using these definitions, the proposition (P ∧ c Q) ⇒ c P is then:

(1) ¬¬((¬¬ None of them is exactly the negative translation of (P ∧ Q) ⇒ P that is

(P ∧ Q)) ⇒ P ) (2) (¬¬((¬¬P ) ∧ (¬¬Q))) ⇒ (¬¬P ) (3) ¬¬((¬¬¬¬((¬¬P ) ∧ (¬¬Q))) ⇒ (¬¬P ))
¬¬((¬¬((¬¬P ) ∧ (¬¬Q))) ⇒ (¬¬P ))
With Definition (1), the double negations on atomic propositions are missing. This can be repaired in two ways. Predicate symbols of the language can be duplicated [START_REF] Prawitz | Classical versus intuitionistic logic[END_REF] into a constructive and a classical counterpart, the latter being the the double negation of the former. Or the syntax of predicate logic can be modified [START_REF] Gilbert | Extending higher-order logic with predicate subtyping: Application to PVS[END_REF]. First, terms are defined. Then, atoms are defined as terms of the form P (t 1 , . . . , t n ) where P is a predicate symbol and t 1 , . . . , t n are terms. Finally, propositions are defined as either explicitly embedded atoms, conjunctions of two propositions, etc. Atoms can be constructively embedded into propositions with the symbol £ or classically with a double-negation version of £. This way, the proposition above is now written

(£ c P ∧ c £ c Q) ⇒ c £ c P , which is, by definition, equal to ¬¬((¬¬((¬¬ £ P ) ∧ (¬¬ £ Q))) ⇒ (¬¬ £ P )).
With Definition (2) [START_REF] Allali | Semantic A-translation and super-consistency entail classical cut elimination[END_REF], the double negation at the root of the proposition is missing. This again can be repaired [START_REF] Grienenberger | A logical system for an Ecumenical formalization of mathematics[END_REF] by modifying the syntax of Predicate logic, defining first terms, then pre-propositions, that are defined like the propositions in Predicate logic and then propositions, a proposition being obtained by applying a symbol • c to a preproposition. Again, this symbol has also a classical version defined as the double negation of the constructive one. This way, the proposition above is written

• c ((P ∧ c Q) ⇒ c P ) and this proposition is, by definition, equal to ¬¬((¬¬((¬¬P ) ∧ (¬¬Q))) ⇒ (¬¬P )).
Definition (3) [START_REF] Dowek | On the definition of the classical connectives and quantifiers[END_REF] is closer to the negative translation except that, in some places, the two negations are replaced with four. But, as ¬¬¬A is equivalent to ¬A, these extra negations can be removed. Yet, a classical atomic proposition P is the same as its constructive version, while its negative translation is ¬¬P , and in (1) P c or £ c P is equal to ¬¬P , as well as • c P in (2). As atomic propositions are not provable anyway, this does not affect provability. But it affects hypothetical provability, leading to duplicate the notion of entailment.

In the theory U, we use Definition (2). Indeed, as we already have a distinction between the proposition A and the type Prf A of its proofs, we can just include the symbol

• c into the constant Prf introducing a classical version Prf c of this constant Prf c : Prop → TYPE (Prf c -decl) Prf c → λx : Prop, Prf (¬ ¬ x) (Prf c -red)
We can then define the classical connectives and quantifiers as follows

⇒ c : Prop → Prop → Prop (written infix) (⇒ c -decl) ⇒ c → λx : Prop, λy : Prop, (¬ ¬ x) ⇒ (¬ ¬ y) (⇒ c -red) ∧ c : Prop → Prop → Prop (written infix) (∧ c -decl) ∧ c → λx : Prop, λy : Prop, (¬ ¬ x) ∧ (¬ ¬ y) (∧ c -red) ∨ c : Prop → Prop → Prop (written infix) (∨ c -decl) ∨ c → λx : Prop, λy : Prop, (¬ ¬ x) ∨ (¬ ¬ y) (∨ c -red) ∀ c : Πa : Set, (El a → Prop) → Prop (∀ c -decl) ∀ c → λa : Set, λp : (El a → Prop), ∀ a (λx : El a, ¬ ¬(p x)) (∀ c -red) ∃ c : Πa : Set, (El a → Prop) → Prop (∃ c -decl) ∃ c → λa : Set, λp : (El a → Prop), ∃ a (λx : El a, ¬ ¬(p x)) (∃ c -red)
Vol. 19:1

A MODULAR CONSTRUCTION OF TYPE THEORIES 12:9

3.9. Propositions as objects. So far, we have mainly reconstructed the Predicate logic notions of object-term, proposition, and proof. We can now turn to two notions coming from Simple type theory: propositions as objects and functionality. Simple type theory is often presented as an independent system, but it can be expressed in several logical frameworks, such as Predicate logic, Isabelle, Deduction modulo theory, Pure type systems, and also λΠ/≡. Yet, the relation between Predicate logic and Simple type theory is complex because

• Simple type theory can be expressed in Predicate logic • and Predicate logic is a restriction of Simple type theory, allowing quantification on variables of type ι only.

So, in Predicate logic, we can express Simple type theory, that contains, as a restriction, Predicate logic, in which we can express Simple type theory, that contains, as a restriction, Predicate logic, in which we can express Simple type theory, that contains, etc. Stacking encodings in this way leads to nonsensical expressions of Simple type theory. But this remark shows that, after having reconstructed Predicate logic in λΠ/≡, we have a choice: we can either express Simple type theory in Predicate logic, that is itself expressed in λΠ/≡, or express Simple type theory directly in λΠ/≡, letting Predicate logic be, a posteriori, a restriction of it, that is, build Simple type theory, not in Predicate logic, but as an extension of Predicate logic.

In the theory U, we choose the second option that leads to a simpler expression of Simple type theory, avoiding the stacking of two encodings. Simple type theory is thus expressed by adding two axioms on top of Predicate logic: one for propositions as objects and one for functionality.

Let us start with propositions as objects. So far, the term ι is the only closed term of type Set. So, we can only quantify over the variables of type El ι, that is I. In particular, we cannot quantify over propositions.

El (x Y y) → El x → El y (Y-red)
For instance, these rules enable the construction of the λΠ/≡ term ι Y ι of type Set that expresses the simple type ι → ι. The λΠ/≡ term El (ι Y ι) of type TYPE rewrites to I → I. The simply typed term λx : ι, x of type ι → ι is then expressed as the term λx : I, x of type I → I that is, El (ι Y ι).

3.11. Dependent arrow. The axiom (Y) enables us to give simple types to the objectterms expressing functions. We can also give them dependent types, with the dependent versions of this axiom

Y d : Πx : Set, (El x → Set) → Set (written infix) (Y d -decl) El (x Y d y) → Πz : El x, El (y z) (Y d -red)
Note that, if we apply the constant Y d to a term t and a term λz : El t, u, where the variable z does not occur in u, then El (t Y d λz : El t, u) rewrites to El t → El u, just like El (t Y u). Thus, the constant Y d is useful only if we can build a term λz : El t, u where the variable z occurs in u. With the symbols we have introduced so far, this is not possible. The only constants that can be used to build a term of type Set are ι, o, Y, and Y d , and the variable z cannot occur free in a term built from these four constants and a variable z of type El t.

Just like we have a constant ι of type Set, we could add a constant array of type I → Set such that array n is the type of arrays of length n. We could then construct the term (ι Y d λn : I, array n) of type Set. Then, the type El (ι Y d λn : I, array n) that rewrites to Πn : I, El (array n), would be the type of functions mapping a natural number n to an array of length n.

So, this symbol Y d becomes useful, only if we add such a constant array, object-level dependent types, or the symbols π or psub below.

3.12. Dependent implication. In the same way, we can add a dependent implication, where, in the proposition A ⇒ B, the proof of A may occur in B

⇒ d : Πx : Prop, (Prf x → Prop) → Prop (written infix) (⇒ d -decl) Prf (x ⇒ d y) → Πz : Prf x, Prf (y z) (⇒ d -red)
3.13. Proofs in object-terms. To construct an object-term, we sometimes want to apply a function symbol to other object-terms and also to proofs. For instance, we may want to apply the Euclidean division div to two numbers t and u and to a proof that u is positive. We would like the type of div to be something like

El (ι Y ι Y d λy : I, (positive y Y ι))
But the term (positive y Yι) is not well typed, as the constant Y expects, as a first argument, a term of type Set and not of type Prop, that is, a type of object-terms and not of proofs. Thus, we must declare another constant π : Prop → Set → Set and a rewriting rule El (π x y) → (Prf x) → (El y) 12:11 Just like for the constant Y and ⇒, we can also have a dependent version of this constant. In fact, in the theory U, we only have this dependent version

π : Πx : Prop, (Prf x → Set) → Set (π-decl) El (π x y) → Πz : Prf x, El (y z) (π-red)
This way, we can give, to the constant div , the type The proposition x/y = x/y is well-formed, but it contains, besides x and y, an implicit free variable p, for a proof of y > 0. This variable is bound by the implication, that needs therefore to be a dependent implication. Hence, the only free variables in y > 0 ⇒ x/y = x/y are x and y.

3.14. Proof irrelevance. If p and q are two non convertible proofs of the proposition positive 2, the terms div 7 2 p and div 7 2 q are not convertible. As a consequence, the proposition = ι (div 7 2 p) (div 7 2 q)

would not be provable.

To make these terms convertible, we embed the theory into an extended one, that contains another constant

div † : El (ι Y ι Y ι)
and a rule div x y p → div † x y and we define convertibility in this extended theory. This way, the terms div 7 2 p and div 7 2 q are convertible, as they both reduce to div † 7 2.

Note that, in the extended theory, the constant div † enables the construction of the erroneous term div † 1 0. But the extended theory is only used to define the convertibility in the restricted one and this term is not a term of the restricted theory. It is not even the reduct of a term of the form div 1 0 r [FT19, BH21].

12:12 F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet, and F. Thiré

Vol. 19:1 3.15. Dependent pairs and predicate subtyping. Instead of declaring a constant div that takes three arguments: a number t, a number u, and a proof p that u is positive, we can declare a constant that takes two arguments: a number t and a pair pair ι positive u p formed with a number u and a proof p that u is positive.

The type of the pair pair ι positive u p whose first element is a number and the second a proof that this number is positive is written psub ι positive, or informally {x : ι | positive x}. It can be called "the type of positive numbers", especially if the pair is proof-irrelevant in its second argument. It is a subtype of the type of natural numbers defined with the predicate positive. Therefore, the symbol psub introduces predicate subtyping.

We thus declare a constant psub and a constant pair To avoid introducing a new positive number pair ι positive 3 p with each proof p that 3 is positive, we make this symbol pair proof irrelevant by introducing a symbol pair † and a rewriting rule that discards the proof

pair † : Πt : Set, Πp : El t → Prop, El t → El (psub t p) (pair † -decl) pair t p m h → pair † t p m (pair-red)
This declaration and this rewriting rule are not part of the theory U but of the theory U † used to define the conversion on the terms of U.

Finally, we declare the projections fst and snd together with an associated rewriting rule fst : Πt : Set, Πp : El t → Prop, El (psub t p) → El t (fst-decl) fst t p (pair † t p m) → m (fst-red) snd : Πt : Set, Πp : El t → Prop, Πm : El (psub t p), Prf (p (fst t p m))

(snd-decl)

Note that the left hand side of the rule (fst-red) is not well-typed, but it can match a well-typed term fst A B (pair † A B m). Yet, we prefer this rule to the non linear one fst t p (pair † t p m) → m that would make confluence proofs more difficult.

Note that there is no rewriting rule for the second projection as the second element of pairs is discarded during rewriting. To make this type an element of the image of an embedding we can introduce dependent types at the level of objects-terms. To do so, we introduce a constant Set1 of type TYPE and a constant set of type Set1 The type I → Set, is now equivalent to Ty (ι d (λn : I, set)) and is thus in the image of the embedding Ty. One could think in simply taking set : Set, saving constants Set1, Ty and d and their rewrite rules. However, such a declaration would encode the product ( , , ) of system λU -which is inconsistent [START_REF] Th | An analysis of Girard's paradox[END_REF][START_REF] Hurkens | A simplification of Girard's paradox[END_REF].

3.17. Prenex predicative type quantification in types. Using the symbols of the theory U introduced so far, the symbol for equality = has the type Πx : Set, El x → El x → Prop which is not a type of object terms. This motivates the introduction of object-level polymorphism [START_REF] Girard | Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur[END_REF][START_REF] Reynolds | Towards a theory of type structure[END_REF]. However extending Simple type theory with object-level polymorphism makes it inconsistent [START_REF] Hurkens | A simplification of Girard's paradox[END_REF][START_REF] Th | An analysis of Girard's paradox[END_REF], and similarly it makes the theory U inconsistent. So, object-level polymorphism in U is restricted to prenex polymorphism.

To do so, we introduce a new constant Scheme of type TYPE Scheme : TYPE (Scheme-decl) a constant Els to embed the terms of type Scheme into terms of type TYPE Els : Scheme → TYPE (Els-decl) a constant ↑ to embed the terms of type Set into terms of type Scheme and a rule connecting these embeddings

↑ : Set → Scheme (↑-decl) Els (↑ x) → El x (↑-red)
We then introduce a quantifier for the variables of type Set in the terms of type Scheme and the associated rewriting rule

A : (Set → Scheme) → Scheme ( A -decl) Els ( A p) → Πx : Set, Els (p x) ( A -red)
This way, the type of the identity function is Els ( A (λx : Set, ↑ (x Y x))). It reduces to Πx : Set, El x → El x. Therefore, it is inhabited by the term λx : Set, λy : El x, y. In a similar way, the symbol = can then be given the type Els ( A (λx : Set, ↑ (x Y x Y o))) that reduces to Πx : Set, El x → El x → Prop.

12:14 F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet, and F. Thiré

Vol. 19:1 3.18. Prenex predicative type quantification in propositions. When we express the reflexivity of the polymorphic equality, we need also to quantify over a type variable, but now in a proposition. To be able to do so, we introduce another quantifier and its associated rewriting rule

A : (Set → Prop) → Prop ( A -decl) Prf ( A p) → Πx : Set, Prf (p x) ( A -red)
This way, the reflexivity of equality can be expressed as ( A (λs : Set, ∀ s (λx : El s, = s x x))).

3.19.

The theory U: putting everything together. As mentioned in Section 2, we call "axiom" a constant declaration together with its rewrite rules if any. Hence, in the following, we denote by (ι) the axiom consisting of (ι-decl) and (ι-red), and similarly for all the other axioms.

The theory U is then formed with 43 axioms: (I), (Set), (El), (ι), (Prop), (Prf), (⇒), (∀), ( ), (⊥), (¬), (∧), (∨), (∃), (Prf c ), (⇒ c ), (∧ c ), (∨ c ), (∀ c ), (∃ c ), (o), (Y), (Y d ), (⇒ d ), (π), (0), (succ), (pred), (positive), (psub), (pair), (pair † ), (fst), (snd), (Set1), (set), ( d ), (Ty), (Scheme), (Els), (↑), ( A ), ( A ). Note that, strictly speaking, the declaration (pair † -decl) and the rule (pair-red) are not part of the theory U, but of its extension U † used to define the conversion on the terms of U.

Among these axioms, 14 only have a constant declaration, 27 have a constant declaration and one rewriting rule, and 2 have a constant declaration and two rewriting rules. So Σ U contains 43 declarations and R U 31 rules.

This large number of axioms is explained by the fact that λΠ/≡ is a weaker framework than Predicate logic. The 20 first axioms are needed just to construct notions that are primitive in Predicate logic: terms, propositions, with their 13 constructive and classical connectives and quantifiers, and proofs. So the theory U is just 23 axioms on top of the definition of Predicate logic.

It is also explained by the fact that axioms are more atomic than in Predicate logic: 4 axioms are needed to express "the" axiom of infinity: (0), (succ), (pred), and (positive); 5 to express predicate subtyping: (psub), (pair), (pair † ), (fst), and (snd); 4 to express dependent types: (Set1),(set),( d ),(Ty); and 5 to express prenex polymorphism: (Scheme), (Els), (↑), ( A ), and ( A ). The 5 remaining axioms express propositions as objects (o); various forms of functionality: (Y), (Y d ), and (π); and dependent implication (⇒ d ).

Sub-theories

Not all proofs require all these axioms. Many proofs can be expressed in sub-theories built by bringing together some of the axioms of U, but not all.

Given subsets Σ S of Σ U and R S of R U , we would like to be sure that a proof in U, using only constants in Σ S , is a proof in (Σ S , R S ). Such a result is trivial in Predicate logic: for instance, a proof in ZFC which does not use the axiom of choice is a proof in ZF, but it is less straightforward in λΠ/≡, because (Σ S , R S ) might not be a theory. So we should not consider any pair (Σ S , R S ). For instance, as Set occurs in the type of El, if we want El in Σ S , we must take Set as well. In the same way, as positive (succ x) rewrites to , if we want (positive) and (succ) in Σ S , we must include in Σ S and the rule rewriting positive (succ x) to in R S .

Proof. The relation → βR U is confluent on Λ(Σ U ) since it is an orthogonal combinatory reduction system [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF]. Hence, after the fragment theorem, it is sufficient to prove that every rule of R U preserves typing in any fragment (Σ 1 , R 1 ) containing the symbols of the rule.

To this end, we will use the criterion described in [Bla20, Theorem 19] which consists in computing the equations that must be satisfied for a rule left-hand side to be typable, which are system-independent, and then check that the right-hand side has the same type modulo these equations in the desired system: for all rules l → r ∈ Λ(Σ 1 ), sets of equations E and terms T , if the inferred type of l is T , the typability constraints of l are E, and r has type type T in the system Λ(Σ 1 ) whose conversion relation ≡ βRE has been enriched with E, then l → r preserves typing in Λ(Σ 1 ).

This criterion can easily be checked for all the rules but (pred-red2) and (fst-red) because, except in those two cases, the left-hand side and the right-hand side have the same type.

In (pred-red2), pred (succ x) → x, the left-hand side has type I if the equation type(x) = I is satisfied. Modulo this equation, the right-hand side has type I in any fragment containing the symbols of the rule.

In (fst-red), fst t p (pair † t p m) → m, the left-hand side has type El t if type(t) = Set, type(p) = El t → P rop, El (psub t p ) = El (psub t p), type(t ) = Set, type(p ) = El t → P rop, and type(m) = El t . But, in U, there is no rule of the form El (psub t p) → r. Hence, by confluence, the equation El (psub t p ) = El (psub t p) is equivalent to the equations t = t and p = p. Therefore, the right-hand side is of type El t in every fragment of U containing the symbols of the rule.

Examples of sub-theories of the theory U

We finally identify 15 sub-theories of the theory U, that correspond to known theories. For each of these sub-theories (Σ S , R S ), according to the Corollary 4.6, if Γ, t, and A are in Λ(Σ S ), and Γ Σ U ,R U t : A, then Γ R S ,Σ S t : A. 12:19

succ pred positive pair † 0 Y d Scheme, Els, ↑, A , A π ⇒ d Set1 set Ty, d psub, pair, fst, snd Prf c , ⇒ c , ∧ c , ∨ c , ∀ c , ∃ c Y o , ⊥, ¬, ∧, ∨, ∃ I, Set, ι, El ∀ ⇒ Prop, Prf

I : TYPE

Set : TYPE El : Set → TYPE ι : Set El ι → I Prop : TYPE Prf : Prop → TYPE ⇒ : Prop → Prop → Prop Prf (x ⇒ y) → Prf x → Prf y ∀ : Πx : Set, (El x → Prop) → Prop Prf (∀ x p) → Πz : El x, Prf (p z)
We could save the declaration (I-decl) and the rule (ι-red) by using El ι instead of I.

This theory can be proven equivalent to more common formulations of Minimal predicate logic. To do so, consider a language L in predicate logic. We define a corresponding λΠ/≡ context Γ L containing for each constant f of L a constant f of type I → . . . → I → I and for each predicate symbol P of L a constant P of type I → . . . → I → Prop. A term (resp. a proposition) of minimal predicate logic t of L translates in the natural way to a λΠ/≡ term of type I (resp. Prop) in the theory (Σ M , R M ) and in the context Γ L , ∆, where ∆ contains, for each variable x free in t, a variable x of type I. We use the same notation for the term (resp. the proposition) and its translation.

Theorem 5.1. Let L be a language and A 1 , ..., A n B be a sequent of minimal predicate logic in L. Let Γ L containing for each constant f of L a constant f of type I → . . . → I → I and for each predicate symbol P of L a constant P of type I → . . . → I → Prop. Let ∆ be a context containing for each variable x free in A 1 , ..., A n B, a variable x of type I. Let ∆ be a context containing, for each hypothesis A i , a variable a i of type Prf A i .

Then, the sequent A 1 , ..., A n B has a proof in minimal logic, if and only if there exists a λΠ/≡ term π such that

Γ L , ∆, ∆ Σ M ,R M π : Prf B.
Proof. The left-to-right implication is a trivial induction on the structure of the proof.

For the converse, it is enough to consider an irreducible term π of type Prf B since one can prove that → βR M terminates, by applying [START_REF] Blanqui | Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting[END_REF] for instance. We then prove, by induction on π, that the sequent A 1 , ..., A n B has a proof in minimal logic. As π has the type Prf B, it is neither a sort, nor a product, thus it is either an abstraction or a term of the form z ρ 1 ... ρ p .

• If π is an abstraction then Prf B is equivalent to a product. Hence, B either has the form C ⇒ D or ∀ ι λx : I, D. In the first case π = λx : Prf C, π and π is a term of type Prf D in Γ L , ∆, ∆ , x : Prf C. By induction hypothesis, the sequent A 1 , ..., A n , C D has a proof and so does the sequent A 1 , ..., A n C ⇒ D. In the second π = λx : I, π and π is a term of type Prf D in Γ L , ∆, x : I, ∆ . By induction hypothesis, the sequent A 1 , ..., A n D has a proof and so does the sequent A 1 , ..., A n ∀ ι λx : I, D. • If π has the form z ρ 1 ... ρ p , then as it has the type Prf B, z can neither be a constant of Σ M , nor a variable of Γ L , ∆. Hence, it is a variable of ∆ . Thus, it has the type Prf A i for some i. We prove, by induction on j that the term z ρ 1 ... ρ j has the type Prf C for some proposition C, such that the sequent A 1 , ..., A n C has a proof. For j = 0, the sequent A 1 , ..., A n A i has a proof. Assume the property holds for j. Then, as the term z ρ 1 ... ρ j ρ j+1 is well typed, the type Prf C is a product type and C either has the form D ⇒ E or ∀ ι λx : I, E. In the first case ρ j+1 is a term of type Prf D, by induction hypothesis, the sequent A 1 , ..., A n D has a proof, hence the term z ρ 1 ... ρ j ρ j+1 has the type Prf E and the sequent A 1 , ..., A n E has a proof. In the second case, ρ j+1 is an irreducible term of type I, thus it is an object-term, the term z ρ 1 ... ρ j ρ j+1 has the type Prf (ρ j+1 /x)E, and the sequent A 1 , ..., A n (ρ j+1 /x)E has a proof.

As Minimal predicate logic is itself a logical framework, it must be complemented with more axioms, such as the axioms of geometry, arithmetic, etc. 5.2. Constructive predicate logic. The 14 axioms (I),(Set), (El), (ι), (Prop), (Prf), (⇒), (∀), ( ), (⊥), (¬), (∧), (∨), and (∃) define Constructive predicate logic. This theory can be proven equivalent to more common formulations of Constructive predicate logic [Dor10, ABC + 16]. 5.3. Ecumenical predicate logic. The 20 axioms (I), (Set), (El), (ι), (Prop), (Prf), (⇒), (∀), ( ), (⊥), (¬), (∧), (∨), (∃), (Prf c ), (⇒ c ), (∧ c ), (∨ c ), (∀ c ), and (∃ c ) define Ecumenical predicate logic. This theory can be proven equivalent to more common formulations of Ecumenical predicate logic [START_REF] Grienenberger | Expressing Ecumenical systems in the lambda-pi-calculus modulo theory[END_REF].

Note that classical predicate logic is not a sub-theory of the theory U, because the classical connectives and quantifiers depend on the constructive ones. Yet, it is known that if 12:21 a proposition contains only classical connectives and quantifiers, it is provable in Ecumenical predicate logic if and only if it is provable in classical predicate logic. 5.4. Minimal simple type theory. Adding the two axioms (o) and (Y) to Predicate logic defines Simple type theory. Indeed, Simple type theory is the theory of propositional contents and functions. A simple type T is naturally translated to λΠ/≡ as a term T of type Set, using types ι and o and the arrow construction Y. The higher order terms are shallowly translated: λ-abstractions and applications are translated using respectively λΠ/≡'s λ-abstractions and applications.

The 10 axioms (I), (Set), (ι), (El), (Prop), (Prf), (⇒), (∀), (o), and (Y) define Minimal simple type theory. And this theory can be proven equivalent to more common formulations of Minimal simple type theory [Ass15, ABC + 16]. Just like we can save the declaration (I-decl) and the rule (ι-red) by replacing everywhere I with El ι, we could save the declaration (Prop-decl) and the rule (o-red) by replacing everywhere Prop with El o. This presentation is the usual presentation of Simple type theory in λΠ/≡ [ABC + 16] with 8 declarations and 3 reduction rules. However, doing so, the obtained presentation of Simple type theory is not an extension of Minimal predicate logic anymore. 5.5. Constructive simple type theory. The 16 axioms (I), (Set), (El), (ι), (Prop), (Prf), (⇒), (∀), ( ), (⊥), (¬), (∧), (∨), (∃), (o) and (Y) define Constructive simple type theory. 5.6. Ecumenical simple type theory. The 22 axioms (I), (Set), (El), (ι), (Prop), (Prf), (⇒), (∀), ( ), (⊥), (¬), (∧), (∨), (∃), (Prf c ), (⇒ c ), (∧ c ), (∨ c ), (∀ c ), (∃ c ), (o) and (Y) define Ecumenical simple type theory. And this theory can be proven equivalent to more common formulations of Ecumenical simple type theory [START_REF] Grienenberger | Expressing Ecumenical systems in the lambda-pi-calculus modulo theory[END_REF]. 5.7. Simple type theory with predicate subtyping. Adding to the 10 axioms of Minimal simple type theory the 5 axioms of predicate subtyping yields Minimal simple type theory with predicate subtyping, formed with the 15 axioms (I), (Set), (ι), (El), (Prop), (Prf), (⇒), (∀), (o), (Y), (psub), (pair), (pair † ), (fst), and (snd). This theory has been studied by F. Gilbert [START_REF] Gilbert | Extending higher-order logic with predicate subtyping: Application to PVS[END_REF] as a verifiable language for a minimal and idealised version of the type system of the PVS proof assistant. It can be proven equivalent to more common formulations of Minimal simple type theory with predicate subtyping [START_REF] Gilbert | Extending higher-order logic with predicate subtyping: Application to PVS[END_REF][START_REF] Blanqui | Encoding of predicate subtyping and proof irrelevance in the λπcalculus modulo theory[END_REF]. Such formulations like PVS [START_REF] Owre | The Formal Semantics of PVS[END_REF] often use predicate subtyping implicitly to provide a lighter syntax without (pair), (pair † ), (fst) nor (snd) but at the expense of losing uniqueness of type and making type-checking undecidable. In these cases, terms generally do not hold the proofs needed to be of a sub-type, which provides proof irrelevance. Our implementation of proof irrelevance of Section 3.14 extends the conversion in order to ignore these proofs. 5.8. Simple type theory with prenex predicative polymorphism. Adding to the 10 axioms of Minimal simple type theory the 5 axioms of prenex predicative polymorphism yields Simple type theory with prenex predicative polymorphism (STT∀) [START_REF] Thiré | Sharing a Library between Proof Assistants: Reaching out to the HOL Family[END_REF][START_REF] Thiré | Interoperability between proof systems using the Dedukti logical framework[END_REF] formed with the 15 axioms (I), (Set), (El), (ι), (Prop), (Prf), (⇒), (∀), (o), (Y), (Scheme), (Els), (↑), ( A ), and ( A ).

5.9. Simple type theory with predicate subtyping and prenex polymorphism.

Adding to the 10 axioms of Minimal simple type theory both the 5 axioms of predicate subtyping and the 5 axioms of prenex polymorphism yields a sub-theory with 20 axioms which is a subsystem of PVS [START_REF] Owre | The Formal Semantics of PVS[END_REF] handling both predicate subtyping and prenex polymorphism.

5.10. The Calculus of constructions. Pure type systems [START_REF] Berardi | Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube[END_REF][START_REF] Terlouw | Een nadere bewijstheoretische analyse van GSTT's[END_REF][START_REF] Barendregt | Lambda calculi with types[END_REF] are a family of typed λ-calculi. An example is the λΠ-calculus, the λ-calculus with dependent types, which is at the basis of λΠ/≡ itself. As we have seen, in λΠ/≡, we have two constants, TYPE and KIND, TYPE has type KIND, and we can build a product type Πx : A, B when both A and B have type TYPE, in which case the product type Πx : A, B itself has type TYPE or when A has type TYPE and B has type KIND, in which case the result has type KIND. A Pure type system, in general, is defined with a set of symbols, such as TYPE and KIND, called "sorts", a set of axioms of the form s 1 , s 2 , expressing that the sort s 1 has type s 2 , for example TYPE, KIND , and a set of rules of the form s 1 , s 2 , s 3 , expressing that we can build the product type Πx : A, B, when A has type s 1 and B has type s 2 , and that the product type itself has type s 3 , for example TYPE, TYPE, TYPE and TYPE, KIND, KIND . When the set of axioms is functional, each sort has at most one type and when the set of rules is functional, each product type has at most one type. In this case the Pure type system is said to be "functional".

To have more compact notation, we often write * for the sort TYPE and P for the sort KIND. So the λΠ-calculus is defined with the sorts * and P, the axiom * , P , and the rules * , * , * and * , P, P . Adding the rules P, * , * and P, P, P yields the Calculus of constructions [START_REF] Th | The calculus of constructions[END_REF].

All functional Pure type systems can be expressed in λΠ/≡ [CD07]: for each sorts s, we introduce two constants U s of type TYPE and ε s of type U s → TYPE, for each axiom s 1 , s 2 , a constant ṡ1 of type U s 2 , and a reduction rule

ε s 2 ṡ1 → U s 1
and for each rule s 1 , s 2 , s 3 , a constant Π s 1 ,s 2 ,s 3 of type Πx : U s 1 , (ε s 1 x → U s 2 ) → U s 3 and a reduction rule

ε s 3 ( Π s 1 ,s 2 ,s 3 x y) → Πz : ε s 1 x, ε s 2 (y z)
We obtain this way a correct and conservative expression of the Pure type system [CD07 So if Γ is a context and A is a term in the Calculus of constructions then A is inhabited in Γ in the Calculus of constructions if and only if the translation A of A in λΠ/≡ is inhabited in the translation Γ of Γ in λΠ/≡ [CD07, ABC + 16]. So, the formulation of the Calculus of constructions in λΠ/≡ is a conservative extension of the original formulation of the Calculus of constructions. In the context Γ , variables have a λΠ/≡ type of the form Prf u or El u, and none of them can have the type Set. However, in λΠ/≡, nothing prevents from declaring a variable of type Set. Hence, in λΠ/≡, the judgement x : Set x : Set can be derived, but it is not in the image of the encoding. 5.11. The Calculus of constructions with variables of type P. To allow the declaration of variables of type P in the Calculus of constructions, a possibility is to add a sort and an axiom P : [START_REF] Geuvers | The Calculus of Constructions and Higher Order Logic[END_REF], making the sort a singleton sort that contains only one closed irreducible term: P.

Expressing this Pure type system in λΠ/≡ introduces two declarations for the sort and one declaration and one rule for the axiom P :

• U : TYPE • ε : U → TYPE • Ṗ : U • ε Ṗ → Set
and the variables in a context Γ now have the type Prf u, El u, or ε u. Just like U * is written Prop in U, U is written Set1, ε is written Ty, and Ṗ is written set.

But this theory can be simplified. Indeed, just like P is the only closed irreducible term of type , set is the only closed irreducible term of type Set1 and thus for any closed term t of type Set1, the term Ty t reduces to Set. So, we can replace everywhere the terms of the form Ty t with Set and drop the symbols Ty and set and the rule Ty set → Set. Then, we can drop the symbol Set1 as well.

So the only difference with the Calculus of constructions without is that translations of contexts now contain variables of type Set, that translate the variables of type P. 5.12. The Calculus of constructions with a constant ι : P. Adding the axiom (ι) to the Calculus of constructions yields a sub-theory with the 10 axioms (Set), (El), (ι), (Prop), (Prf), (⇒ d ), (∀), (o), (Y d ), and (π). It corresponds to the Calculus of constructions with an extra constant ι of type P. Adding a constant of type Set in λΠ/≡, like adding variables of type Set does not require to introduce an extra sort . Some developments in the Calculus of constructions choose to declare the types of mathematical objects such as ι, nat, etc. in * , that would correspond to ι : Prop, fully identifying types and propositions. The drawback of this choice is that it gives the type * to the type ι of the constant 0, and the type P to the type ι → * of the constant positive, while, in Simple type theory, both ι and ι → o are simple types. This is the reason why, in the theory U, we give the type Set and not the type Prop to the constant ι. So, the expression of the simple type ι → o uses the constant Y d , that is, type constructors, as both ι and o have type Set, and not the constant π, dependent types, that would be used if ι had the type Prop and o the type Set. Dependent types, the constant π, are thus marginalized to type functions mapping proofs to terms. 5.13. The Minimal sub-theory. Adding the axioms (⇒) and (Y) yields a sub-theory with the 12 axioms (Set), (El), (ι), (Prop), (Prf), (⇒), (∀), (o), (Y), (Y d ), (⇒ d ), and (π) called the "Minimal sub-theory" of the theory U. It contains both the 10 axioms of the Calculus of constructions and the 9 axioms of Minimal simple type theory. It is a formulation of the Calculus of constructions where dependent and non dependent arrows are distinguished. It is not a genuine extension of the Calculus of constructions as, each time we use a non dependent constant Y or ⇒, we can use the dependent ones instead: a term of the form t Y u can always been replaced with the term t Y d λx : El t, u, where the variable x does not occur in u, and similarly for the implication. Thus, any proof expressed in the Minimal sub-theory, in particular any proof expressed in Minimal simple type theory, can always be translated to the Calculus of constructions.

Conversely, a proof expressed in the Calculus of constructions can be expressed in this theory. In a proof, every symbol Y d or ⇒ d that uses a dummy dependency can be replaced with a symbol Y or ⇒. Every proof that does not use Y d , ⇒ d and π, can be expressed in Minimal simple type theory. 5.14. The Calculus of constructions with dependent types at the object level. In the Calculus of constructions with a constant ι of type P, there are no dependent types at the object level. We have types ι → ι and ι → * , thanks to the rule P, P, P , but no type ι → P. We can introduce such dependent types by adding an extra sort , together with an axiom P : and a rule P, , . We obtain this way a Pure type system whose expression in λΠ/≡ [CD07] contains 13 declarations and 7 rules.

Using the same notations as above, Prop for U * , Set for U 2 , Set1 for U , etc., we get exactly the 13 axioms (Prop), (Prf), (Set), (El), (Set1), (Ty), (o), (set), (⇒ d ), (π), (∀), (Y d ), and ( d ). The theory formed with these 13 axioms is thus equivalent to more common formulations of the Calculus of constructions with dependent types at that object level. 5.15. The Calculus of constructions with prenex predicative polymorphism. In the Calculus of constructions with an extra sort , polymorphism at the object level can be added with the rule , P, P that allows to build terms of the form Πx : P, x → x : P at the expense of making the system inconsistent [START_REF] Hurkens | A simplification of Girard's paradox[END_REF][START_REF] Th | An analysis of Girard's paradox[END_REF]. Thus, just like in Simple type theory, we restrict to prenex predicative polymorphism: so, besides the sort , whose only closed irreducible element is P, we introduce a sort for schemes and two rules , P, to build schemes by quantifying over an element of , that is, over P, in a type and , , to build schemes by quantifying over P in another scheme. We also add a rule , * , * to quantify over P in a proposition.

Alternatively, the Calculus of constructions with prenex predicative polymorphism can be defined as a cumulative type system [START_REF] Barras | Auto-validation d'un système de preuves avec familles inductives[END_REF], making P a subsort of and having just one rule , , to quantify over a variable of type P in a scheme and a rule , * , * to quantify over P in a proposition. As there is no function whose co-domain is P, this subtyping does not need to propagate to product types.

Expressing this Cumulative type system in λΠ/≡ introduces 8 declarations and 4 rules on top of the Calculus of constructions: 2 declarations for the sort • a constant U of type TYPE, • and a constant ε of type U → TYPE, 1 declaration and 1 rule for the axiom P :

Conclusion

The theory U is thus a candidate for a universal theory where proofs developed in various proof systems: HOL Light, Isabelle/HOL, HOL 4, Coq, Matita, Lean, PVS, etc. can be expressed. This theory can be complemented with other axioms to handle inductive types, recursive functions, universes, etc. [START_REF] Assaf | A framework for defining computational higher-order logics[END_REF][START_REF] Thiré | Interoperability between proof systems using the Dedukti logical framework[END_REF][START_REF] Genestier | Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting[END_REF]. Note however that the various axioms currently proposed for encoding recursive functions are based on rewriting and may be difficult to translate to systems requiring termination proofs. Using recursors should make this much easier.

Each proof expressed in the theory U can use a sub-theory of the theory U, as if the other axioms did not exist: the classical connectives do not impact the constructive ones, propositions as objects and functionality do not impact predicate logic, dependent types and predicate subtyping do not impact simple types, etc.

The proofs in the theory U can be classified according to the axioms they use, independently of the system they have been developed in. Finally, some proofs using classical connectives and quantifiers, propositions as objects, functionality, dependent types, or predicate subtyping may be translated into smaller fragments and used in systems different from the ones they have been developed in, making the theory U a tool to improve the interoperability between proof systems.

In some cases, a proof can be directly transferred from one system to the other if it does not use some axioms. For instance, [START_REF] Wang | Higher order proof engineering: Proof collaboration, transformation, checking and retrieval[END_REF] showed that many proofs coming from HOL were in fact constructive. However, we usually need to apply some transformations on proofs to transfer them from one sub-theory to the other. For instance, by replacing a dependent arrow by a non-dependent one when the second argument is not actually dependent, by applying some morphism on type universes [START_REF] Thiré | Interoperability between proof systems using the Dedukti logical framework[END_REF], or by trying to eliminate some uses of the excluded middle [START_REF] Cauderlier | A rewrite system for proof constructivization[END_REF], which is part of the axioms of Isabelle/HOL [START_REF] Paulson | Isabelle's logics[END_REF], Lean [START_REF] Carneiro | The type theory of Lean[END_REF] and automated theorem provers. Some of the sub-theories of U are known to be consistent, but one may wonder whether the theory U itself is consistent. We conjecture that it is but leave this difficult problem for future work. A solution may be to extend the model developed by the second author in [START_REF] Dowek | Models and Termination of Proof Reduction in the λΠ-Calculus Modulo Theory[END_REF] for proving the consistency of the encoding of HOL.

El

  (ι Y ι Y d λy : I, π (positive y) (λz : Prf (positive y), ι)) that is I → Πy : I, Prf (positive y) → I In the same way, if we add a symbol = of type Πx : Set, El x → El x → Prop, we can express the proposition positive y ⇒ d λp : Prf (positive y), (= ι (div x y p) (div x y p)) enlightening the meaning of the proposition usually written y > 0 ⇒ x/y = x/y

  psub : Πt : Set, (El t → Prop) → Set (psub-decl) pair : Πt : Set, Πp : El t → Prop, Πm : El t, Prf (p m) → El (psub t p) (pair-decl) This way, instead of giving the type El (ι Y ι Y d λy : Prf (positive y), ι) to the constant div, we can give it the type El (ι Y psub ι positive Y ι).

3. 16 .

 16 Dependent types. When we have the axioms (El), (ι), and (Y), the type I → I of the term succ is equivalent to the type El (ι Y ι). Hence, this type I → I is in the image of the embedding El. The symbol array introduced in Section 3.11 has the type I → Set and similarly if we have a predicate symbol ≤: El (ι Y ι Y o), the term λn : I, psub ι (λm : I, m ≤ n) also has the type I → Set. Unlike the type I → I the type I → Set is not in the image of any embedding. It is well-formed in the framework but not in the theory itself.

  Set1 : TYPE (Set1-decl) set : Set1 (set-decl) 12:13 a new arrow d : Πx : Set, (El x → Set1) → Set1 ( d -decl) and an embedding of Set1 into TYPE, similar to the embeddings Prf and El Ty : Set1 → TYPE (Ty-decl) and we identify Ty set with Set-like El o is identified with Prop-and the dependent arrow d with a product type Ty set → Set (set-red) Ty (x d y) → Πz : El x, Ty (y z) ( d -red)

Figure 2 :

 2 Figure 2: The wind rose. In black: Minimal, Constructive, and Ecumenical predicate logic. In orange: Minimal, Constructive, and Ecumenical simple type theory. In green: Simple type theory with prenex polymorphism. In blue: Simple type theory with predicate subtyping. In cyan: Simple type theory with predicate subtyping and prenex polymorphism. In pink: the Calculus of constructions with a constant ι, without and with prenex polymorphism.

  To do so, we just need to declare a constant o of type Set El ι, that is I, there are no terms of type o, but terms, such as , which have type El o, that is Prop.Applying the constant ∀ to the constant o, we obtain a term of type (El o → Prop) → Prop, that is (Prop → Prop) → Prop, and we can express the proposition ∀p (p ⇒ p) as ∀ o (λp : Prop, p ⇒ p). The type Prf (∀ o (λp : Prop, p ⇒ p)) of the proofs of this proposition rewrites to Πp : Prop, Prf p → Prf p. So, the term λp : Prop, λx : Prf p, x is a proof of this proposition.3.10. Functionality. Besides ι and o, we introduce more types in the theory, for functions and sets. To do so, we declare a constant

o : Set (o-decl) and a rule identifying El o and Prop El o → Prop (o-red) Note that just like there are no terms of type ι, but terms, such as 0, which have type Y : Set → Set → Set (written infix) (Y-decl) and a rewriting rule 12:10 F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet, and F. Thiré Vol. 19:1

  , ABC + 16]. For instance, the expression of the Calculus of constructions yields 9 declarations and 5 rules. Writing Prop for U * , Prf for ε * , Set for U 2 , El for ε 2 , o for * , ⇒ d for Π * , * , * , ∀ for Π 2, * , * , π for Π * ,2,2 , and Y d for Π 2,2,2 we get exactly the 9 axioms (Prop), (Prf), (Set), (El), (o), (⇒ d ), (π), (∀), and (Y d ) and this theory is equivalent to more common formulations of the Calculus of constructions.As⇒ d is Π * , * , * , ∀ is Π 2, * , * , π is Π * ,2,2, and Y d is Π 2,2,2 , using the terminology of Barendregt's λ-cube[START_REF] Barendregt | Lambda calculi with types[END_REF], the axiom (π) expresses dependent types, the axiom (∀) polymorphism, and the axiom (Y d ) type constructors.

Note that these constants have similar types ⇒ d : Πx : Prop, (Prf x → Prop) → Prop π : Πx : Prop, (Prf x → Set) → Set ∀ : Πx : Set, (El x → Prop) → Prop Y d : Πx : Set, (El x → Set) → Set 12:23

(empty)Γ Σ,R A : s Σ,R Γ, x : A well-formed (decl) Σ,R Γ well-formed Γ Σ,R TYPE : KIND (sort) Σ,R Γ well-formed Σ,R A : s Γ Σ,R c : A (const) c : A ∈ Σ Σ,R Γ well-formed Γ Σ,R x : A (var) x : A ∈ Γ Γ Σ,R A : TYPE Γ, x : A Σ,R B : s Γ Σ,R Πx : A, B : s (prod) Γ Σ,R A : TYPE Γ, x : A Σ,R B : s Γ, x : A Σ,R t : B Γ Σ,R λx : A, t : Πx : A, B(abs)

Γ well-formed Γ 0 TYPE : KIND (sort)as Γ is in Λ(Σ

), by induction hypothesis, 1 Γ well-formed is derivable. Thus, by the rule (sort), Γ 1 TYPE : KIND is derivable. So there exists D = KIND in Λ(Σ 1 ) such that KIND → * 0 D and Γ 1 TYPE : D . • If the last rule of the derivation is0 Γ well-formed 0 A : s Γ 0 c : A (const) c : A ∈ Σ 0 as Γ is in Λ(Σ 1 ), by induction hypothesis, 1 Γ well-formed is derivable. And as c is in Λ(Σ 1 ), it is in |Σ 1 |, thus c : A is in Σ 1 and, since (Σ 1 , R 1 ) is a fragment of (Σ 0 , R 0 ), A ∈ Λ(Σ 1 ).Thus, by induction hypothesis, there exists A such that 1 A : A is derivable and s → * 0 A . As s is a sort, A = s. So 1 A : s is derivable. Thus, by the rule (const), Γ 1 c : A is derivable. So, there exists D = A in Λ(Σ 1 ) such that A → * 0 D and Γ 1 c : D is derivable.• If the last rule of the derivation is0 Γ well-formed Γ 0 x : A (var) x : A ∈ Γ as Γ is in Λ(Σ 1 ), by induction hypothesis, 1 Γ well-formed is derivable. Thus, by the rule (var), Γ 1 x : A is derivable. So there exists D = A in Λ(Σ 1 ) such that A → *

12:20 F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet, and F. Thiré

Vol. 19:1

Acknowledgments. The authors want to thank Michael Färber, César Muñoz, Thiago Felicissimo, and Makarius Wenzel for helpful remarks on a first version of this paper, as well as the anonymous reviewers for their useful comments.

Vol. 19:1 A MODULAR CONSTRUCTION OF TYPE THEORIES 12:15

This leads to a definition of a notion of sub-theory and to prove that, if (Σ 1 , R 1 ) is a sub-theory of a theory (Σ 0 , R 0 ), Γ, t and A are in Λ(Σ 1 ), and Γ Σ 0 ,R 0 t : A, then Γ Σ 1 ,R 1 t : A.

This property implies that, if π is a proof of A in U and both A and π are in Λ(Σ 1 ), then π is a proof of A in (Σ 1 , R 1 ), but it does not imply that if A is in Λ(Σ 1 ) and A has a proof in U, then it has a proof in (Σ 1 , R 1 ). 4.1. Fragments. Definition 4.1 (Fragment). A signature Σ 1 is included in a signature Σ 0 , denoted Σ 1 ⊆ Σ 0 , if each declaration c : A of Σ 1 is a declaration of Σ 0 .

A system (Σ 1 , R 1 ) is a fragment of a system (Σ 0 , R 0 ), if the following conditions are satisfied:

Proof. By induction on the position where the rule is applied. We only detail the case of a top reduction, the other cases easily follow by induction hypothesis.

So, let → r be the rule used to rewrite t in u and θ such that t = θ and u = θr. As t ∈ Λ(Σ 1 ), we have ∈ Λ(Σ 1 ) and, for all x free in , θx ∈ Λ(Σ 1 ). Thus, as (Σ 1 , R 1 ) is a fragment of (Σ 0 , R 0 ), r ∈ Λ(Σ 1 ) and → r ∈ R 1 . Therefore t → 1 u and u = θr ∈ Λ(Σ 1 ).

Lemma 4.3 (Preservation of confluence). Every fragment of a confluent system is confluent.

Proof. Let (Σ 1 , R 1 ) be a fragment of a confluent system (Σ 0 , R 0 ). We prove that → 1 is confluent on Λ(Σ 1 ). Assume that t, u, v ∈ Λ(Σ 1 ), t → * 1 u and t → * 1 v. Since |Σ 1 | ⊆ |Σ 0 |, we have t, u, v ∈ Λ(Σ 0 ). Since R 1 ⊆ R 0 , we have t → * 0 u and t → * 0 v. By confluence of → 0 on Λ(Σ 0 ), there exists a w in Λ(Σ 0 ) such that u → * 0 w and v → * 0 w. Since u, v ∈ Λ(Σ 1 ), by Lemma 4.2, w ∈ Λ(Σ 1 ), u → * 1 w and v → * 1 w. Definition 4.4 (Sub-theory). A system (Σ 1 , R 1 ) is a sub-theory of a theory (Σ 0 , R 0 ), if it is a fragment of (Σ 0 , R 0 ) and it is a theory.

As we already know that R 1 is confluent, this amounts to say that each rule of R 1 preserves typing in (Σ 1 , R 1 ). 4.2. The fragment theorem. Theorem 4.5. Let (Σ 0 , R 0 ) be a confluent system and (Σ 1 , R 1 ) be a sub-theory of (Σ 0 , R 0 ). • If the judgement Γ 0 t : D is derivable, Γ ∈ Λ(Σ 1 ) and t ∈ Λ(Σ 1 ), then there exists D ∈ Λ(Σ 1 ) such that D → * 0 D and the judgement Γ 1 t : D is derivable. • If the judgement 0 Γ well-formed is derivable and Γ ∈ Λ(Σ 1 ), then the judgement 1 Γ well-formed is derivable. Proof. By mutual induction on the derivations, and by case analysis on the last typing rule. Before detailing each case, note that the most difficult cases are (abs), (app), and (conv), the other cases are a simple application of the induction hypothesis.

• If the last rule of the derivation is

as Γ, A, and t are in Λ(Σ 1 ), by induction hypothesis, there exists A in Λ(Σ 1 ) such that TYPE → * 0 A and Γ 1 A : A is derivable, and there exists

As B is typable and every subterm of a typable term is typable, KIND does not occur in B. As B → * 0 B and no rule contains KIND, KIND does not occur in B as well. Hence, B = KIND. By Lemma 2.2, as Γ, x : A 1 t : B is derivable and B = KIND, there exists a sort s such that Γ, x : A 1 B : s is derivable.

Thus, by the rule (abs), Γ 1 λx : A, t : Πx :

as Γ, t, and u are in Λ(Σ 1 ), by induction hypothesis, there exist C and A 2 in Λ(Σ 1 ), such that Πx : A, B → * 0 C, Γ 1 t : C is derivable, A → * 0 A 2 , and Γ 1 u : A 2 is derivable. As Πx : A, B → * 0 C and rewriting rules are of the form (c l 1 . . . l n → r), there exist A 1 and B 1 in Λ(Σ 1 ) such that C = Πx : A 1 , B 1 , A → * 0 A 1 , and B → * 0 B 1 . By confluence of → 0 , there exists A such that A 1 → * 0 A and A 2 → * 0 A . By Lemma 4.2, as A 1 ∈ Λ(Σ 1 ) and A 1 → * 0 A , we have A ∈ Λ(Σ 1 ) and A 1 → * 1 A . In a similar way, as A 2 ∈ Λ(Σ 1 ) and A 2 → * 0 A , we have A 2 → * 1 A . By Lemma 2.2, as Γ 1 t : Πx : A 1 , B 1 is derivable and Πx : A 1 , B 1 = KIND, there exists a sort s such that Γ 1 Πx : A 1 , B 1 : s is derivable. Thus, by Lemma 2.2, Γ 1 A 1 : TYPE is derivable.

As Γ 1 Πx : A 1 , B 1 : s, Πx : A 1 , B 1 → * 1 Πx : A , B 1 , and (Σ 1 , R 1 ) preserves typing, Γ 1 Πx : A , B 1 : s is derivable. In a similar way, as Γ 1 A 1 : TYPE is derivable, and

Therefore, by the rule (conv), Γ 1 t : Πx : A , B 1 and Γ 1 u : A are derivable. Therefore, by the rule (app), Γ 1 t u : (u/x)B 1 is derivable. So there exists D = (u/x)B 1 in Λ(Σ 1 ), such that (u/x)B → * 0 D and Γ 1 t u : D is derivable.

as Γ, A, and B are in Λ(Σ 1 ), by induction hypothesis, there exists A in Λ(Σ 1 ) such that TYPE → * 0 A and Γ 1 A : A is derivable and there exists B in Λ(Σ 1 ) such that s → * 0 B and Γ, x : A 1 B : B is derivable. As TYPE and s are sorts, A = TYPE and B = s. Therefore, Γ 1 A : TYPE and Γ, x : A 1 B : s are derivable. Thus, by the rule (prod), Γ 1 Πx : A, B : s is derivable. So there exists D = s in Λ(Σ 1 ) such that s → * 0 D and Γ 1 Πx : A, B : D is derivable.

12:18 F. Blanqui, G. Dowek, E. Grienenberger, G. Hondet, and F. Thiré

Vol. 19:1

Corollary 4.6. Let (Σ 0 , R 0 ) be a confluent system, (Σ 1 , R 1 ) be a sub-theory of (Σ 0 , R 0 ). If Γ 0 t : D, Γ ∈ Λ(Σ 1 ), t ∈ Λ(Σ 1 ), and D ∈ Λ(Σ 1 ), then Γ 1 t : D.

In particular, if (Σ 0 , R 0 ) is a theory, (Σ 1 , R 1 ) is a sub-theory of (Σ 0 , R 0 ), Γ 0 t : D, Γ ∈ Λ(Σ 1 ), t ∈ Λ(Σ 1 ), and D ∈ Λ(Σ 1 ), then Γ 1 t : D. Theorem 4.7 (Sub-theories of U). Every fragment (Σ 1 , R 1 ) of U (including U itself ) is a theory, that is, is confluent and preserves typing. 12:25

• a constant Ṗ of type U ,

• and a rule ε Ṗ → Set (remember that Set is U 2 ), 2 declarations for the sort

• a constant U , that we write Scheme, of type TYPE,

• and a constant ε , that we write Els, of type Scheme → TYPE, 1 declaration and 1 rule to express that P is a subtype of

• and a rule Els (↑ x) → El x (remember that El is ε 2 ), 1 declaration and 1 rule for the rule , ,

• a constant Π , , , that we write A , of type Πz : U , (ε z → Scheme) → Scheme, • and a rule Els But, again, this theory can be simplified. Indeed, just like P is the only closed irreducible term of type , Ṗ is the only closed irreducible term of type U and thus for any closed term t of type U , the term ε t reduces to Set. So in the type of the constants A and A : Πz : U , (ε z → Scheme) → Scheme and Πz : U , (ε z → Prop) → Prop, we can replace the expression ε z with Set. Then, as there is no point in building a function space whose domain is a singleton, we can simplify these type further to (Set → Scheme) → Scheme and (Set → Prop) → Prop. Accordingly, the associated reduction rules simplify to