We are excited to announce a Day of Logic at the Department of Computer Science, University of Verona (Strada le Grazie 15 - 37134 Verona) on Wednesday, October 23, 2024.
The event, titled “Categorical Logic and Constructive Mathematics,” is scheduled to start at 9:15 AM in Aula M and to continue until the late afternoon.
Speakers:
- Iosif Petrakis (University of Verona)
- Giulio Fellin (University of Brescia)
- Francesco Ciraulo (University of Padua)
- Marco Benini (University of Insubria)
- Logic seminar: Hajime Ishihara (Toho University)
- Department seminar: Tarmo Uustalu (Reykjavik University & Tallinn University of Technology)
Substructural Logics à la Lambek: Proof Theory and Categorical Semantics Tarmo Uustalu (Reykjavik University & Tallinn University of Technology)
October 21–30, 2024
Abstract
In the 1960s, Joachim Lambek pioneered an approach to substructural logics that unifies proof theory and category theory, motivated by linguistics. ‘Substructural’ means here that some basic principles like “A implies true,” “A implies A and A,” and “A and B imply B and A” do not hold. In sequent calculus terms, this corresponds to the absence of the structural rules of left weakening, contraction, and exchange, indicating that logic is more about resources than truth. What is now known as Lambek calculus is a noncommutative intuitionistic linear logic with a (multiplicative) conjunction and two implications, left and right.
In this minicourse, I will review this approach first on Lambek calculus and a number of variations of it. Then I will focus on skew logics—logics that are even weaker than substructural in that the conjunction connective is only semiunital and semiassociative.
The course will be self-contained. Basic knowledge of classical and intuitionistic logic (Hilbert-style systems and sequent calculi) is desirable for good intuitions. I will introduce the necessary ingredients of proof theory and category theory.
Timetable
Monday, 21: 11:30–13:30 in Aula D
Tuesday, 22: 8:30–10:30 in Aula C
Friday, 25: 15:30–18:30 in Aula B
Monday, 28: 11:30–13:30 in Aula D
Tuesday, 29: 8:30–10:30 in Aula C
Wednesday, 30: 10:30–11:30 in Aula M
Monadic second order limit laws for natural well orderings
We prove monadic second order limit laws for ordinals stemming from segments of some prominent proof-theoretic ordinals like ωω , ε0, Γ0, . . . . The results are based on a combination of automata theoretic results, tree enumeration theory and Tauberian methods. We believe that our results will hold in very general contexts.
Some results have been obtained jointly with Alan R. Woods (who unfortunately passed away in 2011).
Reverse Mathematics of WQO’s of Transfinite Sequences with Finite Range
In this talk I will present the result about the provability in ATR_0 of the theorem of Nash-Williams that sequences with finite range over a wqo form a wqo. For this we develop a framework where we work with α-wqo’s over primitive recursive set theory extended with a global enumeration function and then transfer the results obtained there to ATR_0.
The talk is based on a research project joint with Giovanni Soldà.
On the logical structure of some maximality and well-foundedness principles equivalent to choice principles: the contrapositive case of Teichmüller-Tukey lemma and Berger’s update induction
I will present the main ideas of a research proposal in the making. It aims to develop a dynamic (potentialist) account of an agent’s first-order intentional attitudes as representative models of (possible) reality. The account introduces the new notion of the intentum, and formally develops intentic models consisting of such intenta. These are meant to be structures that an agent can dynamically construct mentally, and which consequently help us philosophically explain and reason about beliefs, wishes, imaginations, etc. Here follow some promising applications of this framework:
It offers a novel theory of propositions and intentionality, somewhat in the spirit of Frege, but with distinct advantages compared to the two classical accounts of Frege and Russell.
It provides a foundational approach of value to the fragmented field of theoretical research on AI agenthood.
It enables a modular account of the notoriously complex notion of reference.
It provides a lens for approaching philosophical questions about identity.
It helps to philosophically explain knowledge of mathematics.
It provides a modern formal basis for the Kantian theory of categories, with a particular application to mathematical induction (as “synthetic a priori” knowledge).
It sheds light on arbitrary objects.
In my talk, I will explain the basic ideas of the framework and explain a select few of these applications.
Subintuitionistic logics and their modal companions: a nested approach
In the present talk we deal with subintuitionistic logics and their modal companions. In particular, we introduce nested calculi for subintuitionistic systems and for modal logics in the S5 modal cube ranging from K to S4. The latter calculi differ from standard nested systems, as there are multiple rules handling the modal operator. As an upshot, we get a purely syntactic proof of the Gödel–McKinsey–Tarski embedding which preserves the structure and the height of the derivations. Finally, we obtain a conservativity result for classical logic over a weak subintuitionistic system.
Modal logic for induction: from chain conditions to arithmetic
j.w.w. S. Negri and P. Schuster
We use modal logic to obtain syntactical, proof-theoretic versions of transfinite induction as axioms or rules within an appropriate labelled sequent calculus. While transfinite induction proper, also known as Noetherian induction, can be represented by a rule, the variant in which induction is done up to an arbitrary but fixed level happens to correspond to the Gödel–Löb axiom of provability logic. To verify the practicability of our approach in actual practice, we sketch a fairly universal pattern for proof transformation and test its use in several cases. Among other things, we give a direct and elementary syntactical proof of Segerberg’s theorem that the Gödel–Löb axiom characterises precisely the (converse) well-founded and transitive Kripke frames. We then show that, by adding appropriate rules, this approach allows us to obtain a calculus for a bounded version of Peano Arithmetic. Finally, we observe that, by slightly modifying the rules, we can do the same for arithmetic in ordinals other than ω.
in cooperation with A. Knapp (Univ. of Augsburg)
and M. Wirsing (LMU Munich)
An ensemble is formed by a collection of agents which
run concurrently to accomplish (together) a certain task.
For that purpose agents must collaborate in some way,
for instance by explicit interaction via message passing.
In this talk we present an epistemic approach where
collaboration is based on the knowledge that agents have
about themselves, about other agents and about their
environment. Any change of knowledge caused by an action
of one agent may influence the behaviour of other agents.
Hence, interaction is implicit.
For specifying properties of epistemic ensembles we propose
a dynamic logic style such that necessary and possible
ensemble behaviours are expressed by modalities on (complex)
epistemic actions. Our semantic models are labelled transition
systems with ensemble actions as labels. Such transitions
model two aspects, (i) the control flow of an ensemble and
(ii) changes of epistemic information caused by the epistemic
effect of an agent action.
Epistemic ensembles are implemented by epistemic processes,
one for each ensemble agent, which are composed in parallel
to form an ensemble realisations. We provide a structured
operational semantics for such processes which allows us to
introduce a (formal) correctness notion: An ensemble realisation
is correct w. r. t. an ensemble specification if its semantics
is an epistemic model of the specification. Two ensemble
realisations are equivalent, if their models are epistemically
bisimilar. We show that this can be checked by checking
bisimilarity of their single processes in the usual sense
of process algebra.
Implicative algebras were introduced by A.Miquel to provide a common foundation for Heyting/Boolean-valued logic and realizability. In this talk I will show how one can produce models for intuitionistic and classical Zermelo-Fraenkel set theory (I)ZF using implicative algebras, generalizing forcing and realizability models for set theory, both intuitionistic and classical . This result has an application to the theory of toposes, since it entails that every topos which is obtained from Set by means of the tripos-to-topos construction contains a model of (I)ZF, provided one assumes a large enough inaccessible cardinal exists. This talk is based on a joint work with A.Miquel.
Intended audience: Computer scientists and mathematicians (PhD-level and advanced Master’s-level)
Abstract: Martin-Löf’s type theory (MLTT) is a predicative modification of lambda-calculus with many applications to the theory of programming languages. The recent extension of MLTT with the axiom of univalence (UA) by the late Fields medalist Voevodsky reveals surprising connections between homotopy theory and logic. Homotopy Type Theory (HoTT) can be described as MLTT + UA + Higher Inductive Types. HoTT and Category Theory (CaT), are currently among the most actively studied mathematical frameworks for the logical foundations of mathematics and theoretical computer science. The following topics are planned to be covered: introduction to MLTT, function-extensionality axiom, the groupoid model of Hofmann and Streicher, Voevodsky’s axiom of univalence, homotopy n-types, higher inductive types, the fundamental group of the higher circle, relations between HoTT and constructive mathematics, relations between HoTT and CaT.
No prior knowledge of homotopy theory and type theory is required.
Lecture notes will be available.
References:
E. Rijke: Introduction to Homotopy Type Theory, https://arxiv.org/abs/2212.11082, 2022, pre-publication version, which will be published by Cambridge University Press.
The Univalent Foundations Program Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, Princeton, 2013. https://homotopytypetheory.org/book/
Marco Benini (Università degli Studi dell’Insubria)
1. Homotopy Type Theory: A Gentle Introduction: Monday, September 25th, 16:00, Aula G (Ca’ Vignal 2).
Abstract:
Homotopy Type Theory (HoTT) is, syntactically, Martin-Löf Type Theory
(MLTT) plus the axiom called “univalence”.
Hence, it is, at the same time, an abstract functional programming
language, a logical system, and a synthetic way to describe homotopy
spaces.
The seminar introduces the type system, focusing on the homotopy
interpretation, univalence, and higher inductive types, i.e., the main
novelties of HoTT with respect to MLTT.
The seminar aims at providing the fundamental ideas of HoTT to
mathematicians and computer scientists willing to understand what is
HoTT without the burden of a formal, in-depth presentation.
2. Homotopy Type Theory: Equality as Equality: Tuesday, September 26th, 16:00, Aula I (Ca’ Vignal 2).
Abstract:
The seminar aims at discussing the logical properties of judgemental
and propositional equalities in HoTT. It shows the fundamental
reasoning techniques of HoTT, and a few small novel results.
Also, the material provides a critical view of the current stage of
development of the theory, showing to what extent a systematic
approach is needed.
This talk is intended for mathematicians and computer scientists
willing to see more of the formal and technical side of HoTT, and some
minimal
knowledge about type theories, algebraic topology, and constructive
mathematics is presumed.
The talks will be held both in presence and on Zoom. In order to get the Zoom link, please contact Giulio Fellin.
Synthetic scheme theory: a simpler framework for algebraic geometry
Note: This talk has been postponed to a later date.
Abstract:
The modern framework for algebraic geometry put forward by Grothendieck
and his school has been enormously successful, providing the basis for
many deep cornerstone results of the subject. Not least, we owe to this
basis the proof of Fermat’s Last Theorem.
Despite these successes, Grothendieck himself expressed discontent with his framework,
and especially in recent years, concerns about the limitations and
technical difficulties of the modern theory of algebraic geometry arose.1
With the benefit of hindsight, now that the mathematical content of the
then-revolutionary new approach to algebraic geometry is
well-understood, we propose an update to the foundations of algebraic
geometry, called synthetic scheme theory, built on three postulates.
These postulates capture essential geometric properties and allow us to
reason constructively, avoiding the use of transfinite principles and
other highly abstract concepts. Our hope is that this approach will
allow for a clearer and more intuitive expression of the central notions
and insights of algebraic geometry, requiring less technical machinery,
will facilitate integrated developments, and promote computer-assisted
proofs in the subject.
Crucially, our approach rests on the greater axiomatic freedom provided
by constructive mathematics: The three postulates are inconsistent with
classical logic.
_Algebraic Representation of the Fixed-Point Closure of *-continuous Kleene Algebras_
Abstract:
The theorem of Chomsky and Schützenberger says that each context-free language L over a finite alphabet X is the image of the intersection
of a regular language R over X+Y and the context-free Dyck-language
D over X+Y of strings with balanced brackets from Y under the
bracket-erasing homomorphism from the monoid of strings over X+Y to
that of strings over X.
Within Hopkins’ algebraization of formal language theory we show that
the algebra C(X) of context-free languages over X has an isomorphic
copy in a suitable tensor product of the algebra R(X) of regular
languages over X with a quotient of R(Y) by a congruence describing
bracket matches and mismatches. It follows that all context-free
languages over X can be defined by regular(!) expressions over X+Y
where the letters of X commute with the brackets of Y, thereby
providing a substitute for a fixed-point-operator.
This generalizes the theorem of Chomsky and Schützenberger and leads
to an algebraic representation of the fixed-point closure of
*-continuous Kleene algebras.
Perhaps the most pressing are that the currently framework heavily
relies on the axiom of choice and other classical principles–even though
high-level reasoning in algebraic geometry is often constructive–and
that the framework references and requires gadgets of little geometric
significance, such as injective or flabby resolutions. These
foundational issues block integrated developments of algorithms in
algebraic geometry, hindering us from extracting certified algorithms
directly from proofs, and render computer formalization of algebraic
geometry particularly challenging.↩︎
Quantificatori moltiplicativi, esponenziali e cut-elimination
(j.w.w. Carlo Nicolai e Mario Piazza)
Abstract:
L’aggiunta di un predicato di verità governato da regole ingenue conduce spesso a sistemi contraddittori. Un metodo per recuperare la consistenza consiste nell’adottare una logica priva di contrazione: questa strada è stata seguita - tra gli altri - da Grishin e Cantini. Successivamente un ulteriore approccio basato su quantificatori moltiplicativi è stato proposto da Zardini, ma il sistema si è rivelato inconsistente. Nel presente talk proponiamo un’analisi della logica dei quantificatori moltiplicativi. In primo luogo offriamo una presentazione consistente di un sistema con predicato di verità decitazionale con quantificatori additivi. In seguito mostriamo come gli esponenziali (! e ?) possano essere interpretati in modo corretto e fedele mediante l’uso dei quantificatori moltiplicativi. Infine proponiamo una dimostrazione sintattica di eliminazione del taglio per un calcolo con quantificatori moltiplicativi. L’analisi della strategia porterà alla luce la presenza di contrazione implicita nelle regole dei quantificatori.
Tatsuji Kawai (Japan Advanced Institute of Science and Technology)
Predicative theory of stably locally compact locales
We give a predicative presentation of stably locally compact locales, the class of locales which includes locally compact regular locales (e.g., localic reals) as its subclass. In our setting, a stably locally compact locale is presented as a quasi-proximity lattice, a quasi-bounded distributive lattice (distributive lattice without top) together with a certain idempotent relation on it. Using this structure, we construct a coreflection from the category of locally compact regular locales and cobounded maps to that of stably locally compact locales and perfect maps. The construction of this coreflection generalizes Dedekind’s construction of real numbers as pairs of a lower and an upper cut.
16:30
Hajime Ishihara (Japan Advanced Institute of Science and Technology)
Reflexive combinatory algebras
We introduce the notion of reflexivity for combinatory algebras. Reflexivity can be thought of as an equational counterpart of the Meyer-Scott axiom of combinatory models, which indeed allows us to characterise an equationally definable counterpart of combinatory models. This new structure, called strongly reflexive combinatory algebra, admits a finite axiomatisation with seven closed equations, and the structure is shown to be exactly the retract of combinatory models. Lambda algebras can be characterised as strongly reflexive combinatory algebras which are stable.
This is a joint work with Marlou M. Gijzen and Tatsuji Kawai.
The minicourse On the Algebra of Logic [2 ETCS Mat/01] by Tommaso Moraschini, University of Barcelona, is being videoregistered from now on.
Attendees are expected to have verified, refreshed or acquired adequate basic knowledge of universal algebra before following the videolectures by working through chapters 1 and 2 of the course notes.
Members of the University of Verona are kindly asked to register for the course mailing list by writing to Giulio Fellin. Students of the University of Verona who want to obtain credits for this course also in the future should contact prof. Peter Schuster.
Homotopy type theory (HoTT) extends Martin-Löf type theory with the univalence axiom, which establishes a tight connection between types and homotopy spaces and allows to identify isomorphic objects. Univalence has very useful applications, but it has also drawbacks: properties that are not invariant under homotopy cannot be expressed internally. An important case is the concept of semisimplicial types, whose definition is so far elusive in HoTT.
Two-level type theory (2LTT) is a formal theory which allows constructions that require access to non-homotopy-invariant notions. It is composed of two separate levels of types related by a conversion function that preserves context extensions; the outer level is Martin-Löf type theory plus the uniqueness of identity proofs, and the inner level is HoTT.
In this talk we will discuss the consequences of univalence, and introduce 2LTT as a way to overcome some difficulties. Then, we will introduce the notion of model for this system, and define the syntactical category as a first step to prove an initiality result for the syntax of 2LTT. The last part of the talk is based on a joint work-in-progress with Benedikt Ahrens and Nicolai Kraus.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster or Giulio Fellin.
Gianluca Amato (Chieti-Pescara) Universal Algebra in UniMath (joint work with Marco Maggesi and Cosimo Perini Brogi)
Abstract:
In this talk we will report on recent experiments in implementing the basic notions of universal algebra in the Unimath library. Unimath is a replacement of the standard library of the Coq proof assistant based on the univalent foundations of mathematics. Since the use of general higher order inductive types is forbidden in Unimath, a relevant part of this work has been the implementation of terms as lists of function symbols in such a way that the operations on terms are computable by the standard Coq evaluation mechanism.
Thierry Coquand (Göteborg) Sheaf models and constructive mathematics
Abstract:
Sheaf models over sites, introduced by Grothendieck in algebraic geometry, are also important in the meta-theory of intuitionistic mathematics for showing that some properties are not valid constructively or for providing models of the notion of choice sequences. In this talk, I would like to explain another use of sheaf models in constructive mathematics, suggested by Joyal in 1975, which is to provide a way to build an algebraic closure of an arbitrary field.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster or Giulio Fellin.
Paolo Pistone (Bologna) The Yoneda Reduction of Polymorphic Types (joint work with Luca Tranchini)
Abstract:
We explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under theories of equivalence stronger than βη-equivalence, like those induced by parametricity and dinaturality. Based on such isomorphisms, we investigate a rewriting over types, that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We then demonstrate some applications of this rewriting to problems like counting the inhabitants of a type or characterizing program equivalence in some fragments of System F.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster or Giulio Fellin.
Thursday, January 21st, 2021, 10:30, on Zoom.PLEASE NOTICE THAT THE TALK WAS POSTPONED
Eugenio Orlandelli (Bologna) FULL CUT ELIMINATION AND INTERPOLATION FOR INTUITIONISTIC LOGIC WITH EXISTENCE PREDICATE
Abstract:
In previous work by Baaz and Iemhoff, a Gentzen calculus for intuitionistic logic with existence predicate is presented that satisfies partial cut elimination and Craig’s interpolation property; it is also conjectured that interpolation fails for the implication-free fragment. In this paper an equivalent calculus is introduced that satisfies full cut elimination and allows a direct proof of interpolation via Maehara’s lemma. In this way, it is possible to obtain much simpler interpolants and to better understand and (partly) overcome the failure of interpolation for the implication-free fragment.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster or Giulio Fellin.
The minicourse “Modal logics and intuitionistic logic” (12h) has been videoregistered in August 2020. Members of the University of Verona who wish to follow the course but are not authorised to access this link are kindly asked to contact Giulio Fellin.
Abstract
Modal logics capture concepts of necessity and possibility;
intuitionistic logic models computation and construction. This
minicourse is intended to introduce into both kinds of logic with
particular attention on their interaction, from the angles of syntax
and semantics but with a certain proof-theoretic flavour. One
highlight will be Gödel’s embedding of intuitionistic propositional
logic into the modal logic S4, which stood at the beginning of
provability logic.
The dynamical method in commutative algebra
Ihsen Yengui (Univ. Sfax, Tunisia)
The minicourse “The dynamical method in commutative algebra” (12h) has been videoregistered in August 2020. Members of the University of Verona who wish to follow the course but are not authorised to access this link are kindly asked to contact Giulio Fellin.
Abstract
Transfinite methods, typically in the form of a variant of Zorn’s Lemma, are frequently invoked during proofs in commutative algebra. Dynamical methods have proved practicable to still render constructive proofs of that kind. Roughly speaking, ideal objects such as prime ideals are approximated by paths in finite trees which are grown as the proofs in question demand and carry the information required for the desired computation.
Jacopo Emmenegger (Birmingham) Elementary doctrines as coalgebras (j.w.w. Fabio Pasquali and Pino Rosolini)
Abstract:
Lawvere’s hyperdoctrines mark the beginning of applications of category theory to logic. The connection between (typed) logical theories and certain functors taking values in the category of posets is exemplified by two embeddings: of elementary doctrines into primary ones, and of elementary doctrines with effective quotients into elementary ones. In logical terms these correspond to the inclusion of Λ=-theories into Λ-theories, resp. of Λ=-theories with quotients into Λ=-theories. Each of the two inclusions is part of an adjunction whose right, resp. left, functor adds quotients for equivalence relations. After discussing the above adjunctions and their connection to logic and type theory, I shall present a recent result, obtained with Fabio Pasquali and Pino Rosolini, showing that the first embedding is 2-comonadic. Finally, if time allows, I shall delve into the connections to model theory and discuss how the comonadic adjuntion provides an algebraic description of Shelah’s construction of a theory that eliminates imaginaries from classical model theory.
The talk is based on the paper E., Pasquali, Rosolini. Elementary doctrines as coalgebras. J. Pure Appl. Algebra 224, 2020. doi:10.1016/j.jpaa.2020.106445
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.
COQ introductory mini-course Andrea Masini (Università di Verona)
Program
1) Recalls of natural deduction (classical and intuitionist) and of typed lambda calculus.
2) Examples of simple proofs in Coq (Goal, Assumptions and Tactics).
3) Functional programming in CoQ.
4) Structured data types.
5) Polymorphism and higher order functions.
6) The basic tactics.
7) Logic in CoQ.
8) Induction
Unfortunately, in a course of only 12 hours, even if intensive, it will not be possible to tackle the applications of COQ, which range from the specification and proof of properties of complex computer systems (SW and HW) to the mechanisation of mathematics (continuous and discrete).
Timetable
Wednesday 9 September 2020, at [10.00-13.00]
Thursday 10 September 2020, at [10.00-13.00]
Wednesday 16 September 2020, at [10.00-13.00]
Thursday 17 September 2020, at [10.00-13.00]
The course is open to everyone, the only pre-requisite is to have the basic knowledge of logic.
It is still not clear whether the course will be held in presence or on-line. We’re waiting for precise indications from the doctoral school.
Davide Trotta (Università di Verona) Hilbert ϵ-operator and existence property in categorical logic (j.w.w. M. Zorzi and M.E. Maietti)
Abstract:
In this talk we present some choice principles in the context of categorical logic and their applications in logic. In particular we focus on the existence property, the choice rule and the Hilbert ϵ-operator. We use the language of doctrines and the existential completion to present these principles and their characterization. Then we provide some direct applications in a fragment of intuitionistic logic.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.
!! The seminar was moved to 16:30 !!
Thursday, July 2nd, 2020, 16:30, on Zoom.
Gianluigi Bellin (Università di Verona) Relational sequent calculus for Bi-Intuitionistic Linear Logic (j.w.w. W. Heijltjes)
Abstract: The relational sequent calculus for BILL used in [Bellin & Heijltjes, {Proof nets for
bi-intuitionistic linear logic}, FSCD 2018] is unsound. The problem extends to
Hyland and De Paiva Full Iintuitionistic Linear Logic FILL 1993, but only to the
treatment of the unit ⊥, as shown by an example of failure of interpolation
in the sequent calculus, which yields unsoundness with respect to Hyland and De Paiva’s
categorical semantics. We revise the sequent calculus, sketch the proof of interpolation
and of cut elimination for it.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.
Luca Tranchini (Tübingen) Proof-terms for dual-intuitionistic logic and refutation-terms for intuitionistic logic (j.w.w. Gianluigi Bellin)
Abstract:
In the present paper, we present a term-assignment for the fragment of bi-intuitionistic logic whose only type-forming operation is the dual of intuitionistic implication. Typing judgements have the form x : C ⊢ t1 : A1, ..., tn : An i.e. a set of terms is typed by declaring a single variable (somewhat dualizing the simply typed λ-calculus, where a single term is typed declaring a set of variables). The main distinguishing feature of our term calculus is its distributed nature: whereas in the λμ-calculus all conclusions but one are μ-variables, in our calculus the computational content is distributed among the conclusions, i.e. to each conclusion one assigns a possibly complex term; moreover, reduction is also distributed, in the sense that the reduction acts globally on a set of terms, and not on a single one. The duality between our calculus and the simply typed λ-calculus suggests the possibility to use it not only to encode the dual-intuitionistic notion of provability, but an intuitionistic notion of refutability as well. We spell out this idea by using our terms to decorate Prawitz’s rules of intuitionistic natural deduction from the bottom to the top, thereby expressing a backwards reading of intuitionistic rules: given refutations of the conclusions one computes refutations of the premises.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.
Paolo Maffezioli (University of Barcelona) Intuitionistic mereology (j.w.w. A. Varzi)
Abstract:
Like any formal theory, mereology consists of axioms concerning the propositional connectives and quantifiers (logical axioms) and axioms concerning the parthood relation (proper axioms). Over the years, philosophical reasons have motivated interest in departing from the traditional axiomatization of mereology. Proper axioms such as the principle of strong supplementation or the principle of unrestricted composition have been weakened or rejected altogether and even elementary axioms like the anti-symmetry of parthood or its transitivity are no longer regarded as uncontentious. Logical axioms have been challenged, too. For example, many-valued logic, free logic and plural quantification have long been considered as sensible alternatives to classical first-order logic and, more recently, mereological theories based on paraconsistent logic have also been proposed. The two kinds of revisions are normally seen as independent from each other, but this isn’t always the case. For instance, I will show that developing an intuitionistic mereology by rejecting the law of excluded middle without touching the proper axioms would fails to validate nearly all the compelling principles of extensionality. If, one the other hand, the logical revision (from classical to intuitionistic logic) is accompanied by a suitable revision of the proper axioms, extensionality can be fully recovered. I will also show that change of the proper axioms can easily be made if the traditional mereological primitives are defined in terms of notions that have been investigated in constructive mathematics, mainly (though not exclusively) the notion of apartness (Brouwer, Heyting) and excess (von Plato).
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.
Michele Pra Baldi (University of Cagliari) Extensions of paraconsistent weak Kleene logic (j.w.w. F. Paoli)
Abstract:
Paraconsistent Weak Kleene Logic (PWK) is the 3-valued logic based on the weak Kleene matrices and with two designated values. In this paper, we investigate the poset of prevarieties of generalised involutive bisemilattices, focussing in particular on the order ideal generated by Alg(PWK).
Applying to this poset a general result by Alexej Pynko, we prove that, apart from classical logic, the only proper nontrivial extension of PWK is its maximally structurally incomplete companion: PWKE, Paraconsistent Weak Kleene Logic plus Explosion. We describe its consequence relation via a variable-inclusion criterion and identify its Suszko reduced models.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.
Margherita Zorzi (University of Verona) Compositional theories for embedded programming
Abstract:
Embedded programming style allows to split the syntax in two parts, representing respectively a host language H and a core language C embedded in H. This formally models several situations in which a user writes code in a main language and delegates some tasks to an ad hoc domain specific language. Moreover, as showed in recent years, a particular case of the host-core approach allows a flexible management of data linearity, which is particularly useful in non-classical computational paradigms such as quantum computing.
The definition of a systematised type theory to capture and standardize common properties of embedded languages is partially unexplored. We present a flexible fragment of such a type theory, together with its semantics in terms of enriched categories.
We introduce the calculus HC0 and we use the notion of internal language of a category to relate the language to the class of its models, showing the equivalence between the category of models and the one of theories. This provides a stronger result w.r.t. standard soundness and completeness since it involves not only the models but also morphisms between models. We observe that the definition of the morphisms between models highlights further advantages of the embedded languages and we discuss some concrete instances, extensions and specializations of the syntax and the semantics.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.
Abstract: Mathematical methods always played an important role in the verification of Railway control systems.
In this talk we present two different approaches, the first for discrete systems, the second for hybrid systems. Both were used in our collaboration with Industry.
We start with traditional solid state Railway interlockings, often specified using a graphical language called Ladder Logic. We give a semantics for this language
and show how to get from aladder logic specification to a satisfiability problem. This process has been automated, and several existing Interlocking case studies,
provided by our Industrial partner Siemens Rail Automation, have been verified using automated theorem proving tools.
We further applied our own SAT solver, which we extracted from a formal constructive proof of the completeness of the Davis-Putnam-Logemann-Loveland (DPLL) proof
system. The extracted SAT solver is a verified algorithm, which either yields a model or a DPLL refutation of a given clause set [1].
In the second part, we present our modelling of the European Rail Traffic Management System ERTMS, a state-of-the-art train control system, which aims at improving
the performance/capacity of rail traffic systems, without compromising their safety.
It generalizes from traditional interlockings to a system that includes on-board equipment and communication between trains and interlockings via radio block processors. Whilst
the correctness of discrete interlocking systems is well-researched, it is challenging to verify ERTMS based systems for safety properties such as collision freedom due to the
involvement of continuous data. The modelling and verification is done in Real-Time Maude, a tool that allows for both simulation and verification of real-time and hybrid
systems [2].
[1] U. Berger, A. Lawrence, F. Nordvall Forsberg, M. Seisenberger, Extracting Verified Decision Procedures: DPLL and Resolution, Logical Methods in Computer Science, 2015.
[2] U. Berger, P. James, A. Lawrence, M. Roggenbach, M. Seisenberger, Verification of the European Rail Traffic Management System in Real-Time Maude,
Science of Computer Programming, JSP 2018.
Giulio Fellin (Universities of Verona, Trento and Helsinki) Modal Logic for Induction (j.w.w. Sara Negri and Peter Schuster)
Abstract: We use modal logic to obtain syntactical, proof-theoretic versions of transfinite induction as axioms or rules within an appropriate labelled sequent calculus. While transfinite induction proper, also known as Noetherian induction, can be represented by a rule, the variant in which induction is done up to an arbitrary but fixed level happens to correspond to the Gödel–Löb axiom of provability logic. To verify the practicability of our approach in actual practice, we give a fairly universal pattern for proof transformation and test its use in several cases. Among other things, we give a direct and elementary syntactical proof of the theorem that the Gödel–Löb axiom characterises precisely the well-founded and transitive Kripke frames.
The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster.
The course will take place on March 9-27, 2020. Timetable below.
Category theory and point-free topology
The Compact Course “Category Theory and Point-Free Topology” is primarily
aimed at both undergraduate, graduate and postgraduate students in mathematics
with an interest in the intersection between logic, algebra and
topology. The event will take place at the Department of Computer
Science of the University of Verona, located in Strada le Grazie 15,
Verona (Italy).
Summary
“Point-free topology” is the theory of “locales”. They are a type of
spaces, very similar to topological spaces, except that they might not
have an underlying set of points. Locales that have enough points are
the same as topological spaces, but some locales have no points and are
completely new objects. We will see how many notions and constructions
of ordinary topology carry over to locales. Later in the course I will
talk about the internal logic of categories of sheaves, which provide an
extremely powerful tool to work with locales. I will explain how these
mysterious “spaces without points” are closely connected to ‘forcing’ in
set theory, as well as the strong connection between the the theory of
locales and intuitionistic mathematics. The course will start with a
basic introduction to category theory, including limits and co-limits,
epi and monomorphisms, adjoint functors and adjoint functor theorem,
etc. The theory of locales will give many illustrations and interesting
example of these concepts.
Timetable
Monday, March 9, 13:40-16:10, Aula M.
Wednesday, March 11, 13:40-15:20, Aula G.
Friday, March 13, 13:40-16:10, Sala Riunioni Secondo Piano.
Monday, March 16, 13:40-16:10, Aula M.
Wednesday, March 18, 13:40-15:20, Aula G.
Friday, March 20, 13:40-16:10, Sala Riunioni Secondo Piano.
Monday, March 23, 13:40-16:10, Aula M.
Wednesday, March 25, 13:40-15:20, Aula G.
Friday, March 27, 13:40-16:10, Sala Riunioni Secondo Piano.
Registration
Participation is free. Participants not affiliated at the University of Verona are kindly asked
to register by sending an e-mail to Giulio Fellin no later than 27 February 2020.
Acknowledgements
This compact course is run as part of the “Mathematics Mini-Courses” of the University of Verona,
and within the projects “A New Dawn of Intuitionism: Mathematical and Philosophical Advances” (ID 60842)
of the John Templeton Foundation, and “Reducing complexity in algebra, logic, combinatorics - REDCOM”
belonging to the programme “Ricerca Scientifica di Eccellenza 2018” of the Fondazione Cariverona.
Wednesday, November 27th, 2019, 15:30, Sala riunioni secondo piano.
Davide Trotta (Università degli Studi di Trento) Doctrines in categorical logic and the existential completion
Abstract: The notion of hyperdoctrine was introduced by F.W. Lawvere in a
series of seminal papers to synthesize the structural properties of logical
systems. His crucial intuition was to consider logical languages and theories
as indexed categories and to study their 2-categorical properties. For
instance, connectives and quantifiers are determined by adjunctions. In this
seminar we introduce the notions of primary and existential doctrine, which
generalize that of hyperdoctrine, and we present the existential completion. In
particular we show how we can add left adjoints along certain functors to a
primary doctrine obtaining an existential doctrine. Moreover we show that the
2-monad obtained from this free construction is lax-idempotent, and that the
2-category of existential doctrines is isomorphic to the 2-category of algebras
for this 2-monad. Finally we extend the notion of exact completion of an
elementary existential doctrine to an arbitrary elementary doctrine.
Wednesday, November 27th, 2019, 16:45, Sala riunioni secondo piano.
Branko Nikolić (Macquarie University, Sydney, Australia) On Directed Colimits of Hilbert Spaces
Abstract: We will show that the category of Hilbert spaces and contractions
has directed colimits, and that tensoring preserves them. We will also discuss
(problems with) the generalization to bounded maps.
Roberta Bonacina (Università degli Studi dell’Insubria) A simpler semantics for a large fragment of Homotopy Type Theory
Abstract: The standard homotopical interpretation for homotopy type theory is
deep and useful, but it sounds odd that the full power of higher-order category
theory is needed to describe what is a piece “computable’’ mathematics. We show
that those complex categorical tools are not necessary, by proposing a novel
semantics, based on 1-category theory, for a big fragment of homotopy type
theory which contains the whole Martin-Löf type theory and some higher
inductive types. We also describe some proof theoretic results for this system;
in particular, we prove a normalisation theorem, extending Girard’s
reducibility candidates technique.
Thursday, September 10th, 2019, 16:30, Sala Verde.
Olaf Beyersdorff (Friedrich Schiller University, Jena) Solving and Proof Complexity for SAT and QBF
Abstract: SAT and QBF solvers have become ubiquitous tools for the solution of hard
computational problems from almost all application domains. In this talk we
explain the underlying algorithmic principles of solving, both for
propositional satisfiability (SAT) and for the more complex case of quantified
Boolean formulas (QBF). Particular emphasis will be placed on how these solving
approaches can be modelled proof theoretically and which techniques are
available to evaluate their proof complexity.
Bio: Since 2018 Olaf Beyersdorff is Professor of Theoretical Computer Science
at the Friedrich Schiller University Jena. His research interests are in
algorithms, complexity, computational logic, and in particular proof
complexity. Before coming to Jena he spent six years at the University of
Leeds, as Professor of Computational Logic (2017–18), Associate Professor
(2015–17), and Lecturer (2012–15). Since 2018 he is a visiting professor at the
University of Leeds. Before that he was a visiting professor (2011/12) and
visiting researcher (2009/10) at Sapienza University Rome, Lecturer at Leibniz
University Hanover (2007–12) and postdoc at Humboldt University Berlin
(2006/07). Beyersdorff obtained a PhD from Humboldt University Berlin in 2006
and completed the habilitation at Leibniz University Hanover in 2011.
Michael Rathjen (University of Leeds) Graph Theory and the Transfinite
A bit more than a 100 years ago, as a response to the foundational crisis in
mathematics, Hermann Weyl published his “Das Kontinuum” in which he tried to
rebuild mathematics from a stance that assumes the existence of the set of
natural numbers as an actual completed infinity but no higher infinities. Much
later in the 1970s, logicians began to systematically scour various chunks of
ordinary mathematics to determine the existential commitments to the infinite
that they required. This is known as “Reverse Mathematics”. To put it roughly,
it turned out that most of “ordinary” mathematics didn’t need more than what
Weyl had assumed. However, there are some notable exceptions. In particular
graph theory sports some very nice theorems that require more of the
transfinite. The talk will discuss some famous theorems and their relationships
with the infinite world.
Wednesday, 3. April 2019, 10:30, Sala Riunioni (2nd floor).
Satoru Niki (Japan Advanced Institute of Science and Technology) Empirical Negation and Beth Semantics
The negation in intuitionistic logic has a ‘future-oriented’ character, as
elucidated by the valuation in Kripke models. Its application in mathematical
contexts has been validated by the success of constructive mathematics. Its
applicability in non-mathematical contexts, in contrast, is argued to have some
problems. The existence of a different, ‘empirical’ notion of negation within
the framework of intuitionistic logic has been discussed by Heyting, Dummett
and others. De (2013) proposed empirical negation as falsity at the bottom root
of a Kripke model, and De and Omori (2014) gave the axiomatisation of this
logic.
In this talk, I will discuss how the choice of semantics in formulating
empirical negation affects the logic one obtains, with Beth semantics as a
particular example. This is followed by an examination of arithmetic with
empirical negation.
Proof interpretations: A modern perspective Thomas Powell (Technische Universität Darmstadt)
The aim of this course is to provide an introduction to proof
interpretations and program extraction, up to the point where some of
their applications in modern mathematics and computer science can be
understood. I begin in the first lecture with a broad historical overview,
tracing the origins of Gödel’s functional interpretation in Hilbert’s
program and the early days of proof theory. The second and third lectures
comprise an introduction to the extraction of computational content from
proofs, both in the intuitionistic and classical setting. I conclude with
a high level overview of the proof mining program, and present some recent
applications of program extraction in functional analysis.
Fri 15 Mar 14:30-16:30
Mon 18 Mar 09:30-12:30
Tue 19 Mar 15:30-18:30
Wed 20 Mar 09:30-12:30
A new application of proof mining in the fixed point theory of uniformly convex Banach spaces
Proof mining is a branch of proof theory which makes use of
proof theoretic techniques to extract quantitative information from
seemingly nonconstructive proofs. In this talk, I present a new
application of proof mining in functional analysis, which focuses on the
convergence of Picard iterates for generalisations of nonexpansive
mappings in uniformly convex Banach spaces.
Venue:
Dipartimento di Informatica, Università di Verona
37134 Verona, Strada Le Grazie 15,
Cà Vignal 2, 2nd floor, sala riunioni
Given first order theories S,T and a functor F:Mod(S) –>Mod(T) between their categories of models, one can ask whether objects in the range of F satisfy first-order sentences other than those of T, and whether the essential image of F is an elementary class. Under certain conditions on F we can give criteria for this for so-called k-geometric first-order sentences and k-geometric elementary classes.
These criteria are obtained by considering classifying toposes associated to S and T, such that F is induced by a geometric morphism between them, and then factorizing this geometric morphism appropriately. The involved notions will be explained and examples will be given.
Dávid Natingga (University of Leeds)
Introduction to α-Computability Theory
An ordinal α is admissible iff the α-th level Lα of Gödel’s constructible hierarchy satisfies the axioms of Kripke-Platek set theory (roughly predicative part of ZFC).
α-computability theory is the study of the first-order definability theory over Gödel’s Lα for an admissible ordinal α.
Equivalently, α-computability theory studies the computability on a Turing machine with a transfinite tape and time of an order type α for an admissible ordinal α.
The field of α-computability theory is the source of deep connections between computability theory, set theory, model theory, definability theory and other areas of mathematics.
Margherita Zorzi (Università di Verona) A logic for quantum register measurements
(joint work with Andrea Masini)
We know that quantum logics are the most prominent logical systems associated to the lattices of closed Hilbert subspaces. But what happens if, following a quantum computing perspective, we want to associate a logic to the process of quantum registers measurements? This paper gives an answer to that question, and, quite surprisingly, shows that such a logic is nothing else but the standard propositional intuitionistic logic.
16:45
Ingo Blechschmidt (Università di Verona) New reduction techniques in commutative algebra driven by logical methods
We present a new reduction technique which proposes the following trade-off: If we agree to restrict to constructive reasoning, then we may assume without loss of generality that a given reduced ring is Noetherian and in fact a field, thereby reducing to one of the easiest situations in commutative algebra.
This technique is implemented by constructing a suitable sheaf model and cannot be mimicked by classical reduction techniques. It has applications both in constructive algebra, for mining classical proofs for constructive content, and in classical algebra, where it has been used to substantially simplify the 50-year-old proof of Grothendieck’s generic freeness lemma.
Workshop
Friday, October 6th
Sala riunioni (2° piano)
Department of Computer Science
09:30 Thomas Streicher - An Effective Version of the Spectral Theorem
10:20 Hajime Ishihara - The Hahn-Banach theorem, constructively revisited
11:10 Coffee break
11:50 Ihsen Yengui - Algorithms for computing syzygies over V[X1,…,Xn], V a valuation ring 12:40 Takako Nemoto - Finite sets and infinite sets in weak intuitionistic arithmetic
13:30 Lunch break
15:30 Fabio Pasquali - Choice principles and the tripos-to-topos construction
16:40 Chuangjie Xu - Unifying (Herbrand) functional interpretations of (nonstandard) arithmetic
We review known constructive versions, such as the separation theorem and continuous extension theorem, of the Hahn-Banach theorem and their proofs, and consider new versions including the dominated extension theorem and their proofs.
Takako NemotoFinite sets and infinite sets in weak intuitionistic arithmetic
We consider, for a set A of natural numbers, the following notions of finiteness
FIN1: There are k and m0,…,mk-1 such that A={m0,…,mk-1} ;
FIN2: There is an upper bound for A;
FIN3: There is m such that for all B ⊆ A (|B|<m);
FIN4: It is not the case that, for all x, there is y such that y∈ A;
FIN5: It is not the case that, for all m, there is B ⊆ A such that |B|=m,
and infiniteness
INF1: There are no k and m0,…,mk-1 such that A={m0,…,mk-1};
INF2: There is no upper bound for A;
INF3: There is no m such that for all B ⊆ A (|B|<m);
INF4: For all y, there is x>y such that x∈ A;
INF5: For all m, there is B ⊆ A such that |B|=m.
We systematically compare them in the method of constructive reverse mathematics. We show that the equivalence among them can be characterized by various combinations of induction axioms and non-constructive principles, including the axiom called bounded comprehension.
Fabio PasqualiChoice principles and the tripos-to-topos construction
In this talk we study the connections between choice principles expressed in categorical logic and the Tripos-to-Topos construction [HJP80].
This is a joint work with M. E. Maietti and G. Rosolini based on [MPR, MR16, Pas17].
[HJP80] J.M.E. Hyland, P.T. Johnstone and A.M. Pitts. Tripos Theory. Math. Proc. Camb. Phil. Soc., 88:205-232, 1980.
[MR16] M.E. Maietti and G. Rosolini. Relating quotient completions via categorical logic. In Dieter Probst and Peter Schuster (eds), editors, Concepts of Proof in Mathematics, Philosophy and Computer Science, pages 229 - 250. De Gruyter, 2016.
[Pas17] F. Pasquali. Hilbert’s epsilon-operator in Doctrines. IfCoLog Journal of Logics and their Applications. Vol 4, Num 2: 381-400, 2017
[MPR] M.E. Maietti, F. Pasquali and G. Rosolini. Triposes, exact completions and Hilbert’s epsilon operator. In preparation.
Chuangjie XuUnifying (Herbrand) functional interpretations of (nonstandard) arithmetic
We extend Oliva’s method [3] to obtain a parametrised functional interpretation for nonstandard arithmetic. By instantiating the parametrised relations, we obtain the Herbrand functional interpretations introduced in [2,4] for nonstandard arithmetic as well as the usual, well-known ones for Berger’s uniform Heyting arithmetic [1].
[1] U. Berger, Uniform Heyting arithmetic, Annals of Pure and Applied Logic 133 (2005), no. 1, 125-148.
[2] F. Ferreira and J. Gaspar, Nonstandardness and the bounded functional interpretation, Annals of
Pure and Applied Logic 166 (2015), no. 6, 701-712.
[3] P. Oliva, Unifying functional interpretations, Notre Dame J. Formal Logic 47 (2006), no. 2, 263-290.
[4] B. van den Berg, E. Briseid, and P. Safarik, A functional interpretation for nonstandard arithmetic, Annals of Pure and Applied Logic 163 (2012), no. 12, 1962-1994.
Organised by Peter Schuster and Daniel Wessel.
Please note further that on Thursday, October 5th, 4pm,
there will be a departmental seminar with Olivia Caramello:
The proof-theoretic relevance of Grothendieck topologies
Lorenzo Rossi (Paris Lodron University of Salzburg)
A unified approach to truth and implication
The truth predicate is commonly thought to be symmetric, at least in the sense that for every sentence A, A and “A is true” should be inter-substitutable salva veritate. In this paper, we study an object-linguistic predicate for implication obeying similar symmetry requirements. While several non-classical logics are compatible with symmetric truth, theories of symmetric implication can only be formulated in a small class of substructural logics. We present an axiomatic theory of symmetric implication and truth over Peano Arithmetic, called SyIT, formulated in a non-reflexive logic, and we study its semantics and proof-theory. First, we show that SyIT axiomatizes a class of fixed-point models that generalize Saul Kripke’s (1975) fixed points for symmetric truth. Second, we compare SyIT with the theory PKF_ _(Halbach and Horsten 2006), an axiomatization of Kripke’s fixed points for truth in strong Kleene logic, and we show that SyIT and PKF are proof-theoretically equivalent. The latter result shows that going substructural and adding a symmetric implication predicate to a theory of symmetric truth comes at no proof-theoretical costs.
