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.