Publications

In this paper we intend to study implications in their most general form, generalizing different classes of implications including the Heyting implication, sub-structural implications and weak strict implications. Following the topological interpretation of the intuitionistic logic, we will introduce non-commutative spacetimes to provide a more dynamic and subjective interpretation of an intuitionistic proposition. These combinations of space and time are natural sources for well-behaved implications and we will show that their spatio-temporal implications represent any other reasonable abstract implication. Then to provide a faithful well-behaved syntax for abstract implications, we will develop a logical system for the non-commutative spacetimes for which we will present both topological and Kripke semantics. These logics unify sub-structural and sub-intuionistic logics by embracing them as their special fragments.

∇-algebras are the natural generalization of Heyting algebras, unifying many algebraic structures including bounded lattices, Heyting algebras, temporal Heyting algebras and point-free formalization for dynamical systems. They are also powerful enough to represent any “natural" abstract modality and any abstract implication. In this paper, we will study the algebraic and topological properties of different varieties of these algebras. These investigations starts with the algebraic theme of characterizing the sub-directly and simple ∇-algebras, the Dedekind-MacNeille completion, the canonical construction and the amalgamation property. Then, we will move to the topological theme to provide a unification of Priestley and Esakia dualities to capture the dual spaces corresponding to these algebras. This, then leads to spectral duality and finally to some ring-theoretic representation for some of these algebras.

In this paper we will present a class of rules called the \textitalmost positive rules to show that any proof system for an intuitionistic modal logic that consists of theses rules, the cut and the necessitation rule has the feasible disjunction property. This method uniformly proves the property for the usual sequent-style and Hilbert-style proof systems for a broad range of intuitionistic modal logics, including IK, IKT, IK4, IS4, IS5, their Fisher-Servi versions, the intuitionistic logics for bounded depth and bounded width and the propositional lax logic. On the negative side, though, it shows that if an intuitionistic modal logic does not admit the Visser rules or specially does not have the disjunction property, then it does not have a calculus consisting only of almost positive rules, the cut rule and the necessitation rule. As the class of these rules is a general and natural class to consider, this negative result presents an interesting proof theoretical result about generic proof systems and their existence.

In this paper, a proof-theoretic method to prove uniform Lyndon interpolation for non-normal modal logics is introduced and applied to show that the logics E, M, MC, EN, MN have that property. In particular, these logics have uniform interpolation. Although for some of them the latter is known, the fact that they have uniform Lyndon interpolation is new. Also, the proof-theoretic proofs of these facts are new, as well as the constructive way to explicitly compute the interpolants that they provide. It is also shown that the non-normal modal logics EC and ECN do not have Craig interpolation, and whence no uniform (Lyndon) interpolation.

In [7] and [8], Iemhoff introduced a connection between the existence of a terminating sequent calculus of a certain kind and the uniform interpolation property of the super-intuitionistic logic that the calculus captures. In this paper, we will generalize this relationship to also cover the substructural 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 suciently 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 FL_e, FL_ew, CFL_e, CFL_ew, IPC, CPC and some of their K and KD-type modal extensions. However, on the negative side the relationship nds its more interesting application to show that many substructural logics including L_n, G_n, BL, R and RM^e, almost all super-intutionistic logics (except at most seven of them) and almost all extensions of S4 (except thirty seven of them) do not have a semi-analytic calculus. It also shows that the logic K4 and almost all extensions of the logic S4 (except six of them) do not have a terminating semi-analytic calculus.

A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this paper we will develop a theory for these computational flows to design a classical direct reading of the Dialectica interpretation. This theory makes a sound and complete interpretation for bounded theories of arithmetic as well as the low complexity statements of strong unbounded systems. We will first use this fact to extract the computational content of the low complexity statements in some bounded theories of arithmetic such as IU_k, T^k_n, I\Delta_0(\exp) and \PRA. And then we will apply the theory on some strong unbounded mathematical theories such as \PA and \PA+\TI(α) using the bridge of continuous cut elimination technique.

In [1], we have developed a theory of deterministic flows to extend the spirit of the Dialectica interpretation to weak bounded theories of arithmetic. In this paper, we will generalize that theory to introduce the notion of a non-deterministic flow as a sequence of computational problems together with a sequence of non-deterministic version of game reductions. It provides a proof mining method for a general notion of bounded arithmetic which turns out helpful in program extractions. More specifically, it leads to a characterization of all the higher total search problems in all the higher order bounded theories of arithmetic including the interesting case of ∀\hatΣ^b_j-consequences of the hierarchy S^k_2, for 1 ≤j ≤k. Moreover, the method is also useful to provide another proof for the strong witnessing theorem for the theories S^k_2.

One of the elegant achievements in the history of proof theory is the characterization of the provably total recursive functions of the strong theories of arithmetic. This characterization relates the provability of the totality of a function on the one hand and its computability via the ordinal recursion on the theory’s proof theoretic ordinal, on the other. Unfortunately, this correspondence is not sufficiently fine-grained to also understand the bounded world of the bounded low complexity functions, i.e., the bounded functions with low complexity definitions.\{In this paper we intend to develop a refined version of the mentioned correspondence. We will characterize the provably total low complexity functions of a theory via a suitable family of syntactical ordinal-based algorithms. More precisely, we will show that a feasibly defined function is provably total in a theory iff there exists a sequence of \PV-provable polynomial time reductions with the length of the proof theoretic ordinal of the theory, starting in a feasibly computable value and ending in the value of the function itself. This characterization is useful in the classification of the feasibly defined bounded functions in a theory. More specifically, it is useful in generalizing the Beckmann’s characterization [1] of the total \NP-search problems of \PA to any theory with a reasonable ordinal analysis.

In 1933, Gödel introduced a provability interpretation of the propositional intuitionistic logic to establish a formalization for the BHK interpretation. He used the modal system, S4, as a formalization of the intuitive concept of provability and then translated IPC to S4. His work suggested the problem to find a concrete provability interpretation of the modal logic S4. In this paper, we will try to answer this problem. In fact, we will generalize Solovay’s provability interpretation of the modal logic GL to capture other modal logics such as K4, KD4 and S4. Then we will use these results to find a formalization for the BHK interpretation and we will show that with different interpretations of the BHK interpretation, we can capture some of the propositional logics such as Intuitionistic logic, minimal logic and Visser-Ruitenburg’s basic logic. Moreover, we will show that there is no provability interpretation for any extension of KD45 and also there is no BHK interpretation for the classical propositional logic.

The branch of provability logic investigates the provability-based behavior of the mathematical theories. In a more precise way, it studies the relation between a mathematical theory T and a modal logic L via the provability interpretation which interprets the modality as the provability predicate of T. In this paper we will extend this relation to investigate the provability-based behavior of a hierarchy of theories. More precisely, using the modal language with infinitely many modalities, {□n}_n=0^∞, we will define the hierarchical counterparts of some of the classical modal theories such as K4, KD4, GL and S4. Then we will define their canonical provability interpretations and their corresponding soundness-completeness theorems.

The BHK interpretation interprets propositional statements as descriptions of the world of proofs; a world which is hierarchical in nature. It consists of different layers of the concept of proof; the proofs, the proofs about proofs and so on. To describe this hierarchical world, one approach is the Russellian approach in which we use a typed language to reflect this hierarchical nature in the syntax level. In this case, since the connective responsible for this hierarchical behavior is implication, we will use a typed language equipped with a hierarchy of implications, {\to_n}^∞_n=0. In fact, using this typed propositional language, we will introduce the hierarchical counterparts of the logics BPC, EBPC, IPC and FPL and then by proving their corresponding soundness-completeness theorems with respect to their natural BHK interpretations, we will show how these different logics describe different worlds of proofs embodying different hierarchical behaviors.