Let K be an arbitrary Kripke model of Heyting Arithmetic, HA. For every node k in K, we can view the classical structure of k, m_k, as a model of some classical theory of arithmetic. Let T be a classical theory in the language of arithmetic. We say K is locally T, iff for every k in K, m_k models T. A well-studied question in the model theory of HA is the following question: Is every Kripke model of HA locally PA? We answer this question negatively by constructing a Kripke model of HA which is not locally B\Sigma_1.
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.
Not all Kripke models of HA are locally PA
Erfan Khaniki
IM CAS
Monday, 12. October 2020 - 16:00 to 17:30
Globalisers
Fedor Pakhomov
Institute of Mathematics
Monday, 13. July 2020 - 13:30 to 15:00
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.
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.