slideshow 3

Logic seminar

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

Feasible set theory, part 2

Neil Thapen
Institute of Mathematics
Monday, 14. December 2015 - 13:30 to 15:00
The Cobham recursive set functions (CRSF) generalize the polynomial time functions to arbitrary sets. We define a weak fragment of Kripke-Platek set theory analogous to Buss's S^1_2 and prove, with some caveats, that the CRSF functions are exactly the provably recursive functions of this theory. Joint work with Arnold Beckmann, Sam Buss, Sy Friedman and Moritz Mueller.

Feasible set theory

Neil Thapen
Institute of Mathematics
Monday, 7. December 2015 - 13:30 to 15:00
The Cobham recursive set functions (CRSF) generalize the polynomial time functions to arbitrary sets. We define a weak fragment of Kripke-Platek set theory analogous to Buss's S^1_2 and prove, with some caveats, that the CRSF functions are exactly the provably recursive functions of this theory. Joint work with Arnold Beckmann, Sam Buss, Sy Friedman and Moritz Mueller.

Proof complexity of intuitionistic implicational formulas, Part 2

Emil Jeřábek
Institute of Mathematics
Monday, 30. November 2015 - 13:30 to 15:00
We study implicational formulas in the context of proof complexity of intuitionistic logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions. In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrubes [1], generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jerabek [2], can be realized by implicational tautologies. [1] P. Hrubes, A lower bound for... more

Proof complexity of intuitionistic implicational formulas

Emil Jeřábek
Institute of Mathematics
Monday, 23. November 2015 - 13:30 to 15:00
We study implicational formulas in the context of proof complexity of intuitionistic logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions. In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrubes [1], generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jerabek [2], can be realized by implicational tautologies. [1] P. Hrubes, A lower bound for... more

Pages