Search

In this paper we analyze k -ary inclusion–exclusion logic, INEX[ k ], which is obtained by extending first order logic with k -ary inclusion and exclusion atoms. We show that every formula of INEX[ k ] can be expressed with a formula of k -ary existential second order logic, ESO[ k ]. Conversely, every formula of ESO[ k ] with at most k -ary free relation variables can be expressed with a formula of INEX[ k ]. From this it follows that, on the level of sentences, INEX[ k ] captures the expressive power of ESO[ k ]. We also introduce several useful operators that can be expressed in INEX[ k ]. In particular, we define inclusion and exclusion quantifiers and so-called term value preserving disjunction which is essential for the proofs of the main results in this paper. Furthermore, we present a novel method of relativization for team semantics and analyze the duality of inclusion and exclusion atoms. [ABSTRACT FROM AUTHOR]

In this paper, we axiomatize the negatable consequences in dependence and independence logic by extending the systems of natural deduction of the logics given in [22] and [11]. We prove a characterization theorem for negatable formulas in independence logic and negatable sentences in dependence logic, and identify an interesting class of formulas that are negatable in independence logic. Dependence and independence atoms, first-order formulas belong to this class. We also demonstrate our extended system of independence logic by giving explicit derivations for Armstrong's Axioms and the Geiger-Paz-Pearl axioms of dependence and independence atoms. [ABSTRACT FROM AUTHOR]

In this paper we present a procedure allowing the extension of a CERES -based cut-elimination method to intuitionistic logic. Previous results concerning this problem manage to capture fragments of intuitionistic logic, but in many essential cases structural constraints were violated during normal form construction resulting in a classical proof. The heart of the CERES method is the resolution calculus, which ignores the structural constraints of the well known intuitionistic sequent calculi. We propose, as a method of avoiding the structural violations, the generalization of resolution from the resolving of clauses to the resolving of cut-free proofs, in other words, what we call proof resolution . The result of proof resolution is a cut-free proof rather than a clause. Note that resolution on ground clauses is essentially atomic cut, thus using proof resolution to construct cut-free proofs one would need to join the two proofs together and remove the atoms which where resolved. To efficiently perform this joining (and guarantee that the resulting cut-free proof is intuitionistic) we develop the concept of proof subsumption (similar to clause subsumption) and indexed resolution , a refinement indexing atoms by their corresponding positions in the cut formula. Proof subsumption serves as a tool to prove the completeness of the new method CERES -i, and indexed resolution provides an efficient strategy for the joining of two proofs which is in general a nondeterministic search. Such a refinement is essential for any attempt to implement this method. Finally we compare the complexity of CERES -i with that of Gentzen-based methods. [ABSTRACT FROM AUTHOR]

The Gödel–Artemov framework offered a formalization of the Brouwer–Heyting–Kolmogorov (BHK) semantics of intuitionistic logic via classical proofs. In this framework, the intuitionistic propositional logic is embedded in the modal logic , is realized in the Logic of Proofs , and has a provability interpretation in Peano Arithmetic. Self-referential -formulas of the type ‘t is a proof of a formula ϕ containing t itself’ are permitted in the realization of in , and if such formulas are indeed involved, it is then necessary to use fixed-point arithmetical methods to explain intuitionistic logic via provability. The natural question of whether self-referentiality can be avoided in realization of was answered negatively by Kuznets who provided an -theorem that cannot be realized without using directly self-referential -formulas. This paper studies the question of whether can be embedded in and then realized in without using self-referential formulas. We consider a general class of Gödel-style modal embeddings of in and by extending Kuznetsʼ method, show that there are -theorems such that, under each such embedding, are mapped to -theorems that cannot be realized in without using directly self-referential formulas. Interestingly, all double-negations of tautologies that are not -theorems, like , are shown to require direct self-referentiality. Another example is found in , the purely implicational fragment of . This suggests that the BHK semantics of intuitionistic logic (even of intuitionistic implication) is intrinsically self-referential. This paper is an extended version of [26]. [ABSTRACT FROM AUTHOR]

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for S4LPN based on Artemov–Fitting models. [ABSTRACT FROM AUTHOR]

Abstract: We introduce several concepts concerning the indiscernibility of trees. A tree is by definition an ordered set such that, for any , the initial segment determined by a is a linearly ordered set. A typical example of a tree is the set of finite ω-sequences with the order relation , where means that η is a proper initial segment of ν. In this paper, we consider some structure M in the language L and are interested in sets A of the form , where O is a tree, and labeled by η is an element in M. Such a set A is also called a tree in this paper. We study the indiscernibility of trees A in general settings and apply the obtained results to the study of unstable theories. [Copyright &y& Elsevier]

Abstract: This paper presents new constructions of models of Hume’s Principle and Basic Law V with restricted amounts of comprehension. The techniques used in these constructions are drawn from hyperarithmetic theory and the model theory of fields, and formalizing these techniques within various subsystems of second-order Peano arithmetic allows one to put upper and lower bounds on the interpretability strength of these theories and hence to compare these theories to the canonical subsystems of second-order arithmetic. The main results of this paper are: (i) there is a consistent extension of the hypearithmetic fragment of Basic Law V which interprets the hyperarithmetic fragment of second-order Peano arithmetic, and (ii) the hyperarithmetic fragment of Hume’s Principle does not interpret the hyperarithmetic fragment of second-order Peano arithmetic, so that in this specific sense there is no predicative version of Frege’s Theorem. [Copyright &y& Elsevier]

Abstract: Justification logic is a new generation of epistemic logics which along with the traditional modal knowledge/belief operators also consider justification assertions ‘ is a justification for .’ In this paper, we introduce a prefixed tableau system for one of the major logics of this kind S4LPN, which combines the Logic of Proofs (LP) and epistemic logic S4 with an explicit negative introspection principle . We show that the prefixed tableau system for S4LPN is sound and complete with respect to Fitting-style semantics. We also introduce a hypersequent calculus HS4LPN and show that HS4LPN is complete. We establish this fact by using a translation from the prefixed tableau system to the hypersequent calculus. This completeness result gives us a semantic proof of cut-admissibility for S4LPN. We conclude the paper by discussing a subsystems of S4LPN, namely S4LP. [Copyright &y& Elsevier]

Abstract: In this paper, we study the notions related to tree property 1 (=TP1), or, equivalently, SOP2. Among others, we supply a type-counting criterion for TP1 and show the equivalence of TP1 and - TP1. Then we introduce the notions of weak - TP1 for , and also supply type-counting criteria for those. We do not know whether weak - TP1 implies TP1, but at least we prove that each weak - TP1 implies SOP1. Our generalization of the tree-indiscernibility results in Džamonja and Shelah (2004) is crucially used throughout the paper. [Copyright &y& Elsevier]

Abstract: This paper is a sequel to the papers Baaz and Iemhoff (2006, 2009) in which an alternative skolemization method called eskolemization was introduced that, when restricted to strong existential quantifiers, is sound and complete for constructive theories. In this paper we extend the method to universal quantifiers and show that for theories satisfying the witness property it is sound and complete for all formulas. We obtain a Herbrand theorem from this, and apply the method to the intuitionistic theory of equality and the intuitionistic theory of monadic predicates. [ABSTRACT FROM AUTHOR]

Abstract: This paper shows that the inhabitation problem in the lambda calculus with negation, product, polymorphic, and existential types is decidable, where the inhabitation problem asks whether there exists some term that belongs to a given type. In order to do that, this paper proves the decidability of the provability in the logical system defined from the second-order natural deduction by removing implication and disjunction. This is proved by showing the quantifier elimination theorem and reducing the problem to the provability in propositional logic. The magic formulas are used for quantifier elimination such that they replace quantifiers. As a byproduct, this paper also shows the second-order witness theorem which states that a quantifier followed by negation can be replaced by a witness obtained only from the formula. As a corollary of the main results, this paper also shows Glivenko’s theorem, Double Negation Shift, and conservativity for antecedent-empty sequents between the logical system and its classical version. [Copyright &y& Elsevier]

Abstract: First order reasoning about hyperintegers can prove things about sets of integers. In the author’s paper Nonstandard Arithmetic and Reverse Mathematics, Bulletin of Symbolic Logic 12 (2006) 100–125, it was shown that each of the “big five” theories in reverse mathematics, including the base theory , has a natural nonstandard counterpart. But the counterpart of has a defect: it does not imply the Standard Part Principle that a set exists if and only if it is coded by a hyperinteger. In this paper we find another nonstandard counterpart, , that does imply the Standard Part Principle. [Copyright &y& Elsevier]

Abstract: LP can be seen as a logic of knowledge with justifications. See [S. Artemov, The logic of justification, The Review of Symbolic Logic 1 (4) (2008) 477–513] for a recent comprehensive survey of justification logics generally. Artemov’s Realization Theorem says justifications can be extracted from validities in the more conventional Hintikka-style logic of knowledge S4, in which they are not explicitly present. Justifications, however, are far from unique. There are many ways of realizing each theorem of S4 in the logic LP. If the machinery of justifications is to be applied to artificial intelligence, or better yet, to everyday reasoning, we will need to work with whatever justifications we may have at hand—one version may not be interchangeable with another, even though they realize the same S4 formula. In this paper we begin the process of providing tools for reasoning about justifications directly. The tools are somewhat complex, but in retrospect this should not be surprising. Among other things, we provide machinery for combining two realizations of the same formula, and for replacing subformulas by equivalent subformulas. (The second of these is actually weaker than just stated, but this is not the place for a detailed formulation.) The results are algorithmic in nature—semantics for LP plays no role. We apply our results to provide a new algorithmic proof of Artemov’s Realization Theorem itself. This paper is a much extended version of [M.C. Fitting, Realizations and LP, in: S. Artemov, A. Nerode (Eds.), Logical Foundations of Computer Science—New York ’07, in: Lecture Notes in Computer Science, vol. 4514, Springer-Verlag, 2007, pp. 212–223]. [Copyright &y& Elsevier]

Abstract: In this paper, we study (), the interpretability logic of . As is neither an essentially reflexive theory nor finitely axiomatizable, the two known arithmetical completeness results do not apply to : () is not or . () does, of course, contain all the principles known to be part of (All), the interpretability logic of the principles common to all reasonable arithmetical theories. In this paper, we take two arithmetical properties of and see what their consequences in the modal logic () are. These properties are reflected in the so-called Beklemishev Principle , and Zambella’s Principle , neither of which is a part of (All). Both principles and their interrelation are submitted to a modal study. In particular, we prove a frame condition for . Moreover, we prove that follows from a restricted form of . Finally, we give an overview of the known relationships of () to important other interpretability principles. [Copyright &y& Elsevier]

Abstract: The jump operator on the -enumeration degrees was introduced in [I.N. Soskov, The -enumeration degrees, J. Logic Computat. 17 (2007) 1193–1214]. In the present paper we prove a jump inversion theorem which allows us to show that the enumeration degrees are first order definable in the structure of the -enumeration degrees augmented by the jump operator. Further on we show that the groups of the automorphisms of and of the enumeration degrees are isomorphic. In the second part of the paper we study the jumps of the -enumeration degrees below . We define the ideal of the almost zero degrees and obtain a natural characterization of the class of the -enumeration degrees below which are high for some and of the class of the -enumeration degrees below which are low for some . [Copyright &y& Elsevier]

Abstract: In 1981, Paris and Wilkie raised the open question about whether and to what extent the axiom system did satisfy the Second Incompleteness Theorem under Semantic Tableaux deduction. Our prior work showed that the semantic tableaux version of the Second Incompleteness Theorem did generalize for the most common definition of appearing in the standard textbooks. However, there was an alternate interesting definition of this axiom system in the Wilkie–Paris article in the Annals of Pure and Applied Logic 35 (1987), pp. 261–302 which we did not examine in our year-2002 article in the Journal of Symbolic Logic. Our first goal is to show that the incompleteness results of our prior paper can generalize in this alternate context. We will also develop a formal analysis, using a new technique called Passive Induction, that is simpler than the formalism we had used before. A further reason our results are of interest is that we have shown in a companion paper published in Electronic Notes in Theoretical Computer Science 165 (2006), pp. 213–226 that some very unorthodox axiomizations for are anti-thresholds for the Herbrandized version of the Second Incompleteness Theorem. Thus, different axiomizations for have nearly fully opposite incompleteness properties. This paper is self-contained. It will not require a knowledge of our earlier results. [Copyright &y& Elsevier]

Abstract: In this paper, we present a categorical model for Multiplicative Additive Polarized Linear Logic , which is the linear fragment (without structural rules) of Olivier Laurent’s Polarized Linear Logic. Our model is based on an adjunction between reflective/coreflective full subcategories / of an ambient -autonomous category (with products). Similar structures were first introduced by M. Barr in the late 1970’s in abstract duality theory and more recently in work on game semantics for linear logic. The paper has two goals: to discuss concrete models and to present various completeness theorems. As concrete examples, we present (i) a hypercoherence model, using Ehrhard’s hereditary/anti-hereditary objects, (ii) a Chu-space model, (iii) a double gluing model over our categorical framework, and (iv) a model based on iterated double gluing over a -autonomous category. For the multiplicative fragment of , we present both weakly full (Läuchli-style) as well as full completeness theorems, using a polarized version of functorial polymorphism in a double-glued hypercoherence model. For the latter, we introduce a notion of polarized -softness which is a variation of Joyal’s softness. This permits us to reduce the problem of polarized multiplicative full completeness to the nonpolarized MLL case, which we resolve by familiar functorial methods originating with Loader, Hyland, and Tan. Using a polarized Gustave function, we show that full completeness for fails for this model. [Copyright &y& Elsevier]

Abstract: Constructive Zermelo–Fraenkel set theory, CZF, can be interpreted in Martin-Löf type theory via the so-called propositions-as-types interpretation. However, this interpretation validates more than what is provable in CZF. We now ask ourselves: is there a reasonably simple axiomatization (by a few axiom schemata say) of the set-theoretic formulae validated in Martin-Löf type theory? The answer is yes for a large collection of statements called the mathematical formulae. The validated mathematical formulae can be axiomatized by suitable forms of the axiom of choice. The paper builds on a self-interpretation of CZF (developed in [M. Rathjen, The formulae-as-classes interpretation of constructive set theory, in: Proof Technology and Computation (Proceedings of the International Summer School Marktoberdorf 2003) IOS Press, Amsterdam, 2004 (in press)]) that provides an “inner” model of CZF which also validates the so-called -axiom of choice, . The crucial technical step taken in the present paper is to investigate the absoluteness properties of this model under the hypothesis . It is also shown that CZF plus the -axiom of choice possesses the disjunction property, the numerical existence property and the existence property for an important group of formulae. [Copyright &y& Elsevier]

Abstract: In this paper we give a rather detailed algebraic investigation of interpolation and Beth’s property in propositional many-valued logics extending Hájek’s Basic Logic [P. Hájek, Metamathematics of Fuzzy Logic, Kluwer, 1998], and we connect such properties with amalgamation and strong amalgamation in the corresponding varieties of algebras. It turns out that, while the most interesting extensions of in the language of have deductive interpolation, very few of them have Beth’s property or Craig interpolation. Thus in the last part of the paper we look for conservative extensions of having such properties. [Copyright &y& Elsevier]

Abstract: The paper shows elimination of imaginaries for real closed valued fields to suitable sorts. We also show that this result is in some sense optimal. The paper includes a quantifier elimination theorem for real closed valued fields in a language with sorts for the field, value group and residue field. [Copyright &y& Elsevier]

Abstract: While it is known that intuitionistic ZF set theory formulated with Replacement, IZF R , does not prove Collection, it is a longstanding open problem whether IZF R and intuitionistic set theory ZF formulated with Collection, IZF, have the same proof-theoretic strength. It has been conjectured that IZF proves the consistency of IZF R . This paper addresses similar questions but in respect of constructive Zermelo–Fraenkel set theory, CZF. It is shown that in the latter context the proof-theoretic strength of Replacement is the same as that of Strong Collection and also that the functional version of the Regular Extension Axiom is as strong as its relational version. Moreover, it is proved that, contrary to IZF, the strength of CZF increases if one adds an axiom asserting that the trichotomous ordinals form a set. Unlike IZF, constructive Zermelo–Fraenkel set theory is amenable to ordinal analysis and the proofs in this paper make pivotal use thereof in the guise of well-ordering proofs for ordinal representation systems. [Copyright &y& Elsevier]

This paper provides a unifying axiomatic account of the interpretation of recursive types that incorporates both domain-theoretic and realizability models as concrete instances. Our approach is to view such models as full subcategories of categorical models of intuitionistic set theory. It is shown that the existence of solutions to recursive domain equations depends upon the strength of the set theory. We observe that the internal set theory of an elementary topos is not strong enough to guarantee their existence. In contrast, as our first main result, we establish that solutions to recursive domain equations do exist when the category of sets is a model of full intuitionistic Zermelo–Fraenkel set theory. We then apply this result to obtain a denotational interpretation of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. By exploiting the intuitionistic logic of the ambient model of intuitionistic set theory, we analyse the relationship between operational and denotational semantics. We first prove an “internal” computational adequacy theorem: the model always believes that the operational and denotational notions of termination agree. This allows us to identify, as our second main result, a necessary and sufficient condition for genuine “external” computational adequacy to hold, i.e. for the operational and denotational notions of termination to coincide in the real world. The condition is formulated as a simple property of the internal logic, related to the logical notion of 1-consistency. We provide useful sufficient conditions for establishing that the logical property holds in practice. Finally, we outline how the methods of the paper may be applied to concrete models of FPC. In doing so, we obtain computational adequacy results for an extensive range of realizability and domain-theoretic models. [Copyright &y& Elsevier]

This paper deals with Tarski's first axiomatic presentations of the syntax of deductive system. Andrzej Grzegorczyk's significant results which laid the foundations for the formalization of metalogic, are touched upon briefly. The results relate to Tarski's theory of concatenation, also called the theory of strings, and to Tarski's ideas on the formalization of metamathematics. There is a short mention of author's research in the field. The main part of the paper surveys research on the theory of deductive systems initiated by Tarski, in particular research on (i) the axiomatization of the general notion of consequence operation, (ii) axiom systems for the theories of classic consequence and for some equivalent theories, and (iii) axiom systems for the theories of nonclassic consequence.In this paper the results of Jerzy Sl̵upecki's research are taken into account, and also the author's and other people belonging to his circle of scientific research. Particular study is made of his dual characterization of deductive systems, both as systems in regard to acceptance (determined by the usual consequence operation) and systems in regard to rejection (determined by the so-called rejection consequence). Comparison is made, therefore, with axiomatizations of the theories of rejection and dual consequence, and the theory of the usual consequence operation. [Copyright &y& Elsevier]

This paper investigates a connection between the semantic notion provided by the ordering ◃* among theories in model theory and the syntactic (N)SOPn hierarchy of Shelah. It introduces two properties which are natural extensions of this hierarchy, called SOP2 and SOP1. It is shown here that SOP3 implies SOP2 implies SOP1. In Shelah''s article (Ann. Pure Appl. Logic 80 (1996) 229) it was shown that SOP3 implies ◃*-maximality and we prove here that ◃*-maximality in a model of GCH implies a property called SOP2″. It has been subsequently shown by Shelah and Usvyatsov that SOP2″ and SOP2 are equivalent, so obtaining an implication between ◃*-maximality and SOP2. It is not known if SOP2 and SOP3 are equivalent.Together with the known results about the connection between the (N)SOPn hierarchy and the existence of universal models in the absence of GCH, the paper provides a step toward the classification of unstable theories without the strict order property. [Copyright &y& Elsevier]

This paper is concerned with notions of consequence. On the one hand, we study admissible consequence, specifically for substitutions of Σ10-sentences over Heyting arithmetic (HA). On the other hand, we study preservativity relations. The notion of preservativity of sentences over a given theory is a dual of the notion of conservativity of formulas over a given theory. We show that admissible consequence for Σ10-substitutions over HA coincides with NNIL-preservativity over intuitionistic propositional logic (IPC). Here NNIL is the class of propositional formulas with no nestings of implications to the left. The identical embedding of IPC-derivability (considered as a preorder and, thus, as a category) into a consequence relation (considered as a preorder) has in many cases a left adjoint. The main tool of the present paper will be an algorithm to compute this left adjoint in the case of NNIL-preservativity. In the last section, we employ the methods developed in the paper to give a characterization the closed fragment of the provability logic of HA. [Copyright &y& Elsevier]

Abstract: This paper discusses what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals , where L is a learning procedure for a rate of convergence which succeeds after at most -many mind changes. This -learnability provides quantitative information strictly in between a full rate of convergence (obtainable in general only from semi-constructive proofs) and a rate of metastability in the sense of Tao (extractable also from classical proofs). In fact, it corresponds to rates of metastability of a particular simple form. Moreover, if a certain gap condition is satisfied, then B and L yield a bound on the number of possible fluctuations. We explain recent applications of proof mining to ergodic theory in terms of these results. [Copyright &y& Elsevier]

Abstract: This paper discusses an extension of Answer Set Programming (ASP) called Hybrid Answer Set Programming (H-ASP) which allows the user to reason about dynamical systems that exhibit both discrete and continuous aspects. The unique feature of Hybrid ASP is that it allows the use of ASP type rules as controls for when to apply algorithms to advance the system to the next position. That is, if the prerequisites of a rule are satisfied and the constraints of the rule are not violated, then the algorithm associated with the rule is invoked. [Copyright &y& Elsevier]

Dependence logic, introduced in Väänänen (2007) [11], cannot be axiomatized. However, first-order consequences of dependence logic sentences can be axiomatized, and this is what we shall do in this paper. We give an explicit axiomatization and prove the respective Completeness Theorem. [ABSTRACT FROM AUTHOR]

Abstract: The fact that “natural” theories, i.e. theories which have something like an “idea” to them, are almost always linearly ordered with regard to logical strength has been called one of the great mysteries of the foundation of mathematics. However, one easily establishes the existence of theories with incomparable logical strengths using self-reference (Rosser-style). As a result, is not the least theory whose strength is greater than that of PA. But still we can ask: is there a sense in which is the least “natural” theory whose strength is greater than that of PA? In this paper we exhibit natural theories in strength strictly between PA and by introducing a notion of slow consistency. [Copyright &y& Elsevier]

Abstract: This paper develops an order-theoretic generalization of Blok and Pigozziʼs notion of an algebraizable logic. Unavoidably, the ordered model class of a logic, when it exists, is not unique. For uniqueness, the definition must be relativized, either syntactically or semantically. In sentential systems, for instance, the order algebraization process may be required to respect a given but arbitrary polarity on the signature. With every deductive filter of an algebra of the pertinent type, the polarity associates a reflexive and transitive relation called a Leibniz order, analogous to the Leibniz congruence of abstract algebraic logic (AAL). Some core results of AAL are extended here to sentential systems with a polarity. In particular, such a system is order algebraizable if the Leibniz order operator has the following four independent properties: (i) it is injective, (ii) it is isotonic, (iii) it commutes with the inverse image operator of any algebraic homomorphism, and (iv) it produces anti-symmetric orders when applied to filters that define reduced matrix models. Conversely, if a sentential system is order algebraizable in some way, then the order algebraization process naturally induces a polarity for which the Leibniz order operator has properties (i)–(iv). [Copyright &y& Elsevier]

Abstract: In this paper we study interpretations and equivalences of propositional deductive systems by using a quantale-theoretic approach introduced by Galatos and Tsinakis. Our aim is to provide a general order-theoretic framework which is able to describe and characterize both strong and weak forms of interpretations among propositional deductive systems also in the cases where the systems have different underlying languages. [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: Canonical extension has proven to be a powerful tool in algebraic study of propositional logics. In this paper we describe a generalisation of the theory of canonical extension to the setting of first order logic. We define a notion of canonical extension for coherent categories. These are the categorical analogues of distributive lattices and they provide categorical semantics for coherent logic, the fragment of first order logic in the connectives ∧, ∨, 0, 1 and ∃. We describe a universal property of our construction and show that it generalises the existing notion of canonical extension for distributive lattices. Our new construction for coherent categories has led us to an alternative description of the topos of types, introduced by Makkai (1981) in . This allows us to give new and transparent proofs of some properties of the action of the topos of types construction on morphisms. Furthermore, we prove a new result relating, for a coherent category C, its topos of types to its category of models (in Set). [Copyright &y& Elsevier]

Abstract: We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Gödel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of and , strengthening earlier results by Moerdijk and Palmgren, and Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To conclude the paper, we will point out some open problems and directions for future research, including some initial results on saturation principles. [Copyright &y& Elsevier]

Abstract: In his recent work, Woodin has defined new axioms stronger than I0 (the existence of an elementary embedding from to itself), that involve elementary embeddings between slightly larger models. There is a natural correspondence between I0 and Determinacy, but to extend this correspondence in the new framework we must insist that these elementary embeddings are proper. Previous results validated the definition, showing that there exist elementary embeddings that are not proper, but it was still open whether properness was determined by the structure of the underlying model or not. This paper proves that this is not the case, defining a model that generates both proper and non-proper elementary embeddings, and compare this new model to the older ones. [Copyright &y& Elsevier]

Abstract: Total search problems (TFNP problems) typically have their totality guaranteed by some combinatorial property. This paper proves that, if there is a polynomial time Turing reduction between two TFNP problems, then there are quasipolynomial size, polylogarithmic height, constant depth, free-cut free propositional (Frege) proofs of the combinatorial property associated with the first TFNP problem from the property associated with the second problem. In addition, they have Nullstellensatz derivations of polylogarithmic degree. These results extend the previous work of Buresh-Oppenheim and Morioka first by applying to Turing reductions in place of many-one reductions and second by giving tight bounds on the height of the Frege proofs. As a corollary, PLS-complete problems are not polynomial time Turing reducible to PPA problems relative to a generic oracle. We establish a converse construction as well, by showing that a polynomial time Turing reduction can be obtained from a family of quasipolynomial size, polylogarithmic depth, propositional proofs which are based on “decision tree” substitutions. This establishes the optimality of our constructions, and partially resolves an open question posed by Buresh-Oppenheim and Morioka. We observe that the classes PPA, PPAD, PPADS, and PLS are closed under Turing reductions, and give an example of a TFNP class that is not closed under Turing reductions. [Copyright &y& Elsevier]

Abstract: Memory logics are a family of modal logics in which standard relational structures are augmented with data structures and additional operations to modify and query these structures. In this paper we present sound and complete axiomatizations for some members of this family. We analyze the use of nominals to achieve completeness, and present one example in which they can be avoided. [Copyright &y& Elsevier]

Abstract: Justification logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound. The proof method is then extended to provide a uniform proof that the corresponding full pure justification logics are -hard, reproving and generalizing an earlier result by Milnikel. [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]

Abstract: In this paper, we prove that the derivability problems for product-free Lambek calculus and product-free Lambek calculus allowing empty premises are NP-complete. Also we introduce a new derivability characterization for these calculi. [Copyright &y& Elsevier]

Abstract: This paper gives two definability results in the local theory of the -enumeration degrees. First, we prove that the local structure of the enumeration degrees is first order definable as a substructure of the -enumeration degrees. Our second result is the definability of the classes and of the high and low n  -enumeration degrees. This allows us to deduce that the first order theory of true arithmetic is interpretable in the local theory of the -enumeration degrees. [Copyright &y& Elsevier]

Abstract: One of the main lines of research in algorithmic randomness is that of lowness notions. Given a randomness notion , we ask for which sequences does relativization to leave unchanged (i.e., )? Such sequences are called low for . This question extends to a pair of randomness notions and , where is weaker: for which is still weaker than ? In the last few years, many results have characterized the sequences that are low for randomness by their low computational strength. A few results have also given measure-theoretic characterizations of low sequences. For example, Kjos-Hanssen (following Kučera) proved that is low for Martin-Löf randomness if and only if every -c.e. open set of measure less than 1 can be covered by a c.e. open set of measure less than 1. In this paper, we give a series of results showing that a wide variety of lowness notions can be expressed in a similar way, i.e., via the ability to cover open sets of a certain type by open sets of some other type. This provides a unified framework that clarifies the study of lowness for randomness notions, and allows us to give simple proofs of a number of known results. We also use this framework to prove new results, including showing that the classes and coincide, answering a question of Nies. Other applications include characterizations of highness notions, a broadly applicable explanation for why low for randomness is the same as low for tests, and a simple proof that , where is the class of Martin-Löf, computable, or Schnorr random sequences. The final section gives characterizations of lowness notions using summable functions and convergent measure machines instead of open covers. We finish with a simple proof of a result of Nies, that . [Copyright &y& Elsevier]

Abstract: This paper gathers together a number of loosely connected thoughts about Bishop’s notion of “function space”. In particular, it provides constructive proofs of some natural, classically straightforward results about morphisms between metrical function spaces, and examines connections between function spaces and pre-apartness spaces. [Copyright &y& Elsevier]

Abstract: If are structures for a first-order language , is said to be algebraically (existentially) closed in just in case every positive existential (existential) -sentence true in is true in . In 1976 Elliott showed that unital AF (‘approximately finite-dimensional’) algebras are classified up to isomorphism by corresponding dimension groups with order unit. This paper shows that one dimension group with order unit is algebraically (existentially) closed in another just in case the corresponding AF algebras, viewed as metric structures, fall in the same relation. [Copyright &y& Elsevier]

Abstract: In this second paper of the series we do a local analysis of quadratic forms over completions of a non-standard model of . [Copyright &y& Elsevier]

Abstract: This paper exhibits a general and uniform method to prove axiomatic completeness for certain modal fixpoint logics. Given a set of modal formulas of the form , where occurs only positively in , we obtain the flat modal fixpoint language by adding to the language of polymodal logic a connective for each . The term is meant to be interpreted as the least fixed point of the functional interpretation of the term . We consider the following problem: given , construct an axiom system which is sound and complete with respect to the concrete interpretation of the language on Kripke structures. We prove two results that solve this problem. First, let be the logic obtained from the basic polymodal by adding a Kozen–Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective . Provided that each indexing formula satisfies a certain syntactic criterion, we prove this axiom system to be complete. Second, addressing the general case, we prove the soundness and completeness of an extension of . This extension is obtained via an effective procedure that, given an indexing formula as input, returns a finite set of axioms and derivation rules for , of size bounded by the length of . Thus the axiom system is finite whenever is finite. [Copyright &y& Elsevier]

Abstract: This paper studies intersection and union type assignment for the calculus (Curien and Herbelin, 2000 ), a proof-term syntax for Gentzen’s classical sequent calculus, with the aim of defining a type-based semantics, via setting up a system that is closed under conversion. We will start by investigating what the minimal requirements are for a system, for to be complete (closed under redex expansion); this coincides with System , the notion defined in Dougherty et al. (2004) ; however, we show that this system is not sound (closed under subject reduction), so our goal cannot be achieved. We will then show that System is also not complete, but can recover from this by presenting System as an extension of (by adding typing rules) and showing that it satisfies completeness; it still lacks soundness. We show how to restrict so that it satisfies soundness as well by limiting the applicability of certain type assignment rules, but only when limiting reduction to (confluent) call-by-name or call-by-value reduction; in restricting the system this way, we sacrifice completeness. These results when combined show that, with respect to full reduction, it is not possible to define a sound and complete intersection and union type assignment system for . [Copyright &y& Elsevier]

Abstract: Classical proof forests are a proof formalism for first-order classical logic based on Herbrand’s Theorem and backtracking games in the style of Coquand. First described by Miller in a cut-free setting as an economical representation of first-order and higher-order classical proof, defining features of the forests are a strict focus on witnessing terms for quantifiers and the absence of inessential structure, or ‘bureaucracy’. This paper presents classical proof forests as a graphical proof formalism and investigates the possibility of composing forests by cut-elimination. Cut-reduction steps take the form of a local rewrite relation that arises from the structure of the forests in a natural way. Yet reductions, which are significantly different from those of the sequent calculus, are combinatorially intricate and do not exclude the possibility of infinite reduction traces, of which an example is given. Cut-elimination, in the form of a weak normalisation theorem, is obtained using a modified version of the rewrite relation inspired by the game-theoretic interpretation of the forests. It is conjectured that the modified reduction relation is, in fact, strongly normalising. [Copyright &y& Elsevier]

Abstract: A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named and , which we claim correspond closely to the classical predicative systems of second order arithmetic and . We justify this claim by translating each second order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used to formalise different approaches to the foundations of mathematics. The two LTTs we construct are subsystems of the logic-enriched type theory , which is intended to formalise the classical predicative foundation presented by Herman Weyl in his monograph Das Kontinuum. The system has also been claimed to correspond to Weyl’s foundation. By casting and as LTTs, we are able to compare them with . It is a consequence of the work in this paper that is strictly stronger than . The conservativity proof makes use of a novel technique for proving one LTT conservative over another, involving defining an interpretation of the stronger system out of the expressions of the weaker. This technique should be applicable in a wide variety of different cases outside the present work. [Copyright &y& Elsevier]

Abstract: In this paper we define a notion of relativization for higher order logic. We then show that there is a higher order theory of Grothendieck topoi such that all Grothendieck topoi relativizes to all models of set theory with choice. [Copyright &y& Elsevier]