Wormshop 2019

There are many notions of algorithmic randomness in addition to classic Martin-Löf randomness, such as 2-randomness, weak 2-randomness, computable randomness, and Schnorr randomness. For each notion of randomness, we consider the statement "For every set $Z$, there is a set $X$ that is random relative to $Z$" as a set-existence principle in second-order arithmetic, and we compare the strengths of these principles. We also show that a well-known characterization of 2-randomness in terms of incompressibility can be proved in $RCA_0$, which is non-trivial because it requires avoiding the use of $\Sigma^0_2$ bounding.

This is joint work with André Nies.

Given a problem $P$, one associates to $P$ a degree of unsolvability $\deg(P)$. Here $\deg(P)$ is a quantity which measures the "difficulty" of $P$, i.e., the amount of algorithmic unsolvability which is inherent in $P$. We focus on two degree structures: the semilattice of Turing degrees $\mathcal{D}_\mathrm{T}$, and its completion $\mathcal{D}_\mathrm{w}=\widehat{\mathcal{D}_\mathrm{T}}$, the lattice of Muchnik degrees. We emphasize specific, natural degrees in $\mathcal{D}_\mathrm{T}$ and $\mathcal{D}_\mathrm{w}$. We remark that $\mathcal{D}_\mathrm{w}$ gives rise to a natural recursion-theoretic interpretation of Kolmogorov's non-rigorous "calculus of problems." We also emphasize the analogy between $\mathcal{E}_\mathrm{T}$, the countable subsemilattice of $\mathcal{D}_\mathrm{T}$ consisting of the Turing degrees associated with recursively enumerable subsets of $\mathbb{N}$, and $\mathcal{E}_\mathrm{w}$, the countable sublattice of $\mathcal{D}_\mathrm{w}$ consisting of the Muchnik degrees of nonempty $\Pi^0_1$ subsets of $\{0,1\}^\mathbb{N}$.

Plato is well-known in mathematics for the eponymous foundational philosophy "Platonism" based on ideal objects. Plato’s "allegory of the cave" provides a powerful visual illustration of the idea that we only have access to shadows or reflections of these ideal objects. An inquisitive mind might then wonder what the current foundations of mathematics, like e.g. Reverse Mathematics and the associated Goedel hierarchy, are reflections of. In this talk, we show that the aforementioned are reflections of a much richer higher-order hierarchy under the canonical embedding of higher-order into second-order arithmetic. We make use of well-known generalisations e.g. nets versus sequences and the gauge integral versus Riemann's integral. Philosophical discussion is kept to a minimum.

Local and global interpretability are two reduction relations between theories, where local interpretability extends global interpretability. A class $\mathcal T$ of theories has globalisation if it satisfies the following condition. Consider a theory $T$ in $\mathcal T$. Then, there is a theory $T^\ast$ in $\mathcal T$ such that, for any $U$ in $\mathcal T$, we have that $T$ locally interprets $U$ iff $T^\ast$ globally interprets $U$. We call $T^\ast$ a globaliser of $T$.

It is well known that sequential theories have globalisation. We show that pair theories also have globalisation. Addition of Uniform Tarski Biconditionals is an example of a functor that maps a pair theory to a globaliser.

Propositional dynamic logic (PDL) is presented in Schütte-style mode as one-sided semiformal tree-like sequent calculus with standard cut rule and omega-rule with principal formulas [P*]A. The omega-rule-free derivations are finite (trees) and sequents deducible by these finite derivations are valid in PDL. Moreover the cut-elimination theorem is provable in Peano Arithmetic (PA) extended by transfinite induction up to a suitable (predicative) Veblen's ordinal. It follows by the cutfree subformula property that such predicative extension of PA proves that any given [P*]-free sequent is valid in PDL iff it is deducible by a finite cut- and omega-rule-free derivation, while PDL-validity of arbitrary star-free sequents is decidable in polynomial space. By standard Hermand-style arguments this eventually yields PSPACE-decidability of PDL-formulas in a suitable basic conjunctive normal form. Furthermore we show that cut-free-derivability (and hence the validity) of PDL-formulas S in the dual basic disjunctive normal form is equivalent to plain validity of a suitable transparent quantified boolean formulas S'. Hence the conjecture EXPTIME = PSPACE holds true iff the validity problem for any S' involved is solvable by a polynomial-space deterministic TM. This may reduce the former problem to a more transparent complexity problem in quantfied boolean logic.

In this talk, I discuss modal satisfiability problems on sums of relational structures (Kripke frames). Given a family ${(F_i \mid i \text{ in }I)}$ of frames indexed by elements of another frame $I$, the sum of the frames $F_i$'s over $I$ is obtained from their disjoint union by connecting elements of $i$-th and $j$-th distinct components according to the relations in $I$. Given a class $\mathcal{F}$ of frames-summands and a class $\mathcal{I}$ of frames-indices, $\sum_{\mathcal{I}}{\mathcal{F}}$ denotes the class of all sums of $F_i$'s in $\mathcal{F}$ over $I$ in $\mathcal{I}$.

This natural operation (being a particular case of generalized sum of models introduced by S. Shelah in the 1970th) has had several important applications in the context of modal logic over the last decade. Iterated sums of Noetherian orders were used by L. Beklemishev to study models of the polymodal provability logic. Then it was noted by the author that sums of frames provide a natural way to study computational complexity of modal satisfiability problems. S. Babenyshev and V. Rybakov considered an operation on frames called refinement, and showed that under a very general condition this operation preserves the finite model property and decidability of logics; refinements can be considered as special instances of sums of frames. The lexicographic product of modal logics, introduced by Ph. Balbiani, is another example of an operation that can be defined via sums of frames.

In this talk, I first discuss general semantic tools for operating with sums of Kripke frames, and apply them to study the finite model property and decidability. Then, I provide conditions under which the modal satisfiability problem on $\sum_{\mathcal{I}}{\mathcal{F}}$ is polynomial space Turing reducible to the modal satisfiability problem on $\mathcal{F}$.

Important syntactic fragments of first-order logic (FO) typically come with model-theoretic characterizations in terms of preservation properties. For example, preservation under reduced products characterizes the Horn fragment of FO and preservation under bisimulations characterizes its modal fragment. In this talk, I will discuss model-theoretic characterizations of various important fragments of modal logic, including its positive existential fragment and its Horn fragment. The operations used in the characterizations range from products and variants of bisimulations to new operations covering aspects of both. I'll also discuss open questions regarding the proper definition of the Horn fragment of modal logic.

Modal logics are known to widely enjoy interpolation and modal $\mu$-calculus does so in a very strong sense: given a formula $A$ and a finite set of propositions and modality operators $L$, there exists a formula $B$ (an interpolant) in the language common to $A$ and $L$ such that $A \to B$ is valid and for every formula $C$ from $L$, $A\to C$ is valid if and only if $B\to C$ is valid. This property, called uniform interpolation, easily implies Craig interpolation and was established for modal $\mu$-calculus by D'Agostino and Hollenberg [2] utilising (disjunctive) modal automata to show that bisimulation quantifiers are definable in modal $\mu$-calculus and can readily be used to obtain interpolants.

Aside from the method of propositional quantification, there are syntactical approaches to interpolation apt for non-classical and modal logics. Following the proof-theoretic tradition, in this talk I will show how to directly extract interpolants for modal $\mu$-calculus formulae from the "cyclic" proofs introduced in [1]. The interpolants obtained in this way are structurally identical to the proofs witnessing the interpolated implication and from this observation one can infer results on the logical form of the interpolant.

1. Afshari, B., & Leigh, G. E. (2017). Cut-free completeness for modal mu-calculus. In Proceeding of Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Lecture Notes in Computer Science. Springer.
2. D'Agostino, G., & Hollenberg, M. (2000). Logical questions concerning the $\mu$-calculus. The Journal of Symbolic Logic, 65(1), 310--332.

The "standard" theories of truth, typed compositional, Friedman-Sheard, Kripke-Feferman (and more), were all originally motivated by semantic considerations. That is to say, these axiomatic theories are considered "good" theories of truth because they have "good" intended models (revision semantics, fixed-point constructions, ...). This talk will examine the proof-theoretic justification behind the differing theories. In particular, we will see that strong compositional theories of truth can be characterised in terms of formal reflection principles.

A computable quotient presentation of a mathematical structure $\mathcal A$ consists of a computable structure on the natural numbers $\langle \mathbb{N},\star,\ast,\dots \rangle$, meaning that the operations and relations of the structure are computable, and an equivalence relation $E$ on $\mathbb{N}$, not necessarily computable but which is a congruence with respect to this structure, such that the quotient $\langle \mathbb{N},\star,\ast,\dots \rangle$ is isomorphic to the given structure $\mathcal{A}$. Thus, one may consider computable quotient presentations of graphs, groups, orders, rings and so on. A natural question asked by B. Khoussainov in 2016, is if the Tennenbaum Thoerem extends to the context of computable presentations of nonstandard models of arithmetic. In a joint work with J.D. Hamkins we have proved that no nonstandard model of arithmetic admits a computable quotient presentation by a computably enumerable equivalence relation on the natural numbers. However, as it happens, there exists a nonstandard model of arithmetic admitting a computable quotient presentation by a co-c.e. equivalence relation. Actually, there are infinitely many of those. The idea of the proof consists is simulating the Henkin construction via finite injury priority argument. What is quite surprising, the construction works (i.e. injury lemma holds) by Hilbert's Basis Theorem. During the talk I'll primarily present ideas of the proof of the latter result, which is joint work with T. Slaman and L. Harington.

Proof mining is a program whose aim is to formulate quantitative versions of theorems of mathematics and, from the proof of the theorem, extract explicit bounding information. In the first part of the talk, we emphasize the first aspect of proof mining. We give two examples, one in analysis, the other in algebra, where the so-called bounded functional interpretation helps in formulating appropriate quantitative versions. In the second part of the talk, we argue that some principles of the bounded functional interpretation - to wit the very same that guide the formulation of the quantitative versions - help in explaining why certain minings are possible. These principles generalize weak König’s lemma and yield conservation results, a particular case being Harvey Friedman’s well-known theorem. A curious feature is that these principles may be false (in contrast to weak König’s lemma) but, by conservativity, only have true quantitative consequences. We illustrate this latter feature with the discussion of a famous fixed point theorem of Felix Browder.

The idea of treating negation as a modal operator manifests itself in various logical systems, and especially in Došen's propositional logic N, whose negation is even weaker than that of Johansson's minimal logic J. Further — N can be extended to the so-called Heyting–Ockham logic N*, which was proposed by Cabalar, Odintsov and Pearce as a framework for studying foundations of well-founded semantics for logic programs with negation. It should be remarked that N* has an attractive Routley-style semantics; more precisely, it is complete with respect to the class of all star information frames. Moreover, Odintsov has recently observed that, in fact, the propositional version of the logic HYPE advocated by Leitgeb as a basic system for dealing with hyperintensional contexts can be obtained from N* by adding double negation introduction and elimination laws. I shall introduce and study predicate versions of N and N*, and provide a suitable Routley-style semantics for the predicate version of HYPE; in particular, the corresponding completeness results will be presented.

Hilbert's epsilon calculus is based on an extension of the language of predicate logic by a term-forming operator $\varepsilon_{x}$. Two fundamental results about the epsilon calculus, the first and second epsilon theorem, play a role similar to that which cut-elimination or decomposition techniques in other logical formalisms. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. In the talk I will present the epsilon theorems and present new results (for the case with equality) on the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential theorems obtained by this elimination procedure.

This is joint work with Kenji Miyamoto.