Polynomially bounded recursive realizability (Q817959): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
Created claim: Wikidata QID (P12): Q57533063, #quickstatements; #temporary_batch_1712190744730 |
||
Property / Wikidata QID | |||
Property / Wikidata QID: Q57533063 / rank | |||
Normal rank |
Revision as of 02:45, 4 April 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Polynomially bounded recursive realizability |
scientific article |
Statements
Polynomially bounded recursive realizability (English)
0 references
23 March 2006
0 references
The strength of a theory can be measured by characterizing its provably total functions. Those of Heyting Arithmetic (HA), for example, are known to be specified as recursive according to Kleene's recursive realizability. The author proved in his earlier work that provably total functions of Basic Arithmetic (BA) are primitive recursive, where BA was introduced by Ruitenburg in a similar way as HA by featuring his Basic Logic in place of intuitionistic logic. In this paper the author introduces a polynomially bounded recursive realizability by restricting the recursive functions used in Kleene's realizability to the polynomially bounded ones, and proves that the earlier result is sharpened by them, where the polynomially bounded ones are primitive recursive. It is also shown that a polynomially bounded schema of Church's Thesis is realizable in the polynomially bounded sense. The schema, therefore, is consistent with BA, whereas it is inconsistent with HA.
0 references
Provably total function
0 references
basic arithmetic
0 references
basic logic
0 references
realizability
0 references
polynomially bounded recursive function
0 references
primitive recursive function
0 references