FOM: Infinity

[JoeShipman@aol.com]

Ferreira:
<<ACA_0 is a well-known conservative extension of PA, and it is finitely axiomatizable. It has two sorts of variables, but it can be reformulated with only one sort of variables (at the cost of introducing new predicates).>>

The problem is that this finite axiomatization is extremely complicated, at least as it is done in Simpson's book "Subsystems of Second-Order Arithmetic".  You need to use a "universal lightface pi^0_1 formula", whose complexity is comparable to that of a Universal Turing machine.  I want a finitely axiomatizable system that you can actually write down, where the axioms are intuitively understandable, which conservatively extends PA or Finite Set Theory.

The system of Godel-Bernays conservatively extends ZFC and the axioms are easy to write down and intuitively understandable, though not at all elegant.  What happens if we take GB and omit the axiom of infinity for sets, or replace it with its negation?  Will this give a finitely axiomatized system that proves the same theorems about integers that PA does?  (Using the standard formalization of integers as finite ordinals.)

-- Joe Shipman