Аннотация:The famous de Jongh’s theorem of 1970 stated that the intuitionistic logic
captured all the logical formulas which have all arithmetical instances derivable
in the Heyting Arithmetic HA. In this note we extend de Jongh’s arithmetical
completeness property from IPC to the basic intuitionistic logic of proofs, which
allows proof assertion statements of the sort x is a proof of F. The logic of proofs
seems to provide an appropriate language of describing admissible rules in HA.
URL:
http://sartemov.ws.gc.cuny.edu/files/2012/10/artemov.pdf