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.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

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

1. Graham Priest, Plurivalent logics, The Australasian Journal of Logic, vol. 11 (2014), no. 1.
2. Chris Brink, Power structures, Algebra Universalis, vol. 30 (1993), pp. 177–216.
3. Fredrik Engström, Orvar Lorimer Olsson, The propositional logic of teams, arXiv preprint, (2023), arXiv.2303.14022

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.

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.

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.

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.)

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

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.

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.

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.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

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.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

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.

Around 1930 a major paradigm shift occurred in the foundations of mathematics; we may call it the METAMATHEMATICAL TURN. Until then the task of a logician had been to design and explain a full-scale formal language that was adequate for the practice of mathematical analysis in such a way that the axioms and rules of inference of the theory were rendered evident by the explanations.

The metamathematical turn changed the status of the formal languages: now they became (meta)mathematical objects of study. We no longer communicate with the aid of the formal systems – we communicate about them. Kleene’s realizability (JSL 1945) gave a metamathematical (re-)interpretation of arithmetic inside arithmetic. Heyting and Kolmogorov (1931-2), on the other hand, had used “proofs” of propositions, respectively “solutions” to problems, in order to explain the meaning of the mathematical language, rather than reinterpret it internally.

We now have the choice to view the Curry-Howard isomorphism, say, as a variant of realizability, when it will be an internal mathematical re-interpretation, or to adopt an atavistic, Frege-like, viewpoint and look at the language as being rendered meaningful. This perspective will be used to discuss another paradigm shift, namely that of distinguishing constructivism and intuitionism. The hesitant attitude of Gödel, Kreisel, and Michael Dummett, will be spelled out, and, at the hand of unpublished source material, a likely reason given.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

The model SHARP is a result of (somewhat naively) implementing a tableaux-based reasoning algorithm of the description logic ALE into the cognitive architecture ACT-R. Its aim is to predict the inference time of human performance on deciding inconsistency of an ALE ABox, thereby giving rise to a complexity measure on ABoxes that is cognitively adequate. Ten predictions following from SHARP are tested against empirical data and their implications for the model are discussed.

In this presentation I focus on a framework that generalizes dynamic epistemic logic in order to model a wider range of scenarios including those in which agents read or communicate (or somehow gain access to) all the information stored at specific sources, or possessed by some other agents (including information of a non-propositional nature, such as data, passwords, secrets etc). The resulting framework allows one to reason about the state of affairs in which one agent (or group of agents) has ‘epistemic superiority’ over another agent (or group). I will present different examples of epistemic superiority and I will draw a connection to the logic of functional dependence by A. Baltag and J. van Benthem. At the level of group attitudes, I will further introduce the new concept of ‘common distributed knowledge’, which combines features of both common knowledge and distributed knowledge. This presentation is based on joint work with A. Baltag in [1].

[1] A. Baltag and S. Smets, Learning what others know, in L. Kovacs and E. Albert (eds.), LPAR23 proceedings of the International Conference on Logic for Programming, AI and Reasoning, EPiC Series in Computing, 73:90-110, 2020. https://doi.org/10.29007/plm4

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

One quarter of the talk presents background on how facts about entailments and non-entailments can single out the constants in a language, and in particular on an idea originating with Carnap that the standard relation of logical consequence in a formal language should fix the (model-theoretic) meaning of its logical constants. Carnap’s focus was classical propositional logic (CPL), but his question can be asked for any logical language. The rest of the talk gives a very general positive answer to this question for IPL: the usual IPL consequence relation does indeed determine the standard intuitionistic meaning of the propositional connectives, according to most well-known semantics for IPL, such as Kripke semantics, Beth semantics, Dragalin semantics, topological semantics, and algebraic semantics.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

We prove that ω² strictly bounds the iterations required for modal definable functions to reach a fixed point across all countable structures. In doing so, we both extend and correct the previously claimed result on closure ordinals of the alternation-free μ-calculus. The new approach sees a reincarnation of Kozen’s well-annotations, originally devised for showing the finite model property for the modal μ-calculus. We develop a theory of conservative well-annotations where minimality of the annotation is guaranteed, and isolate relevant parts of the structure that necessitate an unfolding of fixed points. This adoption of well-annotations enables a direct and clear pumping process that rules out closure ordinals between ω² and the limit of countability.

Boole, Tarski, Stone, Lawvere, Reyes, Makkai

Compositional theories of truth tend to follow the Tarskian tradition, either the model-theoretic semantics for classical predicate logic or its natural generalisations to many-value and possible-worlds. Other realisations of truth, which includes computational interpretations and game semantics, have been largely ignored by truth theorists. In this talk I will present axiomatic rendering of Krivine’s “classical realisability”, a ‘truth as programs’ semantics for classical logic that validates extensions of Peano arithmetic. What sets this conception of truth apart from the Tarskian view is its treatment of falsity as primitive and truth as a derived notion. This is joint work with Daichi Hayashi (Hokkaido University, Japan).

Dynamic Epistemic Logic (DEL) can be used as a formalism for agents to represent the mental states of other agents: their beliefs and knowledge, and potentially even their plans and goals. Hence, the logic can be used as a formalism to give agents, e.g. robots, a Theory of Mind, allowing them to take the perspective of other agents. In my research, I have combined DEL with techniques from automated planning in order to describe a theory of what I call Epistemic Planning: planning where agents explicitly reason about the mental states of others. The talk will introduce epistemic planning based on DEL, address issues of computational complexity, and demonstrate applications in cognitive robotics and human-robot collaboration.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressive criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.

There is now an acute need for intensive research on the possibility of effective learning with small data. The conference LSD running 11–12 September, organised by the Centre for Linguistic Theory and Studies in Probability (CLASP) and at the department of Philosophy, Linguistics and Theory of Science is devoted to work on this problem, with application to computational linguistics.

See the conference webpage for details.

Normal modal logics are closed under conjunctive closure. There are, however, interesting non-normal logics that are not, but which nevertheless satisfy a weak form of conjunctive closure. One example is a notion of group knowledge in epistemic logic: somebody-knows. While something is general knowledge if it is known by everyone, this notion holds if it is known by someone. Somebody-knows is thus weaker than general knowledge but stronger than distributed knowledge. We introduce a modality for somebody-knows in the style of standard group knowledge modalities, and study its properties. Unlike most other group knowledge modalities, somebody-knows is not a normal modality; in particular it lacks the conjunctive closure property. We provide an equivalent neighbourhood semantics for the language with a single somebody-knows modality, together with a completeness result: the somebody-knows modalities are completely characterised by the modal logic EMN extended with a particular weak conjunctive closure axiom. The neighbourhood semantics and the completeness and complexity results also carry over other logics with weak conjunctive closure, including the logic of so-called local reasoning (Fagin et al., 1995) with bounded “frames of mind”, correcting an existing completeness result in the literature (Allen 2005). The talk is based on joint work with Yi N. Wang.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

In this talk, we introduce a general family of sequent-style calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Calling these calculi constructive, we show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser’s rules, i.e., there is a polynomial time algorithm that reads a proof of the premise of a Visser’s rule and provides a proof for its conclusion. As a positive application, we show the feasible admissibility of Visser’s rules in several sequent calculi for intuitionistic modal logics, including CK, IK and their extensions by the modal axioms T, B, 4, 5, the modal axioms of bounded width and depth and the propositional lax logic. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser’s rules, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than IPC has a constructive sequent calculus. (joint work with Amir Tabatabai)

There are interpretations of Herbrand’s theorem extending its scope to formal number theory, though at the expense of analyticity, its most desirable property. Therefore, deepening our understanding of the analyticity boundary is important to many areas of computer science, as inductive theorem proving has a wide range of applications. One approach to studying this bound is through cut-elimination and how we can transform proofs using inductive reasoning. In this talk, we discuss cut-elimination by resolution, how to extend the method to proof schema, infinite sequences of proofs, and the framework presented in “Schematic Refutations of Formula Schemata.”

The SHACL Shapes Constraint Language was recommended in 2017 by the W3C for describing constraints on web data (specifically, on RDF graphs) and validating them. At first glance, it may not seem to be a topic for logicians, but as it turns out, SHACL can be approached as a formal logic, and actually quite an interesting one. In this paper, we give a brief introduction to SHACL tailored towards logicians and frame key uses of SHACL as familiar logic reasoning tasks. We discuss how SHACL relates to description logics, which are the basis of the OWL Web Ontology Languages, a related yet orthogonal standard for web data. Finally, we summarize some of our recent work in the SHACL world, hoping that this may shed light on how ideas, results, and techniques from well-established areas of logic can advance the state of the art in this emerging field.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

In 1994, Rineke Verbrugge did a postdoc in Gothenburg, as a scientific guest of Professor Per Lindström, who was writing his landmark book Aspects of Incompleteness at the time. Even though the two of them did not co-author any papers that year, there was still significant mutual influence and there were very lively discussions in the weekly seminars of the logic group. In this research lecture, Rineke Verbrugge will present some of the questions and results around bounded arithmetic, provability and interpretability logic that she was working on that year, for example, a small reflection principle for bounded arithmetic and the lattice of feasible interpretability types.

It has been shown in the late 1960s that each formula of first-order logic without constants and function symbols obeys a zero-one law: As the number of elements of finite models increases, every formula holds either in almost all or in almost no models of that size. For modal logics, limit behavior for models and frames may differ. In 1994, Halpern and Kapron proved zero-one laws for classes of models corresponding to the modal logics K, T, S4, and S5. They also proposed zero-one laws for the corresponding classes of frames, but their zero-one law for K-frames has since been disproved, and so has more recently their zero-one law for S4-frames.

Provability logic was one of the main interests of Per Lindström. In this talk, we prove zero-one laws for provability logic with respect to both model and frame validity. Moreover, we axiomatize validity in almost all irreflexive transitive finite models and in almost all irreflexive transitive finite frames, leading to two different axiom systems. In the proofs, we use a combinatorial result by Kleitman and Rothschild about the structure of finite (strict) partial orders: almost all of them consist of only three layers. Finally, we present empirical results in order to give an idea of the number of elements from which onwards a formula’s almost sure validity or almost sure invalidity stabilizes in such three-layer Kleitman-Rothschild frames. We also discuss possible extensions of the zero-one laws to the modal logics S4 and K4.

Public defence of Dominik Wehr’s Licentiate thesis.

Opponent Associate Professor Anupam Das, University of Birmingham
Examiner Docent Fredrik Engström, Göteborgs universitet
Thesis available at the Gothenburg University Library Archive.

Cyclic proof systems allow derivations whose underlying structure is a finite graph, rather than a well-founded tree. The soundness of cyclic proofs is usually ensured by imposing additional conditions beyond well-formedness. Distinct cyclic representations of the same logic can be obtained by combining the same stock of logical rules with different soundness conditions.

This thesis is a compilation of work in cyclic proof theory with a focus on the representation of cyclic proofs. The perspective is justified two-fold: First, the choice of representation of cyclic proofs has significant impact on proof theoretic investigations of cyclic proofs, dictating the effort required to derive desired results. Second, arguments which focus on the ‘cyclic’ aspects of cyclic proof systems, such as proof representations, rather than relying on specifics of logics, transfer more easily between different logics.

This thesis makes several contributions to the field of cyclic proof theory. First, we present a method for generating reset proof systems, a representation of cyclic proofs which has previously been key to proof theoretic investigations, from cyclic proof systems with global trace conditions, by far the most common representation of cyclic proofs in the literature. Because the method is presented in a generic manner, this yields reset proof systems for most logics considered in the cyclic proof theory literature. Second, we transfer a proof method of the equivalence of cyclic and ‘inductive’ proof systems, first employed by Sprenger and Dam, to the setting of Heyting and Peano arithmetic. Whereas previous proofs of this equivalence for arithmetic theories have relied on intricate arithmetical formalisations of meta-mathematical concepts, our proof operates at the level of cyclic proof representations. Third, using insights into the aforementioned proof method, we put forward a novel form of representation for cyclic proof systems which is of interest to cyclic proof theory beyond the proving of cyclic-inductive equivalences.

See also the public announcement of the event.

The logic group is hosting a two-day workshop on Thursday, 27 April and Friday, 28 April. This workshop brings together researchers from different aspects of fixed point logics and ill-founded proofs. The event is sponsored by the Knut and Alice Wallenberg Foundation via the research project Taming Jörmungandr: The Logical Foundations of Circularity. See the workshop webpage for details of talks and locations. Attendence is open to all.

We set out five basic requirements for a logical system to be adequate for the regimentation of deductive reasoning in mathematics and science. We raise the question whether there are any further requirements, not entailed by these five, that ought to be imposed. One possible reply is dismissed: that the logical system should allow one to infer any proposition at all from an inconsistent set—i.e., it should have as primitive, or allow one to derive, the rule Ex Falso Quodlibet. We then propose that the logic should be implosive: it should not allow an inconsistent set to have any consequences other than absurdity. This proposal may appear to be very radical; but we hope to show that it is robust against objections.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Automata theory has various applications in the theory of the modal µ-calculus. One such application is for the tableaux games for the modal µ-calculus introduced by Niwinski and Walukiewicz, in which one player has a winning strategy iff the formula is satisfiable. The winning condition of that game can be naturally checked by a nondeterministic parity automaton. We show how the determinisation of that automaton may be used to obtain a proof system. We then introduce a determinisation method for nondeterministic parity automata, which will be used to define a new annotated cyclic proof system for the modal µ-calculus.

(joint work with Johannes Marti and Yde Venema)

The World Wide Web Consortium (w3c) set Web Ontology Language (owl) and Shape Constraint Language (shacl) as international standards for managing semantically enriched data on the web. However, there is a difference in how these languages handle the completeness of data. In owl, not all information has to be explicitly present; part of the information can be implied by logical rules. Whereas shacl, which enables us to check for certain structures in a given knowledge graph, assumes completeness of it. Thus, with shacl we can validate the given data, while with owl we can infer knowledge. Combining the functionalities of the two into one standard is relevant and not straightforward.

In this seminar talk, we will introduce a new semantics for validating stratified shacl constraints, a specific family of queries, in presence of an ontology. We developed a refined chase technique, producing for each ontology a minimal model, i.e., a labeled graph, in which we can evaluate shacl constraints. However, this technique might still produce infinite models. This can be avoided by rewriting the shacl constraints with respect to the ontology, resulting in a standalone set of shacl constraints that can directly be verified only over the data; our second contribution.

The notion of (relative) interpretation for first order theories was introduced in a landmark 1953 monograph by Alfred Tarski, Andrzej Mostowski and Raphael Robinson, where it was developed as a powerful tool for establishing undecidability results. By now the domain of interest and applicability of interpretability theory far exceeds undecidability theory owing to its multifaceted interactions with both proof theory and model theory. Special attention will be paid to recent advances in the subject that indicate the distinctive character of Peano Arithmetic, Zermelo-Fraenkel set theory, and their higher order analogues in the realm of interpretability theory. This talk will present a personal overview of the interpretability analysis of arithmetical and set theoretical theories.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Starting from a logic given by traditional semantics formulated in terms of semantic objects (assignments, valuations or worlds) team semantics lifts the denotations of formulas to sets, or teams, of semantic objects instead enabling the formulation of properties, such as variable dependency, not available in the traditional setting. Since the introduction by Hodges, and refinement by Väänänen, team semantic constructions have been used to generate expressively enriched logics still conserving nice properties, such as compactness or decidability. In contrast these logics fail to be substitutional, limiting any algebraic treatment, and rendering fully schematic proof systems impossible. This shortcoming can be attributed to the flatness principle, commonly adhered to when generating team semantics.

Investigating the formation of team logics from an algebraic perspective, and disregarding the flatness-principle, I will present the logic of teams (LT), a substitutional logic for which important propositional team logics are axiomatisable as fragments. Starting from classical propositional logic and Boolean algebras, we give semantics for LT by considering algebras of the form P(B) being the powerset of a Boolean algebra B, treated with treated with an internal (derived from B) and an external (set-theoretic) set of connectives. Furthermore, we present a well-motivated labelled natural deduction system for LT, for which a further analysis motivates a generalisation to constructions of logics by combinations of an internal and an external logic, where for LT both are classical propositional logic.

This is joint work with Fredrik Engström.

One of the major problems in formal epistemology is the difficulty of combining probabilistic and full (dichotomous, all-or-nothing) beliefs in one and the same formal framework. Major properties of actual human belief systems, including how they are impacted by our cognitive limitations, are used to introduce a series of desiderata for realistic models of such belief systems. This leads to a criticism of previous attempts to combine representations of both probabilistic and full beliefs in one and the same formal model. Furthermore, a formal model is presented in which this is done differently. One of its major features is that contingent propositions can be transferred in both directions between full beliefs and lower degrees of belief, in a way that mirrors real-life acquisitions and losses of full beliefs. The subsystem consisting of full beliefs has a pattern of change that constitutes a credible system of dichotomous belief change.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Public defence of Tjeerd Fokkens’ Licentiate thesis.

Opponent Dr Ing Stefan Borgwardt, Technische Universität Dresden
Examiner Professor Simon Dobnik, Göteborgs universitet

The problem of optimising automated explanations for entailments in knowledge bases is tackled by modelling deductive reasoning processes using the cognitive architecture ACT-R. This results in the model SHARP which simulates the algorithm for deciding inconsistency of an ABox in the description logic ALE as executed by a human. More precisely, SHARP enables predicting the inference time of this task, which is assumed to reflect cognitive load of a human agent. With the inference time, two complexity measures on ABoxes are defined that should correlate with cognitive load by design.

A copy of Tjeerd’s thesis can be obtained by sending an email to the contact person Fredrik Engström.

I will present recent results and work in progress on adapting proof theoretic methods to non-well-founded notions of proof.

Compositional semantics that acknowledge vagueness by positing degrees of truth intermediate between truth and falsity can retain classical sentential calculus, provided the degrees form a Boolean algebra. A valid deduction guarantees that the degree of truth of the conclusion be at least as great as every lower bound on the degrees of the premises. If we extend the language to allow infinite disjunctions and conjunctions, the Boolean algebra will need to be complete and atomic. If we extend further by adding quantifiers ranging over a fixed domain, we get the supervaluations proposed by Bas van Fraassen.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

I will present some of the fundamental aspects of classical realizability. Firstly, we will have a brief look into the history and motivation behind the study of realizability, starting from the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic and Kleene’s original number realizability. Afterwards we will examine how these ideas can be adapted to classical logic by exploring the mechanisms behind Krivine’s classical realizability. This talk is the result of a reading course in the Master of Logic programme.

Public defence of Giacomo Barlucchi’s Licentiate thesis.

Opponent Docent Sebastian Enqvist, Stockholms universitet
Examiner Docent Fredrik Engström, Göteborgs universitet

We study the computational content of fixed points in relation to two logical systems with distinct characteristics. Common to both research strands is a method for dealing with the iterative nature of fixed points. In the first part the interest is directed to a cyclic system ICA for intuitionistic arithmetic. The formal definition of the system is followed by the introduction of typed λY-calculus, whose terms represent the deductive process of cyclic proofs. A method for producing recursion schemes from instances of cyclic proofs is given. The result is a grammar whose language consists of λ-terms, capturing the computational content implicit in the initial proof. In the second part, we look at the iteration of fixed points in terms of closure ordinals of formulas in the modal μ-calculus. A method for determining an upper bound on closure ordinals is presented and applied to formulas in fragments of the Σ1 class, with results that are in line with the already existing works. Annotated structures, to track how model changes affect the ordinals, and a pumping technique for these structures are the main tools used to establish an upper bound.

A copy of Giacomo’s thesis can be obtained by sending an email to the contact person Bahareh Afshari.

I present a topological epistemic logic, motivated by a famous epistemic puzzle: the Surprise Exam Paradox. It is a fixed-point modal logic, with modalities for knowledge (modelled as the universal modality), knowability of a proposition (represented by the topological interior operator), and (un)knowability of the actual world. The last notion has a non-self-referential reading (modelled by Cantor derivative: the set of limit points of a given set) and a self-referential one (modelled by the so-called perfect core of a given set: its largest subset which is a fixed point of relativized derivative). I completely axiomatize this logic, showing that it is decidable and PSPACE-complete, as well as briefly explain how the same model-theoretic method can be elaborated to prove the completeness and decidability of the full topological mu-calculus. Finally, I apply it to the analysis of the Surprise Exam Paradox and other puzzles.

References:

• A. Baltag, N. Bezhanishvili, D. Fernández-Duque. The Topology of Surprise. Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning. Vol. 19 (1), 33-42, 2022. Available online in ILLC Prepublication (PP) series PP-2022-06.
• A. Baltag, N. Bezhanishvili, D. Fernández-Duque. The Topological Mu-Calculus: Completeness and Decidability. LICS ‘21: Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, vol 89: 1-13, 2021. doi:10.1109/lics52264.2021.9470560. Available online in ILLC Prepublication (PP) series PP-2021-07.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

I will first give a brief background, with some examples, on ‘Carnap’s problem’: to what extent a consequence relation in a formal language fixes the meaning, relative to some given semantics, of the logical constants in that language. I then focus on intuitionistic propositional logic and show that it is ‘Carnap categorical’: the only interpretation of the connectives consistent with the usual intuitionistic consequence relation is the standard one. This holds relative to most well-known semantics with respect to which intuitionistic logic is sound and complete; among them Kripke semantics, Beth semantics, Dragalin semantics, and topological semantics. It also holds for algebraic semantics, although categoricity in that case is different in kind from categoricity relative to possible worlds style semantics. This is joint work with Haotian Tong.

In the book Das Kontinuum (1918), Hermann Weyl presents a coherent and sophisticated approach to analysis from a predicativist perspective. In the first chapter of (Weyl 1918), Weyl introduces a predicative concept of set, according to which sets are built ‘from the bottom up’ starting from the natural numbers. Weyl clearly contrasts this predicative concept of set with the concept of arbitrary set, which he finds wanting, especially when working with infinite sets. In the second chapter of Das Kontinuum, he goes on to show that large portions of 19th century analysis can be developed on the basis of his predicative concept of set.

Das Kontinuum inspired fundamental ideas in mathematical logic and beyond, such as the logical analysis of predicativity of the 1950-60’s, Solomon Feferman’s work on predicativity and Errett Bishop’s constructive mathematics. The seeds of Das Kontinuum are already visible in the early (Weyl 1910), where Weyl, among other things, offers a clarification of Zermelo’s axiom schema of Separation.

In this talk, I examine Weyl’s predicative concept of set in (Weyl 1918) and discuss its origins in (Weyl 1910).

Bibliography

• Weyl, H., 1910, Über die Definitionen der mathematischen Grundbegriffe, Mathematischnaturwissenschaftliche Blätter, 7, pp. 93-95 and pp. 109-113.
• Weyl, H., 1918, Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis, Veit, Leipzig. Translated in English, Dover Books on Mathematics, 2003.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Ill-founded and cyclic proof systems have proven to be fruitful alternatives to traditional, finitary proof systems when dealing with modal fixed point logics. The question arises whether ill-founded and cyclic systems can be also be designed for intuitionistic versions of these logics. In this talk, I will present ongoing research aimed at developing an ill-founded sequent calculus for intuitionistic linear temporal logic. In particular, I will focus on our attempt to show completeness of such a calculus using backwards proof search. This is joint work with Lukas Zenger, Bahareh Afshari and Graham Leigh.

In standard proof theory a proof is a finite tree whose nodes are labelled by sequents and which is generated by a finite set of rules. One such rule is the cut rule, which is a sequent calculus analogue of the well-known modus ponens rule. As the cut rule introduces new formulas into a proof, it makes proofs non-analytic. Therefore, much effort is devoted to show that the cut rule can be eliminated from a given calculus without changing the set of derivable sequents. Such a cut-elimination theorem is established by showing how instances of the cut rule in a given proof can be pushed upwards until the premises of the instances are axioms. One then shows that in this case the instances of cut can be eliminated from the proof. However, this standard strategy does not work when one considers so-called non-wellfounded proofs, which are proofs in which some branches are allowed to be infinitely long. Clearly, in such a setting it is not enough to simply push instances of cut upwards, as a leaf might never be reached. In this talk I will present ongoing research on cut-elimination for non-wellfounded proofs for a fragment of the modal mu-calculus. I will discuss the basic idea how to construct a cut-free proof from a given non-wellfounded proof and present some of the current problems of my method.

Modal fixed point logics are extensions of modal logics with operators denoting least, respectively greatest, fixed points of certain positive formulas. Logics of this kind include temporal logics, logics of common knowledge, program logics, and most famously, the modal mu-calculus. We present a survey of deductive systems for the logic of common knowledge as a typical example of a model fixed point logic. In particular, we present two different Hilbert-style axiomatizations and several infinitary cut-free sequent systems that are based on omega-rules. Further, we discuss the problem of syntactic cut-elimination for common knowledge and its generalization to the modal mu-calculus.

Strict/tolerant logic, ST, has been of considerable interest in the last few years, in part because it forces consideration of what it means for two logics to be different, or the same. And thus, of what it means to be a logic. The basic idea behind ST is that it evaluates the premises and the conclusions of its consequence relation differently, with the premises held to stricter standards while conclusions are treated more tolerantly. More specifically, ST is a three-valued logic with left sides of sequents understood as if in Kleene’s Strong Three Valued Logic, and right sides as if in Priest’s Logic of Paradox. Surprisingly, this hybrid validates the same sequents that classical logic does, though it differs from classical logic at the metaconsequence level. A version of this result has been extended to meta, metameta , etc. consequence levels, creating a very interesting hierarchy of logics. All this is work of others, and I will summarize it.

My contribution to the subject is to show that the original ideas behind ST are, in fact, much more general than it first seemed, and an infinite family of many valued logics have Strict/Tolerant counterparts. Besides classical logic, this family includes both Kleene’s and Priest’s logics themselves, as well as first degree entailment. For instance, for both the Kleene and the Priest logic, the corresponding strict/tolerant logic is six-valued, but with differing sets of strictly and tolerantly designated truth values. There is a reverse notion, of Tolerant/Strict logics, which exist for the same structures. And the hierarchy going through meta, metameta, \ldots consequence levels exists for the same infinite family of many valued logics. In a similar way all this work extends to modal and quantified many valued logics. In brief, we have here a very general phenomenon.

I will present a sketch of the basic generalizations, of Strict/Tolerant and Tolerant/Strict, but I will not have time to discuss the hierarchies of such logics, nor will I have time to give proofs, beyond a basic sketch of the ideas involved.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Full Computation Tree Logic, commonly denoted CTL*, extends Linear Temporal Logic LTL by path quantification for reasoning about branching time. In contrast to traditional Computation Tree Logic CTL, path quantifiers may be freely combined with temporal operators, resulting in a more expressive language. We present a sound and complete hypersequent calculus for CTL*. The proof system is cyclic in the sense that proofs are finite trees with back-edges. A simple annotation mechanism on formulas provides a syntactic success condition on non-axiomatic leaves to guarantee soundness. Completeness is established by relating cyclic proofs to a natural ill-founded sequent calculus for the logic. This is joint work with B. Afshari and Graham E. Leigh.

The study of Gödel’s shorthand notebooks in the ERC project GODELIANA has revealed two main aspects of his work: First, there is behind each of his relatively few published papers an enormous amount of notes. They typically reveal how he arrived at his results, as with the incompleteness theorem. An extreme case are Gödel’s 1938 results on set theory, preceded by some 700 pages of notes never studied before. Secondly, his threshold for publishing was by 1940 so high that some two thousand pages of developments and results remained unknown. One highlight here is a series of notebooks titled “Resultate Grundlagen” in which numerous anticipations of later results in set theory are found. A second main topic are the relations between modal and intuitionistic logic. In particular, Gödel gives a syntactic translation from S4 to intuitionistic logic by methods that are readily generalizable to any decent intermediate logics. These newly discovered methods are, even by today’s standards, a clear step ahead in the study of interrelations between systems of non-classical logics.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

(Dis)embodiment is a conference organized by the Centre for Linguistic Theory and Studies in Probability (CLASP), at the Department of Philosophy, Linguistics and Theory of Science. The conference will be held between September 14 to September 16. See the conference webpage for more details.

We describe a theory of computable functionals (TCF) which extends Heyting’s arithmetic in all simple types by (i) adding inductively and coinductively defined predicates, (ii) distinguishing computationally relevant (c.r.) and non-computational (n.c.) predicates, (iii) adding realizability predicates, and (iv) allowing partial functionals defined by equations (possibly non-terminating, like corecursion). The underlying (minimal) logic has just implication and universal quantification as primitive connectives; existence, disjunction and conjunction are inductively defined. The axioms of TCF are the defining axioms for (co)inductive predicates, bisimilarity axioms and invariance axioms stating that ‘‘to assert is to realize’’ (Feferman 1978) for realizability-free formulas. Using these one can prove in TCF a soundness theorem: the term extracted from a realizability-free proof of a formula A is a realizer of A. TCF is implemented in the Minlog proof assistant.

Motivated by the difficulty in proving faithfulness of various modal embeddings (starting with Gödel’s translation of intuitionistic logic into S4), we use labelled calculi to obtain simple and uniform faithfulness proofs for the embedding of intermediate logics into their modal companions, and of intuitionistic logic into provability logic, including extensions to infinitary logics.

Syntax and semantics, often considered as conflicting aspects of logic, have turned out to be intertwined in a methodology for generating complete proof systems for wide families of non-classical logics. In this formal semantics, models can be considered as purely mathematical objects with no ontological assumptions upon them. More specifically, by the “labelled formalism”, which now is a well-developed methodology, the semantics is turned into an essential component in the syntax of logical calculi. Thus enriched, the calculi not only constitute a tool for the automatisation of reasoning, but can also be used at the meta-level to establish general structural properties of logical systems and direct proofs of completeness up to decidability in the terminating case. The calculi, on the other hand, can be used to find simplified models through conservativity results. The method will be illustrated with gradually generalised semantics, including topological ones such as neighbourhood semantics.

Conservative extensions are a fundamental notion in logic. In the area of description logic, deciding whether a logical theory is a conservative extension of another theory is a fundamental reasoning problem with applications in ontology engineering tasks, such as ontology modularity, ontology reuse and ontology versioning. It has been observed in recent years that conservative extensions are decidable in many modal and description logics, given that they can often be characterized elegantly in terms of appropriate notions of bisimulations. But no work has been done for more expressive logics such as the two-variable fragment and the guarded fragment, which are considered to be generalizations of modal and description logics, and are typically used to explain their good computational behavior.

In this talk, I attempt to fill this gap by considering the decidability of conservative extensions in the two-variable guarded fragment (gfo2). I will show that conservative extensions are decidable in gfo2 and that the computational complexity is 2exptime-complete. To prove these results I will rely on an automata-based approach, which consists in first giving a model-theoretic characterization of conservative extensions in terms of guarded bisimulations, to then use it as a foundation for a decision procedure based on tree automata. Since the usual notion of guarded bisimulations fail to characterize conservative extensions in gfo2, I will report on alternative model-theoretic characterizations in terms of bounded guarded bisimulations and the challenge of combining them with automata techniques.

This talk is based on joint work with Carsten Lutz, Jean Christoph Jung, Thomas Schneider, and Frank Wolter: https://drops.dagstuhl.de/opus/volltexte/2017/7464/pdf/LIPIcs-ICALP-2017-108.pdf

Aristotle famously claimed that the only coherent form of infinity is potential, not actual. However many objects there are, it is possible for there to be yet more; but it is impossible for there in fact to be infinitely many objects. Although this view was superseded by Cantor’s transfinite set theory, even Cantor regarded the collection of all sets as “unfinished” or incapable of “being together”. In recent years, there has been a revival of interest in potentialist approaches to the philosophy and foundations of mathematics. The lecture provides a survey of such approaches, covering both technical results and associated philosophical views, as these emerge both in published work and in work in progress.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

In constructive type theory and explicit mathematics, the idea of universes has been used to strengthen the expressive power or the proof-theoretic strength of a given system. Similarly, Cantini (1996) and Kahle (2003) introduced universes for axiomatic truth theories over TON (total applicative theory). Set-theoretic universes are usually large sets that are closed under several operations like complements, whereas truth-theoretic universes can be seen as quasi-truth predicates which satisfy some axioms for the truth predicate. Cantini and Kahle then showed that by adding the axiom assuring the existence of universes, several truth theories become proof-theoretically stronger.

In this talk, I will formulate the theory VFU, an extension of Cantini’s supervaluational truth theory VF (cf. Kahle, 2002) with the universe-generating axiom, and then prove that VFU has the same proof-theoretic strength as KPi (Kripke-Platek set theory with the recursively inaccessible universe) and T0 (Feferman’s explicit mathematics with the inductive generation axiom). To determine the lower bound, I show that T0 is relatively interpretable in VFU. As for the upper bound, I give a truth-as-provability interpretation for VFU, where the truth predicate is understood as the provability in a certain infinite derivation system. As this is formalisable in KPi, a relative interpretation of VFU in KPi is obtained. Therefore, all the three systems are proof-theoretically equivalent. Finally, I would like to mention the possibility of constructing natural numbers in VFU.

What is a Gödel sentence? Is there such a thing as the Gödel sentence of a given theory?

Lajevardi and Salehi, in a short paper from last year, argue against the use of the definite article in the expression ‘the Gödel sentence’, by claiming that any unsound theory has Gödelian sentences with different truth values. We show that the two theorems of their paper are special cases (modulo Löb’s theorem and the first incompleteness theorem) of general observations pertaining to fixed points of any formula, and argue that the false sentences of Lajevardi and Salehi are in fact not Gödel sentences. We conclude with a discussion of the roles played by soundness and truth in drawing further consequences from the incompleteness theorems.

This paper on which this talk is based is joint work with Christian Bennet.

Progressions of theories along paths through Kleene’s Omega adding the consistency of the previous theory at every successor step, can deduce every true \( \Pi^0_1 \)-statement. This was shown by Turing in his 1938 thesis who called these progressions “ordinal logics”. In 1962 Feferman proved the amazing theorem that progressions based on the “uniform reflection principle” can deduce every true arithmetic statement. In contrast to Turing’s, Feferman’s proof is very complicated, involving several cunning applications of self-reference via the recursion theorem. Using Schütte’s method of search trees (or decomposition trees) for omega-logic and reflexive induction, however, one can give a rather transparent proof.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

I present an untyped theory of knowledge and truth that solves the knower paradoxes of Kaplan and Montague from the 1960’s. The underlying idea is (1) to formalize the principle of veracity (that whatever is known is true) more precisely, and (2) to embrace self-reference in the spirit of the Friedman-Sheard theory of truth and its associated revision semantics. It turns out that this facilitates expedient reasoning with common-knowledge predicates defined by self-referential formulas obtained by Gödel diagonalization. Moreover, the revision semantics is generalized to accommodate my theory. Apart from answering questions of consistency, this opens up for philosophical insights on the meaning of sentences involving iterations of knowledge and truth, such as ‘“Kim knows A” is true’ and ‘Kim knows “Kim knows A”’.

The practice of foundations of mathematics is built around a firm distinction between syntax and semantics. But how stable is this distinction, and is it always the case that semantically presented mathematical objects in the form e.g. of a model class might give rise to a “natural logic”? In this talk I will investigate different scenarios from set and model theory in which an investigation of the notion of an implicit or internal logic or syntax becomes possible. Time permitting we will also discuss the question whether logics without a syntax can be considered logics at all.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Substructural logics are logics with restricted use of structural rules like weakening, contraction and exchange. There are several motivations for investigating substructural logics from the study of algebraic structures like residuated (semi)lattices to the study of type systems which allow for greater control over the number of times and the order in which variables are used.

Enriched with fixed point operators, these logics are highly expressive. In this talk, I will give a brief overview of substructural logics with fixed points and concentrate specifically on linear logic with fixed points discussing various proof systems, their expressivity, and semantics.

Transitive Closure Logic (TCL) enriches the language of first order logic with a recursive operator, expressing the transitive closure of a binary relation. Cyclic sequent calculi proofs for this logic have been introduced in the literature. In this talk, I will present a new cyclic proof system for TCL, which employs hypersequents. The main motivation behind this work is that, differently from sequent TCL proofs, hypersequent proofs for TCL successfully simulate cyclic proofs in the transitive fragment of Propositional Dynamic Logic (PDL+), without using the non-analytic rule of cut.

After introducing the cyclic hypersequent calculus for TCL, I will present two main results. First, I will sketch a proof of soundness for the calculus, which requires a more involved argument than the one used in traditional cyclic proofs. Second, I will show how PDL+ cyclic proofs can be translated into TCL hypersequent proofs. This result allows to lift the completeness result for cyclic PDL+ to the hypersequent calculus. This talk is based on joint work with Anupam Das.

The first part will be about representation of mathematics on a computer. Questions that arise there are naturally reminiscent of issues that arise when teaching formal proofs in a basic logic course, e.g. how to deal with free and bound variables, and instantiation rules. As discussed in a 1962 paper of Tarski, these issues are “clearly experienced both in teaching an elementary course in mathematical logic and in formalizing the syntax of predicate logic for some theoretical purposes.” I will present two quite different approaches to this problem: one inspired by Tarski’s paper (N. Megill, system Metamath) and one using dependent type theory (N.G. de Bruijn).

The second part will then try to explain how notations introduced by dependent type theory suggest new insights for old questions coming from Principia Mathematica (extensionality, reducibility axiom) through the notion of universe, introduced by Grothendieck for representing category theory in set theory, and introduced in dependent type theory by P. Martin-Löf.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Description Logics (DLs) are a family of knowledge representation languages, used to reason with information sets in a structured and well-understood way. They play a big role in any field using large amounts of data, e.g. artificial intelligence, databases, and they are of importance in providing a logical formalism for ontologies and the Semantic Web. A common battle in the world of DLs is the one between expressivity, where we add fixpoints, inverses, role restrictions, etc, to a standard DL, and decidability. That is why more expressive as well as light-weight DLs are considered, which both benefit from different derivation system. In this talk I will first give an introduction on the general area of Description Logic, and then focus on the different reasoning problems and how they are solved proof-theoretically. The main result will be on Martin Hofmann’s paper, presenting the sequent calculus for the light description logic EL with the fixpoint extension, and see how cyclic proofs are used in this context. This talk is based on the reading course I did together with Bahareh Afshari as a preparation for my Master thesis.

Reasoning with generalized quantifiers in natural language combines logical and arithmetical features, transcending divides between qualitative and quantitative. This practice blends with inference patterns in ‘grassroots mathematics’ such as pigeon-hole principles. Our topic is this cooperation of logic and counting on a par, studied with small systems and gradually moving upward. We start with monadic first-order logic with counting. We provide normal forms that allow for axiomatization, determine which arithmetical notions are definable, and conversely, discuss which logical notions and reasoning principles can be defined out of arithmetical ones. Next we study a series of strengthenings in the same style, including second-order versions, systems with multiple counting, and a new modal logic with counting. As a complement to our fragment approach, we also discuss another way of controlling complexity: changing the semantics of counting to reason about ‘mass’ or other aggregating notions than cardinalities. Finally, we return to the basic reasoning practices that lie embedded in natural language, confronting our formal systems with linguistic quantifier vocabulary, monotonicity reasoning, and procedural semantics via semantic automata. We conclude with some pointers to further entanglements of logic and counting in the metamathematics of formal systems, the philosophy of logic, and cognitive psychology. (Joint work with Thomas Icard)

Paper available at: https://eprints.illc.uva.nl/id/eprint/1813/1/Logic.Counting.pdf

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

I will introduce some of our research on Iris, a higher-order concurrent separation logic framework, implemented and verified in the Coq proof assistant, which can be used for mathematical reasoning about safety and correctness of concurrent higher-order imperative programs. Iris has been used for many different applications; see iris-project.org for a list of research papers. However, in this talk I will focus on the Iris base logic (and its semantics) and sketch how one may define useful program logics on top of the base logic. The base logic is a higher-order intuitionistic modal logic, which, in particular, supports the definition of recursive predicates and whose type of propositions is itself recursively defined.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Cyclic proof systems permit derivations to contain cycles, thereby serving as finite representations of non-wellfounded derivation trees. Such cyclic proof systems have been proposed for a broad range of logics, especially those with fixed-point features or inductively defined objects of reasoning. The soundness of such systems is commonly ensured by only considering those cyclic derivations as proofs which satisfy a so-called global trace condition.

In this talk, I will present a category theoretical notion, the trace category, which generalizes the trace condition of many cyclic proof systems. Indeed, a handful of different trace categories are sufficient to capture the trace conditions of all cyclic proof systems from the literature I have examined so far. The arising abstract notion of cyclic proof allows for the derivation of generalized renditions of standard results of cyclic proof theory, such as the decidability of proof-checking and the regularizability of certain non-wellfounded proofs. It also opens the door to broader inquiries into the structural properties of trace condition based cyclic and non-wellfounded proof systems, some of which I will touch on in this talk, time permitting. The majority of this talk will be based on my Master’s thesis.

Cognitive scientists Spelke and Kintzler (2007) and Carey (2009) propose objects, actions, space and numbers as ‘core domains of knowledge’ that underpin the framework of concepts people use to describe and communicate about the world. Gärdenfors (2019, 2020) argues that humans make sense of domains by appealing to various types of invariances in sensory signals. In this talk, I present work by Quinon and Gärdenfors (manuscript) in which the aim is to extend the analysis in terms of invariances to the domain of numbers. We focus on several perspectives relating invariances: cognitive modeling, formal mathematical and experimental.

As theoretical background, we assume that numbers are properties of collections (Simons 1982, 2007, 2011; Johansson 2015; Angere 2014). We observe that the domain of number is determined by two types of invariances. First, the concept of collection itself depends on being invariant under the location of its objects. Second, the determinant invariance of the domain of number is the fungibility of objects: If an object in a collection is exchanged for another object, the collection will still contain the same number of objects. Fungibility will be shown to be closely related to one-to-one correspondences.

We first introduce the concept of a collection and show how it differs from the concept of a set. Then we present the invariance of location of objects that applies to collections and we introduce fungibility as a second type of invariance. We illustrate our theoretical analysis by empirical material from experiments of developmental psychologists.

This is joint work with Peter Gärdenfors (Lund).

In 1672 John Eliot, English Puritan educator and missionary, published The Logick Primer: Some Logical Notions to initiate the INDIANS in the knowledge of the Rule of Reason; and to know how to make use thereof [1]. This roughly 80 page pamphlet focuses on introducing basic syllogistic vocabulary and reasoning so that syllogisms can be created from texts in the Psalms, the gospels, and other New Testament books. The use of logic for proselytizing purposes is not distinctive: What is distinctive about Eliot’s book is that it is bilingual, written in both English and Wôpanâak (Massachusett), an Algonquian language spoken in eastern coastal and southeastern Massachusetts. It is one of the earliest bilingual logic textbooks, it is the only textbook that I know of in an indigenous American language, and it is one of the earliest printed attestations of the Massachusett language.

In this talk, I will:

• Introduce John Eliot and the linguistic context he was working in.
• Introduce the contents of the Logick Primer—vocabulary, inference patterns, and applications.
• Discuss notions of “Puritan” logic that inform this primer.
• Talk about the importance of his work in documenting and expanding the Massachusett language and the problems that accompany his colonial approach to this work.

References

[1] J.[ohn] E.[liot]. The Logick Primer: Some Logical Notions to initiate the INDIANS in the knowledge of the Rule of Reason; and to know how to make use thereof. Cambridge, MA: Printed by M.[armaduke] J.[ohnson], 1672.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

I will demonstrate how Walukiewicz’ seminal proof of completeness for the propositional μ-calculus can be derived (and refined) from the cyclic proof theory of the logic, notably the uniform interpolation theorem for the logic.

Team semantics is, when compared to standard Tarskian semantics, a more expressive framework that can be used to express logical connectives, operations and atoms that can’t be expressed in Tarskian semantics. This includes branching quantifiers, notions of dependence and independence, trace quantification in linear-time temporal logic (LTL), and probabilistic notions from quantum mechanics.

Team semantics is based on the same notion of structure as Tarskian semantics, but instead of a single assignment satisfying a formula (or not), in team semantics a set, or a team, of assignments satisfies a formula (or not). In other words, the semantic value of a formula is lifted from a set of assignments (those that satisfy the formula) to a set of teams of assignments.

In almost all (with only one exception that I’m aware of) logical systems based on team semantics this lifting operation is the power set operation, and as a result the set of teams satisfying a formula is closed downwards. This is often taken as a basic and foundational principle of team semantics.

In this talk I will discuss this principle and present some ideas on why, or why not, the power set operation is the most natural lift operation. By using other lift operations we can get a more powerful semantics, but, it seems, also a more complicated one.

References:

• Engström, F. (2012) “Generalized quantifiers in dependence logic”
• Nurmi, V. (2009) “Dependence Logic: Investigations into Higher-Order Semantics Defined on Teams”
• Väänänen, J. (2007) “Dependence logic: A new approach to independence friendly logic”

Semiring semantics of logical formulae generalises the classical Boolean semantics by permitting multiple truth values from certain semirings. In the classical Boolean semantics, a model of a formula assigns to each (instantiated) literal a Boolean value. K-interpretations, for a semiring K, generalize this by assigning to each such literal a value from K. We then interpret 0 as false and all other semiring values as nuances of true, which provide additional information, depending on the semiring: For example, the Boolean semiring over {0,1} corresponds classical semantics, the Viterbi-semiring can model confidence scores, the tropical semiring is used for cost analysis, and min-max-semirings (A, max, min, a, b) for a totally ordered set (A,<) can model different access levels. Most importantly, semirings of polynomials, such as N[X], allow us to track certain literals by mapping them to different indeterminates. The overall value of the formula is then a polynomial that describes precisely what combinations of literals prove the truth of the formula.

This can also be used for strategy analysis in games. Evaluating formulae that define winning regions in a given game in an appropriate semiring of polynomials provides not only the Boolean information on who wins, but also tells us how they win and which strategies they might use. For this approach, the case of Büchi games is of special interest, not only due to their practical importance, but also because it is the simplest case where the logical definition of the winning region involves a genuine alternation of a greatest and a least fixed point. We show that, in a precise sense, semiring semantics provide information about all absorption-dominant strategies – strategies that win with minimal effort, and we discuss how these relate to positional and the more general persistent strategies. This information enables further applications such as game synthesis or determining minimal modifications to the game needed to change its outcome.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Sets of uniqueness and their properties are traditionally investigated in Harmonic Analysis. The study of such sets has a long and illustrious history, witnessing fruitful interdisciplinary interactions, often enriching the subject with a vibrant fertility for crossover of ideas. In this talk, we set up the modern framework used to study such sets with particular emphasis on some (classical) descriptive set-theoretic aspects. We present some results concerning the family of closed sets of uniqueness of a locally compact Polish group - more concretely, we will talk about their complexity and the (in)existence of a Borel basis.

We employ the lens provided by formal truth theory to study axiomatizations of PA (Peano Arithmetic). More specifically, let EA (Elementary Arithmetic) be the fragment I∆0 + Exp of PA, and CT⁻[EA] be the extension of EA by the commonly studied axioms of compositional truth CT⁻. The truth theory delivers a natural preorder on the set of axiomatizations: an axiomatization A is greater or equal to an axiomatization B if and only if, over CT^-[EA], the assertion “All axioms from A are true” implies “All axioms from B are true”. Our focus is dominantly on two types of axiomatizations, namely: (1) schematic axiomatizations that are deductively equivalent to PA, and (2) axiomatizations that are proof-theoretically equivalent to the canonical axiomatization of PA.

The first part of the talk focuses on the axiomatizations of type (1). We adapt the argument by Visser and Pakhomov (“On a question of Krajewski’s”, JSL 84(1), 2019) to show that there is no weakest axiomatization of this form (even if the axiomatizations are ordered by relative interpretability). Secondly, we sketch an argument showing that such axiomatizations with the given ordering form a countably universal partial order. This part is based on our joint work with Ali Enayat, available at https://www.researchgate.net/publication/353496287_Axiomatizations_of_Peano_Arithmetic_A_truth-theoretic_view

In the second part of the talk we discuss axiomatizations of type (2). We narrow our attention to such axiomatizations A for which CT^-[EA] + “All axioms from A are true” is a conservative extension of PA. We explain why such theories have very diverse metamathematical properties (e.g. large speed-up). To illustrate our methods we show that, with the given ordering, such axiomatizations do not form a lattice. This is a work still in progress.

Cyclic (or circular) proofs are now a common technique for demonstrating metalogical properties of systems incorporating (co)induction, including modal logics, predicate logics, type systems and algebras. Inspired by automaton theory, cyclic proofs encode a form of self-dependency of which induction/recursion comprise special cases. An overarching question of the area, the so-called ‘Brotherston-Simpson conjecture’, asks to what extent the converse holds.

In this talk I will discuss a line of work that attempts to understand the expressivity of circular reasoning via forms of proof theoretic strength. Namely, I address predicate logic in the guise of first-order arithmetic, and type systems in the guise of higher-order primitive recursion, and establish a recurring theme: circular reasoning buys precisely one level of ‘abstraction’ over inductive reasoning.

This talk will be based on the following works:

• https://arxiv.org/abs/1807.10248
• https://arxiv.org/abs/2012.14421

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Fitch-style modal lambda calculi (Borghuis 1994; Clouston 2018) provide a solution to programming necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator (denoted by a lock). The addition of locks simplifies the formulation of typing rules for calculi that incorporate different modal axioms, but obscures weakening and substitution, and requires tedious and seemingly ad hoc syntactic lemmas to prove normalization.

In this work, we take a semantic approach to normalization, called Normalization by Evaluation (NbE) (Berger and Schwichtenberg 1991), by leveraging the possible world semantics of Fitch-style calculi. We show that NbE models can be constructed for calculi that incorporate the K, T and 4 axioms, with suitable instantiations of the frames in their possible world semantics. In addition to existing results that handle beta reduction (or computational rules), our work also considers eta expansion (or extensional equality rules).

References:

• Borghuis, V.A.J. (1994). “Coming to terms with modal logic : on the interpretation of modalities in typed lambda-calculus”.
• Clouston, Ranald (2018). “Fitch-Style Modal Lambda Calculi”.
• Berger, Ulrich and Helmut Schwichtenberg (1991). “An Inverse of the Evaluation Functional for Typed lambda-calculus”.

In his address to the International Congress of Mathematics in Vancouver, 1974, Harvey Friedman launched a program where the aim would be to find the minimal set of axioms needed to prove theorems of ordinary mathematics. More than often, it turned out that the axioms then would be provable from the theorems, and the subject was named Reverse Mathematics. In this talk we will survey some of the philosophy behind, and results of, the early reverse mathematics, based on the formalisation of mathematics within second order number theory.

In 2005, Ulrich Kohlenbach introduced higher order reverse mathematics, and we give a brief explanation of the what and why? of Kohlenbach’s approach. In an ongoing project with Sam Sanders we have studied the strength of classical theorems of late 19th/early 20th century mathematics, partly within Kohlenbach’s formal typed theory and partly by their, in a generalised sense, constructive content. In the final part of the talk I will give some examples of results from this project, mainly from the perspective of higher order computability theory. No prior knowledge of higher order computability theory is needed.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

In its modern formulation, Hilbert’s tenth problem asks to find a general algorithm which decides the solvability of Diophantine equations. While this problem was shown to be unsolvable due to the combined work of Davis, Putnam, Robinson and Matiyasevich, similar question can be posed over domains other than the integers. Among the most important open questions in this area of research is if a version of Hilbert’s tenth problem for F_p((t)), the field of formal Laurent series over the finite field F_p, is solvable or not. The fact that this remains open stands in stark contrast to the fact that the first order theory of the much similar object Q_p, the field of p-adic numbers, is completely understood thanks to the work by Ax, Kochen and, independently, Ershov. In light of this dichotomy, I will present new decidability results obtained during my doctoral research on extensions of F_p((t)). This work is motivated by recent progress on Hilbert’s tenth problem for F_p((t)) by Anscombe and Fehm and builds on previous decidability results by Kuhlman.

When is a property of a model a logical property? According to the so-called Tarski-Sher criterion this is the case when the property is preserved by isomorphisms. We relate this to the model-theoretic characteristics of abstract logics in which the model class is definable, resulting in a graded concept of logicality (in the terminology of Sagi’s paper “Logicality and meaning”). We consider which characteristics of logics, such as variants of the Löwenheim-Skolem Theorem, Completeness Theorem, and absoluteness, are relevant from the logicality point of view, continuing earlier work by Bonnay, Feferman, and Sagi. We suggest that a logic is the more logical the closer it is to first order logic, and offer a refinement of the result of McGee that logical properties of models can be expressed in L_∞∞ if the expression is allowed to depend on the cardinality of the model, based on replacing L_∞∞ by a “tamer” logic. This is joint work with Jouko Väänänen.

Almost exactly a thousand years ago a teenager known today as Avicenna lived in what is now Uzbekistan. He made a resolution to teach himself Aristotelian logic, armed with an Arabic translation of Aristotle and a century-old Arabic textbook of logic. A couple of years later, around his eighteenth birthday, he wrote a brief report of what he had learned. Six months ago I started to examine this report - I suspect I am the first logician to do that. It contains many surprising things. Besides introducing some new ideas that readers of Avicenna know from his later works, it also identifies some specific points of modal logic where Avicenna was sure that Aristotle had made a mistake. People had criticised Aristotle’s logic before, but not at these points. At first Avicenna had no clear understanding of how to do modal logic, and it took him another thirty years to justify all the criticisms of Aristotle in his report. But meanwhile he discovered for himself how to defend a new logic by building new foundations. I think the logic itself is interesting, but the talk will concentrate on another aspect. These recent discoveries mean that Avicenna is the earliest known logician who creates new logics and tells us what he is doing, and why, at each stage along the way.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

I will present work in progress (together with Graham Leigh) on a novel proof of the conservativity of the intuitionistic fix-point theory over Heyting arithmetic (HA), originally proved in full generality by Arai [1]. We make use of the work of van den Berg and van Slooten [2] on realizability in Heyting arithmetic over Beeson’s logic of partial terms (HAP). Let IF be the extension of Heyting arithmetic by fix-points, denoted \hat{ID}ⁱ₁ in the literature. The proof is divided into four parts: First we extend the inclusion of HA into HAP to IF into a similar theory IFP in the logic of partial terms. We then show that every theorem of this theory provably has a realizer in the theory IFP(Λ) of fix-points for almost negative operator forms only. Constructing a hierarchy stratifying the class of almost negative formulae and partial truth predicates for this hierarchy, we use Gödel’s diagonal lemma to show IFP(Λ) is interpretable in HAP. Finally we use use the result of [2] that adding the schema of “self-realizability” for arithmetic formulae to HAP is conservative over HA. The result generalises the work presented at my half-time seminar 2020-08-28.

References

[1] Toshiyasu Arai. Quick cut-elimination for strictly positive cuts. Annals of Pure and Applied Logic, 162(10):807–815, 2011.

[2] Benno van den Berg and Lotte van Slooten. Arithmetical conservation results. Ind- agationes Mathematicae, 29:260–275, 2018.

Focusing is a general technique for syntactically compartmentalising the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing was traditionally specified as a restriction of the sequent calculus, the technique had not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some modal or substructural logics.

With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents, which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.

Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a substructural logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed again by a polarised and focused variant that we show is sound and complete via a cut-elimination argument.

In the traditional so-called Tarski’s Truth Definition the semantics of first order logic is defined with respect to an assignment of values to the free variables. A richer family of semantic concepts can be modelled if semantics is defined with respect to a set (a “team”) of such assignments. This is called team semantics. Examples of semantic concepts available in team semantics but not in traditional Tarskian semantics are the concepts of dependence and independence. Dependence logic is an extension of first-order logic based on team semantics. It has emerged that teams appear naturally in several areas of sciences and humanities, which has made it possible to apply dependence logic and its variants to these areas. In my talk I will give a quick introduction to the basic ideas of team semantics and dependence logic as well as an overview of some new developments, such as quantitative analysis of team properties, a framework for a multiverse approach to set theory, and probabilistic independence logic inspired by the foundations of quantum mechanics.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

In the field of axiomatic theories of truth, conservativity properties of theories are much investigated. Conservativity can be used to argue that, despite the well-known undefinability of truth, there is a sense in which a primitive truth predicate can be reduced to the resources of an underlying mathematical theory that provides basic syntactic structure to truth ascriptions. Conservativity is typically proved model-theoretically, or proof-theoretically via the elimination of cuts on formulae containing truth (Tr-cuts). The original Tr-cut-elimination argument for the theory of Tarskian, compositional truth CT[B] by Halbach is not conclusive. This strategy has been corrected by Graham Leigh: Leigh supplemented Halbach’s strategy with the machinery of approximations (introduced by Kotlarski, Krajewski and Lachlan in the context of their M-Logic). In the talk we investigate a different, and arguably simpler way of supplementing Halbach’s original strategy. It is based on an adaptation of the Takeuti/Buss free-cut elimination strategy for first-order logic to the richer truth-theoretic context. If successful, the strategy promises to generalize to the type-free setting in a straightforward way. This is joint work with Luca Castaldo.

An account of inferences should take into account not only inferences from established premisses but also inferences made under assumptions. This makes it necessary to consider arguments, chains of inferences in which assumptions and variables may become bound. An argument is valid when all its inferences are valid, and it then amounts to a proof in case it has no unbound assumptions or variables. The validity of an inference – not to confuse with the conclusion being a logical consequence of the premisses – seems in turn best explained in terms of proofs. This means that the concepts of valid inference and valid argument depend on each other and cannot be defined independently but have to be described by principles that state how they are related. A number of such principles will be proposed. It is conjectured that inferences that can be expressed in the language of first order intuitionistic predicate logic and are implied to be valid by these principles are all provable in that logic.

This talk is part of the Nordic Online Logic Seminar Series. Zoom link is shared via the NOL mailing list

Conditional perfection is the phenomenon in which conditionals are strengthened to biconditionals. In some contexts, “If A, B” is understood as if it meant “A if and only if B.” I’ll present and discuss a series of experiments designed to test one of the most promising pragmatic accounts of conditional perfection. This is the idea that conditional perfection is a form of exhaustification, triggered by a question that the conditional answers. If a speaker is asked how B comes about, then the answer “If A, B” is interpreted exhaustively to meaning that A is the only way to bring about B. Hence, “A if and only if B.” The evidence suggests that conditional perfection is a form of exhaustification, but not that it is triggered by a relationship to a salient question. (This is joint work with Fabrizio Cariani.)

Project presentations

A cyclic proof is a, possibly infinite but, regular derivation tree in which every infinite path satisfies a certain soundness criterion, the form of which depends on the logic under study. Circular and, more generally, non-wellfounded derivations are not traditionally regarded as formal proofs but merely as an intermediate machinery in proof-theoretic investigations. They are, however, an important alternative to finitary proofs and in the last decade have helped break some important barriers in the proof theory of logics formalising inductive and co-inductive concepts. In this talk we focus on cyclic proofs for modal logics, ranging from Gödel-Löb logic to more expressive languages such as the modal mu-calculus, and reflect on how they can contribute to the development of the theory of fixed point modal logic.

This talk is about two different generalisations of Gödel’s incompleteness theorems and the (natural?) idea of trying to merge the two into a stronger result. The first generalisation I have in mind is Feferman’s theorem on the “interpretability of inconsistency”. This result strengthens the second incompleteness theorem, by showing that the sentence expressing that PA is inconsistent is not only consistent with PA, but even that PA + “PA is inconsistent” is interpretable in PA. The second generalisation is due to Kripke, who showed that there is a flexible formula: a formula “whose extension as a set is left undetermined” by PA. In particular, he constructed a Σ-1 formula γ(x), such that for every Σ-1 formula σ(x), the theory PA + “γ = σ” is consistent. This result generalises the first incompleteness theorem, since any instance of such a γ must be independent of PA. Unfortunately, the straightforward combination of Feferman’s and Kripke’s theorems — the “interpretability of flexibility” — is a false claim. Indeed, it is easy to show that there can be no Σ-1 formula γ such that for all Σ-1 formulae σ, the theory PA + “γ = σ” is interpretable in PA.

There are, however, several weaker results available, due to Enayat, Hamkins, Shavrukov, Woodin, and me. These results either (1) relax the restriction on γ, (2) further restrict the allowed choices of σ’s, (3) strengthen the interpreting theory beyond PA, or (4) use equality modulo finite differences. I will present these four intermediate results, along with the remaining question that they all fail to answer. Finally, I will discuss why the known proof method does not seem to lend itself to giving a positive answer to this remaining question, as well as explain how any counterexample would have to look.

As anyone who reads the literature on bi-intuitionistic logic will know, the numerous papers by Cecylia Rauszer are foundational but confusing. For example: these papers claim and retract various versions of the deduction theorem for bi-intuitionistic logic; they erroneously claim that the calculus is complete with respect to rooted canonical models; and they erroneously claim the admissibility of cut in her sequent calculus for this logic. Worse, authors such as Crolard, have based some of their own foundational work on these confused and confusing results and proofs. We trace this confusion to the axiomatic formalism of RBiInt in which Rauszer first characterized bi-intuitionistic logic and show that, as in modal logic, RBiInt can be interpreted as two different consequence relations. We remove this ambiguity by using generalized Hilbert calculi, which are tailored to capture consequence relations. We show that RBiInt leads to two logics, wBIL and sBIL, with different extensional and meta-level properties, and that they are, respectively, sound and strongly complete with respect to the Kripkean local and global semantic consequence relations of bi-intuitionistic logic. Finally, we explain where they were conflated by Rauszer.

A formula equation is a formula in first-order logic with unknowns representing predicates. Solving a formula equation consists of finding first-order instances of these unknowns that result in a valid formula. In this talk I will first give an overview of this topic and, in particular, describe its connections to well-known problems in logic and its applications in computer science. I will then concentrate on specific classes of formula equations and present

1. joint work with J. Kloibhofer on solutions of Horn formula equations in first-order logic with least fixed points and
2. joint work with S. Zivota showing that solvability of affine formula equations is decidable, thus generalising previous results about loop invariant generation.

An important fact about type theory, and something which is also heavily exploited in implementations, is that type checking is decidable However, from a complexity-theoretic point of view the worst case upper bounds are quite serious: according to a result by Statman from 1979, the problem is not elementary recursive. Recently, in the context of homotopy type theory people have started to consider a version of type theory in which all computation rules are replaced by propositional equalities. In this talk, I will discuss this version of type theory, which one could call “objective type theory”. In particular, I will show that if one formulates this objective type theory with sufficient care, type checking can be done in quadratic time. (This is joint work with my PhD student Martijn den Besten.)

The talk will be devoted to the formal connections between two canonical types of axiomatizations for the truth predicate: the disquotational scheme and the compositional clauses. We will be interested in measuring the “logical distance” between the two canonical sets of principles and determining whether each of them “determine” the other. Working in the framework of axiomatic truth theories we shall consider various ways of formalizing the above two questions and present the current state of art. The talk initializes the project (under the same name) which started in Warsaw at the beginning of September. At the current time there are still much more questions than answers, but we believe that it is worth uncovering this research perspective. Some questions will be investigated jointly with the Gothenburg logic group.

We develop an untyped semantic framework for the multiverse of set theory and show that its proof-theoretic commitments are mild. ZF is extended with semantical axioms utilizing the new symbols M(U) and M(U,σ), expressing that U is a universe and that σ is true in the universe U, respectively. Here σ ranges over the augmented language, leading to liar-style phenomena that are analysed. The framework is both compatible with a broad range of multiverse conceptions and suggests its own philosophically and semantically motivated multiverse principles.

We propose to unify the treatment of a broad range of modalities in typed lambda calculi. We do so by defining a generic structure of modalities, and show that this structure arises naturally from the structure of intuitionistic logic, and as such finds instances in a wide range of type systems previously described in literature. Despite this generality, this structure has a rich metatheory, which we expose.

Joint work with Andreas Abel.

Dependence logic, proposed by Väänänen, is an elegant way of introducing dependencies between variables into the object language. The framework of Dependence logic, so-called team semantics, has turned out to be very flexible and allows for interesting generalizations. Instead of considering satisfaction with respect to a single assignment s, team semantics considers sets of assignments X, called teams. While the semantics of Dependence logic is based on the principle that a formula φ is satisfied by a team X if every assignment s ∈ X satisfies φ, we will replace this principle by the following: a formula φ is satisfied by a team X if for every assignment s: s ∈ X iff s satisfies φ, replacing an implication by an equivalence. When only first-order logic is considered nothing exciting happens, it is only when we introduce new logical operations that things start to get more exciting.