Proof-functional semantics for relevant implication

Abstract

In this thesis I provide a theory of implication from within the Gentzen/Curry formalist constructivist tradition. Formal consecution and natural deduction systems, which satisfy the formalist and also the intuitionist desiderata for constructivity (including Lorenzen's principle of inversion), are provided for all implication logics. The similar-but simplified- binary relational ("Kripke-style") semantics are also given. The driving force behind this research has been the desire to provide an explanatory semantics for relevant implication in terms of "use as a subproof in a proof". To this end relevant consecution systems which exploit various precisely characterised notions of use are described. The basis of this work has been the development of a way of describing the shapes of proofs in the "object language". In chapter 2 I motivate and introduce the basic machinery used to describe proofs, and show how thereby to capture use. This involves a more detailed consideration of the internal structure of formal systems than exploited by Curry in his epitheory of formal systems. In chapter 3 the completely general "cloned" consecution systems are described, and it is shown that every logic with an axiomatic formulation is captured by such a system. In chapter 4 the corresponding natural deduction systems are described and it is shown that Lorenzen's principle of inversion holds for them by proving the appropriate reduction theorem. Thus every implication logic has a formulation which satisfies the intuitionist formal criterion for constructivity. In chapter 5 we return to the business of providing explanatory semantics for relevant implication, using the similar style of consecution system as in chapter 3, but with list (proof-description) manipulation rules which capture use. In chapter 6 "cloned" binary relation semantics are described which also capture every logic with an axiomatic formulation. These don't quite correspond to the consecution systems of chapter 3 in that they exploit a dramatic simplification of the list machinery (but do involve other complications). The similar relevant semantics using use rules is also given. The corresponding "simplified" consecution and natural deduction systems are described in appendix B .2. These systems do not satisfy the Lorenzen principle of inversion and so are not constructive. Chapter 7 rounds off and offers some thoughts about possible further developments. Appendix A shows an early attempt to capture relevant implication, and is notable as the most complex formulation of intuitionist implication ever devised. Show more