Premium
On the Proof Method for Constructive Falsity
Author(s) -
Akama Seiki
Publication year - 1988
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19880340502
Subject(s) - falsity , constructive , computer science , citation , information retrieval , epistemology , library science , philosophy , programming language , process (computing)
The present paper gives a syntactical treatment of the so-called constructive falsity on the basis of Gentzen-type formulation. The main purpose is a proof of a cut-elimination theorem for this system. We will also gain several results such as completeness theorem, embedding theorems in classical (or intuitionistic) predicate logic and modal predicate logic 54, and interpolation theorem. Most of them have already proved in our previous paper AEAMA [l] by means of Kripke semantics. But some are more easily obtained by proof-theoretic way than model-theoretic one as shown in the subsequent sections.