STRICTLY PRIMITIVE RECURSIVE REALIZABILITY

被引:13
作者
DAMNJANOVIC, Z
机构
关键词
D O I
10.2307/2275700
中图分类号
O1 [数学];
学科分类号
0701 ; 070101 ;
摘要
A realizability notion that employs only primitive recursive functions is defined, and, relative to it, the soundness of the fragment of Heyting Arithmetic (HA) in which induction is restricted to SIGMA1(0) formulae is proved. A dual concept of falsifiability is proposed and an analogous soundness result is established for a further restricted fragment of HA.
引用
收藏
页码:1210 / 1227
页数:18
相关论文
共 11 条
[1]  
AXT P, 1963, Z MATH LOGIK GRUNDLA, V9, P53
[2]  
DAMNJANOVIC Z, IN PRESS ELEMENTARY
[3]  
KLEENE SC, 1979, INTRO METAMATHEMATIC, V25, P411
[4]   SYNTACTIC TRANSLATIONS AND PROVABLY RECURSIVE FUNCTIONS [J].
LEIVANT, D .
JOURNAL OF SYMBOLIC LOGIC, 1985, 50 (03) :682-688
[5]  
LOPEZESCOBAR EGK, 1974, FUND MATH, V82, P25
[6]   CLASSES OF RECURSIVE FUNCTIONS BASED ON ACKERMANNS FUNCTION [J].
RITCHIE, RW .
PACIFIC JOURNAL OF MATHEMATICS, 1965, 15 (03) :1027-&
[7]  
Rose H.E., 1984, SUBRECURSION FUNCTIO
[8]  
Troelstra A., 1988, STUDIES LOGIC FDN MA, V1
[9]  
Troelstra A.S., 1973, METAMATHEMATICAL INV
[10]  
[No title captured]