Wright's First-Order Logic of Strict Finitism

TL;DR

This paper develops a classical first-order logic for strict finitism, extending previous propositional logic work, with soundness, completeness, and semantics, highlighting differences when certain conditions are imposed.

Contribution

It introduces a first-order logic of strict finitism without auxiliary conditions, providing semantics and proof systems, extending prior propositional logic results.

Findings

Sound and complete Kripke semantics for the logic

Natural deduction system for the logic

Extensions match previous propositional results under conditions

Abstract

A classical reconstruction of Wright's first-order logic of strict finitism is presented. Strict finitism is a constructive standpoint of mathematics that is more restrictive than intuitionism. Wright sketched the semantics of said logic in Wright (Realism, Meaning and Truth, chap 4, 2nd edition in 1993. Blackwell Publishers, Oxford, Cambridge, pp.107-75, 1982), in his strict finitistic metatheory. Yamada (J Philos Log. https://doi.org/10.1007/s10992-022-09698-w, 2023) proposed, as its classical reconstruction, a propositional logic of strict finitism under an auxiliary condition that makes the logic correspond with intuitionistic propositional logic. In this paper, we extend the propositional logic to a first-order logic that does not assume the condition. We will provide a sound and complete pair of a Kripke-style semantics and a natural deduction system, and show that if the condition is imposed, then the logic exhibits natural extensions of Yamada (2023)'s results.