A foundational delineation of poly-time (Q1327386)

It is shown that a function is computable in polynomial time if and only if it is computed by an equational program which can be proved to be everywhere converging in constructive second-order logic with set- existence restricted to positive quantifier-free formulas, or alternatively, with set-existence for positive existential formulas. These set-existence principles convey an ontology of infinite sets as evolving, not completed, totalities. These characterization results can be viewed as a foundational justification for identifying polynomial time with feasibility.