Abstract: This article articulates and assesses a Fine-inspired approach to the foundations of mathematics. After Fine, we call the program `procedural postulationism’. The core idea for the program is that mathematical domains of interest can fruitfully be viewed as the outputs of construction procedures. Fine argues that this viewpoint has various potential epistemic and ontological benefits in philosophy of mathematics; and in any case we think the guiding idea is interesting enough to warrant close inspection.
To this date little formal flesh has been put on the program’s conceptual bones, at least in the published literature. This article seeks to remedy that deficit. We offer a logic for `creative’ imperatives — imperatives that command the introduction of new objects into the domain — and show how to treat the concept of indefinite iteration in that logic.
We then give consistency proofs for arithmetic and set theory starting from the formalized hypothesis that certain commands statable in the resulting logic are executable.
We also *begin* an assessment of Fine’s philosophical goals for the program in light of our formal framework.