Skip navigation
Skip navigation

Proof-functional semantics for relevant implication

Lavers, Peter

Description

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...[Show more]

dc.contributor.authorLavers, Peter
dc.date.accessioned2013-09-19T00:08:43Z
dc.date.available2013-09-19T00:08:43Z
dc.identifier.otherb17715763
dc.identifier.urihttp://hdl.handle.net/1885/10488
dc.description.abstractIn 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.
dc.language.isoen_AU
dc.titleProof-functional semantics for relevant implication
dc.typeThesis (PhD)
local.contributor.supervisorSylvan, Richard
local.contributor.supervisorMcRobbie, Michael
local.contributor.supervisorMeyer, Bob
dcterms.valid1990
local.description.notesSupervisors: Dr Richard Sylvan, Prof Michael McRobbie and Dr Bob Meyer. This thesis has been made available through exception 200AB to the Copyright Act.
local.description.refereedYes
local.type.degreeDoctor of Philosophy (PhD)
dc.date.issued1990
local.contributor.affiliationAustralian National University
local.identifier.doi10.25911/5d78d4b9141d6
local.mintdoimint
CollectionsOpen Access Theses

Download

File Description SizeFormat Image
01Front_Lavers.pdfFront Matter159.88 kBAdobe PDFThumbnail
02Whole_Lavers.pdfWhole Thesis2.49 MBAdobe PDFThumbnail


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator