The Wormshop
We are proud to announce the lustrum edition of the international workshop "Proof Theory, Modal Logic and Reflection Principles." The workshop (also known as the "Wormshop") will take place at the University of Barcelona from Tuesday, November 5 until Friday, November 8, 2019.
The tradition of modal logics inspired on the notion of formal proof dates back to Gödel, but their study has gained great momentum in the last decade due to novel applications in the foundations of mathematics. Their study moreover requires the interaction of several disciplines in mathematical logic and beyond, including computational logic, proof theory, and point-set topology.
The aim of this workshop is to bring together experts in relevant fields in order to discuss recent advances and foster new collaborations. Topics include but are not restricted to:
- Provability logics and algebras
- Lightweight fragments of modal logics
- Proof theory and ordinal analysis
- Weak and strong systems of arithmetic
- Modalities in topology and set theory
- Justification logics and logics of proofs
- Computability and complexity
This edition of the workshop is the fifth in the series. The previous conferences took place in Barcelona (2012), Mexico City (2014), Tbilisi (2016) and Moscow (2017). This year we are returning to our roots in Barcelona to celebrate the lustrum edition, with a stellar lineup of invited speakers from across the globe.
Registration
To register please fill out this form. There are limited places left!
Early registration is now closed. Reduced conference fees are no longer available.
Regular conference fee: 150 €
Reduced conference fee: 70 €
Minimal conference fee: 35 €
Speakers
Juan Pablo Aguilera
Anton Freund
Michał Tomasz Godziszewski
Lev Gordeev
Evgeny Kolmakov
Félix Lara-Martín
Graham E. Leigh
Mateusz Łełyk
Georg Moser
Sam Sanders
Ilja Shapirovsky
Thomas Studer
Mikhail Svyatlovsky
Albert Visser
Bartosz Wcisło
Gunnar Wilken
Program
Tuesday, November 5, 2019
In his book "Admissible Sets and Structures", Barwise studies the admissible cover of arbitrary models of set theory. A similar move in proof theory studies the admissible cover of a theory T whereby the urelement domain is axiomatized by T and the set-theoretic world erected on top of it is described by KP. We apply this to well-known theories from reverse mathematics.
This is joint work with Gerhard Jäger and Steve Simpson.
This is part of a joint project with T. Arai, D. Fernández-Duque and A. Weiermann, ("Predicatively unprovable termination of the Ackermannian Goodstein process" to appear in Proc. AMS) aimed at developing a range of Goodstein-style independence results for theories between elementary arithmetic and (so far) ID$_1$. This requires normal form representations for natural numbers, and collapsing results between slow and fast growing sub-recursive hierarchies in order to connect-up with proof- theoretic ordinal measures. It turns out that a parametrized Ackermann function lies at the basis of nearly all the number-theoretic representations involved. The key is a strong analogy between the Ackermann function and the Veblen function on ordinals.
The classical Goodstein process is based on writing numbers in "normal form" in terms of addition and exponentiation with some base k. By iteratively changing base and subtracting one, one obtains very long sequences of natural numbers which eventually terminate. The latter is proven by comparing base-k normal forms with Cantor normal forms for ordinals, and in fact this proof relies heavily on the notion of normal form. The question then naturally arises: what if we write natural numbers in an arbitrary fashion, not necessarily using normal forms? What if we allow not only addition and exponentiation, but also multiplication for writing numbers?
A "Goodstein walk" is any sequence obtained by following the standard Goodstein process but arbitrarily choosing how each element of the sequence is represented. As it turns out, any Goodstein walk is finite, and indeed the longest possible Goodstein walk is given by the standard normal forms. In this talk we sketch a proof of this fact and discuss how a similar idea can be applied to other variants of the Goodstein process, including those based on the Ackermann function.
Joint work with T. Arai, S. Wainer and A. Weiermann.
On the first-order consequences of Ramsey's theorem over RCA$_0^*$
Studying the strength of Ramsey's theorem is one of the central topic in reverse mathematics. Over RCA$_0$, the standard base theory for reverse mathematics, it is well-known that the first-order part of Ramsey's theorem for triplets (or higher) is the same as Peano Arithmetic, while deciding the first-order part of Ramsey's theorem for pairs is a long-standing open question. On the other hand, it is known that Ramsey's theorem behaves in a very different manner over the weaker base system RCA$_0^*$, which is a system of recursive comprehension without $\Sigma^0_1$-induction. Particularly, Ramsey's theorem for two colors does not imply the infinite pigeonhole principle, and its consistency strength is fairly weak. In this talk, we will mainly study the first-order consequences of Ramsey's theorem over RCA$_0^*$, and compare them with the situation over RCA$_0$.
This is a joint work with Leszek Kołodziejczyk, Katarzyna Kowalik and Tin Lok Wong.
I will talk about some observations concerning proof size in first-order theories and speedup phenomena, made jointly with Tin Lok Wong and Keita Yokoyama. The observations were inspired by our work on proof speedup results related to Ramsey's Theorem for pairs.
It is well-known that in typical cases where a stronger theory T is conservative over a weaker theory S for some class of sentences, either T has at most polynomial proof speedup over S or the function describing the amount of speedup T has over S lies exactly on the 4-th level of the Grzegorczyk hierarchy (the one occupied by iterated exponential, "tower" functions). I will propose some criteria, formulated in terms of cut-free consistency statements, that imply each of these two possible behaviours. I will also give some examples of pairs of theories for which a different amount of speedup is observed.
Several of the most well-known results on provability algebras of arithmetical theories were obtained by V. Yu. Shavrukov. In particular, he provided sufficient conditions for the existence and non-existence of isomorphisms between such algebras. Later the improvements to Shavrukov's non-isomorphism theorem were found by G. Adamsson. We discuss further refinements of these results and possible applications to the case of bimodal provability algebras.
Equivalences between reflection and induction principles are well-known from the context of first and second order arithmetic. In this talk I present an analogous result in set theory: the principle that any true first order formula with real parameters reflects into some transitive set model is equivalent to induction along $\Delta(\mathbb{R})$-definable well-founded classes, over a suitable weak base theory (see arXiv:1909.00677 for full details).
The order of reflection
Extending Aanderaa’s classical result that the least $\Pi^1_1$-reflecting ordinal is smaller than the least $\Sigma^1_1$-reflecting ordinal, we determine the order between the least ordinals satisfying any two patterns of iterated $\Pi^1_1$- and $\Sigma^1_1$-reflection.
I'll discuss Mahlo classes for proof-theoretic studies on first-order reflecting ordinals.
I consider Hilbert-style non-well-founded derivations in the Gödel-Löb provability logic GL and discuss different forms of semantics for GL with the obtained derivability relation. In particular, I show global neighbourhood completeness of GL enriched with non-well-founded derivations.
Extended bar induction and $\beta_n$-model reflection
Our main result is that over $\mathsf{ACA}_0$ the scheme of $\beta_n$-model reflection is equivalent to the scheme $\mathsf{EBI}(\Pi^1_n)$ of transfinite induction for all $\Pi^1_n$-definable well-founded class-size partial orders $X \prec Y$. To achieve this we develop an approach to the theory of ptykes (higher order well-foundedness preserving operators) in the terms of the category of classes of structures that are closed under isomorphisms and substructures. And develop an approach to formalization of functorial infinitary proofs as proofs generated from a possibly ill-founded proof trees in a variant of ordinary first-order logic. Note that in fact our construction achieves a stronger result. In terms of ptykes we define well-founded classes $\mathbb{W}_{n+1}(\mathbb{W}_n)$ and prove that the scheme of transfinite induction on $\mathbb{W}_{n+1}(\mathbb{W}_n)$ is equivalent to $\mathsf{EBI}(\Pi^1_n)$.
Wednesday, November 6, 2019
Bus from Pl. Catalunya to Can Cuch
Randomness notions and reverse mathematics
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.
Degrees of unsolvability: a survey
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 and the foundations of mathematics
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.
Nonequivalent axiomatizations of PA and the Tarski Boundary
We study a family of axioms expressing \begin{equation}\label{axiomstrue}\tag{$*$} ``\text{All axioms of PA are true.}" \end{equation} where PA denotes Peano Arithmetic. More precisely, each such axiom states that all axioms from a chosen axiomatization of PA are true.
We start with a very natural theory of truth $\text{CT}^-(\text{PA})$ which is a finite extension of PA in the language of arithmetic augmented with a fresh predicate $T$ to serve as a truth predicate for the language of arithmetic. Additional axioms of this theory are straightforward translations of inductive Tarski truth conditions. To study various possible ways of expressing \eqref{axiomstrue}, we investigate extensions of $\text{CT}^-(\text{PA})$ with axioms of the form \begin{equation}\label{deltaaxiom}\tag{$**$} \forall x\ \ \bigl(\delta(x)\rightarrow T(x)\bigr). \end{equation} In the above (and throughout the whole abstract) $\delta(x)$ is an arithmetical $\Delta_0$ formula which is proof-theoretically equivalent to the standard axiomatization of PA with the induction scheme, i.e. the equivalence \begin{equation*} \forall x \bigl(\text{Prov}_{\delta}(x)\equiv \text{Prov}_{\text{PA}}(x)\bigr). \end{equation*} is provable in $I\Sigma_1$. For every such $\delta$, the extension of $\text{CT}^-(\text{PA})$ with axiom \eqref{deltaaxiom} will be denoted $\text{CT}^-[\delta]$.
In particular we are interested in the arithmetical strength of theories $\text{CT}^-[\delta]$. The "line" demarcating extensions of $\text{CT}^-(\text{PA})$ which are conservative over PA from the nonconservative ones is known in the literature as the Tarski Boundary. So far, there seemed to be the least (in terms of deductive strength) natural extension of $\text{CT}^-(\text{PA})$ on the nonconservative side of the boundary, whose one axiomatization is given by $\text{CT}^-(\text{PA})$ and $\Delta_0$ induction for the extended language (the theory is called $\text{CT}_0$). In contrast to this, we prove the following result:
- $\text{CT}_0\vdash \text{Th}$
- there exists $\delta$ such that $\text{CT}^-[\delta]$ and $\text{Th}$ have the same arithmetical consequences.
Secondly, we use theories $\text{CT}^-[\delta]$ to measure the distance between $\text{CT}^-(\text{PA})$ and the Tarski Boundary. We prove
- for every $f\in \omega^{<\omega}$, $\text{CT}^-[\delta_f]$ is conservative over PA;
- if $f\subsetneq g$, then $\text{CT}^-[\delta_g]$ properly extends $\text{CT}^-[\delta_f]$;
- if $f\perp g$ then $\text{CT}^-[\delta_g]\cup\text{CT}^-[\delta_f]$ is nonconservative over PA.
Compositional truth and local collection
Our talk concerns compositional truth theory over Peano arithmetic, called $\text{CT}^-$. It is a theory obtained by adjoining to $\text{PA}$ a fresh unary predicate $T(x)$ and the axioms stating that $T$ behaves compositionally for arithmetical sentences. For instance, one of the axioms states that $T(\phi \vee \psi)$ holds for a disjunction of two arithmetical sentences $\phi, \psi$ iff either $T(\phi)$ or $T(\psi)$ holds.
By a classical argument which can be traced back to Tarski, if we add to $\text{CT}^-$ full induction scheme for formulae containing the truth predicate, the obtained theory $\text{CT}$ can prove uniform reflection over $\text{PA}$ (in fact, it can iterate it through transfinite levels) and therefore, it is not conservative over $\text{PA}$. In contrast, $\text{CT}^-$ without induction is conservative over $\text{PA}$, by a highly nontrivial result due to Kotlarski, Krajewski, and Lachlan. Moreover, it is known due to Łełyk (preceded with a similar result of Kotlarski, obtained by different methods and with a serious gap in the proof) that already $\text{CT}^-$ enriched by induction for $\Delta_0$-formulae is not conservative over $\text{PA}$ and in fact has arithmetical strength equal exactly to $\omega$-many iterations of the uniform reflection over $\text{PA}$.
Richard Kaye conjectured that adding the full collection scheme to $\text{CT}^-$ without adding $\Delta_0$-induction yields a conservative extension of $\text{PA}$. In our talk, we will show a partial positive result towards this conjecture. We introduce a principle of \emph{local collection} which says that for any $c$ if we restrict the truth predicate $T$ to formulae of quantifier depth at most $c$, the resulting predicate satisfies full collection scheme. This result already allows us to contrast collection with induction, since the analogous principle of local induction, "every restriction of the predicate $T$ to formulae of a fixed complexity enjoys full induction," turns out to be arithmetically equivalent to $\text{CT}^-$ with $\Delta_0$ induction and thus non-conservative over $\text{PA}$.
Bus from Can Cuch to Pl. Catalunya
Thursday, November 7, 2019
Globalisation and pairing
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.
Complexity of interpretability logics
It follows from PSPACE-hardness of GL that interpretability logics such as IL, ILW, ILM, and ILP are PSPACE-hard. Unlike GL, already the closed fragment of IL is PSPACE-hard. It was proved recently that IL is, like GL, PSPACE-complete.
We will discuss proving complexity results for ILW, ILM, and ILP. For ILW and ILP, complexity results can be obtained similarly as for IL. With ILM, a different but similarly intuitive approach is probably required.
Predicative proof theory of PDL and basic applications
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.
Modal decision problems on sums of Kripke frames
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}$.
Model-theoretic characterizations of fragments of modal logic
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.
Strictly positive fragments and modal companions of GL
A formula is called strictly positive, if it is built from propositional variables and constant $\top$ with conjunction and diamond operators. The strictly positive fragment (SP-fragment) of a logic L is the set of all provable in L implications $A\to B$, where A and B are strictly positive formulas. We call two logics modal companions, if they have the same SP-fragments. Starting from the result of E. V. Dashkov, who has proved that Godel-Lob provability logic GL and the logic K4 are modal companions, we will answer the question "is it a modal companion of GL or not?" for some of GL's extensions.
Direct interpolation for modal $\mu$-calculus
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.
- 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.
- D'Agostino, G., & Hollenberg, M. (2000). Logical questions concerning the $\mu$-calculus. The Journal of Symbolic Logic, 65(1), 310--332.
Note on globally sound analytic calculi for quantifier macros
This paper focuses on a (joint work with Anela Lolic) globally sound but possibly locally unsound analytic sequent calculus for the quantifier macro Q defined by $\text{Q} x,y A(x, y) = \forall x \exists y A(x, y)$. It is demonstrated that no locally sound analytic representation exists.
Subset semantics for justification logic
Justification logic is a refinement of modal logic that includes explicit justifications for an agent’s knowledge. So far, most semantics for justification logic interpret justifications symbolically, that is, as sets of formulas. We present a different and more flexible approach, called subset semantics, that models justifications as sets of possible worlds. We compare two variants of subset semantics and show that they are essentially different. Moreover, we discuss subset semantics in the context of hyperintensionality and sketch some further applications of this new semantics.
Truth, on reflection
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.
By a well-known theorem of G. Kreisel and A. Lévy, Peano Arithmetic is equivalent (over Primitive Recursive Arithmetic, $PRA$) to the Uniform Reflection principle for $PRA$. This seminal result was refined by D. Leivant by proving the equivalence between $\Sigma_n$-induction and Uniform Reflection for $\Sigma_n$-formulas. L. Beklemishev obtained further refinements equating parameter free fragments of Peano Arithmetic and (relativized forms of) Local Reflection and showed the equivalence between induction rules and several forms of Iterated Uniform Reflection. Nevertheless, although we have a detailed view of the correspondence between induction and Uniform Reflection principles, our knowledge of such a correspondence for Local Reflection principles is very poor. In this work we show that Local Induction principles provide us with a good number of results à la Kreisel-Levy that give us a rather complete (and informative) picture of the relationships between Local Reflection and induction principles.
Joint work with Andrés Cordón-Franco.
Research partially supported by grant MTM2017-86777-P, Ministerio de Economía, Industria y Competitividad, Spain.
Tennebaum's Theorem for quotient presentations of nonstandard models of arithmetic
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.
Friday, November 8, 2019
A new take on proof mining
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.
On negation as a modal operator in a quantified setting
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.
Monadic second order limit laws for natural well orderings
We prove monadic second order limit laws for ordinals stemming from segments of some prominent proof-theoretic ordinals. The techniques used will be a combination of automata theoretic results and Tauberian methods. We believe that our results will hold in a very general context.
Some results have been obtained jointly with Alan R. Woods (who unfortunately passed away in 2011).
Crosslinking pattern notations
I will discuss crosslinks between different views on ordinal notation systems.
Hibert's epsilon calculus with equality and Herbrand complexity
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.
Interpreting modal logics in classical first-order theories
Consider a standard translation $A\mapsto A^*$ of propositional modal formulas into classical first-order formulas of the signature $(R,=)$; it preserves Boolean connectives and translates $\square$ as the relativized quantifier: $(\square A)^*(x)=\forall y (R(x,y)\rightarrow A^*(y))$.
Let $L$ be a propositional modal logic, $T$ a classical first-order theory in $(R,=)$. We consider the following properties for $(L,T)$.
- De Jongh property (DJP): for any $A$, $L\vdash A$ iff for any $^*$ $T\vdash \forall x A^*(x)$;
- Uniform De Jongh property (UDJP): there exists $^*$ such that for any $A$, $L\vdash A$ iff for any $^*$ $T\vdash \forall x A^*(x)$.
Theories of Tarskian truth predicates and reflection principles
We study extensions of Peano arithmetic by iterated truth predicates satisfying Tarski biconditionals for truth. We consider reflection principles for such theories and study the associated reflection algebras from the point of view of modal logic. On the basis of these methods we obtain conservation results and the results characterizing proof-theoretic ordinals of such theories in various levels of the hyperarithmetical hierarchy. These theories can then be related to the standard second-order theories of "predicative" strength, which gives an alternative method of analysing these well-known systems.
Joint work with F. Pakhomov.
Münchhausen provability and its formalisation
In this talk we revisit some main results from what we call Münchhausen provability. According to this notion of provability we say that a formula $\varphi$ is provable a level $\alpha$ if and only if $\varphi$ is provable outright or if it can be proven from a true oracle sentence of the form $\langle \beta \rangle \psi$ for some formula $\psi$ and ordinal $\beta$ below $\alpha$. We see how this recursion can be formalised in second order arithmetic when we have sufficiently much transfinite induction. If we wish to lower the proof theoretical strength needed to formalise the equivalence and to prove that the corresponding provability notions satisfy the principles of Japaridze’s transfinite provability logic $\sf GLP$ we will need to do some trickery and slightly change the definition of Münchhausen provability in various directions.
Venue
Mathematics Building, Room T1
Gran Via de les Corts Catalanes, 585
08007 Barcelona
Travel from the airport
Aerobús to
Plaça Universitat
Single ticket: 5.90€ / Return: 10.20€
Duration: 35 minutes
Train
(only from Terminal 2) to
Passeig de Gràcia
T-10
(10 trips, including travel inside Barcelona): 10.20€
Duration: 35 minutes
Getting around
T-10: 10.20€
10 multi-transport trips, including bus, subway, train, and tram
Buy at a train or subway station
Several people can share a T-10 ticket, even during the same trip
Not valid at the subway stations Airport T1 and Airport T2
Wednesday outing (Montseny)
Main bus
Wed 6 Nov at 08:50 in front of the Hard Rock Café in Plaça Catalunya
(the bus leaves strictly at 09:00)
Alternative
Renfe R2N train from Passeig de Gràcia to Cardedeu
and then a taxi to Can Cuch (about 45€)
Accommodation
Bellow are some suggestions of places to stay, at most 15 minutes away by foot.
(Any others with similar characteristics should be fine.)
Committee
Program committee
Lev D. Beklemishev
Steklov Institute of Mathematics.
Andrés Cordón Franco
Dept. of Computer Science and Artificial Intelligence, University of Seville.
David Fernández-Duque
Dept. of Mathematics, University of Ghent.
Eduardo Hermo Reyes
Dept. of Philosophy, UB.
Joost J. Joosten
Dept. of Philosophy, UB.
Félix Lara-Martín
Dept. of Computer Science and Artificial Intelligence, University of Sevilla.
Andreas Weiermann
Dept. of Mathematics, University of Ghent.
Organizing committee
Joan Bagaria
Dept. of Mathematics and Computer Science, UB, ICREA
Ana de Almeida Borges
Dept. of Philosophy, UB.
Juan José Conejero Rodrı́guez
Dept. of Philosophy, UB.
Mireia González Bedmar
Dept. of Philosophy, UB.
Eduardo Hermo Reyes
Dept. of Philosophy, UB.
Joost J. Joosten (Chair)
Dept. of Philosophy, UB.
Eric Sancho Adamson
Dept. of Philosophy, UB.
Contact information
Artist impression on the worm battle
Andreas Weiermann, 2019
Joost J. Joosten
jjoosten@ub.edu
+34 934 037 984
Carrer de Montalegre, 6
08001 Barcelona
Poster (thanks to Eric Sancho Adamson)