Searcharxiv⌕ Search

arXiv subjects

Joost J. Joosten

Publications and source records attributed to Joost J. Joosten.

At least 37 records · Page 2Linked to original sources
arXiv2020

An overview of Generalised Veltman Semantics

Interpretability logics are endowed with relational semantics à la Kripke: Veltman semantics. For certain applications though, this semantics is not fine-grained enough. Back in 1992, in the research group of de Jongh, the notion of generalised Veltman semantics emerged to obtain certain non-derivability results as was first presented by Verbrugge ([76]). It has turned out that this semantics has various good properties. In particular, in many cases completeness proofs become simpler and the richer semantics will allow for filtration arguments as opposed to regular Veltman semantics. This paper aims to give an overview of results and applications of Generalised Veltman semantics up to the current date.

math.LO↗
arXiv2020

Interpretability in PRA

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

math.LO↗
arXiv2020

Provability and interpretability logics with restricted realizations

The provability logic of a theory T is the set of modal formulas, which under any arithmetical realization are provable in T . We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $Γ$. We make an analogous modification for interpretability logics. This is a paper from 2012. We first studied provability logics with restricted realizations, and show that for various natural candidates of theory T and restriction set $Γ$, where each sentence in $Γ$ has a well understood (meta)-mathematical content in T, the result is the logic of linear frames. However, for the theory Primitive Recursive Arithmetic (PRA), we define a fragment that gives rise to a more interesting provability logic, by capitalizing on the well-studied relationship between PRA and I$Σ_1$. We then study interpretability logics, obtaining some upper bounds for IL(PRA), whose characterization remains a major open question in interpretability logic. Again this upper bound is closely relatively to linear frames. The technique is also applied to yield the non-trivial result that IL(PRA) $\subset$ ILM.

math.LO↗
arXiv2020

A new principle in the interpretability logic of all reasonable arithmetical theories

The interpretability logic of a mathematical theory describes the structural behavior of interpretations over that theory. Different theories have different logics. This paper from 2011 revolves around the question what logic describes the behavior that is present in all theories with a minimum amount of arithmetic; the intersection over all such theories so to say. We denote this target logic by ${\textbf{IL}}({\rm All})$. In this paper we present a new principle $\sf R$ in ${\textbf{IL}}({\rm All})$. We show that $\sf R$ does not follow from the logic ${\textbf{IL}}{\sf P_0W^*}$ that contains all previously known principles. This is done by providing a modal incompleteness proof of ${\textbf{IL}}{\sf P_0W^*}$: showing that $\sf R$ follows semantically but not syntactically from ${\textbf{IL}}{\sf P_0W^*}$. Apart from giving the incompleteness proof by elementary methods, we also sketch how to work with so-called Generalized Veltman Semantics as to establish incompleteness. To this extent, a new version of this Generalized Veltman Semantics is defined and studied. Moreover, for the important principles the frame correspondences are calculated. After the modal results it is shown that the new principle $\sf R$ is indeed valid in any arithmetically theory. The proof employs some elementary results on definable cuts in arithmetical theories.

math.LO↗
arXiv2020

Self Provers and $Σ_1$ Sentences

This paper from 2012 is the second in a series of three papers. All three papers deal with interpretability logics and related matters. In the first paper a construction method was exposed to obtain models of these logics. Using this method, we obtained some completeness results, some already known, and some new. In this paper, we will set the construction method to work to obtain more results. First, the modal completeness of the logic ${\textbf{IL}}({\sf M})$ is proved using the construction method. This is not a new result, but by using our new proof we can obtain new results. Among these new results are some admissible rules for ${\textbf{IL}}({\sf M})$ and ${\textbf{GL}}$. Moreover, the new proof will be used to classify all the essentially $Δ_1$ and also all the essentially $Σ_1$ formulas of ${\textbf{IL}}({\sf M})$. Closely related to essentially $Σ_1$ sentences are the so-called \emph{self provers}. A self-prover is a formula $φ$ which implies its own provability, that is $φ\to \Box φ$. Each formula $φ$ will generate a self prover $φ\wedge \Box φ$. We will use the construction method to characterize those sentences of ${\textbf{GL}}$ that generate a self prover that is trivial in the sense that it is $Σ_1$.

math.LO↗
arXiv2020

Modal Matters in Interpretability Logics

This paper from 2008 is the first in a series of three related papers on modal methods in interpretability logics and applications. In this first paper the foundations are laid for later results. These foundations consist of a thorough treatment of a construction method to obtain modal models. This construction method is used to reprove some known results in the area of interpretability like the modal completeness of the logic ${\textbf{IL}}$. Next, the method is applied to obtain new results: the modal completeness of the logic ${\textbf{IL}}{\sf M_0}$, and modal completeness of ${\textbf{IL}}({\sf W^*})$.

math.LO↗
arXiv2020

The closed fragment of IL is PSPACE hard

In this paper from 2011 we consider $\textbf{IL}_0$, the closed fragment of the basic interpretability logic $\textbf{IL}$. We show that we can translate $\textbf{GL}_1$, the one variable fragment of Gödel-Löb's provabilty logic $\textbf{GL}$, into $\textbf{IL}_0$. Invoking a result on the PSPACE completeness of $\textbf{GL}_1$ we obtain the PSPACE hardness of $\textbf{IL}_0$.

math.LO↗
arXiv2020

Propositional proof systems and fast consistency provers

A fast consistency prover is a consistent poly-time axiomatized theory that has short proofs of the finite consistency statements of any other poly-time axiomatized theory. Kraj\'ıček and Pudlák proved that the existence of an optimal propositional proof system is equivalent to the existence of a fast consistency prover. It is an easy observation that ${\sf NP}={\sf coNP}$ implies the existence of a fast consistency prover. The reverse implication is an open question. In this paper we define the notion of an unlikely fast consistency prover and prove that its existence is equivalent to ${\sf NP}={\sf coNP}$. Next it is proved that fast consistency provers do not exist if one considers RE axiomatized theories rather than theories with an axiom set that is recognizable in polynomial time.

math.LO↗
arXiv2020

Hidden variables simulating quantum contextuality increasingly violate the Holevo bound

In this paper from 2011 we approach some questions about quantum contextuality with tools from formal logic. In particular, we consider an experiment associated with the Peres-Mermin square. The language of all possible sequences of outcomes of the experiment is classified in the Chomsky hierarchy and seen to be a regular language. Next, we make the rather evident observation that a finite set of hidden finite valued variables can never account for indeterminism in an ideally isolated repeatable experiment. We see that, when the language of possible outcomes of the experiment is regular, as is the case with the Peres-Mermin square, the amount of binary-valued hidden variables needed to de-randomize the model for all sequences of experiments up to length n grows as bad as it could be: linearly in n. We introduce a very abstract model of machine that simulates nature in a particular sense. A lower-bound on the number of memory states of such machines is proved if they were to simulate the experiment that corresponds to the Peres-Mermin square. Moreover, the proof of this lower bound is seen to scale to a certain generalization of the Peres- Mermin square. For this scaled experiment it is seen that the Holevo bound is violated and that the degree of violation increases uniformly.

cs.LO↗
arXiv2020

Quantified Reflection Calculus with one modality

This paper presents the logic QRC$_1$, which is a strictly positive fragment of quantified modal logic. The intended reading of the diamond modality is that of consistency of a formal theory. Predicate symbols are interpreted as parametrized axiomatizations. We prove arithmetical soundness of the logic QRC$_1$ with respect to this arithmetical interpretation. Quantified provability logic is known to be undecidable. However, the undecidability proof cannot be performed in our signature and arithmetical reading. We conjecture the logic QRC$_1$ to be arithmetically complete. This paper takes the first steps towards arithmetical completeness by providing relational semantics for QRC$_1$ with a corresponding completeness proof. We also show the finite model property, which implies decidability.

math.LO↗
arXiv2019

Münchhausen provability

By Solovay's celebrated completeness result on formal provability we know that the provability logic $\mathrm GL$ describes exactly all provable structural properties for any sound and strong enough arithmetical theory with a decidable axiomatisation. Japaridze generalised this result by considering a polymodal version $\mathrm GLP$ of $\mathrm GL$ with modalities $[n]$ for each natural number $n$ referring to ever increasing notions of provability. Modern treatments of $\mathrm GLP$ tend to interpret the $[n]$ provability notion as "provable in a base theory $T$ together with all true $Π^0_n$ formulas as oracles". In this paper we generalise this interpretation into the transfinite. In order to do so, a main difficulty to overcome is to generalise the syntactical characterisations of the oracle formulas of complexity $Π^0_n$ to the hyper-arithmetical hierarchy. The paper exploits the fact that provability is $Σ^0_1$ complete and that similar results hold for stronger provability notions. As such, the oracle sentences to define provability at level $α$ will recursively be taken to be consistency statements at lower levels: provability through provability whence the name of the paper. The paper proves soundness and completeness for the proposed interpretation for a wide class of theories; namely for any theory that can formalise the recursion described above and that has some further very natural properties. Some remarks are provided on how the recursion can be formalised into second order arithmetic and on lowering the proof-theoretical strength of these systems of second order arithmetic.

math.LO↗
arXiv2019

The Worm Calculus

We present a propositional modal logic $\sf WC$, which includes a logical $verum$ constant $\top$ but does not have any propositional variables. Furthermore, the only connectives in the language of $\sf WC$ are consistency-operators $\langle α\rangle$ for each ordinal $α$. As such, we end up with a class-size logic. However, for all practical purposes, we can consider restrictions of $\sf WC$ up to a given ordinal. Given the restrictive signature of the language, the only formulas are iterated consistency statements, which are called worms. The theorems of $\sf WC$ are all of the form $A \vdash B$ for worms $A$ and $B$. The main result of the paper says that the well-known strictly positive logic $\sf RC$, called Reflection Calculus, is a conservative extension of $\sf WC$. As such, our result is important since it is the ultimate step in stripping spurious complexity off the polymodal provability logic $\sf{GLP}$, as far as applications to ordinal analyses are concerned. Indeed, it may come as a surprise that a logic as weak as $\sf WC$ serves the purpose of computing something as technically involved as the proof theoretical ordinals of formal mathematical theories.

math.LO↗
arXiv2019

The Reduction Property Revisited

In this paper we will study an important but rather technical result which is called The Reduction Property. The result tells us how much arithmetical conservation there is between two arithmetical theories. Both theories essentially speak about the fundamental principle of reflection: if a sentence is provable then it is true. The first theory is axiomatized using reflection axioms and the second theory uses reflection rules. The Reduction Property tells us that the first theory extends the second but in a conservative way for a large class of formulae. We extend the Reduction Property in various directions. Most notably, we shall see how various different kind of reflection axioms and rules can be related to each other. Further, we extend the Reduction Property to transfinite reflection principles. Since there is no satisfactory (hyper) arithmetical interpretation around yet, this generalization shall hence be performed in a purely algebraic setting. For the experts: a consequence of the classical Reduction Property characterizes the $Π^0_{n+1}$ consequences and tells us that for any theories $U$ and $T$ of the right complexity we have \[ U + {\sf Con}_{n+1}(T) \equiv_{Π^0_{n+1}} U \cup \{ {\sf Con}_n^k(T)\mid k<ω\}. \] We will compute which theories can be put at the right-hand side if we are interested in $Π^0_j$ formulas with $j{\leq}n$. We answer the question also in a purely algebraic setting where $Π^0_j$-conservation will be suitably defined. The algebraic turn allows for generalizations to transfinite consistency notions.

math.LO↗
arXiv2018

When logic lays down the law

We analyse so-called computable laws, i.e., laws that can be enforced by automatic procedures. These laws should be logically perfect and unambiguous, but sometimes they are not. We use a regulation on road transport to illustrate this issue, and show what some fragments of this regulation would look like if rewritten in the image of logic. We further propose desiderata to be fulfilled by computable laws, and provide a critical platform from which to assess existing laws and a guideline for composing future ones.

cs.AI↗
arXiv2018

Relational Semantics for the Turing Schmerl Calculus

In arXiv:1604.08705 the authors introduced the propositional modal logic $\textbf{TSC}$ (which stands for Turing Schmerl Calculus) which adequately describes the provable interrelations between different kinds of Turing progressions. The current paper defines a model $\mathcal{J}$ which is proven to be a universal model for $\textbf{TSC}$. The model $\mathcal{J}$ is a slight modification of the intensively studied $\mathcal{I}$ : Ignatiev's universal model for the closed fragment of Gödel Löb's polymodal provability logic $\textbf{GLP}$.

math.LO↗
arXiv2017

The logic of Turing progressions

Turing progressions arise by iteratedly adding consistency statements to a base theory. Different notions of consistency give rise to different Turing progressions. In this paper we present a logic that generates exactly all relations that hold between these different Turing progressions given a particular set of natural consistency notions. Thus, the presented logic is proven to arithmetically sound and complete for a natural interpretation, named the \emph{Formalized Turing progressions} (FTP) interpretation.

math.LO↗
arXiv2016

Fractal dimension versus process complexity

Complexity measures are designed to capture complex behavior and quantify *how* complex, according to that measure, that particular behavior is. It can be expected that different complexity measures from possibly entirely different fields are related to each other in a non-trivial fashion. Here we study small Turing machines (TMs) with two symbols, and two and three states. For any particular such machine $τ$ and any particular input $x$ we consider what we call the 'space-time' diagram which is the collection of consecutive tape configurations of the computation $τ(x)$. In our setting, we define fractal dimension of a Turing machine as the limiting fractal dimension of the corresponding space-time diagram. It turns out that there is a very strong relation between the fractal dimension of a Turing machine of the above-specified type and its runtime complexity. In particular, a TM with three states and two colors runs in at most linear time iff its dimension is 2, and its dimension is 1 iff it runs in super-polynomial time and it uses polynomial space. If a TM runs in time $O(x^n)$ we have empirically verified that the corresponding dimension is $(n+1)/n$, a result that we can only partially prove. We find the results presented here remarkable because they relate two completely different complexity measures: the geometrical fractal dimension on the one side versus the time complexity of a computation on the other side.

cs.CC↗