|
|
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...
|
|
|
A general framework for logics of questions
Punčochář, Vít
This paper provides an overview of basic inquisitive semantics and its generalization proposed in (Punčochář, submitted). It is shown that the generalization allows to model questions over any of a large class of non-classical logics and so avoids paradoxes of material implication and irrelevance in the logic of questions. Moreover, it is advocated that the general framework does not lose any of the characteristic features of basic inquisitive semantics that are needed for modeling of questions.
|
|
|
Undecidability of Some Substructural Logics
Chvalovský, Karel ; Bílková, Marta (advisor) ; Buszkowski, Vojciech (referee) ; Galatos, Nick (referee)
This thesis deals with the algorithmic undecidability (unsolvability) of provability in some non-classical logics. In fact, there are two natural variants of this problem. Fix a logic, we can study its set of theorems or its consequence relation, which is a more general problem. It is well-known that both these problems can be undecidable already for propositional logics and we provide further examples of such logics in this thesis. In particular, we study propositional substructural logics which are obtained from the sequent calculus LJ for intuitionistic logic by dropping structural rules. Our main results are the following. First, (finite) consequence relations in some basic non-associative substructural logics are shown to be undecidable. Second, we prove that a basic associative substructural logic with the contraction rule, which is notorious for being hard to handle, has an undecidable set of theorems. Since the studied logics have natural algebraic semantics, we also obtain corresponding algebraic results which are interesting in their own right.
|
|
| |
guest ::
