Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Feasible constructivism

Paul Gorbow, Øystein Linnebo

TL;DR

The paper addresses the worry that Dummett's intuitionistic program might prove too much by forcing strict finitism. It proposes feasibilism, a middle-ground where feasibility is captured by polynomial-time computability, and formalizes it in a first-order theory $\\ extsf{FA}$ built on Buss's $S^1_2$ with bounded quantifiers and a tailored induction schema. It then establishes a tight link between feasibility and provability: provably total $\Sigma^b_1$-definable functions coincide with polynomial-time computable functions, and a realizability semantics ensures feasible construction and verification for $\Sigma^b_1$ truths, all while preserving inference feasibly. The framework, grounded in Cobham's thesis, yields a coherent sub-intuitionistic account that aligns mathematical meaning with practical computability and offers a robust alternative to strict finitism and unbounded intuitionism. This provides a principled, computationally anchored approach to constructive mathematics with potential broad implications for logic and foundations.

Abstract

Dummett's argument for intuitionism is well known. There is a concern that the argument proves too much, specifically, that it supports the extreme and apparently incoherent position of strict finitism. The central question is how to explicate the notion that it is possible in practice to construct an arithmetical term or verify a statement. The strict finitist answer is plagued by the sorites paradox. We propose and develop feasibilism as a more plausible view, where computational feasibility, as captured by the class of polynomial-time problems, yields a robust and expedient explication of "possible in practice". In this approach, the complexity is bounded by a polynomial function of the input size, rather than bounded by a constant (as in strict finitism), thus resolving the sorites issues. We show that a system of strictly bounded arithmetic, introduced by Sam Buss, precisely formalizes the feasibilist view so as to satisfy Dummett's requirements.

Feasible constructivism

TL;DR

The paper addresses the worry that Dummett's intuitionistic program might prove too much by forcing strict finitism. It proposes feasibilism, a middle-ground where feasibility is captured by polynomial-time computability, and formalizes it in a first-order theory built on Buss's with bounded quantifiers and a tailored induction schema. It then establishes a tight link between feasibility and provability: provably total -definable functions coincide with polynomial-time computable functions, and a realizability semantics ensures feasible construction and verification for truths, all while preserving inference feasibly. The framework, grounded in Cobham's thesis, yields a coherent sub-intuitionistic account that aligns mathematical meaning with practical computability and offers a robust alternative to strict finitism and unbounded intuitionism. This provides a principled, computationally anchored approach to constructive mathematics with potential broad implications for logic and foundations.

Abstract

Dummett's argument for intuitionism is well known. There is a concern that the argument proves too much, specifically, that it supports the extreme and apparently incoherent position of strict finitism. The central question is how to explicate the notion that it is possible in practice to construct an arithmetical term or verify a statement. The strict finitist answer is plagued by the sorites paradox. We propose and develop feasibilism as a more plausible view, where computational feasibility, as captured by the class of polynomial-time problems, yields a robust and expedient explication of "possible in practice". In this approach, the complexity is bounded by a polynomial function of the input size, rather than bounded by a constant (as in strict finitism), thus resolving the sorites issues. We show that a system of strictly bounded arithmetic, introduced by Sam Buss, precisely formalizes the feasibilist view so as to satisfy Dummett's requirements.
Paper Structure (7 sections, 13 equations)

This paper contains 7 sections, 13 equations.

Table of Contents

  1. Introduction
  2. Does Dummett's argument prove too much?
  3. Feasibilism as a coherent and interesting view
  4. Feasibilism explicated and put to use
  5. The system of feasible arithmetic
  6. Feasibly computable functions and relations
  7. Realizing $\Sigma^b_1$-truths

Theorems & Definitions (1)

  • Definition 1