potential vs actual

[Mikhail Katz]

Dear FoMers,

I have a question about the potential/actual distinction that is only
tangentially related to the parallel thread that has been discussed
recently.  Let's define a potentialist as somebody whose universe of
discourse satisfies an axiomatic system that does not prove the
existence of an infinite set.  Thus a potentialist could be working
with Peano Axioms, for example.  There are well-known results that
require the existence of infinite objects and therefore are not
accessible to the potentialist, such as Goodstein's theorem, which can
be proved by the actualist.

My question is, how far can the potentialist actually go in
developing, for example, the calculus, and particularly infinitesimal
calculus?

Some relevant publications include

[1] Parikh, Rohit.  Existence and feasibility in arithmetic.
J. Symbolic Logic 36 (1971), 494-508.

[2] Carbone, A.  Cycling in proofs and feasibility.  Trans. Amer.
Math. Soc.  352 (2000), no. 5, 2049-2075.

[3] Friedman, Harvey.  A strong conservative extension of Peano
arithmetic.  The Kleene Symposium (Proc. Sympos., Univ. Wisconsin,
Madison, Wis., 1978), pp. 113-122, Stud. Logic Foundations Math., 101,
North-Holland, Amsterdam-New York, 1980.

The approach taken in [1] and [2] is to guarantee the consistency of
arguments with a "feasible" predicate by means of suitable bounds on
lengths of proofs.  [3] is billed as an improvement on earlier work by
Feferman and Takeuti.

Looking through [3] I notice that the system ALPO developed here,
while conservative over PA, includes the axiom of infinity (see page
115 there).  The background logic seems to be intuitionistic.  The
system is billed as formalizing Lebesgue integration but I haven't
found too many details.

Part of my interest in this question is historical.  Leibniz adhered
to the part-whole priniple in his work which in particular denied the
existence of (Dedekind-) infinite sets, or what he described as
"infinite wholes".  The question then is to what extent his calculus
can be formalized in an axiomatic system that would adhere to this
principle.

Mikhail Katz