Nonstandard combinatorial ultrafilters and a new local witness model

Johannes Heil, Moritz Müller

A central object in the theory of proof complexity generators is Krajicek's local witness model. We construct a new such model as a definable ultrapower using a definable version o…