Search

Abstract: The larger project broached here is to look at the generally sentence “if is well-ordered then is well-ordered”, where is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded -models for a particular theory whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function . To illustrate this theme, we prove in this paper that the statement “if is well-ordered then is well-ordered” is equivalent to . This was first proved by Marcone and Montalban [Alberto Marcone, Antonio Montalbán, The epsilon function for computability theorists, draft, 2007] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte’s method of proof search (deduction chains) [Kurt Schütte, Proof Theory, Springer-Verlag, Berlin, Heidelberg, 1977] and cut elimination for a (small) fragment of . [Copyright &y& Elsevier]

Abstract: For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius (1991) for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge (Brünnler and Studer, 2009) and by Hill and Poggiolesi (2010) for PDL, which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach can be pushed in general. To this end, we introduce a nested sequent system with syntactic cut-elimination which is incomplete for the modal mu-calculus, but complete with respect to a restricted language that allows only fixed points of a certain form. This restricted language includes the logic of common knowledge and PDL. There is also a traditional sequent system for the modal mu-calculus by Jäger et al. (2008) , without a syntactic cut-elimination procedure. We embed that system into ours and vice versa, thus establishing cut-elimination also for the shallow system, when only the restricted language is considered. [Copyright &y& Elsevier]

Abstract: Starting from Girard’s seminal paper on light linear logic (LLL), a number of works investigated systems derived from linear logic to capture polynomial time computation within the computation-as-cut-elimination paradigm. The original syntax of LLL is too complicated, mainly because one has to deal with sequents which do not just consist of formulas but also of ‘blocks’ of formulas. We circumvent the complications of ‘blocks’ by introducing a new modality which is exclusively in charge of ‘additive blocks’. One of the most interesting features of this purely multiplicative is the possibility of the second-order encodings of additive connectives. The resulting system (with the traditional syntax), called Easy-LLL, is still powerful to represent any deterministic polynomial time computations in purely logical terms. Unlike the original LLL, Easy-LLL admits polynomial time strong normalization together with the Church–Rosser property, namely, cut elimination terminates in a unique way in polytime by any choice of cut reduction strategies. [Copyright &y& Elsevier]