Mathematics, philosophy, and proof theory

Abstract

Our purpose shall be to introduce revisions into the foundational systematic introduced by Brouwer and Hilbert in the early part of the last century. We will apply these revisions to develop a symbolic calculus for the study of extralogical intuition (in formalism, logic at the metalevel), which we shall show to be not weaker than intuitionistic propositional calculus, and rich enough to encode all of nitary set theory. Our calculus will be e cient in its principles and based on a small, compact set of axioms, and its consistency will be shown. In the main it will be based on two departures from traditional developments: (1) the interpretation of logical conjunction as a mathematical operation of set formation, and (2) the interpretation of logical implication as the exchange (in time) of actual or intuited objects. Its rule structure, in addition, will possess two novel features: (1) generalized substitution, or what we call herein deposition, and (2) a formal method of assumption.