|
|
Proof Systems: A Study on Form and Complexity
Jalali Keshavarz, Raheleh ; Pudlák, Pavel (advisor) ; Metcalfe, George (referee) ; Ramanayake, Revantha (referee)
Proof Systems: A Study on Form and Complexity This dissertation includes three parts. The first two parts are related to each other. In [2] and [1], Iemhoff introduced a connection between the existence of a terminating sequent calculus of a certain kind and the uniform inter- polation property of the super-intuitionistic logic that the calculus captures. In the second part, we will generalize this relationship to also cover the sub- structural setting on the one hand and a more powerful type of systems called semi-analytic calculi, on the other. To be more precise, we will show that any sufficiently strong substructural logic with a semi-analytic calculus has Craig interpolation property and in case that the calculus is also terminating, it has uniform interpolation. This relationship then leads to some concrete applications. On the positive side, it provides a uniform method to prove the uniform interpolation property for the logics FLe, FLew, CFLe, CFLew, IPC, CPC and some of their K and KD-type modal extensions. However, on the negative side the relationship finds its more interesting application to show that many sub-structural logics including Ln, Gn, BL, R and RMe , al- most all super-intutionistic logics (except at most seven of them) and almost all extensions of S4 (except thirty seven of them) do not...
|
guest ::
