Fragment of Nonstandard Analysis with a Finitary Consistency Proof

We introduce a nonstandard arithmetic NQA− based on the theory developed by R. Chuaqui and P. Suppes in [2] (we will denote it by NQA+ ), with a weakened external open minimization schema. A finitary consistency proof for NQA− formalizable in PRA is presented. We also show interesting facts about the strength of the theories NQA− and NQA+ ; NQA− is mutually interpretable with I∆0 + EXP, and on the other hand, NQA+ interprets the theories IΣ1 and WKL0.

• Type: Journal
• Year: 2007
• Where: BSL
• Authors: Michal Rössler, Emil Jerábek
• Keywords: BSL 2007, External Open Minimization, Nonstandard Arithmetic Nqa−, finitary Consistency Proof