Tourlakis, George2016-11-252016-11-252016-06-232016-11-25http://hdl.handle.net/10315/32701Since 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.enAuthor owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.Computer scienceElectronic Thesis or Dissertation2016-11-25Modal logicsPredicate calculusProvability logicCut eliminationGentzenisationQuantified GLPredicate modal logicPredicate provability logic