Skip navigation
Skip navigation

Proof theory and proof search of bi-intuitionistic and tense logic

Postniece, Linda

Description

In this thesis, we consider bi-intuitionistic logic and tense logic, as well as the combined bi-intuitionistic tense logic. Each of these logics contains a pair of dual connectives, for example, Rauszer's bi-intuitionistic logic contains intuitionistic implication and dual intuitionistic exclusion. The interaction between these dual connectives makes it non-trivial to develop a cut-free sequent calculus for these logics. In the first part of this thesis we develop a new extended sequent...[Show more]

dc.contributor.authorPostniece, Linda
dc.date.accessioned2018-11-22T00:05:49Z
dc.date.available2018-11-22T00:05:49Z
dc.date.copyright2010
dc.identifier.otherb2569805
dc.identifier.urihttp://hdl.handle.net/1885/150486
dc.description.abstractIn this thesis, we consider bi-intuitionistic logic and tense logic, as well as the combined bi-intuitionistic tense logic. Each of these logics contains a pair of dual connectives, for example, Rauszer's bi-intuitionistic logic contains intuitionistic implication and dual intuitionistic exclusion. The interaction between these dual connectives makes it non-trivial to develop a cut-free sequent calculus for these logics. In the first part of this thesis we develop a new extended sequent calculus for bi-intuitionistic logic using a framework of derivations and refutations. This is the first purely syntactic cut-free sequent calculus for bi-intuitionistic logic and thus solves an open problem. Our calculus is sound, semantically complete and allows terminating backward proof search, hence giving rise to a decision procedure for bi-intuitionistic logic. In the second part of this thesis we consider the broader problem of taming proof search in display calculi, using bi-intuitionistic logic and tense logic as case studies. While the generality of display calculi makes it an excellent framework for designing sequent calculi for logics where traditional sequent calculi fail, this generality also leads to a large degree of non-determinism, which is problematic for backward proof-search. We control this non-determinism in two ways: 1. First, we limit the structural connectives used in the calculi and consequently, the number of display postulates. Specifically, we work with nested structures which can be viewed as a tree of traditional Gentzen's sequents, called nested sequents, which have been used previously by Kashima and, independently, by Brunnler and Strafsburger and Poggiolesi to present several modal and tense logics; 2. Second, since residuation rules are largely responsible for the difficulty in finding a proof search procedure for display-like calculi, we show how to eliminate these residuation rules using deep inference in nested sequents; Finally, we study the combined bi-intuitionistic tense logic, which contains the well-known intuitionistic modal logic as a sublogic. We give a nested sequent calculus for bi-intuitionistic tense logic that has cut-elimination, and a derived deep inference nested sequent calculus that is complete with respect to the first calculus and where contraction and residuation rules are admissible. We also show how our calculi can capture Simpson's intuitionistic modal logic [104] and Ewald's intuitionistic tense logic.
dc.format.extentvii, 228 leaves.
dc.language.isoen_AU
dc.rightsAuthor retains copyright
dc.subject.lccQA9.54.P67 2010
dc.subject.lcshProof theory
dc.subject.lcshLogic, Symbolic and mathematical
dc.titleProof theory and proof search of bi-intuitionistic and tense logic
dc.typeThesis (PhD)
local.description.notesThesis (Ph.D)--Australian National University,
dc.date.issued2010
local.type.statusAccepted Version
local.contributor.affiliationAustralian National University.
local.identifier.doi10.25911/5d5fcc3a4db33
dc.date.updated2018-11-21T00:07:25Z
dcterms.accessRightsOpen Access
local.mintdoimint
CollectionsOpen Access Theses

Download

File Description SizeFormat Image
b25698059_Postniece_Linda.pdf58.81 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