A Translation Characterizing the Constructive Content of Classical Theories

摘要

A simple syntactical translation of theories and of existential formulas ―C~(any) and C~("exist"), 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~(any) (T) |- C~("exist") ("exist" xA(x)). In other words, C~any (T) proves exactly those formulas C~("exist")("exist"xA(x)) for which T can prove "exist"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~(any)(T) |- C~("exist")("exist"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.