Archive of events from 2020
An archive of events from the year
-
Rasmus Blanck (FLoV)
Interpretability and flexible formulas
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.
-
Rajeev Goré (Australian National University)
Bi-Intuitionistic Logics: a New Instance of an Old Problem
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.
-
Stefan Hetzl (TU Wien)
Formula equations
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
- joint work with J. Kloibhofer on solutions of Horn formula equations in first-order logic with least fixed points and
- joint work with S. Zivota showing that solvability of affine formula equations is decidable, thus generalising previous results about loop invariant generation.
-
Benno van den Berg (ILLC, Amsterdam)
Quadratic type checking for objective type theory
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.)
-
Mateusz Łełyk (Warsaw)
Between Disquotation and Compositionality
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.
-
Paul Kindvall Gorbow (FLoV)
The Copernican Multiverse of Sets
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.
-
Jean-Philippe Bernardy (FLoV)
A Unified View of Modalities in Type Systems
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.
-
Fredrik Engström (FLoV)
Dependence logic and generalized quantifiers
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.