The Ghent Logic Seminar takes place weekly, usually at 11am (CET) on Thursdays. Most of the seminars can be attended either in person or on Zoom. For the zoom link, or for the recording of the talks, get in touch with Andreas Weiermann, Fedor Pakhomov, or me.
News: starting from Fall 2023, we plan to make the recordings of the talks available on YouTube. Links are available after the abstract. We also have a new mailing list: to subscribe to it, send a message to listserv@lists.ugent.be, or visit the website https://lists.ugent.be/wws/info/logicseminar.
Abstract: The polymodal provability logic \(\mathsf{GLP}\), studies the provability
predicates for extensions of Peano Arithmetic \(\mathsf{PA}\) by all true \(\Pi_n\)-
sentences and their interactions with each other. In this talk, we
consider the polymodal provability logic of Heyting Arithmetic \(\mathsf{HA}\).
With the aid of the characterization of provability logic of \(\mathsf{HA}\), we are
able to characterize the provability logic of \(\mathsf{HA}^n\), extension of \(\mathsf{HA}\) by
all true \(\Pi_n\)-sentences.
It turns out that \(\mathsf{HA}\) and \(\mathsf{HA}^n\) share the same provability logic for
every \(n\). Moreover we suggest a polymodal provability logic, called
\(\mathsf{iGLPH}\), and prove its soundness for arithmetical interpretations in \(\mathsf{HA}\).
Roughly speaking, \(\mathsf{iGLPH}\) is just the intuitionistic version of \(\mathsf{GLP}\)
together with \([n]A \to [n]B\) for some admissible rules \(A/B\) of \(\mathsf{HA}^n\),
namely those who are verifiable in \(\mathsf{HA}\).
Abstract: The Borel hierarchy gives a robust way to stratify the
complexity of sets of countable structures and is intimately tied with
definability in infinitary logic via the Lopez-Escobar theorem.
However, what happens with sets axiomatizable in finitary first-order
logic, such as the set of structures satisfying a given finitary first-
order theory T? Is the complexity of the set of T's models in any way
related to the quantifier complexity of the sentences axiomatizing it?
In particular, if a theory T is not axiomatizable by a set of sentences
of bounded quantifier complexity, can the set of models of T still be
at a finite level of the Borel hierarchy?
In this talk, we will present results concerning these questions:
In joint work with Andrews, Gonzalez, Lempp, and Zhu we show that the
set of models of a theory T is \Pi^0_\omega-complete if and only if T
does not have an axiomatization by sentences of bounded quantifier
complexity, answering the last question in the negative. We also
characterize the Borel complexity of the set of models of complete
theories in terms of their finitary axiomatizations. Our results
suggest that infinitary logic does not provide any efficacy when
defining first-order properties, a phenomenon already observed by Wadge
and Keisler and, recently, rediscovered by Harrison-Trainor and
Kretschmer using different techniques.
Combining our results with recent results by Enayat and Visser, we
obtain that a large class of theories studied in the foundations of
mathematics, sequential theories, have a maximal complicated set of
models.
Abstract: In this talk, based on a joint work, I will present a
decidable theory called RDF* (Reals with Differentiable Functions);
RDF* is an unquantified first-order theory which extends a fragment of
Tarski's real algebra with one-argument real functions endowed with a
continuous first derivative. The language of RDF* embodies the
addition of functions and multiplication of functions by scalars;
regarding relators, an array of predicates designates various
relationships between functions, as well as function properties, that
may hold over intervals of the real line; those are: function
comparisons, strict and non-strict monotonicity/convexity/concavity,
comparisons between the derivative of a function and a real-valued
term.
Our decision method consists in preprocessing the given formula into an
equi-satisfiable quantifier-free formula of the elementary algebra of
real numbers, whose satisfiability can then be checked by means of
Tarski’s decision method.
Abstract: The abstract of the talk coincides with the title.
Abstract: We give a new proof of Girard's hierarchy comparison theorem relating the slow growing hierarchy along the Bachmann Howard ordinal to the fast growing hierarchy along the proof-theoretic ordinal of first order Peano arithmetic.
Abstract: Continuous Weihrauch degrees have been known and studied for more than thirty years, yet very little is known on their structure. In this talk, we will focus on some recent observations concerning the degrees that are closest to the degree of the identity (but different from it), and we will show that, perhaps unsurprisingly, their configuration depends strongly on set-theoretic assumptions: in particular, the existence of a minimal such degree requires some form of determinacy. We will then move to a smaller class of "tamely discontinuous" multifunctions, still very close to the identity, and show in \(\mathsf{ZFC}\) that they admit a minimum.
Joint work with Arno Pauly.
Abstract: The analogue of Hilbert’s 10th Problem for a first-order structure A with signature \(L\) asks whether there exists an algorithm with input and output as follows:
Abstract: With the rapid growth of distributed computing and networking, the demand for large-scale, complex distributed applications is increasing significantly. Distributed Real-Time Applications (DRTA) are used to control and monitor a wide variety of distributed real-time systems, including aerospace, robotics, and nuclear power plants. DRTAs often operate on eterogeneous computer networks with multiple interconnected components, each equipped with its own local independent clock. These independent clocks have their own rate behavior without synchronization. Timed Automata (TA) can be used to model DRTAs with independent clocks. However, it is important to recognize that in certain scenarios there may be indirect interactions or dependencies between independent clocks. This may be the case in larger systems where different components or subsystems interact or depend on each other for timing information. In this talk, we propose a derivative-based alternative semantics for TA and Hennessy-Milner Logic (HML) with independent clocks. This approach has been implemented in a tool called MIMETIC. We will also discuss the problem of timed bisimulation with our alternative semantics for TA and HML with independent clocks.
Abstract: The topological μ-calculus has gathered attention in recent years as a powerful framework for representation of spatial knowledge. In particular, spatial relations can be represented over finite structures in the guise of weakly transitive (wK4) frames. Together with David Fernández-Duque we have shown that the μ-calculus is equivalent to a simple fragment based on a variant of the "tangle" operator. Similar results were proven for transitive frames by Dawar and Otto, using modal characterisation theorems for the corresponding classes of frames. However these theorems are not available in our setting and so we ended up with a different approach by studying the Σ-final part of the corresponding Kripke models for finite sets of formulae Σ. I will be giving a blackboard presentation starting with an overview of the motivation and the results then, if time allows, we will look into the proof of one of the main theorems of our paper.
Abstract: This talk is about the foundations of mathematics, studying determinacy axioms derived from game theory, with a reverse mathematics point of view. It exposes their relationship with second-order and third-order arithmetic, examining a significant paper in the field by Montalbán and Shore. The proof of Martin of Borel determinacy showed that the existence of the nth iterated power set of \(\omega\) is necessary to prove the determinacy of \(\Pi^0_{n+3}\) Gale-Stewart games (for \(n \geq 1)\). However, it is not known what is the optimal proof for this kind of determinacy nowadays. Most of the work in the area has been led into second-order arithmetic when one only uses natural numbers and sets of natural numbers. The limit of this analysis is the striking result of Montalbàn and Shore. They showed that when taking finite differences of \(\Pi^0_3\) sets, the determinacy axioms grow exponentially in proof-theoretic strength until the limit of provability in \(Z_2\). We present a generalisation of the results of Montalbán and Shore in some natural interpretation of third-order arithmetic about differences of \(\Pi^0_4\) sets. Our work reveals the situation to be slightly different in the uncountable case while generating a plethora of reverse mathematical results about \((\Pi^0_{n+3})_m\) determinacy axioms \((n, m \geq 1)\).
Abstract: This will be an semi-formal blackboard and chalk talk where I present a survey of the work I and my students are currently doing around provability logic. Time permitting this will include the work of Wang on periodic topological models of GLP, Lukashov on the unification problem for GLP, Dvorkin on the provability logic of Niebergall's arithmetic, Kovalev on open induction, Svyatlovsky on well-quasi orders in strictly positive logics.
Abstract: Consider an equation \(ax+by+c=0\) in reals, i.e. assume that \(a\), \(b\) and \(c\) are given parameters seeking for all \(r\) and \(s\) that if we replace them for variables \(x\) and \(y\), the equality holds. What if we consider equations in logical setting? More precisely, an equation like \(p \to x = \bot\), seeking for all formulas \(A\) that if we replace them for the variable \(x\), the equality \(p\to A \equiv \bot\) holds. In this talk we consider this question with a propositional logic in the background: Classical logic, Intuitionistic Logic and Classical Modal Logics.
Abstract: I will be presenting the research that I have done for my Master's Thesis in the area of probabilistic fixed-point modal logic. The main focus will be on a tableau construction that I have developed with the aim of addressing the satisfiability problem of a specific probabilistic fixed-point logic setup.
Abstract: Erickson, Nivasch, and Xu (2021), while studying so-called "fusible numbers", considered the following recursive algorithm \(M(x)\): if \(x<0\) return \(−x\), else return \(M(x−M(x−1))/2\). They showed that \(M\) terminates on real inputs, and that PA cannot prove that \(M\) terminates on all natural inputs. In this talk we investigate conditions under which similar recursive algorithms terminate on all real inputs.
Joint work with Lior Shiboli.
Abstract: For \(\Gamma = \Sigma^1_n\) or \(\Pi^1_n\), the closure ordinal of monotone \(\Gamma\) operators is smaller than the closure ordinal of \(\Gamma\) operators, assuming \(V=L\) or \(\mathsf{PD}\). Half the inequalities are due to Aanderaa (1974) and the rest are new and joint with Philip Welch.
Abstract: As indicated in the title, the subject of the talk will be a certain well-quasi-order of leaf-labeled trees with an ordering which is weaker than the usual Kruskal embedding. The primary goal is the calculation of maximal order types -- an oft-discussed topic during a recent visit by Harry Altman -- as a function of the labeling wqo. Using their correspondence to finitary indecomposable transfinite sequences, we'll also get a nice result for all finitary sequences of length less than \(\omega^\omega\).
This is joint work with Fedor Pakhomov, and overlapping with a recent paper by Andreas Weiermann and Harvey Friedman.
Abstract: The Ramsey theorem is an important result that will be treated from a reverse mathematics perspective. Considering the Hindman theorem and the Increasing Polarized Theorem, we will restrict each other to the version on couples and two colours, and then compare these theorems with other conditions and stronger versions to find some interesting equivalences, and see if over \(\mathsf{RCA}_0\) it is possible to prove that these three theorems are equivalent to each other.
Abstract: We present an analogue of Gödel’s second incompleteness theorem. Whereas Gödel showed that sufficiently strong theories that are \(\Pi^0_1\)-sound and \(\Sigma^0_1\)-definable do not prove their own \(\Pi^0_1\)-soundness, we prove that sufficiently strong theories that are \(\Pi^1_1\)-sound and \(\Sigma^1_1\)-definable do not prove their own \(\Pi^1_1\)-soundness. Our proof does not involve the construction of a self-referential sentence but rather relies on ordinal analysis. If time permits, we will then turn to characterizations of ordinal analysis itself. One of the main goals of ordinal analysis is measuring the “strength” of theories by calculating their proof-theoretic ordinals. But in what sense do proof-theoretic ordinals measure the strength of theories? What is the attendant notion of strength? We provide some abstract answers to this question.
Abstract: In [1], Jackson and Stokes investigate the axiomatisability of classes of algebras that are representable as (i.e. isomorphic to) an algebra of partial functions. Using a uniform method of representation, they give, for around 30 different signatures containing the domain restriction operation, either a finite equational or finite quasi-equational axiomatisation of the class of representable algebras. Only a handful of these classes had previously been axiomatised.
We show that a similar uniform method of representation can be used to characterise many of the corresponding subclasses of completely representable algebras. A complete representation is one that turns any existing infima/suprema into intersections/unions. Specifically, we do this for signatures containing the operation called minus in [1] and which we call antidomain restriction; thus for about half of the signatures treated in [1]. Together with the results of [1], this gives us finite first-order axiomatisations of 11 of these classes of completely representable algebras. Only a couple of complete representation classes had previously been axiomatised (for representation as partial functions).
[1] Marcel Jackson and Tim Stokes, Restriction in Program Algebra, Logic Journal of the IGPL, (2022), 35 pp.
Abstract: It is a known result that any theory T extending RCA_0 which proves that 3 is bqo also proves that any finite poset is bqo. Interestingly, as Freund recently showed, 3 being bqo is not a trivial statement, as it entails ACA_0^+ over RCA_0 (an implication not known to be strict). Hence, a natural question to be asked is: what can we say about the finite posets P that a "weak" theory (i.e., a theory not proving that 3 is bqo) proves to be bqo? In this talk, we will provide a characterization of these posets, and then extend this result to study the posets that ACA_0 proves to be bqo. Finally, we will show how these considerations can be exploited to show the weakness of some versions of the minimal bar array lemma.
This is joint work with Anton Freund, Alberto Marcone and Fedor Pakhomov.
Abstract: We cover our recent findings regardings the parameterized Friedman's Bolzano Weierstrass theorem FBW_f where f is a positive primitive recursive function. Our aim is to indicate the precise threshold region for f for which FBW_f becomes unprovable in the fragment of PA with one quantifier induction only.
Abstract: The *integer complexity* of a number n, denoted ||n||, is the smallest number of 1's needed to write n using any combination of addition and multiplication. Despite this simple definition many problems about it remain open; for instance, it is unknown whether ||2^k||=2k for all k>=1.
In this talk we'll provide an overview of integer complexity, discussing its approximate magnitude, how fast it may be computed, and some infinite families of numbers we *can* determine the complexity of, but focusing primarily on a well-ordering phenomenon that occurs when one transforms the complexity values into real-valued "defects". We'll also discuss variants of the problem.
Abstract: Given a finite collection of well-orders, the lower sets of their Cartesian product form a well partial order under inclusion. In this talk we'll discuss how the type of this well partial order may be computed (both with and without a boundedness restriction) and why the resulting function takes the specific form that it does. Time permitting we may discuss variants of the problem.
Abstract: Higman’s lemma and Kruskal’s theorem are two of the most celebrated results in the theory of well quasi-orders. In his seminal paper, G. Higman obtained what is known as Higman’s lemma as a corollary of a more general theorem, dubbed here Higman’s theorem.
J.B. Kruskal was well aware of this more general set up; in the very end of his famous article, he explicitly stated how Higman’s theorem is a special version, restricted to trees of finite branching degree, of Kruskal’s own tree theorem.
In this talk, we present proof-theoretic relations between different version of Higman's and Kruskal's theorems, establishing also their proof-theoretic ordinals.
Joint work with Peter Schuster and Andreas Weiermann
Abstract: The notion of better quasi order, due to Nash-Williams, has led to a rich body of results, which includes Laver’s famous proof of Fraïssé’s conjecture. A central tool is the minimal bad array principle. In the present paper, we show that this principle is exceptionally strong from the viewpoint of reverse mathematics, a framework from mathematical logic. Specifically, it is equivalent to Π¹₂-comprehension over the base theory ATR₀.
Joint work with Anton Freund and Giovanni Soldà
Abstract: In this talk we take a step in the program of studying incompleteness and undecidability of theories from a recursion theoretic standpoint. We review some relevant notions and give some historical results.
We explain the notions of *effective strong inseparability* of theories and *effective essential hereditary creativity*. We provide a proof of Vaught’s theorem that the theory R is effectively strongly inseparable and show how Trakhtenbrot’s is a direct consequence of this result.
If time allows, we will also give Hanf’s example of an effectively strongly inseparable theory of an entirely different flavor than R.
We sketch the easy part of the proof that the two salient notions of effective strong inseparability and effective essential hereditary creativity coincide.
Joint work with Taishi Kurahashi.
Abstract: The central open question in Descriptive Complexity is whether there is a logic that characterizes deterministic polynomial time (P-time) on relational structures. Towards this goal, I will present a logic defined algebraically. The algebra can also be viewed as a modal Dynamic Logic, where terms describing programs appear inside modalities.
Semantically, algebraic expressions are partial functions on strings of relational structures. Choice functions select among possible partial mappings, and serve as certificates for the membership in the computational problem specified by a term.
The logic precisely captures non-deterministic polynomial time (NP) computations, and an interesting questions is to find decidable conditions for P-time. I will explain how our proof system could aid this goal. The work is ongoing, and there are challenging mathematical questions to be answered.
Abstract: We will discuss some algebraic structures and their “continuification”. In particular, we’ll consider representations of path algebras, ideals in certain abelian categories, certain kinds of orbit categories, and associahedra. In each case we’ll have a very quick over view of the classical (discrete) case and then an intuitive description of the continuous case. This talk is intended to be accessible to a general mathematical audience.
Abstract: Since 1980 where Albert Visser considered the question for the provability logic of Heyting Arithmetic HA, several related results obtained by e.g. Dick de Jongh, Albert Visser, Rosalie Iemhoff, Mohammad Ardeshir and me. It turns out that intuitionistic provability, is deeply connected with admissibility, preservability, interpretability, projectivity and unification.