On Properties of Feasibility in Non-Standard Heyting Arithmetic
Péter Battyányi · 2024
We examine nonstandard Heyting arithmetic extended with a feasibility predicate. Feasibility is defined as a downward closed property containing all numerals and closed under applications with primitive recursive functions. Making use of Kleene's arithmetical realizability, we demonstrate for a theory slightly weaker than Heyting arithmetic that provably feasible terms coincide with the set of numerals. Moreover, we show that disjunction and existential properties are preserved in our arithmetical theory.