Seminars
Seminars, workshops and other events organised by our group
The Logic Group runs a bi-weekly Research Seminar in Logic, monthly Nordic Online Logic Seminar and the annual Lindström Lecture series, as well as other events. See below for a list of recent and upcoming events or follow the links to jump straight to a category.
The research seminar in Logic meets on alternate Fridays at 10.15. Unless otherwise stated, seminars are held at the department building (Humanisten). Details of online talks are distributed in the GU Logic mailing list. Alternatively, contact Graham E Leigh directly.
-
-
-
The combination of Löwenheim-Skolem Theorem and Compactness Theorem limits the expressive power of a logic to that of first order logic. This maximality principle is the famous Lindström Theorem for first order logic. It reveals that first order logic is at an optimal point of balance: by adding expressive power to it one necessarily loses model-theoretic properties. Soon after Lindström’s result, the question was raised, whether there are other logics at a similar point of equilibrium. More precisely: are there strict strengthenings of first order logic satisfying a Lindström-type characterization? Despite the naturality of this question, it remained unanswered, until recently.
In 2012 Saharon Shelah offered a solution to this problem in the form of a new infinitary logic. It has a Lindström-type characterization in terms of model-theoretic properties combining weak forms of Compactness and a Löwenheim-Skolem type property. In all known cases, a proof of a Lindström-type characterization automatically gives a proof of Craig Interpolation. This is the case for Shelah’s logic, too. There is, however, one aspect where Shelah’s logic seems to be rather weak: the syntax. The logic is derived from a game, in the sense that a sentence is, by definition, a class of structures, closed under a certain Ehrenfeucht-Fraïssé type of a game. This results in the absence of a syntax defined in such a way that the set of all formulas could be obtained by closing the set of atomic formulas under negation, conjunction, quantifiers, and possibly other logical operations. The lack of syntax complicates further study of it and logics in its neighborhood. In the present talk, we address the general question of deriving a syntax from a game, and the more localized question of finding a syntax for Shelah’s logic. Partial answers are provided to both questions. This is joint work with Andres Villaveces and Siiri Kivimäki.
-
Dependence and independence concepts are ubiquitous in natural science, social science, humanities as well as in everyday life. The sentences “I park on this side of the road depending only on the day of the week” and “the time of descent is independent of the weight of the object” are examples of this. The question arises, do these concepts possess enough exactness for us to investigate their logic? There is currently a whole literature on this topic. It is the purpose of this talk to give a non-technical overview of this area of logic.
-
Opponent: TBA
Abstract Description logics are designed to reason efficiently with ontologies in knowledge bases, which are widely used in several industries. Human errors commonly cause mistakes to occur in the axioms of these ontologies, which leads to the logics deducing false conclusions. Ontology engineers spend much time on finding these false axioms to repair the ontology. This process can be facilitated by presenting a justification of the false conclusion, i.e. a set of axioms that entail the conclusion. Typically, the number of justifications for a given conclusion is very large and it is not clear which one should be presented.
It is therefore useful to estimate the cognitively adequate complexity of description logic so that the simplest justification(s) can be identified and selected. This work focusses on the cognitive complexity of deciding the consistency of ABoxes in the description logic $\mathcal{ALE}$. Conceptual considerations entail that the complexity of the ABox consistency problem is expressed as a linear preorder on a large enough set of ABoxes. This linear preorder can be estimated by an ACT-R model called SHARP. The model is a tableau algorithm implemented in a cognitive architecture, thereby modelling a human brain executing the tableau algorithm, which forms an approximation of the cognitive complexity ordering.
A complexity ordering that is a linear preorder can be obtained from experimental data by aggregating the different individual orders from a sample into one so-called proto-order, in which the largest transitive subrelation is the desired linear pre-order. The predicted complexity ordering by SHARP agrees well with the empirical data.
To enable applications in ontology debugging, a surrogate model is needed that accurately approximates SHARP’s output with great computational efficiency. Such a surrogate model can be obtained by the Random Forest algorithm trained on an appropriate dataset generated by SHARP. The complexity ordering thus obtained agrees well with the one predicted by SHARP but can be estimated in a fraction of the time enabling it for practical applications.
Examination committee:
- TBC
-
-
-
A 2½-day workshop dedicated to current and future trends in cyclic and illfounded forms of provability and justification. The event is sponsored by the Knut and Alice Wallenberg Foundation via the research project Taming Jörmungandr: The Logical Foundations of Circularity, the Swedish Research Council through the research project Proofs with Cycles and Computation, and the Department of Philosophy, Linguistics and Theory of Science at the University of Gothenburg.
-
-
-
-
Gödel intended his Dialectica interpretation to provide a foundational reduction of first-order arithmetic to a quantifier-free theory T. It has widely been objected, however, that this theory T tacitly presupposes the very quantificational logic that Gödel was trying to eliminate, hidden within its complicated definition of “computable function of finite type.” This would render the translation philosophically circular. Gödel was adamant that there was no circularity here. He sketched a defense of this claim in a page-long footnote, which however has left readers baffled. In this talk, I will explain Gödel’s footnote and show that there really is no circularity here. Thus, Gödel has achieved a significant foundational reduction. The foundations of T turn out to be stranger than meets the eye; they utilize a (broadly) Leibnizian notion of analyticity in a surprising way.
-
In this talk I will briefly outline Krister’s biography, focusing mainly on the early nineties onwards when I became Krister’s first PhD student. By appeal (mostly) to anecdote I will try to highlight what I take to be some of the most notable features in Krister’s approach to and views on pilosophically inspired logical research and education.
-
Krister Segerberg was one of the architects of modal logic as we know it today. I will highlight a few of his major contributions and show some of their subsequent impact in various academic communities. I conclude with some thoughts on the blend of philosophical logic and formal philosophy embodied in Krister’s distinguished career.
-
On Monday, 25 August the Nordic Online Logic Seminar will host a special event in memory of Krister Segerberg, who passed away in January this year. Krister Segerberg was Professor of Theoretical Philosophy at Uppsala and, among logicians, is widely known for his pioneering work in modal logic where he initiated an influential systematic study of completeness proofs that still is standard in the field.
The seminar will feature talks by two academics that knew Krister Segerberg well:
- Johan van Benthem (UvA), Building Modern Modal Logic: Honoring Krister Segerberg
- John Cantwell (KTH), Some reflections on Krister’s philosophy of philosopy
A URL for this seminar will be distributed via the GU Logic and Nordic Online Logic mailing lists.
-
Opponent: Makoto Fujiwara, Assistant Professor, Tokyo University of Science
Abstract This dissertation concerns first-order theories of iterated 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 positive fixpoints and compositional and disquotational truth for truth-positive sentences, and a comparison with the classical case.
It is known that these theories over classical Peano arithmetic (PA) are mutually interpretable and exceeds the strength of PA. Over intuitionistic Heyting arithmetic (HA), on the other hand, finite iterations of strictly positive fixpoints have been shown to be conservative.
After introducing the setting and presenting the earlier results, as well as the technical tools, the main section of the dissertation can be roughly divided into two parts. The first presents a novel proof of the conservativity result above. The proof interprets the theories into the logic of partial terms where a realizability interpretation is used to reduce the problem to fixpoints for almost negative operator forms. A diagonal argument using a hierarchy of almost negative formulae with corresponding partial satisfaction predicates yields the result.
The second part generalises the tri-interpretation result from the second paragraph to intuitionistic theories, by proposing a new generalisation of positivity called guarded positivity with the aim to better capture the behaviour of intuitionistic implications and their interplay with transfinite iterations of truth and fixpoint predicates. As a corollary, these transfinite theories are stronger than HA.
A discussion of the results and the methods used concludes the dissertation.
Examination committee:
- Vera Koponen, chair (Uppsala University)
- Takako Nemoto (Tohoku University)
- Benno van den Berg (University of Amsterdam)
-
Akama et al. [1] introduced a hierarchical classification of first-order formulas and investigated them in the context of semi-classical arithmetic. In this talk, we first give a justification for the hierarchical classification in a general context of first-order theories. In fact, we formalize the standard transformation procedure for prenex normalization, and show that the classes E_k and U_k introduced in [1] are exactly the classes induced by Sigma_k and Pi_k respectively via the transformation procedure. See [2] for the details. In addition, we restrict the prenex normalization procedures to those which are possible over intuitionistic logic with assuming the decidability of formulas of degree n. Then we introduce new classes E^n_k and U^n_k of formulas with two parameters k and n, and show that they are exactly the classes induced by Sigma_k and Pi_k respectively according to the n-th level semi-classical prenex normalization. This is a joint work with Taishi Kurahashi.
[1] Yohji Akama, Stefano Berardi, Susumu Hayashi, and Ulrich Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS ’04), pp.192–201, 2004.
[2] Makoto Fujiwara and Taishi Kurahashi, Prenex normalization and the hierarchical classification of formulas, Archive for Mathematical Logic, vol. 63, pp. 391-403, 2024.
-
Logics that are obtained by constraining the available syntactic resources, such as first-order logic with a finite number of variables or with bounded quantifier rank, are central to finite model theory and descriptive complexity. In this talk, I will describe a categorical approach, which is model-theoretic in spirit, to study these logics using so-called game comonads. I will explain how these comonads capture various logic fragments (positive, existential, etc.) and combinatorial parameters of structures in a syntax-free manner. Furthermore, I will argue that this categorical perspective suggests a modal approach to various resource-bounded logics.
-
Logical inferentialists hold that the meaning of logical operators is given by their rules of inference. Arthur Prior cast doubt on this by introducing rules for his tonk operator that would allow for the derivation of any sentence whatsoever from any sentence whatsoever. The obvious inferentialist reply was to require some constraints on the defining rules, such as conservativeness (Belnap) or harmony (Dummett). In this talk, I will defend and investigate a different constraint: rules define a classical logical operator just in case they translate into an explicit definition in pure classical second-order logic. The right-hand side of this criterion will be found (i) to be philosophically principled in taking the idea of rules as definitions perfectly seriously, (ii) to explain how the semantic meaning of the operators can be determined from their rules, (iii) to be local in a similar sense as harmony, (iv) to validate the intuitionistic natural deduction rules and the intuitionistic/classical sequent calculus rules as defining the classical propositional operators while ruling out Prior’s rules for tonk, (v) to make clear why already the intuitionistic natural deduction rules define the classical meaning of logical operators so long as metavariables are interpreted as expressing classical propositions, (vi) to validate the classical natural deduction rules as analytic, (vii) to entail consistency, and, in the case of propositional operators (not quantifiers), (viii) to be decidable and (ix) to determine precisely those operators to be definable by rules that correspond to truth-functions.
-
Opponent: Jakub Szymanik, Associate professor at the Center for Brain/Mind Sciences and the Computer Science Department at the University of Trento.
Abstract Description logics are designed to reason efficiently with ontologies in knowledge bases, which are widely used in several industries. Human errors commonly cause mistakes to occur in the axioms of these ontologies, which leads to the logics deducing false conclusions. Ontology engineers spend much time on finding these false axioms to repair the ontology. This process can be facilitated by presenting a justification of the false conclusion, i.e. a set of axioms that entail the conclusion. Typically, the number of justifications for a given conclusion is very large and it is not clear which one should be presented.
It is therefore useful to estimate the cognitively adequate complexity of description logic so that the simplest justification(s) can be identified and selected. This work focusses on the cognitive complexity of deciding the consistency of ABoxes in the description logic $\mathcal{ALE}$. Conceptual considerations entail that the complexity of the ABox consistency problem is expressed as a linear preorder on a large enough set of ABoxes. This linear preorder can be estimated by an ACT-R model called SHARP. The model is a tableau algorithm implemented in a cognitive architecture, thereby modelling a human brain executing the tableau algorithm, which forms an approximation of the cognitive complexity ordering.
A complexity ordering that is a linear preorder can be obtained from experimental data by aggregating the different individual orders from a sample into one so-called proto-order, in which the largest transitive subrelation is the desired linear pre-order. The predicted complexity ordering by SHARP agrees well with the empirical data.
To enable applications in ontology debugging, a surrogate model is needed that accurately approximates SHARP’s output with great computational efficiency. Such a surrogate model can be obtained by the Random Forest algorithm trained on an appropriate dataset generated by SHARP. The complexity ordering thus obtained agrees well with the one predicted by SHARP but can be estimated in a fraction of the time enabling it for practical applications.