Archive of events from 2022

Public defence of Giacomo Barlucchi’s Licentiate thesis.

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

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.

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.

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.

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

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.

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.

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.

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.