A Short and Readable Proof of Cut Elimination for Two 1st Order Modal Logics

Simple item page
dc.contributor.advisorTourlakis, George
dc.creatorGao, Feng
dc.date.accessioned2016-11-25T14:03:55Z
dc.date.available2016-11-25T14:03:55Z
dc.date.copyright2016-06-23
dc.date.issued2016-11-25
dc.date.updated2016-11-25T14:03:55Z
dc.degree.disciplineComputer Science
dc.degree.levelMaster's
dc.degree.nameMSc - Master of Science
dc.description.abstractSince 1960s, logicians, philosophers, AI people have cast eyes on modal logic. Among various modal logic systems, propositional provability logic which was established by Godel modeling provability in axiomatic Peano Arithmetic (PA) was the most striking application for mathematicians. After Godel, researchers gradually explored the predicate case in provability logic. However, the most natural application QGL for predicate provability logic is not able to admit cut elimination. Recently, a potential candidate for the predicate provability logic ML3 and its precursors BM and M3 introduced by Toulakis,Kibedi, Schwartz dedicated that A is always closed. Although ML3, BM and M3 are cut free, the cut elimination proof with the unfriendly nested induction of high multiplicity is difficult to understand. In this thesis, I will show a cut elimination proof for all (Gentzenisations) of BM, M3 and ML3, with much more readable inductions of lower multiplicity.
dc.identifier.urihttp://hdl.handle.net/10315/32701
dc.language.isoen
dc.rightsAuthor owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.
dc.subjectComputer science
dc.subject.keywordsModal logics
dc.subject.keywordsPredicate calculus
dc.subject.keywordsProvability logic
dc.subject.keywordsCut elimination
dc.subject.keywordsGentzenisation
dc.subject.keywordsQuantified GL
dc.subject.keywordsPredicate modal logic
dc.subject.keywordsPredicate provability logic
dc.titleA Short and Readable Proof of Cut Elimination for Two 1st Order Modal Logics
dc.typeElectronic Thesis or Dissertation

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Gao_Feng_2016_Masters.pdf
Size:
349.39 KB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
license.txt
Size:
1.83 KB
Format:
Plain Text
Description:
Download
No Thumbnail Available
Name:
YorkU_ETDlicense.txt
Size:
3.38 KB
Format:
Plain Text
Description:
Download

Collections

Computer Science and Engineering

All items in the YorkSpace institutional repository are protected by copyright, with all rights reserved except where explicitly noted.