A globaliser of a c.e. first-order theory T is a c.e. theory U such that U is locally interpretable in T and any c.e. theory V locally interpretable in T is globally interpretable in U. From standard results about reflexive theories (e.g. PA, ZF, ZFC) it follows that any reflexive theory is its own globaliser. In recent years Albert Visser proved that Robinson's arithmetic R is its own globaliser. And that there is a globaliser for any sequential c.e. theory T. In the present talk I would give two proofs of a new result that for any c.e. theory T there is a globaliser. The talk is based on two papers in preparation. One is joint with Albert Visser and the other is joint with Yong Cheng.
Logic seminar
usually takes place each Monday at 13:30 temporarily on Zoom starting at 15:30, normally 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.
Feasible disjunction property and k-DNF resolution
Michal Garlík
Polytechnic University of Catalonia
Monday, 29. June 2020 - 15:15 to 16:45
We discuss feasible disjunction property and reflection principles for propositional proof systems. For every integer $k \geq 2$, we show that $k$-DNF resolution does not have the feasible disjunction property. This contrasts with the case $k = 1$ (the usual resolution). Time permitting, we look at some consequences.
Consistency of Nondeterministic Circuit Upper Bounds
Ján Pich
University of Oxford
Monday, 15. June 2020 - 13:30 to 15:00
We show unconditionally that Jeřábek's theory of approximate counting APC_1 formalizing probabilistic poly-time reasoning cannot prove, for any non-deterministic poly-time machine M, that M is inapproximable by co-nondeterministic circuits of sub-exponential size. We also show several related results concerning worst-case and zero-error average case lower bounds for various versions of the Minimum Circuit Size Problem against co-nondeterministic circuits.
This is joint work with Rahul Santhanam.
The logical strength of Büchi's decidability theorem
Leszek Kolodziejczyk
University of Warsaw
Monday, 25. May 2020 - 13:30 to 15:00
I will talk about a result obtained a few years ago jointly with Henryk Michalewski, Pierre Pradic and Michał Skrzypczak. Our aim was to describe the strength of axioms needed to prove Büchi's theorem, which says that the monadic second order theory of the natural number order is decidable.
The axiomatic requirements of theorems involving second-order quantification over the naturals, like Büchi's theorem, are commonly studied within a research programme known as reverse mathematics, and often characterized in terms of an equivalence between the theorem and some fragment of so-called second order arithmetic. I plan to give a (brief) introduction to second order arithmetic and to monadic second order logic. Then I will discuss our main result, which says that Büchi's theorem (suitably formulated) is, over the usual base theory considered in reverse mathematics, equivalent to the induction scheme for Sigma^0_2 formulas. Various automata-theoretic statements related to Büchi... more
The axiomatic requirements of theorems involving second-order quantification over the naturals, like Büchi's theorem, are commonly studied within a research programme known as reverse mathematics, and often characterized in terms of an equivalence between the theorem and some fragment of so-called second order arithmetic. I plan to give a (brief) introduction to second order arithmetic and to monadic second order logic. Then I will discuss our main result, which says that Büchi's theorem (suitably formulated) is, over the usual base theory considered in reverse mathematics, equivalent to the induction scheme for Sigma^0_2 formulas. Various automata-theoretic statements related to Büchi... more