Speed-up by theories with infinite models

We prove that if S is a finite set of schemata and A is a sentence undecided by S such that S U {-,A} has an infinite model then S U (A) is an unbounded speed-up of S for substitution instances of tautologies. As a corollary, we obtain a conjecture of Parikh's. I. Let P be any of the usual (schematic) formulations of predicate logic with equality, relation and function symbols, and individual constants and let S be a finite set of schemata; by 'S g A' we mean that there is a P-derivation of A from (substitution instances of members of) S with , I and V; for the proof it will be convenient to distinguish relation constants from relation parameters, the latter being the arguments of substitutions. Let S and A be fixed as above; if C is a propositional formula, built up from propositional variables, -> and I, a code F of C is any formula A -> B where B is obtained from C by a 1-1 substitution of equations u, = vi for propositional variables pi such that all the ui and v, are distinct. Note that if F is a code of C then; S t F.,#>. C is a tautology (this only requires that S U { --A} has a > 2 element model), and S u {A } ) F. Consequently, it suffices to prove the following: There is no number m such that if -A -> B is the code of a tautology then S U { -A)}' B. We shall prove the following bounded speed-up result: There is a functionf such that