Syntactic translations and provably recursive functions.

*(English)*Zbl 0593.03038In this paper conservation results for classical theories over the corresponding intuitionistic theories are given using Kolmogorov’s version of the so-called double-negation translation (1925). The author provides conditions under which a formula \(\phi\) is provable from a set \(\Gamma\) of formulas in minimal logic (intuitionistic logic resp.) if it is classically. From certain formulas satisfying these conditions he concludes that a recursive function is provably total in so-called intuitionistic full arithmetic, if it is in classical full arithmetic. The same holds for Heyting and Peano Arithmetic and for functionals of higher type instead of recursive functions. If a recursive function is provably total in classical ZF, so it is in intuitionistic ZF. The author introduces another map from formulas to formulas, which translates intuitionistic provability into provability in minimal logic. He establishes conditions for \(\Gamma\) and \(\phi\) such that \(\Gamma\) \(\vdash \neg \neg \phi\) entails \(\Gamma \vdash_ M\phi\) respectively \(\Gamma \vdash_ I\phi\). These results cover some work of H. Friedman on closure of theories under Markov’s and other rules.

As the author stresses by himself, in his paper strong results are obtained by familiar and easy methods, and simple proofs, and - that he does not mention - cleverly chosen concepts.

As the author stresses by himself, in his paper strong results are obtained by familiar and easy methods, and simple proofs, and - that he does not mention - cleverly chosen concepts.

Reviewer: H.Pfeiffer

##### MSC:

03F50 | Metamathematics of constructive systems |

03D20 | Recursive functions and relations, subrecursive hierarchies |

##### Keywords:

conservation results for classical theories over the corresponding; intuitionistic theories; double-negation translation; minimal logic; intuitionistic full arithmetic; Peano Arithmetic; functionals of higher type; classical ZF; intuitionistic ZF; intuitionistic provability; conservation results for classical theories over the corresponding intuitionistic theories
Full Text:
DOI

##### References:

[1] | The L.E.J. Brouwer centenary symposium pp 459– (1982) |

[2] | Bolletino delta Unione Matematica Italiana 2 pp 1– (1969) |

[3] | Natural deduction (1965) |

[4] | Doklady Akademii Nauk SSSR 152 pp 553– (1963) |

[5] | Twenty-fourth annual symposium on foundations of computer science pp 460– (1983) |

[6] | A note on translations from C into 1 (1971) |

[7] | Elementary completeness properties of intuitionistic logic, with a note on negations of prenex formulas 23 pp 317– (1958) |

[8] | Metamathematical investigation of intuitionistic arithmetic and analysis 344 (1974) |

[9] | Mathematical significance of consistency proofs 23 pp 155– (1958) |

[10] | Matématicéskij Sbornik 32 pp 646– (1925) |

[11] | Introduction to metamathematics (1952) |

[12] | Ergehnisse eines Mathematischen Kolloquiums 4 pp 34– (1932) |

[13] | Bulletin de l’Académie Royale de Belgique, Classe des Sciences 15 pp 183– |

[14] | Clôture par rapport à Markov (1973) |

[15] | Higher set theory 699 pp 21– (1978) |

[16] | The consistency of classical set theory relative to a set theory with intuitionistic logic 38 pp 315– (1973) · Zbl 0278.02045 |

[17] | A programming logic (1978) |

[18] | Contributions to mathematical logic pp 215– (1965) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.