The website of the Logic Seminar Verona has moved. For the time being, this website will keep existing, but it won’t be updated anymore.
The new address is: https://logicverona.it/
Departmental Seminar
Wednesday, 10. April 2019, 15:00, Aula M.
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.
Seminar
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.
Compact Course & Research Seminar
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
___
The lecture on Wednesday will comprise a research seminar:
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
For further information, please see the course webpage.
Seminar
Monday, 11 February 2019, Sala Verde.
Both talks have been recorded.
___
15:30
Takako Nemoto (Japan Advanced Institute of Science and Technology)
Systems for constructive reverse mathematics
abstract
___
17:00
Peter Arndt (Heinrich-Heine-Universität Düsseldorf)
Ranges of functors and elementary classes via topos theory
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.
Seminar
Thursday, 31 January 2018, 15:30, Sala Verde.
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.
Seminar
Monday, 3 Dec 2018, Sala Verde.
___
15:00
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
Programme and abstracts can be found here.
Workshop
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
Abstracts:
Hajime Ishihara
The Hahn-Banach theorem, constructively revisited
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 Nemoto
Finite 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 Pasquali
Choice 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 Xu
Unifying (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
Past events
11. May 2017
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.
(Joint work with Carlo Nicolai, LMU Munich)
8. May 2017
Categories, Constructions, Sets and Types
Minisymposium
LOGIC SEMINAR VERONA 