A translation characterizing the constructive content of classical theories

Abstract

A simple syntactical translation of theories and of existential formulas-C∀ and C∃, respectively-is described for which the following holds: For any classical theory T and all formulas A(x), T⊩ A(t) for some term t ⇔ C∀ (T)⇔ C∃ (∃xA(x)). In other words, C∀(T) proves exactly those formulas C∃ (∃xA(x)) for which T can prove ∃xA(x) constructively and thus circumscribes the constructive fragment of T. The proof of the theorem is based on properties of the resolution calculus; which allows to extract a primitive recursive bound on the size of the witness term t, with respect to the size of a proof of C∀(T) ⇔ C∃( ∃xA(x)). In fact, a generalization of the above statement, that takes into account a designation of certain function symbols as 'constructor symbols' is proved. Different types of examples are provided: Some formalize well known non-constructive arguments from mathematics, others illustrate the use of the theorem for characterizing classes of classical theories that are constructive with respect to certain types of existential formulas.