Provably Total Functions of Arithmetic with Basic Terms

TL;DR

This paper introduces a new way to characterize provably recursive functions in first-order arithmetic using only basic terms like 0, successor, and variables, simplifying the understanding of these functions.

Contribution

It provides a novel characterization of provably recursive functions by restricting terms to basic components, enhancing the conceptual clarity of their structure.

Findings

New characterization of provably recursive functions

Simplifies the understanding of function structure in arithmetic

Uses only basic terms in the quantifier rules

Abstract

A new characterization of provably recursive functions of first-order arithmetic is described. Its main feature is using only terms consisting of 0, the successor S and variables in the quantifier rules, namely, universal elimination and existential introduction.