Search

We investigate the non-elementary computational complexity of a family of substructural logics without contraction. With the aid of the technique pioneered by Lazi\'c and Schmitz (2015), we show that the deducibility problem for full Lambek calculus with exchange and weakening ($\mathbf{FL}_{\mathbf{ew}}$) is not in Elementary (i.e., the class of decision problems that can be decided in time bounded by an elementary recursive function), but is in PR (i.e., the class of decision problems that can be decided in time bounded by a primitive recursive function). More precisely, we show that this problem is complete for Tower, which is a non-elementary complexity class forming a part of the fast-growing complexity hierarchy introduced by Schmitz (2016). The same complexity result holds even for deducibility in BCK-logic, i.e., the implicational fragment of $\mathbf{FL}_{\mathbf{ew}}$. We furthermore show the Tower-completeness of the provability problem for elementary affine logic, which was proved to be decidable by Dal Lago and Martini (2004)., Comment: The full version of the paper accepted to CSL 2023

There have been investigations into type-theoretic foundations for metaprogramming, notably Davies and Pfenning���s (2001) treatment in S4 modal logic, where code evaluating to values of type A is given the modal type Code A (���A in the original paper). Recently Kavvos (2017) extended PCF with Code A and intensional recursion, understood as the deductive form of the GL (G��del-L��b) axiom in provability logic, but the resulting type system is logically inconsistent. Inspired by staged computation, we observe that a term of type Code A is, in general, code to be evaluated in a next stage, whereas S4 modal type theory is a special case where code can be evaluated in the current stage, and the two types of code should be discriminated. Consequently, we use two separate modalities ��� and ��� to model S4 and GL respectively in a unified categorical framework while retaining logical consistency. Following Kavvos��� (2017) novel approach to the semantics of intensionality, we interpret the two modalities in the P-category of assemblies and trackable maps. For the GL modality ��� in particular, we use guarded type theory to articulate what it means by a ���next��� stage and to model intensional recursion by guarded recursion together with Kleene���s second recursion theorem. Besides validating the S4 and GL axioms, our model better captures the essence of intensionality by refuting congruence (so that two extensionally equal terms may not be intensionally equal) and internal quoting (both A ��� ���A and A ��� ���A). Our results are developed in (guarded) homotopy type theory and formalised in Agda., LIPIcs, Vol. 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), pages 14:1-14:17

Publisher Copyright: © Sandu G. This paper contains some philosophical reflections on Gödelian (undecidable) sentences and the recognition of their truth using semantic arguments. These reflections are not new, similar matters have been extensively addressed in the philosophical literature. The matter is rather one of emphasis.

Universality is one of the most important ideas in computability theory. There are various criteria of simplicity for universal Turing machines. Probably the most popular one is to count the number of states/symbols. This criterion is more complex than it may appear at a first glance. In this note we review recent results in Algorithmic Information Theory and propose three new criteria of simplicity for universal prefix-free Turing machines. These criteria refer to the possibility of proving various natural properties of such a machine (its universality, for example) in a formal theory, PA or ZFC. In all cases some, but not all, machines are simple.

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.

This thesis examines the method of forcing in set theory and focuses on aspects that are set aside in the usual presentations or applications of forcing. It is shown that forcing can be formalized in Peano arithmetic (PA) and that consis- tency results obtained by forcing are provable in PA. Two ways are presented of overcoming the assumption of the existence of a countable transitive model. The thesis also studies forcing as a method giving rise to interpretations between theories. A notion of bi-interpretability is defined and a method of forcing over a non-standard model of ZFC is developed in order to argue that ZFC and ZF are not bi-interpretable. 1

A recent development in the theory of M-sets has paved a new means of an approach to CH. Here we further clarify the theory and form part two of our previous paper[P].

There are many classical connections between the proof-theoretic strength of systems of arithmetic and the provable totality of recursive functions. In this paper we study the provability strength of the totality of recursive functions by investigating the degree structure induced by the relative provability order of recursive algorithms. We prove several results about this proof-theoretic degree structure using recursion-theoretic techniques such as diagonalization and the Recursion Theorem.

Provability logic is a modal logic for studying properties of provability predicates, and Interpretability logic for studying interpretability between logical theories. Their natural models are GL-models and Veltman models, for which the accessibility relation is well-founded. That's why the usual counterexample showing the necessity of finite image property in Hennessy-Milner theorem (see [1]) doesn't exist for them. However, we show that the analogous condition must still hold, by constructing two GL-models with worlds in them that are modally equivalent but not bisimilar, and showing how these GL-models can be converted to Veltman models with the same properties. In the process we develop some useful constructions: games on Veltman models, chains, and general method of transformation from GL-models/frames to Veltman ones.

Ein Aspekt dieser dissertation ist, einige bekannte Ordinalzahlbezeichnungssysteme für Peano Arithmetik zu untersuchen. Es wird gezeigt, dass Phasenübergänge in Bezug auf Beweisbarkeit und Unbeweisbarkeit beobachtet werden. Schließlich kommt man zu Vergleichen von Ordinalzahlbezeichnungssystemen. Diese Dissertation zeigt auch, wie man generell solche Phasenübergänge in Systemen, die stark genug im Sinne von Gödel sind, feststellen kann. Dabei spielt die Friedmansche Miniaturisierung die entscheidende Rolle. Ein anderer Punkt der Dissertation ist das Kanamori-McAloon-Prinzip mit Parameterfunktionen. Sie sind Varianten vom endlichen Ramseysatz und äquivalent zum Paris-Harrington-Prinzip. Es wird gezeigt, dass Phasenübergänge bezüglich der Beweisbarkeit des Kanamori-McAloon-Prinzips vorkommen, wenn die Parameterfunktionenen variieren. An aspect of the thesis is to investigate well-known ordinal notation systems for Peano arithmetic. It will be shown that the so-called phase transition phenomenon can be observed, i.e., there are thresholds between provability and unprovability. This investigation leads to a comparison of the ordinal notation systems. The thesis gives also a guide how one can generally establish such phase transitions in every logic system which is strong enough in the sense of Gödel. We shall see that Friedman style miniaturizations play the central role. Another point of the thesis is the parametrized version of the Kanamori-McAloon principle. This variants of the finite Ramsey theorem is equivalent to the Paris-Harrington principle. It will be shown that phase transitions occur with respect to the provability of the Kanamori-McAloon principle as the parameter function varies.

In persuasion games, it is well known that a perfectly revealing equilibrium may fail to exist when the decision maker is uncertain about the interested party\'s payoff-relevant information. However, by explicitly integrating higher order uncertainty into the information structure, this paper shows that a perfectly revealing equilibrium does exist when disclosures are not restrained to intervals of the payoff-relevant state space. On the contrary, when payoff-irrelevant disclosures are impossible, a perfectly revealing equilibrium fails to exist as long as there is a strictly positive probability that the decision maker does not know whether the interested party is informed or not. In this case, a partially revealing equilibrium and associated inferences are characterized.

A Truth Maintenance -System (TMS) maintains a consistent state of belief given a set J of justifications, i.e. arguments for belief. To resolve contradictions dependency-directed backtracking is performed. In this paper we introduce a method that can, be used to track all dependency-directed backtracking methods simultaneously. This has been, previously done, by adding the contrapositions of justifications to J. We will show that contrapositions are not mandatory, namely that the same result can be reached by adding one disjunctive justification (the consequent is not one atom, but can be a disjunction of atoms). Simplifying the added disjunctive justification leads to more informative models [Ross 89b]. Furthermore, we will give an alternative proof for the correctness of Witteveen's method [Witteveen 90a] for computing the Well-Founded model

A Truth Maintenance -System (TMS) maintains a consistent state of belief given a set J of justifications, i.e. arguments for belief. To resolve contradictions dependency-directed backtracking is performed. In this paper we introduce a method that can, be used to track all dependency-directed backtracking methods simultaneously. This has been, previously done, by adding the contrapositions of justifications to J. We will show that contrapositions are not mandatory, namely that the same result can be reached by adding one disjunctive justification (the consequent is not one atom, but can be a disjunction of atoms). Simplifying the added disjunctive justification leads to more informative models [Ross 89b]. Furthermore, we will give an alternative proof for the correctness of Witteveen's method [Witteveen 90a] for computing the Well-Founded model

We show that a consistent, finitely axiomatized, sequential theory cannot prove its own inconsistency on every definable cut. A corollary is that there are at least three degrees of global interpretability of theories equivalent modulo local interprelability to a consistent, finitely axiomatized, sequential theory U.

We show that a consistent, finitely axiomatized, sequential theory cannot prove its own inconsistency on every definable cut. A corollary is that there are at least three degrees of global interpretability of theories equivalent modulo local interprelability to a consistent, finitely axiomatized, sequential theory U.

We use an alternative graphical representation for formulas in implicational intuitionistic logic in order to obtain and demonstrate results concerning provability. We demonstrate the adequateness of the method in this area, showing that one can easily recognize and prove new results and simplify the proofs of others. As such, we extend a known class of formulas for which uniqueness of β-η-normal proofs is true and define a new one for uniqueness of β-normal proofs. We also give a precise characterization of the set of provable monatomic formulas and obtain as a corollary a necessary condition for intuitionistic theorems in general.