Affordable Access

Publisher Website

On the completenes principle: A study of provability in heyting's arithmetic and extensions

Authors
Journal
Annals of Mathematical Logic
0003-4843
Publisher
Elsevier
Publication Date
Volume
22
Issue
3
Identifiers
DOI: 10.1016/0003-4843(82)90024-9
Disciplines
  • Logic
  • Mathematics

Abstract

Abstract In this paper extensions of HA are studied that prove their own completeness, i.e. they prove A → □ A, where □ is interpreted as provability in the theory itself. Motivation is three-fold: (1) these theories are thought to have some intrinsic interest, (2) they are a tool for producing and studying provability principles, (3) they can be used to proved independence results. Work done in the paper connected with these motivations is respectively: 1. (i) A characterization is given of theories proving their own completeness, including an appropriate conservation result. 2. (ii) Some new provability principles are produced. The provability logic of HA is not a sublogic of the of PA. A provability logic plus completeness theorem is given for a certain intuitionistic extension of HA. De Jongh's theorem for propositional logic is a corollary. 3. (iii) FP-realizability in Beeson's proof that ∦ HA KLS is replaced by theories proving their own completeness. New consequences are ∦ HA+− M PR KLS , ∦ HA+DNS KLS .

There are no comments yet on this publication. Be the first to share your thoughts.