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.
Logic seminar
usually takes place each Monday at 16:00 in IM, rear building, ground floorChair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.
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
Recursive functions meet existentially closed structures, Part 2
Emil Jerabek
ASCR
Monday, 15. December 2014 - 13:30
Robinson's theory R, which axiomatizes the true Sigma_1 sentences, is one of the weakest known essentially undecidable theories. It also has an interesting structural characterization due to Visser, being the strongest locally finite r.e. theory with respect to interpretation. The essential undecidability of R is a consequence of the fact that it can represent all recursive functions, and it is a natural question whether the converse also holds: i.e., does every r.e. theory that represents all (partial) recursive functions interpret R?
The answer is negative, and more generally, R is not interpretable in any consistent theory axiomatized by existential sentences. The explanation comes from model theory. Generalizing the theory of random relational structures (graphs), we will show that for an arbitrary language L (even with functions), the empty L-theory has a model completion EC_L: i.e., EC_L has quantifier elimination, and every L-structure extends to a model of EC_L, so that... more
Recursive functions meet existentially closed structures
Emil Jerabek
ASCR
Monday, 8. December 2014 - 13:30
Robinson's theory R, which axiomatizes the true Sigma_1 sentences, is one of the weakest known essentially undecidable theories. It also has an interesting structural characterization due to Visser, being the strongest locally finite r.e. theory with respect to interpretation. The essential undecidability of R is a consequence of the fact that it can represent all recursive functions, and it is a natural question whether the converse also holds: i.e., does every r.e. theory that represents all (partial) recursive functions interpret R?
The answer is negative, and more generally, R is not interpretable in any consistent theory axiomatized by existential sentences. The explanation comes from model theory. Generalizing the theory of random relational structures (graphs), we will show that for an arbitrary language L (even with functions), the empty L-theory has a model completion EC_L: i.e., EC_L has quantifier elimination, and every L-structure extends to a model of EC_L, so that... more
On the Parameterized Complexity of Equational Logic
Mateus de Oliveira Oliveira
Institute of Mathematics ASCR
Monday, 1. December 2014 - 13:30
In this work we study the validity problem in equational logic under the perspective of parameterized complexity theory. First we introduce a variant of equational logic in which sentences are pairs of the form $(t_1=t_2,omega)$ where $omega$ is an arbitrary ordering of the positions corresponding to subterms of $t_1$ and $t_2$. We call such pairs {em ordered equations}. To each ordered equation one may naturally associate a notion of width and to each proof of validity of an ordered equation one may naturally associate a notion of depth. We define the width of such a proof to be the maximum width of an ordered equation occurring in it. Finally, we introduce a parameter $b$ which restricts the way in which variables are substituted for terms. We say that a proof is $b$-bounded if all substitutions used in it satisfy such restriction.
In a surprising result, we show that one may determine whether an ordered equation $(t_1=t_2,omega)$ has a $b$-bounded proof of width $c$ and depth $d$... more