Some Neglected Work in General Metamathematics

David Miller
University of Warwick

The logic of deductive theories (including theories that may not be finitely axiomatizable) was initiated by Tarski in the double paper `Foundations of the Calculus of Systems' of 1935/1936.  In effect he showed that if the meet and join operations on theories are extensions of  the same operations on sentences, then deductive theories form a Brouwerian lattice under the relation of implication. That is, the logic of  deductive theories is dual to intuitionistic logic. Although the theory of Brouwerian lattices is quite well developed, its purely logical  applications have received little attention.

Starting from frankly verificationist assumptions in the theory of meaning, Dummett has argued that intuitionistic logic is the correct logic not only in mathematics but in all discourse. Luntley and Milne have separately claimed that the same result is obtained even if the premises are falsificationist.  But Dummett himself later reached a different & more congenial conclusion, that falsificationist premises lead to something  like dual-intuitionistic logic.  These writers were not helped by their assumption that logic must support a material conditional (an operation  that does not exist everywhere in a Brouwerian lattice).

It is suggested in the paper that Dummett's later speculations were on the right lines, though little sympathy is shown for his doctrine that matters of meaning are important in determining which logic should be used.  If we represent our state of knowledge not by what has been proved but by what has not been falsified, then we can provide in an obvious way a Kripke-style semantics for dual- intuitionistic logic.  This logic, which is paraconsistent, is not a logic of truth, for which classical logic suffices at the level of sentences, but a logic of what is falsified, or of what must be regarded as falsified.  It is shown how these ideas connect naturally with the logic of deductive theories with which the paper began.