Carrés exacts et carrés déductifs

During 1978 (cf (Guitart, 1980)) I have introduced the notion of exact square in 2-category theory and I have shown their usefulness in the special case of the 2-category $\Cat$. Subsequently, I have shown in many occasions (cf (Guitart, 1982)) why these exact squares play the same role of the logic equivalence relation $\iff$ in propositional calculus, at the level of general model theory.

Here, I want to present together the arguments in this direction, those already given, and some new. This will allow me to isolate a new concept meant to play, at the level of general model theory, the same role played by logical implication in propositional calculus; it’s the concept of a deductive square.

Starting from the concept of deductive square it’s very easy to define proofs. An axiomatic theory is then a 2-category where we have outlined certain zig-zags of morphisms (the axioms), and where we are given certain squares, called “deductive” (the deduction rules). Theorems are then terminal zig-zags of proofs starting from the axioms.

The idea of working in additive categories with exact squares instead of exact sequences dates back to Lambek, Mac Lane, Puppe, and a large part of what can be done is exposed in Hilton (Hilton, 1966). About te use of exact squares in non-additive categories, and the relation with the problem of embedding the ambient category in various categories with involution, we advise the reader to consult (Grandis, 1977) or other references (for example Čalenko and Conte).

The advantage of this point of view lies in the following key observation: we can obtain the composition of two relations-spans $A\leftarrow X\to B$ and $B\leftarrow Y\to C$ as follows: where $*$ is any exact square (see (Guitart, 1975), p. 35 and (Guitart, 1982), p 22). As a consequence, the study of formation laws for exact squares in a category of the form $\Set^{C^\op}$ allows to understand the calculus of relations of $\Set^{C^\op}$ and as a consequence the deductive logic of this topos.

However, since we know that the logics of categories like $\Set^{C^\op}$ “are” the natural semantics for intuitionistic logic, we see that the method of exact squares is, in fact, larger than intuitionism. Intuitionism is, in some sense, the discrete or 1-dimensional part of fibered exact logic introduced in (Guitart, 1982) as a principal part of categorical logic. Fibered exact logic in a category $C$ is the study of formation laws of exact squares in the 2-categories $\Cat^{C^\op}$, $\Fib(C)$, $\underline{D}(C)$, $\Cat/C$,… (the second principal part of categorical logic on $C$ is the study of fibered monads on $C$, i.e. of monads in $\Cat^{C^\op}$, $\Fib(C)$, $\underline{D}(C)$, $\Cat/C$,…)

Exact squares in $\Cat$, in representable 2-categories or in 2-categories equipped with a Yoneda structure have been introduced in (Guitart, 1980) and, subsequently, the theory has been developed by Van den Bril (Van den Bril, 1980), (Van den Bril, 1982) Guitart (Guitart, 1982), Guitart-Lair (Guitart & Lair, 1980) (in the case of $\Cat$, see here some complementary remarks to §12).

One first reason for the success of these 2-dimensional exact squares is that more or less everything one can do in $\Cat$ (e.g., defining comma and co-comma squares, rich functors, opaque functors, co-fully faithful functors, limits and absolute extensions, adjunctions and relative adjunctions, pointwise Kan extensions) is naturally and directly expressible in terms of exact squares.

A second reason is that, in the case of $\Cat$, profunctor composition seen as bi-fibrations is performed again taking into account the key observation of our §2.

Every first-order formula can be written in terms of continuity and co-continuity conditions (Guitart-Lair, to appear) and such conditions can be expressed in their own right as exactness of squares in $\Cat$, in such a way that the study of the validity of formulas and the theory of deduction for formulæ-theorems starting from formulæ-axioms can be reconducted, in principle, to problems in exact logic. In particular, usual rules of deduction (the principle of contraposition, modus ponens) must be expressible in terms of construction rules for exaxct squares. This is the case, as we outline in (Guitart, 1982) and (Guitart & Lair, 1980), with modelization rules, syntactization rules, and exact extension (mod, syn, ex.ex). In order to realize the scope of a rule like ex.ex, it is enough to observe that it directly entails Mac-Donald and Deleanu-Hilton’s theorems on Kan extensions of cohomolgy theories and K-theories.

We address the reader to (Guitart, 1982) for more details on exact logic.

The fact that deduction theory can be transformed (cf. §4) in the theory of construction of exact squares means that (cf. §2) exact squares are the building blocks to describe relational composition, that deduction is the study of a category of relations and, in particular, the determination of triples of relations $R : X \pto Y$, $S: Y \pto Z$, $T=X\pto Z$ such that $S\circ R=T$.

Since in the case of $\Set$, the relational composition of $R,S$ is obtained as a union of subobjects of $Z$, deduction theory can still be defined as the description of the structure of “objects of subobjects” $PZ$. In general we argue that since $PZ$ is the free complete lattice over $Z$ (an observation true in $\Set$, which remains valid in every topos taken as an ambient category). I have observed that the structure of $PZ$ can also be analyzed as that of an extensor (see (Guitart, 1980) an §7). Either way, the structure of $PZ$ is that of a free $P$-algebra, and it can thus be described once we know the structure of $P$. I have suggested in (Guitart, 1982) that we can elucidate such structure as that of an algebraic universe strong enough to perform all construction of first order mathematics, and pliable enough to be valid when the ambient category is a general topos, or some category of fuzzy sets.

Since the overall problem with $PZ$ is to allow for a deduction theory (cf. §5), Lambek-Scott proposed in (Lambek & Scott, 1981) to understand $PZ$ as a deductive set, i.e. a set $E$ equipped with a relation $\vdash \subseteq (\mathcal{P}_\text{f}E)\times E$ called deduction, satisfying the following axioms: If $(L,\le)$ is a complete lattice, we can obtain a deduction structure $\vdash$ as follows:

If $C$ is a category equipped with an involutive monad $(\boldsymbol{P},I)$ (for example if $C$ is an algebraic universe), each $\boldsymbol P$-algebra $(E,\theta)$ (and in particular every free algebra $PZ$) carries an extension structure $\text{Ex}$: for each $f : I\to E$ and $h : I\to J$ we can define an extension of $f$ along $h$ as follows:

If $C$ is a topos or the category of fuzzy sets, $\text{Ex}$ satisfies the axioms of an extension structu.

If $E$ has an extension structure, it also has a deduction structure, namely we can define

if and only if there exists a diagram where $\text{Ex}_u f$ and $\text{Ex}_w(k\circ v)=g$.

In (Guitart & Lair, 1980), pp. 82 and 91, we have considered the figure

We have that $(a.b.c)$ is exact if and only if $\smat{a.b.c\\ d.e.f}$ is exact, which we can write as $F\vDash \lim g \iff h(s)F\vDash g$ (“dialectic” between abstract model / concrete formula, on one side, and developed [concrete] model / abstract formula on the other).

This is an important instance of application of the concept of exact grid (cf. (Guitart, 1980)), where a plane grid is called exact if filling the “empty blocks” with small exact squares, the big square obtained pasting all together is itself exact.

The calculus of exact squares can be seen as a calculus of exchange for right 2-fractions $s\circ t^\ast$ and left 2-fractions $u^\ast\circ v$, and the calculus of exact grids corresponds to higher-order exchanges as $s_1\circ t_1^\ast\circ s_2\circ t_2^\ast \sim u_1^\ast\circ v_1 \circ u_2^\ast \circ v_2$.

As an example, consider the (solid arrows in the) grid below, completed (by the dotted arrows) as follows: If the outer square (solid and dotted arrows together) is exact, i.e. if the grid is exact, then we have an exact modification of the path $(a,b,c,d,e,f)$ towards the path $(g,h,ij,k,l)$ described by the sequence of “1-step reductions”

In general, an exact modification should be undertsood as a strict proof of the relation represented by the path $(g,h,i,j,k,l)$ starting from the relation represented by the path $(a,b,c,d,e,f)$. The “proof theory” in $\Cat$ can be undertsood, from this point of view, as the study of commutation of limits in $\Set$: a proof is a tree where each node is labeled with a commutation rule for limits in $\Set$. The rules of classical first orderlogic (manipulation of quantifiers, propositional calculus) are in fact of this type. More in detail, if $P,Q$ are propositions, we prove that $P\iff Q$ by means of the application of commutation rules like

if $a’=\lnot a,b’=\lnot b$, and all these rules can be grouped in a single statement as follows:

If $P$ is a proposition, its DNF (disjunctive normal form) equals its CNF (conjunctive normal form), and it equals $P$ itself.

There exists a “syntax and semantics” adjunction between the theory of exactness and the theory of relations.

In order to make this precise, let’s work in a category $C$ (the generalization to 2-categories is straightforward) and let’s consider:

1. The category $P(C^\square)$ whose objects are subsets of the set of commutative squares of $C$, and where morphisms are inclusions;
2. The category $PMI(C)$ of involutive promonads $(L,I)$ on $C$ whose objects are bijective-on-objects functors $L : C\to R$ coupled with involutions on $R$, i.e. functors $I : R\to R^\op$ that are the identity on objects and such that $I^\op\circ I=1_R$, and where morphisms $H : (L,I)\to (L’,I’)$ are functors $H : R\to R’$ such that $H\circ L = L’$ and $I’\circ H = H\circ I$.

From this we can define a functor

sending an involutive promonad $(L,I)$ to the set of commutative squares

which moreover are “anticommutative in $R$”, meaning that $Ls\circ ILt = ILu\circ Lv$.

Such a functor admits a left adjoint

that we can describe as follows:

• Denote by $\Ch(C)$ the free category of paths in $C$, whose objects are those of $C$ and where morphisms from $A$to $B$ are tuples $(X_1,\dots,X_n;f_1,\dots,f_n)$ for which $X_1=A, X_n=B$ and for each $i\le n$, each $X_i$ is an object of $C$ and $f_i = X_i\to X_{i+1}$ or $f_i : X_{i+1}\to X_i$ (the composition of such morphisms is then defined by mere juxtaposition).
• Denote by $ZZ(C)$ the free category with involution over $C$, whose objects are the same of $C$ and whose morphisms from $A$ to $B$ are zig-zags (or paths) such that fo each $i\le n$, $f_i$ and $f_{i+1}$ are not composable (composition is then juxtaposition, followed if necessary by reduction, if $f_1’$ and $f_n$ are composable; so, $ZZ(C)$ is a certain quotient of $\Ch(C)$).
• Finally, for any given $E\subseteq C^\square$, define $Re(E)$ to be the category obtained quotienting $\Ch(C)$ by the equivalence relation induced by the following rules:
  1. In every given path we can replace a pair $X \xto{f_i} Y \xto{f_{i+1}} Z$ with $f_{i+1}f_i : X\to Z$;
  2. In any given path we can replace $_i : X\to Y$ with a pair $X \xto{u} K \xto{v} Y$ if $f_i=v\circ u$;
  3. In any given path we can replace a span $X \xot{f_i} Y \xto{f_{i+1}} Z$ with a cospan $X \xto{u} K \xot{v} Z$ provided that the square belongs to $E$;
  4. In any given path we can replace a cospan $X \xto{f_i} Y \xot{f_{i+1}} Z$ with a span $X \xot{u} K \xto{v} Z$ provided that the square belongs to $E$;

Given this, two paths are equivalent if and only if there exists a sequence of transformations of type 1,2,3,4 such that, applied to one, leads to the other. Such a sequence is called an $E$-exact modification (observe that $Re(E)$ always arises as a quozient of $ZZ(C)$: starting from $ZZ(C)$, condition 1 becomes redundant but one never forget to apply condition 2).

The involution n $Re(E)$ is induced by the one on $\Ch(C)$. The verification of the adjunction $Re\dashv Ex$ (i.e. of the equivalence $E\subseteq Ex(R,I)$ if and only if $Re(E)\to (R,I)$, or in other words of the fact that the set of morphisms $Re(E)\to (R,I)$ is nonempty if and only if $E\subseteq Ex(R,I)$, and in such case it has a single element), is immediate.

We see then that $Re(E)$-algebras are precisely $E$-extensors.

Many classes $E$ of squares are built starting from a pseudo-functor $S : C^\op\to\Cat$ such that, for each object $X$ in $C$ the category $SX$ is a “category of formal subobjects” of $X$. We define, then, $E_S\subseteq C^\square$ to be the set of commutative squares whose image under $S$ ie exact (i.e. it is “anticommutative” in $\Prof\supseteq\Cat$).

In particular, if $S=\cate{Sub}$ is precisely the subobject functor $C^\op\to\Cat$, where $\cate{Sub}(X)$ is the category (=poset) of subobjects of $X$, the resulting theory of relations $Re(E_\cate{Sub})$ is the calculus of functors between $\cate{Sub}(X), \cate{Sub}(Y)$ that are representable by a path in $C$.

If to every path $c$ we associate the projective limit of $c$ regarded as a diagram, we determine, provided all pullback squares are counted as exact, a representation of relations via spans; if $C$ doesn’t have projective limits we can always consider the limit in the category $\widehat{C}=\Set^{C^\op}$ so that $\varprojlim : \Ch(C) \to\Span(\widehat C).$

In fact, exact modifications are “strict” proofs in the sense that if, in an ordinary proof/derivation $H \to A \to B\to C \to\dots\to T$ we agree to repeat at each step the preceding assumptions in the conclusion, we obtain a chain of equivalences of exact modifications of $H$:

Working inside an object of the form $PZ$, this means avoiding to use $A\subseteq B$ and replace it with $A\cup B=B$ or equivalently $A\cap B=A$.

If now the relations are paths, using exact squares we can define what it means $R\iff S$ or $R\To T$: in this last situation, it must exist $Q$ such that $R\lor Q\iff T$. But it is unclear how to define $\lor$: this boils down to define $\To$. And consequently, one defines $R\iff S$ by $R\To S$ and $S\To R$.

This leads to the concept of a deductive square, standing in the same relation $\To$ stands to $\iff$, as I define them in §13.

In the 2-category $\Cat$, an exact square (cf. (Guitart, 1980)) consists of four functors $S,T,U,V$ and a natural transformation $\varphi : U\circ S\To V\circ T$,

such that in $\Prof$ the 2-cell $\tilde\varphi : S\diamond T^o \To U^o\diamond V$ is invertible, or equivalently that the maps

induce an isomorphism

In addition to all examples in (Guitart, 1980) recalled in §3, we also recall that $\varphi$ is exact if and only if for all pointwise Kan extensions in $\Cat$ of the form the composite figure remains a pointwise Kan extension.

Bourn and Cordier have shown in (Bourn & Cordier, 1980) that the same preservation property of pointwise extensions is true in $\Prof$, from whence they deduce that an exact square is the most general situation where one has a factorization where $T_S$ and $T_V$ are, respectively, the codensity monads of $S$ and $V$.

We can also regard an exact square $\varphi$ as a generalized ternary decomposition of $B$, by virtue of the following example.

Let $E,D,M$ be three subcategories of $B$, and let $A$ be the category having as objects all morphisms of $D$ and as morphisms the commutative squares where $u,v$ are invertible. Then $(E,D,M)$ is a ternary decomposition of $B$ if and only if the square is exact, if we posit $\varphi=d$.

An exact square is said to be sub-exact (resp., sur-exact) if and only if for each pair $(x,y)$ of objects in $X\times Y$, $\tilde\varphi_{x,y}$ is injective (resp., surjective).

Any given square $\varphi$ can be decomposed into $\varphi = i \otimes_\epsilon s$, where $\epsilon$ is an exact square, $\otimes_\epsilon$ the multiplicative structure (cf. (Guitart, 1980), §1.5) induced by $\epsilon$, $i$ a sub-exact square, and $s$ a sur-exact square. This result is a 2-dimensional version of the 1-dimensional epi-mono factorization theorem.

Let $\mathbb C$ be a 2-category equipped with a class $\mathbb E$ of squares called exacts (for example, the exact squares in the sense of $H$ or $H^\op$ or $M$, cf. (Guitart, 1980)), and let $K$ be a class of morphisms of $\mathbb C$ called “canonical comparisons” (for example, monomorphisms of $\mathbb C$, or epimorphisms, or morphisms in $\mathbb C$ having an adjoint 1-cell,…). In the same notation of §9 we give the following definition.

The 2-category $\Rel_{\mathbb E,K}(\mathbb C)$ has objects those of $\mathbb C$ and as morphisms the elements of $Re(\mathbb E)$, called relations, and 2-morphisms generated by the $\mathbb E$-$K$-deductive squares, that will be called proofs.

This way to describe the 2-category of relations improves the one given in §3 of (Guitart, 1980).