key: cord-0060852-w3q38d3s
authors: Maruyama, Yoshihiro
title: Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory
date: 2020-04-01
journal: Relational and Algebraic Methods in Computer Science
DOI: 10.1007/978-3-030-43520-2_12
sha: 7d2e92d477298442b75dded5f8bdf6f1f0ac8a57
doc_id: 60852
cord_uid: w3q38d3s

Higher-order intuitionistic logic categorically corresponds to toposes or triposes; here we address what are toposes or triposes for higher-order substructural logics. Full Lambek calculus gives a framework to uniformly represent different logical systems as extensions of it. Here we define higher-order Full Lambek calculus, which boils down to higher-order intuitionistic logic when equipped with all the structural rules, and give categorical semantics for (any extension of) it in terms of triposes or higher-order Lawvere hyperdoctrines, which were originally conceived for intuitionistic logic, and yet are flexible enough to be adapted for substructural logics. Relativising the completeness result thus obtained to different axioms, we can obtain tripos-theoretical completeness theorems for a broad variety of higher-order logics. The framework thus developed, moreover, allows us to obtain tripos-theoretical Girard and Kolmogorov translation theorems for higher-order logics.

Propositional logic corresponds to a class of algebras; for example, the algebras of classical intuitionistic logic are Heyting algebras. What are, then, the algebras of predicate logic? There is seemingly no agreed concept of algebras of predicate logic. Cylindric algebras [11] give a candidate for it. It is not very clear how far and how uniformly cylindric algebraic semantics can be extended so as to treat different sorts of logical systems, especially substructural logics (linear, relevant, fuzzy, etc.). Lawvere's hyperdoctrines [18] give another concept of algebras of predicate logic, and may be seen as a categorical extension of cylindric algebras (see, e.g., Jacobs [13] , which gives a fibrational understanding of cylindric algebras; fibrations and hyperdoctrines as indexed categories are connected with each other via the Grothendieck construction). From an algebraic point of view, a hyperdoctrine is a fibred algebra, i.e., an algebra indexed by a category:

and others as we shall detail below. The intuitive meaning of the base category C is the category of types (aka. sorts) or domains of discourse, and then P (C) is the algebra of predicates on a type C. And P is called a predicate functor. Roughly, if a propositional logic L is complete with respect to a variety Alg L , then the corresponding fibred algebras P : C op → Alg L yield complete semantics for the predicate logic that extends L. This may be called completeness lifting: the completeness of propositional logic with respect to Alg lifts to the completeness of predicate logic with respect to P : C op → Alg. While this completeness lifting is demonstrated for first-order logic in [21] , in the present paper, we demonstrate completeness lifting for higher-order logic of different sorts.

In order to represent different logical systems in a uniform setting, we rely upon the framework of substructural logics over Full Lambek calculus FL and their algebras (see, e.g., Galatos-Jipsen-Kowalski-Ono [8] ); FL algebras (defined below) play the rôle of Alg above. Diverse logical systems can be represented as axiomatic extensions of FL, including classical, intuitionistic, fuzzy, relevant, paraconsistent, and linear logics. In this field, there are vital developments of the correspondence between cut elimination and algebraic completion (see Ciabattoni-Galatos-Terui [3] , which focus upon the propositional case, but might possibly be extended to the first-order and higher-order cases via the framework of substructural hyperdctrines). In this paper we think of higher-order Full Lambek calculus, which boils down to higher-order intuitionistic logic (as in Lambek-Scott [17] ) when equipped with all the structural rules, and give hyperdoctrine semantics for (any extension of) it. Lawvere's hyperdoctrines were originally for intuitionistic logic; yet they are flexible enough so as to be adapted for a variety of substructural logics as we shall see below. Note that, whilst toposes are impredicative, triposes can have their type theories predicative (e.g., Martin-Löf); the two-level structure of triposes allows more flexibility than toposes do.

There is a tight connection between toposes and higher-order hyperdoctrines, which are also called triposes (for triposes, see, e.g., Hyland-Johnstone-Pitts [12] and Pitts [26] ; there are actually several non-equivalent definitions of triposes; we simply call higher-order hyperdoctrines triposes). Indeed, toposes and triposes correspond to each other via the two functors of taking subobject hyperdoctrines and of the tripos-to-topos construction (see, e.g., Coumans [4] and Frey [10] ); note that the subobject functor Sub of a topos plays the rôle of a predicate functor P above. Both toposes and (intuitionistic) higher-order hyperdoctrines give complete semantics for higher-order intuitionistic logic; the completeness result of this paper generalises this classic result quite vastly in terms of higherorder substructural hyperdoctrines or triposes. The contributions of this paper may be summarised succinctly as follows: (i) higher-order completeness via Full Lambek triposes, which can be instantiated for a broad variety of logical systems; (ii) tripos-theoretical Girard's ! translation and Kolmogorov's ¬¬ translation theorems for higher-order logic, in which the internal language of triposes is at work. As illustrated by the translation theorems, the general framework of the present paper allows us to compare different categorical logics within the one setting (many categorical logics have only been developed locally so far; there has been no global framework to compare them in the same setting).

The rest of the paper is organised as follows. We first present the syntax of Higher-order Full Lambek calculus HoFL, which obtains by adapting higherorder intuitionistic logic to Full Lambek calculus FL. And we introduce the concept of Full Lambek tripos (FL tripos for short; aka. higher-order FL hyperdoctrine; for brevity we use the former terminology), thereby obtaining the higher-order completeness theorem for HoFL. Finally, our general framework thus developed is applied, via the internal language of FL triposes, to the categorical analysis of Girard's and Kolmogorov's translation for higher-order logics.

In this section we introduce Higher-order Full Lambek calculus HoFL, which extends quantified FL as in Ono [23, 24] so that HoFL equipped with all the structural rules boils down to higher-order intuitionistic logic, the logic of toposes (see , Jacobs [13] , or Johnstone [15] ). Our presentation of HoFL, especially its type-theoretic part, follows the style of Pitts [25] ; thus we write, e.g., "t : σ [Γ ]" and "ϕ [Γ ]", rather than "Γ t : σ" and "Γ ϕ", respectively, where t is a term of type σ in context Γ , and ϕ is a formula in context Γ .

HoFL is a so-called "logic over type theory" or "logic-enriched type theory" in Aczel's terms; there is an underlying type theory, upon which logic is built (see, e.g., Jacobs [13] ). To begin with, let us give a bird's-eye view of the structure of HoFL. The type theory of HoFL is given by simply typed λ-calculus with finite product types (i.e., 1 and ×; these amount to the structure of CCCs, cartesian closed categories), and moreover, with the special, distinguished type Prop which is a "proposition" type, intended to represent a truth-value object Ω on the categorical side. The logic of HoFL is given by Full Lambek calculus FL. The Prop type plays the key rôle of reflecting the logical or propositional structure into the type or term structure: every formula or proposition ϕ may be seen as a term of type Prop. This is essentially what the subobject classifier Ω of a topos E is required to satisfy, that is,

Spelling out the meaning of this axiom in logical terms, we have got Pred(σ) Term(σ, Prop) which means the structure of predicates on each type σ (or context Γ in general) is isomorphic to the structure of terms from σ to Prop. The logical meaning of Ω may thus be summarised by a sort of reflection principle, namely the reflection of the propositional structure into the type structure, which may also be called the "propositions-as-terms" or "propositions-as-functions" correspondence, arguably lying at the heart of higher-order categorical logic, for Ω would presumably be the raison d'être of higher-order categorical logic (toposes are CCCs with Ω).

The power type P σ of a given type σ can be defined in the present framework as σ → Prop; the comprehension term {x : σ | ϕ} : P σ and the membership predicate s ∈ t : Prop are definable via λ-abstraction or currying (categorically, transposing) and λ-application (categorically, evaluation), respectively. That is, {x : σ | ϕ} may be defined as λx : σ. ϕ where ϕ is seen as a term of type Prop, and also s ∈ t may be defined as ts where t : σ → Prop and s : σ. These definable operations allow us to express set-theoretical reasoning in higher-order logic. There is, of course, some freedom on the choice of primitives, just as toposes can be defined in terms of either subobject classifiers or power objects. All this is to facilitate an intuitive understanding of the essential features of higher-order logic; we give a formal account below.

The syntactic details of HoFL are as follows. HoFL is equipped with the following logical connectives of Full Lambek calculus:

The non-commutativity of HoFL gives rise to two kinds of implication (\ and /). We have basic variables and types, denoted by letters like x and σ, respectively. And as usual x : σ is a formal expression to say that a variable x is of type σ. Note that every variable must be typed in HoFL, unlike untyped FL. A context is a finite list of typings of variables: x 1 : σ 1 , ..., x n : σ n which is often abbreviated as Γ . Formulae and terms are then defined within specific contexts. There are relation symbols and function symbols, both in context: R(x 1 , ..., x n ) [x 1 : σ 1 , ..., x n : σ n ] is a formal expression to say that R is a relation symbol with variables x 1 , ..., x n of types σ 1 , ..., σ n respectively; and also f : τ [x 1 : σ 1 , ..., x n : σ n ] is a formal expression to say that f is a function symbol with its domain (the product of) σ 1 , ..., σ n and with its codomain τ .

The type constructors of HoFL are product ×, function space →, and the proposition type Prop, which is a nullary type constructor. The term constructors of × and → are as usual: pairing -, -and (first and second) projections π 1 , π 2 for product ×, and λ-abstraction and λ-application for function space →. The term constructors of Prop are all the logical connectives of Full Lambek calculus as listed above, the relation symbols taken to be of type Prop and thus working as generators of the terms of type Prop. Formulae in context, ϕ [Γ ], and terms in context, t : τ [Γ ], are then defined in the usual, inductive manner (our terminology and notation mostly follow Pitts [25] ; we are extending his framework so as to encompass higher-order substructural logics). Finally, sequents in contexts are defined as:

where Γ is a context, Φ is a finite list of formulae ϕ 1 , ..., ϕ n , and all the formulae involved are in context Γ . So far we have not touched upon any axiom (or inference rule) involved. In the following, we first give axioms for terms, and then for sequents. The axioms for × and → are as usual (see, e.g., Pitts [25] ). The axiom for Prop is as follows:

This axiom relates the structure of propositions to that of terms, thus guaranteeing the aforementioned "propositions-as-functions" correspondence for higherorder categorical logic. There are several standard rules for contexts and substitution, which are the same as those in Pitts [25] (we do not repeat them here, referring to the Sect. 2 of Pitts [25] for the details). We now turn to inference rules for sequents. We first have the identity and cut rules as follows:

where ψ may be empty; this applies to the following L (Left) rules as well. Note that HoFL has no structural rule other than the cut rule. The rules governing the use of the logical connectives are as follows.

There are eigenvariable conditions on the quantification rules: x must not appear as a free variable in the bottom sequents of the ∀R and ∃L rules. We write ∀x and ∃x when the type of x is obvious. These are all of the rules of HoFL; the provability of sequents in context is defined in the usual way. The essential difference from the first-order case is the existence of function and truth value types; they are what make the logic higher-order, enabling set-theoretical reasoning. For a collection X of axiom schemata (which we often simply call axioms), let us denote by HoFL X the axiomatic extension of HoFL via X. In particular, we can recover higher-order intuitionistic logic as HoFL ecw , i.e., by adding to HoFL the exchange, weakening, and contraction rules (as axiom schemata).

The following sequents-in-context are deducible in HoFL:

where it is supposed that ϕ does not contain x as a free variable, and Γ contains type declarations on those free variables that appear in ϕ and ∃xψ.

As explained in [21] , typed logic allows domains of discourse to be empty; they must be non-empty in the Tarski semantics. A type σ can be interpreted as an initial object in a category. We need no ad hoc condition on domains of discourse if we work with typed logic. This is due to Joyal as noted in Marquis and Reyes [19] . Proof-theoretically, the following is not deducible in HoFL: ∀xϕ ∃xϕ [ ]. Still the following is deducible: ∀xϕ ∃xϕ [x : σ, Γ ]. That is, we can prove the sequent above when a type σ is inhabited (see [21] for more details).

The algebras of propositional FL are FL algebras, the definition of which is reviewed below. The algebras of first-order FL are arguably FL hyperdoctrines; note that complete FL algebras only give us completeness in the presence of the ad hoc condition of so-called safe valuations (cf. [24] ), and yet FL hyperdoctrines allow us to prove completeness without any such ad hoc condition, and at the same time, to recover the complete FL algebra semantics as a special, set-theoretical instance of the FL hyperdoctrine semantics (in a nutshell, the condition of safe valuations is only necessary to show completeness with respect to the restricted class of FL hyperdoctrines with the category of sets their base categories). In this section we define FL triposes, which are arguably the (fibred) algebras of higher-order FL, and prove higher-order completeness, again without any ad hoc condition such as safe valuations or Henkin-style restrictions on quantification (set-theoretical semantics is only complete under this condition). 

A homomorphism of FL algebras is required to preserve all the operations of FL algebras. Let FL denote the category of FL algebras and their homomorphisms.

FL is an algebraic category (namely, a category monadic over the category of sets; see [1] ), and then an axiomatic extension FL X of FL corresponds to an algebraic subcategory of FL, which shall be denoted FL X . Note that algebraic categories are called varieties or equational classes in universal algebra.

such that the base category C of P is a category with finite products, and that the following conditions (to express quantifiers) are satisfied:

And the corresponding Beck-Chevalley condition holds, i.e., the following diagram commutes for any arrow f : Z → Y in C (π : X × Z → Z below denotes a projection):

. The corresponding Beck-Chevalley condition holds:

Furthermore, the Frobenius Reciprocity conditions hold: for any projection π : X × Y → Y in C, any a ∈ P (Y ), and any b ∈ P (X × Y ),

The logical reading of the Beck-Chevalley conditions above is that substitution commutes with quantification. Now, FL triposes are defined as FL hyperdoctrines with their base categories CCCs, and with truth-value objects Ω (i.e., representability via Ω ∈ C): Definition 4. An FL (Full Lambek) tripos, or higher-order FL hyperdoctrine, is an FL hyperdoctrine P : C op → FL such that:

-The base category C is a CCC (Cartesian Closed Category); -There is an object Ω ∈ C such that P Hom C (-, Ω).

We then call Ω the truth-value object of the FL tripos P . Given a set X of axioms, an FL X tripos is defined by replacing FL above with FL X .

For an FL tripos P , each P (C) is called a fibre of the FL tripos P from a fibrational point of view; intuitively, P (C) may be seen as the algebra of propositions on a type or domain of discourse C. Note that it is also possible to define FL triposes in terms of fibrations, even though the present formulation in terms of indexed categories would be categorically less demanding.

FL tripos semantics for HoFL is defined as follows. ].

HoFL above with FL X and HoFL X , respectively.

The categorical conception of interpretation encompasses set-theoretical interpretations and forcing-style model constructions. First of all, interpreting logic in the 2-valued tripos Hom Set (-, 2) (where 2 is the two-element Boolean algebra) is precisely equivalent to the standard Tarski semantics. Yet there is a vast generalisation of this: given a quantale Ω, the representable functor Hom Set (-, Ω) : Set op → FL forms an FL tripos, which gives rise to a universe of quantale-valued sets via the generalised tripos-to-topos construction as in [21] ; if Ω is a locale in particular (i.e., complete Heyting algebra), it is known that Hom Set (-, Ω) yields Sh(Ω) (i.e., the sheaf topos on Ω). This sort of FL tripos models of set theory could hopefully be applied to solve consistency problems for substructural set theories (especially, Cantor-Lukasiewicz set theory).

Note that the base category of an FL tripos is used to interpret the type theory of HoFL, and the value category is used to interpret the logic part of HoFL. In the following, we first prove soundness and then completeness.

is provable in HoFL (resp. HoFL X ), then it is valid in any interpretation in any FL (resp. FL X ) tripos.

Proof. Let P be an FL or FL X tripos, and [ [-] ] an interpretation in P . Soundness for the first-order part can be proven in essentially the same way as in [21] ; due to space limitations, we do not repeat it, and focus upon Prop, which is the most distinctive part of higher-order logic. So For the sake of a completeness proof, let us introduce the syntactic tripos construction (for logic over type theory), which is the combination of the syntactic category construction (for type theory) and the Lindenbaum-Tarski algebra construction (for propositional logic):

where t 1 : σ 1 [Γ ] , ..., t n : σ n [Γ ] and Γ is supposed to be x 1 : σ 1 , ..., x n : σ n . Composition is defined via substitution. The syntactic tripos P HoFL : C op → FL is then defined as follows. Given an object Γ in C, let Form Γ denote the set of formulas in context Γ , and then define where it is supposed that t 1 : σ 1 [Γ ], ..., t n : σ n [Γ ], and that ϕ is a formula in context x 1 : σ 1 , ..., x n : σ n . The syntactic tripos P HoFLX of HoFL X is defined just by replacing FL and HoFL above with FL X and HoFL X , respectively.

The syntactic tripos of higher-order logic is the fibrational analogue of the Lindenbaum-Tarski algebra of propositional logic; each fibre P HoFL (Γ ) of the syntactic tripos P HoFL is the Lindenbaum-Tarski algebra of formulae in context Γ . The syntactic tripos of HoFL has the universal mapping property that inherits from the syntactic base category of the underlying type theory of HoFL, and also from the fibre-wise Lindenbaum-Tarski algebras of the logic part of HoFL. We of course have to verify that the syntactic tripos P HoFL indeed carries an FL tripos structure; this is the crucial part of the completeness proof. Lemma 8. The syntactic tripos P HoFL : C op → FL (resp. FL X ) defined above is an FL (resp. FL X ) tripos. In particular, the base category is a CCC, and there is a truth-value object Ω ∈ C such that P HoFL Hom C (-, Ω).

Proof. The existence of products and exponentials in C is guaranteed by the existence of product types and function space types in the type theory of HoFL. Substitution commutes with all the logical connectives. This means that P ([t 1 , ..., t n ] ) defined above is a homomorphism; so P is a contravariant functor.

P has quantifier structures as follows. Let π : Γ × Γ → Γ denote the projection in C defined above, and consider P (π), which has right and left adjoints in the following way. Recall Γ is x : σ 1 , ..., x n : σ n . Let ϕ ∈ P (Γ × Γ ); we identify ϕ with the equivalence class to which ϕ belongs. Define ∀ π : P (Γ × Γ ) → P (Γ ) by ∀ π (ϕ) = ∀x 1 ...∀x n ϕ.

We also define ∃ π : P (Γ × Γ ) → P (Γ ) by ∃ π (ϕ) = ∃x 1 ...∃x n ϕ. Then, ∀ π and ∃ π give the right and left adjoints of P (π), respectively. We can verify the Beck-Chevalley condition for ∀ as follows. Let ϕ ∈ P (Γ × Γ ), π : Γ × Γ → Γ a projection in C, and π : Γ × Γ → Γ another projection in C for objects Γ, Γ , Γ in C. Then,

where Γ is supposed to be x 1 : σ 1 , ..., x n : σ n , Γ is y 1 : τ 1 , ..., y m : τ m ,  and t 1 : τ 1 [Γ ] , ..., t m : τ m [Γ ]. Likewise we have ∀ π • P ([t 1 , ..., t n ] )(ϕ) = ∀x 1 ...∀x n (ϕ[t 1 /y 1 , ..., t n /y m ]). The Beck-Chevalley condition for ∀ thus follows. The Beck-Chevalley condition for ∃ can be verified in a similar way. The two Frobenius Reciprocity conditions for ∃ follow immediately from Lemma 1.

In the following we prove the existence of a truth-value object Ω. Let

Note that, since the objects of the base category are contexts rather than types, we cannot take Ω to be Prop per se; yet x : Prop practically means the same thing as Prop, thanks to α-equivalence required. We now have to show that for each context Γ , P (Γ ) Hom C (Γ, x : Prop) and this correspondence yields a natural transformation. The required isomorphism is given by mapping ϕ [Γ ] ∈ P (Γ )

to ϕ : Prop [Γ ] ∈ Hom C (Γ, x : Prop).

Note that ϕ above is actually an equivalence class, and yet the above mapping is well defined, and also that ϕ : we obtain the commutativity of the diagram and hence the naturality of the "propositions-as-functions" correspondence.

It is straightforward to see that if Φ ψ [Γ ] is valid in the canonical interpretation in the syntactic tripos P HoFL (resp. P HoFL X ), then it is provable in HoFL (resp. HoFL X ). And this immediately gives us completeness via the standard counter-model argument. Hence the higher-order completeness theorem:

is provable in HoFL (resp. HoFL X ) iff it is valid in any interpretation in any FL (resp. FL X ) tripos.

This higher-order completeness theorem can be applied, with a suitable choice of axioms X, for any of classical, intuitionistic, fuzzy, relevant, paraconsistent, and (both commutative and non-commutative) linear logics; higher-order completeness has not been known for these logics except the first two. The concept of (generalised) tripos, therefore, is so broadly applicable as to encompass most logical systems. Modal logics also can readily be incorporated into this framework by working with modal FL rather than plain FL. Coalgebraic dualities for modal logics (see, e.g., [14, 16, 20, 22] ) then yield models of modal triposes for them; these modal issues are to be addressed in subsequent papers.

We finally analyse Kolmogorov's double negation ¬¬ translation (Kolmogorov found it earlier than Gödel-Gentzen; see Ferreira and Oliva [7] ) and Girard's exponential ! translation from a tripos-theoretical point of view.

Propositional Kolmogorov translation algebraically means that, for any Heyting algebra A, the doubly negated algebra ¬¬A, defined as {a ∈ A | ¬¬a = a}, always forms a Boolean algebra. This ¬¬ construction extends to a functor from the category HA of Heyting algebras to the category BA of Boolean algebras. And then the categorical meaning of first-order Kolmogorov translation is that, for any first-order IL hyperdoctrine P : C op → HA (where IL denotes intuitionistic logic), the following composed functor ¬¬ • P : C op → BA forms a first-order CL hyperdoctrine (where CL denotes classical logic) as in [21] . Yet this strategy does not extend to the higher-order case: in particular, although the base category does not change in the first-order case, in which types and propositions are separated, it must nevertheless be modified in the higherorder case, in which types and propositions interact via Prop or Ω. Technicalities involved get essentially more complicated in the higher-order case. Still, we can construct from a given IL tripos P : C op → HA a CL tripos

For the sake of the description of C ¬¬ (and P ¬¬ ), however, we work within the internal language HoFL P of the tripos P : C op → FL: in HoFL P , we have types C and terms f corresponding to objects C and arrows f in C, respectively, and also formulae R on a type C ∈ C corresponding to elements R ∈ P (C). Now we define the translation on the internal language HoFL P of the tripos P which allows us to describe the double negation category C ¬¬ mentioned above. The basic strategy of translation is this: we leave everything in HoFL P as it is, unless it involves the proposition type Ω of HoFL P ; and if something involves Ω, we always put double negation on it. Formally it goes as follows:

Definition 10. We recursively define the translation on HoFL P as follows.

-If ϕ : Ω [Γ ] then we put ¬¬ on every sub-formula of ϕ (do the same for ϕ seen as formulae). and no Ω appears in it, then t translates into itself.

The double negation category C ¬¬ is then defined as follows: the objects of C ¬¬ are contexts in HoFL P up to α-equivalence (which are essentially the same as objects in C), and the arrows of C ¬¬ are the translations of lists of terms in HoFL P up to equality on terms, with their composition defined via substitution as usual. This intuitively means that those arrows in C that involve Ω are double negated in C ¬¬ whilst the other part of C ¬¬ remains the same as that of C (to give the rigorous definition of this, we work within the internal language). Then it is not obvious that C ¬¬ forms a category again, let alone a CCC. Thus:

Lemma 11. C ¬¬ defined above forms a category, in particular a CCC.

Proof. Since everything involving Ω is doubly negated, we have to verify that all of the relevant categorical structures, that is, composition, identity, projection, paring, evaluation, and transpose, preserve or respect double negation. Here we just give several sample proofs to show essential ideas.

Consider the case of composition. We think of single terms for simplicity. since every occurrence of y in t is replaced by ¬¬y because t ∈ C ¬¬ and since ¬¬¬¬ is equivalent to ¬¬, we have t[¬¬x/y] = t, whence t • ¬¬x = t. More complex cases can be shown in a similar manner.

To show the existence of finite products and exponentials involving Ω (otherwise it is trivial), it is crucial to check that doubly negated projection, pairing, evaluation, and transpose still play their own rôles, just as doubly negated identity still plays the rôle of identity as we have shown above.

Finally we obtain the following, tripos-theoretical Kolmogorov translation theorem for higher-order logic, which may also be seen as a translation from classical set theory to intuitionistic set theory (since higher-order logic is basically set theory in logical form).

Let P : C op → HA be an IL tripos, and C ¬¬ the double negation category as defined above. Then, P ¬¬ defined as Hom C¬¬ (-, Ω) : C ¬¬ → BA forms a CL tripos, called the double negation tripos of P .

Proof. C ¬¬ is a CCC by the lemma, and P ¬¬ is represented by Ω. This completes the higher-order part of the proof. Concerning the first-order part, the existence of quantifiers follows from this fact: if ϕ admits the double negation elimination, then ¬¬∀xϕ and ¬¬∃xϕ are equivalent to ∀x¬¬ϕ and ∃x¬¬ϕ, respectively.

Note that the hyperdoctrinal Kolmogorov translation does not reduce to the construction of toposes via double negation topology because there are more triposes than toposes in the adjunction between them (all toposes come from triposes, but not vice versa). Moreover, our hyperdoctrinal method is designed modularly enough to be applicable to Girard's translation as well as Kolmogorov's. Although Glivenko-type theorems have been shown for substructural propositional and first-order logics (see Ferreira-Ono [6] and Galatos-Ono [9] ), no such result is known for higher-order logic (as to the first-order case, [21] is typed and categorical while [6] is single-sorted and proof-theoretical).

An exponential ! on an FL algebra A is defined as a unary operation satisfying: (i) a ≤ b implies !a ≤!b; (ii) !!a =!a ≤ a; (iii) ! = 1; (iv) !a⊗!b =!(a ∧ b) (Coumans, Gehrke, and van Rooijen [5] ). We denote by FL ! c the category of commutative FL algebras with !, which are algebras for intuitionistic linear logic. FL ! c triposes give sound and complete semantics for higher-order intuitionistic linear logic. The Girard category C ! of an FL ! c tripos P : C op → FL ! c is defined by replacing double negation in the above definition of C ¬¬ with Girard's exponential !. The following is the hyperdoctrinal Girard translation theorem for higher-order logic, which can be shown in basically the same way as above; no such higher-order translation has been known so far. Then, P ! forms an IL tripos (i.e., FL ! ecw tripos), called the Girard tripos of P .

Abstract and Concrete Categories

BI-hyperdoctrines, higher-order separation logic, and abstraction

Algebraic proof theory for substructural logics

Canonical extensions in logic -some applications and a generalisation to categories

Relational semantics for full linear logic

Glivenko theorems and negative translations in substructural predicate logics

On the relation between various negative translations

Residuated Lattices: An Algebraic Glimpse at Substructural Logics

Glivenko theorems for substructural logics over FL

A 2-categorical analysis of the tripos-to-topos construction

Tripos theory

Categorical Logic and Type Theory

Stone Spaces

Sketches of an Elephant

Stone coalgebras

Introduction to Higher-Order Categorical Logic

Reprinted with the author's retrospective commentary

The history of categorical logic

Natural duality, modality, and coalgebra

Full lambek hyperdoctrine: categorical semantics for first-order substructural logics

Duality theory and categorical universal logic

Algebraic semantics for predicate logics and their completeness

Crawley completions of residuated lattices and algebraic completeness of substructural predicate logics

Categorical logic, Chap. 2

Tripos theory in retrospect

Acknowledgements. The author would like to thank the reviewers of the paper for their numerous, substantial comments and suggestions for improvement. The author hereby acknowledges that this work was supported by JST PRESTO (grant code: JPMJPR17G9), JSPS Kakenhi (grant code: 17K14231), and the JSPS Core-to-Core Program "Mathematical Logic and its Applications".