Abstract

An open formalism for arithmetic is presented based on first-order logic supplemented by a very strictly controlled constructive form of the omega-rule. This formalism (which contains Peano Arithmetic) is proved (nonconstructively, of course) to be complete. Besides this main formalism, two other complete open formalisms are presented, in which the only inference rule is modus ponens. Any closure of any theorem of the main formalism is a theorem of each of these other two. This fact is proved constructively for the stronger of them and nonconstructively for the weaker one. There is, though, an interesting counterpart: the consistency of the weaker formalism can be proved finitarily