首页   按字顺浏览 期刊浏览 卷期浏览 Realization of Intuitionistic Logic by Proof Polynomials
Realization of Intuitionistic Logic by Proof Polynomials

 

作者: SergeiN. Artemov,  

 

期刊: Journal of Applied Non-Classical Logics  (Taylor Available online 1999)
卷期: Volume 9, issue 2-3  

页码: 285-301

 

ISSN:1166-3081

 

年代: 1999

 

DOI:10.1080/11663081.1999.10510968

 

出版商: Taylor & Francis Group

 

数据来源: Taylor

 

摘要:

In 1933 Gödel introduced an axiomatic system, currently known as S4, 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 S4 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 S4. 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 S4, 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 Int is complete with respect to this proof realizability.

 

点击下载:  PDF (717KB)



返 回