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.