slideshow 3

Logic seminar

usually takes place each Monday at 16:00 in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

Variations of the Arithmetized Completeness Theorem

Tin Lok Wong
University of Vienna
Monday, 16. February 2015 - 13:30
The Arithmetized Completeness Theorem is a formalization of Goedel's Completeness Theorem within arithmetic. It is one of the most powerful tools in constructing end extensions of models of arithmetic. In this talk, I will present some non-standard applications about expansions and omega-submodels that satisfy the Weak Koenig Lemma. I will discuss, in particular, the problems one has to face when, instead of Sigma1-induction, we only have Sigma1-collection with exponentiation. This research is joint with Ali Enayat in Gothenburg.

Elementary cut-elimination for prenex cuts in disjunction free LJ

Matthias Baaz
Vienna University of Technology
Wednesday, 11. February 2015 - 13:30
The elimination of cuts (lemmas) from given sequent calculus proofs has remained in the focus of proof theory ever since Gentzen's seminal paper from 1934/35. It is well known that the worst case complexity of cut-elimination is non-elementary for first-order intuitionistic as well as classical logic. No elementary upper bound for cut-elimination seems to be known for non-trivial genuine first-order fragments of intuitionistic logics. The purpose of this paper is to show that one can in fact eliminate cuts involving only prenex cut-formulas from disjunction-free intuitionistic sequent proofs without non-elementary increase in the size of proofs. The result is sharp in several respects. As we will show, in all of the following cases there exist non-elementary lower bounds for cut-elimination: (1) classical disjunction-free proofs with quantified atomic cuts (2) intuitionistic disjunction-free proofs with infix cuts, (3) intuitionistic proofs with prenex cuts in the presence of... more

On the complexity of Friedman's Free-set Theorem and Thin-set Theorem

Marcello Stanisci
Sapienza University of Rome
Monday, 12. January 2015 - 13:30
Free-set Theorem (FST) and Thin-set Theorem (TST), both belonging to the second-order family, have been introduced by H. Friedman in a work called Boolean Relation Theory, that is aimed to find independence results under strong systems of Set Theory. This talk exposes two principles, called LTST and FFST, that are first-order adaptions of FST and TST. In particular, we will see some independence results of LTST and a linear lower bound for FFST. Before presenting the main results, there will be an overview of some known facts that motivated such a research of unprovability, as well as a comparison between FST, TST and the classical Ramsey's Theorem.