Polynomial time ultrapowers and the consistency of circuit lower bounds

• Published in: Archive for mathematical logic 2020-02, Vol.59 (1-2), p.127-147
• Main Authors: Bydžovský, Jan, Müller, Moritz
• Format: Article
• Language: English
• Subjects: Algebra; Circuits; Informàtica; Informàtica teòrica; Lower bounds; Mathematical analysis; Mathematical Logic and Foundations; Mathematics; Mathematics and Statistics; Original Study; Polinomis; Polynomials; Production scheduling; Substructures; Time functions; Àrees temàtiques de la UPC
• ISSN: 0933-5846; 1432-0665
• DOI: 10.1007/s00153-019-00681-y

A polynomial time ultrapower is a structure given by the set of polynomial time computable functions modulo some ultrafilter. They model the universal theory ∀ PV of all polynomial time functions. Generalizing a theorem of Hirschfeld (Israel J Math 20(2):111–126, 1975 ), we show that every countable model of ∀ PV is isomorphic to an existentially closed substructure of a polynomial time ultrapower. Moreover, one can take a substructure of a special form, namely a limit polynomial time ultrapower in the classical sense of Keisler (in: Bergelson, V., Blass, A., Di Nasso, M., Jin, R. (eds.) Ultrafilters across mathematics, contemporary mathematics vol 530, pp 163–179. AMS, New York, 1963 ). Using a polynomial time ultrapower over a nonstandard Herbrand saturated model of  ∀ PV we show that ∀ PV is consistent with a formal statement of a polynomial size circuit lower bound for a polynomial time computable function. This improves upon a recent result of Krajíček and Oliveira (Logical methods in computer science 13 (1:4), 2017 ).