Polynomial time ultrapowers and the consistency of circuit lower bounds

polynomial time ultrapower is a structure given by the set of polynomial time computable functions modulo some ultrafilter. They model the universal theory ∀𝖯𝖵 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 ∀𝖯𝖵 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 ∀𝖯𝖵 we show that ∀𝖯𝖵 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 ).