Archive of events from 2024
An archive of events from the year
-
Logic Seminar
-
Pietro Brocci (SNS Pisa)
The justificatory power of Disquotational Truth
Disquotational truth can play a justificatory role for new mathematical knowledge. In particular, we focus on the known case of consistently extending a theory of first-order arithmetic (PA) with a truth predicate governed by disquotational principles for positive sentences. One philosophically interesting feature is that the addition of this truth predicate is conservative over the arithmetical theory, giving disquotational truth the same epistemic status of a mathematical definition. Following Feferman and McGee, we argue in favour of the open-ended nature of the induction schema: once a new mathematical concept is legitimately defined the schema should hold for the extended language. For truth, this results in more justificatory power as one can prove the consistency statement of the arithmetical theory. Moreover, the exact nature of the justificatory power of positive disquotational truth can be pinned down via an ordinal analysis of the theory, as done by Halbach.
We explore the possibility of extending this disquotational definition of truth via a principle of Generalised Induction introduced by Cantini. The principle is conservative over PA, meaning it preserves the epistemic status of a definition. Furthermore, we argue that the adoption of this principle is particularly motivated in the case of positive disquotational truth. Once this new truth predicate is allowed in the induction schema, we obtain significantly more justificatory power than the original disquotational theory. I conclude by sketching a possible strategy via a collapsing procedure to show that this result is sharp.
-
Wesley H Holliday (UC Berkeley)
From constructive mathematics and quantum mechanics to Fundamental Logic
Non-classical logics have been proposed in a number of domains, including constructive mathematics and quantum mechanics. In this talk, I will identify a base logic beneath some of these non-classical logics that I suggest has a certain fundamental status. I will give an introduction to the proof theory and semantics of this “Fundamental Logic.”
An associated paper is available at https://arxiv.org/abs/2207.06993.
-
Paaras Padhiar (University of Birmingham)
Nested sequents for Scott-Lemmon path axioms
Previous works by Goré, Postniece and Tiu have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent. Our aim is to provide (i) a constructive cut-elimination procedure and (ii) alternative modular formulations for these systems. We present our methodology to achieve these two goals on a subclass of path axioms, namely quasi-transitivity axioms.
-
Åsa Hirvonen (University of Helsinki)
Looking at quantum mechanics with model theoretic glasses
The axioms of quantum mechanics present the state of a quantum system as a unit vector in complex Hilbert space. However, when Dirac [1] presented his bra- and ket-vectors, he had a more general space in mind. Schwartz [4] later gave a rigorous account for Dirac’s “vectors” as distributions, but in elementary physics books one still encounters presentations where ket-vectors are presented just as elements of a Hilbert space, and treated with methods from finite-dimensional linear algebra.
During the last years Tapani Hyttinen and I [2,3] have been looking at various models justifying the finite dimensional approaches from such textbooks. Our approaches are based on various embeddings of a Hilbert space into metric ultraproducts of finite-dimensional Hilbert spaces. In this talk I will present the basic ideas, their benefits and limitations. Time permitting, I will also contrast our approach to Boris Zilber’s work on the same questions, that was the original inspiration for us.
- P.A.M. Dirac. The principles of Quantum Mechanics, 3rd ed, Clarendon Press, Oxford, 1947.
- Å. Hirvonen, T. Hyttinen, On eigenvectors, approximations and the Feynman propagator, Ann. Pure Appl. Logic 170 (2019).
- Å. Hirvonen, T. Hyttinen, On Ultraproducts, the Spectral Theorem and Rigged Hilbert Spaces, to appear in J. Symb. Log.
- L. Schwartz, Théory de Distributions, Hermann, Paris, 1950.
-
Mattias Granberg Olsson (FLoV)
Fixed IDs about truth: Truth and fixpoints in intuitionistic logic (final seminar)
This dissertation concerns the properties of and relationship between positive truth and fixpoints over intuitionistic arithmetic in three respects: the strength of these theories relative to the arithmetic base theories, relationships between theories of strictly positive fixpoints and compositional and disquotational truth for strictly truth-positive sentences, and a comparison with the classical case.
Opponent: Gerhard Jäger, Professor Emiratus University of Bern
-
Lide Grotenhuis (University of Amsterdam)
Intuitionistic mu-calculus with the Lewis arrow
Modal logic can be traced back to Lewis’ introduction of a modal connective for ‘strict implication’, also known as the Lewis arrow. Classically, the Lewis arrow is inter-definable with box, and so the connective has fallen into disuse over time. Over an intuitionistic base, however, the arrow is more expressive than the box.
With the aim of setting up a general framework for intuitionistic fixed point modal logics, we study an intuitionistic version of the mu-calculus with the Lewis arrow as modal connective. Formulas are interpreted over bi-relational Kripke models, which satisfy a confluence condition to ensure monotonicity with respect to the intuitionistic order.
In this talk, I will introduce both algebraic and game semantics for the logic, and provide a complete non-wellfounded proof system for guarded formulas. Moreover, I will show how Ruitenburg’s theorem can be used to prove that every formula is equivalent to a guarded one, thereby showing that this well-known result for the classical mu-calculus still holds in the intuitionistic case.
This is joint work with Bahareh Afshari.
-
Nina Gierasimczuk (Danish Technical University)
Coordinating quantity terms: a simulation study in monotonicity and convexity
Natural languages vary in their quantity expressions, but the variation seems to be constrained by general properties, so-called universals. Explanations thereof have been sought among constraints of human cognition, communication, complexity, and pragmatics. In this work, we examine whether perceptual constraints and coordination dynamics contribute to the development of two universals: monotonicity and convexity. Using a state-of-the-art multi-agent language coordination model (originally applied to colour terms) we evolve communicatively usable quantity terminologies. We compare the degrees of convexity and monotonicity of languages evolving in populations of agents with and without approximate number sense (ANS). The results suggest that ANS supports the development of monotonicity and, to a lesser extent, convexity. We relate our results to some classical observations about generalised quantifiers in mathematical logic and to the research on conceptual spaces.
This is joint work with Dariusz Kalociński, Franek Rakowski and Jakub Uszyński.
-
Lide Grotenhuis (University of Amsterdam)
(Cancelled) Intuitionistic mu-calculus with the Lewis arrow
Talk postponed to 10 October.
Modal logic can be traced back to Lewis’ introduction of a modal connective for ‘strict implication’, also known as the Lewis arrow. Classically, the Lewis arrow is inter-definable with box, and so the connective has fallen into disuse over time. Over an intuitionistic base, however, the arrow is more expressive than the box.
With the aim of setting up a general framework for intuitionistic fixed point modal logics, we study an intuitionistic version of the mu-calculus with the Lewis arrow as modal connective. Formulas are interpreted over bi-relational Kripke models, which satisfy a confluence condition to ensure monotonicity with respect to the intuitionistic order.
In this talk, I will introduce both algebraic and game semantics for the logic, and provide a complete non-wellfounded proof system for guarded formulas. Moreover, I will show how Ruitenburg’s theorem can be used to prove that every formula is equivalent to a guarded one, thereby showing that this well-known result for the classical mu-calculus still holds in the intuitionistic case.
This is joint work with Bahareh Afshari.
-
Zach McKenzie (University of Chester)
Well-founded models of fragments of Collection
Let M be the weak set theory obtained from ZF by removing the Collection Scheme, restricting the Separation Scheme to bounded formulae, and adding an axiom asserting that every set is contained transitive set. In this talk I will consider two formulations of the set-theoretic Collection Scheme restricted formulae that are Πn in the Levy hierarchy: Πn-Collection and Strong Πn-Collection. It is known that, over M, Strong Πn-Collection is equivalent to Πn-Collection plus Σn+1-Separation, and Strong Πn-Collection proves the consistency of M + Πn-Collection. In this talk I will show that for all n > 0, every well-founded model of M + Πn-Collection satisfies Strong Πn-Collection. In particular, for n > 0, M + Strong Πn-Collection does not prove the existence of a transitive model of M + Πn-Collection. And, for n > 0, the minimum model of M + Strong Πn-Collection and M + Πn-Collection coincide. If time permits, I will indicate how the assumption that that the model is well-founded can be replaced with the assumption that the model instead satisfies a fragment of Foundation. This reveals new equivalences between subsystems of ZF that include the Powerset axiom.
-
Daniël Otten (University of Amsterdam)
Cyclic Type Theory
We explain some of the connections between two research areas: cyclic proof theory and proof assistants. This talk is based on joint work-in-progress with Lide Grotenhuis.
In cyclic proof theory, we replace induction axioms with circular reasoning. By carefully placing restrictions on cycles, we can make sure that we do not prove more than with induction. Such cyclic proofs can be interpreted as programs using the Curry-Howard correspondence: cycles correspond to recursive calls, while the restrictions make sure that the program always terminates. Using this perspective, we show how the type theory implemented by proof assistants can be seen as a cyclic proof system: one where programs/proofs are defined using (co)pattern matching. We show some of the difficulties that come up specifically in dependent type theory: why unification becomes important, and how one can translate cyclic proofs to inductive proofs while preserving computational behavior. In addition, we show how some of the techniques from cyclic proof theory might be used to extend proof assistants.
-
Eric Pacuit (University of Maryland)
From paradox to principles: Splitting cycles and breaking ties
Voting on two alternatives appears unproblematic compared to voting on three (or more). When faced with only two alternatives, many arguments show that Majority Rule distinguishes itself from all other ways of making a group decision. For three or more alternatives, one faces the so-called “Paradox of Voting”: there may be elections with a majority cycle in which a majority of voters prefer A to B, a majority of voters prefer B to C, and a majority of voters prefer C to A. In this talk, I will explain a series of results that axiomatically characterize rules for resolving majority cycles in elections. These rules avoid the “Strong No Show Paradox” by responding properly to the addition of new voters to an election and mitigate spoiler effects by responding properly to the addition of new candidates to an election.
This talk is based on joint work with Wes Holliday.
-
The Logic Colloquium 2024
The 2024 Annual European Meeting of the Association for Symbolic Logic, also known as the Logic Colloquium, will be held in Gothenburg on 24-28 June, 2024 and hosted by the Faculty of Humanities at the University of Gothenburg. The colloquium comprises 3 tutorials, 7 plenary lectures and 6 special sessions as well as contributed talks. In addition, the 2024 Gödel Lecture was delivered at the meeting.
See lc2024.se for full information.
-
Dominik Kirst (Inria Paris)
Mechanised metamathematics: synthetic computability and incompleteness in Coq
-
Ivano Ciardelli (University of Padua)
Inquisitive modal logic: an overview
Inquisitive modal logic is a generalization of standard modal logic where the language also contains questions, and modal operators that can be applied to them. In this talk, I will provide an introductory overview of inquisitive modal logic. I will review some motivations for the approach, present some prominent examples of inquisitive modal logics, mention some results about them, and outline directions for future work.
-
Ana María Mora-Márquez (University of Gothenburg)
Medieval Aristotelian Logic is Scientific Method
This presentation aims to show that medieval Aristotelian logic can be generally characterized as scientific method. To be sure, this method includes formal logic as one of its parts, but formal logic is by no means the crucial part. In fact, if, as I intend to show, the main aim of medieval Aristotelian logic is to provide methods for knowledge production and distribution, so its crucial parts are the methods for scientific proof provided in commentaries on Aristotle’s Posterior Analytics and Topics.
In the first part of the presentation, I argue for the possibility of talking of medieval ‘science’, ‘scientific knowledge’, and ‘scientific method’ from a modern perspective, and discuss how the modern perspective relates to the Latin ‘scientia’ in its different senses. In the second part, I show the progression from Nicholas of Paris (1240s) and Albert the Great (1250s), who see Aristotelian logic as a systematic scientific method where syllogistic argument is fundamental, but who struggle to coherently organize it around syllogistic argument, to Radulphus Brito (1290s) who, still seeing Aristotelian logic as scientific method, uses the notion of ‘second intention’ in order to coherently structure it around syllogistic argument.
-
Orvar Lorimer Olsson (FLoV)
Logics of Power-Algebras: the Boolean case
Using semantics based on algebras commonplace in the study of logics, however this usage can take forms: Many-valued logics are commonly described in terms of valuations into a single algebra of truth values, whereas other treatments concern full classes of algebraic structures such as varieties defined by equation theories. This has given rise to similar constructions within different fields of study, but where the direct connections may not to be fully spelled out.
Working from the many-valued perspective, in [1], by lifting the consideration of valuations into subsets of an algebra, Priest defines what he calls the plurivalent version of a logic. This process essentially constitutes taking the power-algebra of truth values from the original logic, as described by Brink [2], together with a conservative choice of truth condition inherited from the original algerba essentially through member-hood statements of specific elements. In the simplest example of this construction Priest can identify some well known multivalued logics as plurivalent logics on classical truth values of the two valued Boolean algebra [1]. However this identification fails if the construction was conducted on any other than this specific Boolean algebra.
Continuing work towards general methods for logics with team semantics [3] I will in this presentation consider the power-algebras of arbitrary Boolean algebras and establish a sound and complete labelled natural deduction system for entailments of member-hood statements. This gives rise to the definition and presentation of logics that can be viewed as sub-structural versions of the referred many-valued logics with proof systems for which additional rules can be added to obtain the original logic.
We will finish by reflecting on the achieved construction, and consider how it can be generalised from the class of Boolean Algebras to constructing logics based on other equational classes of algebras.
References
- Graham Priest, Plurivalent logics, The Australasian Journal of Logic, vol. 11 (2014), no. 1.
- Chris Brink, Power structures, Algebra Universalis, vol. 30 (1993), pp. 177–216.
- Fredrik Engström, Orvar Lorimer Olsson, The propositional logic of teams, arXiv preprint, (2023), arXiv.2303.14022
-
Ivan Di Liberti (FLoV)
Is Kripke semantics somewhat canonical?
The talk reports on an ongoing conversation with Graham Leigh on the topic of completeness theorem for modal logics, and more generally on the exploration of their semantics. The usual completeness theorem for modal logic is given over Kripke-style semantics. How necessary is this choice? In this talk we will see how such choice seems almost unavoidable. I will discuss how to tune this technology to handle more complex modal logics, and provide modular completeness theorems for them.
-
Research Lindström Lecture: Phokion G. Kolaitis (University of California Santa Cruz and IBM Research)
Homomorphism Counts: Expressive Power and Query Algorithms
A classical result by Lovász asserts that two graphs G and H are isomorphic if and only if they have the same left profile, that is, for every graph F, the number of homomorphisms from F to G coincides with the number of homomorphisms from F to H. A similar result is also known to hold for right profiles, that is, two graphs G and H are isomorphic if and only if for every graph F, the number of homomorphisms from G to F coincides with the number of homomorphisms from H to F. During the past several years, there has been a study of equivalence relations that are relaxations of isomorphism obtained by restricting the left profile or the right profile to suitably restricted classes of graphs, instead of the class of all graphs. Furthermore, a notion of a query algorithm based on homomorphism counts was recently introduced and investigated. The aim of this talk is to present an overview of some of the main results in this area with emphasis on the differences between left homomorphism counts and right homomorphism counts.
-
Public Lindström Lecture: Phokion G. Kolaitis (University of California Santa Cruz and IBM Research)
Characterizing Rule-based Languages
There is a mature body of work in logic aiming to characterize logical formalisms in terms of their structural or model-theoretic properties. The origins of this work can be traced to Alfred Tarski’s program to characterize metamathematical notions in “purely mathematical terms” and to Per Lindström’s abstract characterizations of first-order logic. For the past forty years, rule-based logical languages have been widely used in databases and in related areas of computer science to express integrity constraints and to specify transformations in data management tasks, such as data exchange and ontology-based data access. The aim of this talk is to present an overview of more recent results that characterize various classes of rule-based logical languages in terms of their structural or model-theoretic properties.
-
Albert Visser (Utrecht University)
Restricted Sequential Theories
Sequential theories form a fundamental class of theories in logic. They have full coding possibilities and allow us to build partial satisfaction predicates for formulas of bounded depth-of-quantifier-alernations. In many respects, they are the proper domain of Gödelian metamathematics. We explain the notion of sequential theory.
A theory is restricted if it can be axiomatised by axioms of bounded depth-of-quantifier-alernations. All finitely axiomatised theories are restriced, but, for example, also Primitive Recursive Arithmetic. We explain the small-is-very-small principle for restricted sequential theories which says that, whenever the given theory shows that a definable property has a small witness, i.e., a witness in a sufficiently small definable cut, then it shows that the property has a very small witness, i.e., a witness below a given standard number.
We sketch two proofs that restricted theories are incomplete (however complex the axiom set). One uses the small-is-very-small principle and the other a direct Rosser argument. (The second argument was developed in collaboration with Ali Enayat.)
-
Daniel Hausmann (CSE, Gothenburg University)
Games for the mu-calculus
There is a fundamental relation between the modal mu-calculus and infinite-duration two-player games, highlighted perhaps best by the well-known equivalence of mu-calculus formula evaluation and the solution of so-called parity games. Furthermore, parity games also feature prominently in tableau-based reasoning methods for the mu-calculus. Recent work has also shown that the close relation between extremal fixpoints in the mu-calculus and parity conditions can be generalized, lifting the connection to the level of fixpoint equation systems over arbitrary complete lattices.
In this talk, I will detail the above-mentioned connections, summing up recent research that shows how results from game theory can be used to improve and generalize existing algorithmic methods for the analysis of mu-calculus formulas. While this approach leads to improved worst-case runtime guarantees on one hand, it also enables the treatment of generalized mu-calculi that involve, e.g., quantitative or probabilistic modalities.
-
Lingyuan Ye
Stack Representation of First-order Intuitionistic Theories
There is a classical result of Pitts that propositional intuitionistic logic eliminates second order propositional quantifiers. Later, Ghilardi and Zawadowski have worked out a semantic proof of this by developing a sheaf representation of finitely presented Heyting algebras. The basic idea is to represent a Heyting algebra via its collection of models on finite Kripke frames, expressed in a suitable categorical and sheaf-theoretic language. Their representation allows them to show, among other things, that the algebraic theory of Heyting algebras has a model companion, and the quantifier elimination result also follows as a consequence. In this talk, I will briefly recall these classical result and show the possibility of extending these developments to a suitable class of first-order intuitionistic theories. In particular, I will explain how to construct higher sheaf representation of first-order intuitionistic theories, and discuss some possible outcomes.
-
Lauri Hella (Tampere University)
Game characterizations for the number of quantifiers
A game that characterizes definability of classes of structures by first-order sentences containing a given number of quantifiers was introduced by Immerman in 1981. In this talk I describe two other games that are equivalent with the Immerman game in the sense that they characterize definability by a given number of quantifiers.
In the Immerman game, Duplicator has a canonical optimal strategy, and hence Duplicator can be completely removed from the game by replacing her moves with default moves given by this optimal strategy. On the other hand, in the other two games there is no such optimal strategy for Duplicator. Thus, the Immerman game can be regarded as a one-player game, but the other two games are genuine two-player games.
The talk is based on joint work with Kerkko Luosto.
-
Peter Pagin (Stockholm University)
Switcher Semantics and quantification
Switcher Semantics is a semantic framework that is basically characterised by allowing switching: when recursively applying a semantic function \(\mu\) to a complex term \(t\), the semantic function applying to an immediate subterm \(t'\) of \(t\) may be a function \(\mu'\), distinct from \(\mu\). An operator-argument-position pair is called a switcher if it induces such a switch. Switcher semantic systems do not satisfy the standard form of compositionality, but a generalized form, which allows greater flexibility. In earlier work (mostly published), some together with Kathrin Glüer, some with Dag Westerståhl, it has been applied to natural language constructions like proper names in modal contexts, general terms in modal contexts, indexicals in temporal contexts, quotation, and belief contexts. This talk will focus on quantifiers and quantification. First-order quantifiers can be regarded as switchers, switching from truth conditions to satisfaction conditions. The larger topic is quantification into switched contexts. I shall begin by giving an introduction to the framework.
-
World Logic Day 2024
The Logic Group at the University of Gothenburg hosts its annual World Logic Day Pub Quiz. For information of this and other World Logic Day events around the world, see http://wld.cipsh.international/wld2024.html.