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.