Let $A$ be a structure with domain the natural numbers. Consider the following properties:
— for each positive integer $n$, the set of $Pi^1_n$-sentences true in $A$ is $Pi^1_n$-complete;
— for each positive integer $n$, if a set of natural numbers is $Pi^1_n$-definable in the standard model of Peano arithmetic and closed under automorphisms of $A$, then it is $Pi^1_n$-definable in $A$.
Intuitively, they mimic two well-known descriptions of the analytical hierarchy, one in terms of many-one reducibility and one in terms of second-order definability. I develop an approach to proving that certain structures (which are much weaker than the standard model of Peano arithmetic from the viewpoint of first-order logic) have one or both of these properties. E.g. any $A$ in which the divisibility relation is first-order definable has both properties. The same holds for some other interesting structures, including the standard model of Presburger arithmetic, the natural... more
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 two interesting properties in monadic second-order arithmetic
Stanislav O. Speranski
Sobolev Institute of Mathematics
Monday, 13. July 2015 - 13:30
Disjoint NP pairs and propositional proof systems
Amir Tabatabai
Charles University
Monday, 15. June 2015 - 13:30
We continue presenting some results relevant to feasible completeness. This week, the 2003 paper "Disjoint NP-Pairs" by Glasser, Selman, Sengupta and Zhang.
In this talk, we will concentrate on the problem of the existence of an optimal proof system. The goal is to show that in a relativized version we could find an oracle relative to which optimal proof systems do not exist. To achieve this goal, we need two major steps. First, we will define the canonical NP pair of a propositional proof system and show that any disjoint NP pair is equivalent to one of them. Moreover, if a propositional proof system is complete then its canonical disjoint NP pair should be complete, as well. Secondly, by constructing an oracle we will show that there is not any complete disjoint NP pair relative to that oracle and this is the relativized version which we need.
Bounded Kripke Platek Set Theory
Arnold Beckmann
Swansea University
Monday, 8. June 2015 - 13:30
Recently, various restrictions of the primitive recursive set functions have been proposed with the aim to capture feasible computation on sets. Amongst these are the "Safe Recursive Set Functions" (Beckmann, Buss, Friedman, accepted for publication in JSL) the "Predicatively Computable Set Functions" (Arai, Archive for Mathematical Logic, vol. 54 (2015), pp. 471–485) and the "Cobham Recursive Set Functions" (Beckmann, Buss, Friedman, Müller, Thapen, in progress).
In this talk, I will identify "bounded" versions of Kripke-Platek set theory inspired by Buss' Bounded Arithmetic, which have the potential to capture some of the above classes as their Sigma-1-definable set functions. I will comment on adding definable symbols to these theories, along the lines of the first chapter of Barwise's book "Admissible Sets and Structures". The main part of my talk will be to sketch a proof that the Sigma-1 definable functions of some bounded Kripke-Platek set theory are exactly the Safe... more
Propositional proof systems, the consistency of first order theories and the complexity of computations
Raheleh Jalali
Charles University
Friday, 5. June 2015 - 13:30
The seminar next week will be on *Friday* (replacing the complexity seminar).
We plan to use the seminar to go through some old papers relevant to the research project on feasible incompleteness. To start off, Raheleh Jalali will present this paper by Jan Krajicek and Pavel Pudlak, with abstract:
We consider the problem about the length of proofs of the sentences Con_S(n) saying that there is no proof of contradiction in S whose length is <= n. We show the relation of this problem to some problems about propositional proof systems.