Realization of intuitionistic logic by proof polynomialsстатья
Информация о цитировании статьи получена из
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 28 мая 2015 г.
Аннотация:In 1933 Gödel introduced an axiomatic system, currently known as 54, for a logic of an absolute provability, i.e. not depending on the formalism chosen (God 33). The problem of finding a fair provability model for 54 was left open. The famous formal provability predicate which first appeared in the Gödel Incompleteness Theorem does not do this job: the logic of formal provability is not compatible with 54. As was discovered in Art 95, this defect of the formal provability predicate can be bypassed by replacing hidden quantifiers over proofs by proof polynomials in a certain finite basis. The resulting Logic of Proofs enjoys a natural arithmetical semantics and provides an intended provability model for 54, thus answering a question left open by Gödel in 1933. Proof polynomials give an intended semantics for some other constructions based on the concept of provability, including intuitionistic logic with its Brouwer-Heyting- Kolmogorov interpretation, λ-calculus and modal λ-calculus. In the current paper we demonstrate how the intuitionistic propositional logic Int can be directly realized by proof polynomials. It is shown, that Intis complete with respect to this proof realizability.