Premium
A Note on the Proof Method for Constructive Falsity
Author(s) -
Tanka Kazuyuki
Publication year - 1991
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.19910370209
Subject(s) - falsity , constructive , citation , computer science , constructive proof , mathematics , library science , epistemology , discrete mathematics , philosophy , programming language , process (computing)
This short note is concerned with a misleading treatment of so-called NELSON’S system of constructive falsity. In [l], S. AKAMA presents an interesting but obscure formalization GS of constructive falsity.’) For instance, we are puzzled with his rule (-3) on p. 387, by which we can derive 0 = 1 from 3x(O = x ) . But without the rules of quantifications. it might serve as a correct propositional system if we restrict the rule (x+) to the case r= A and A = 0. We call it GS’. The rules of GS‘ can be viewed as inversion theorems for the standard Gentzenstyle formulation [3], [4], and vice versa. The most significant difference between this two types of formulations is that GS’ (or GS) may not enjoy the cut elimination theorem while the standard one may. Take a look at the following proof of A 3 A in GS‘: