×

zbMATH — the first resource for mathematics

Dual-intuitionistic logic. (English) Zbl 0869.03008
Summary: The sequent system \({\mathbf L}{\mathbf D}{\mathbf J}\) is formulated using the same connectives as Gentzen’s intuitionistic sequent system \({\mathbf L}{\mathbf J}\), but is dual in the following sense: (i) whereas \({\mathbf L}{\mathbf J}\) is singular in the consequent, \({\mathbf L}{\mathbf D}{\mathbf J}\) is singular in the antecedent; (ii) whereas \({\mathbf L}{\mathbf J}\) has the same sentential counter-theorems as classical \({\mathbf L}{\mathbf K}\) but not the same theorems, \({\mathbf L}{\mathbf D}{\mathbf J}\) has the same sentential theorems as \({\mathbf L}{\mathbf K}\) but not the same counter-theorems. In particular, \({\mathbf L}{\mathbf D}{\mathbf J}\) does not reject all contradictions and is accordingly paraconsistent. To obtain a more precise mapping, both \({\mathbf L}{\mathbf J}\) and \({\mathbf L}{\mathbf D}{\mathbf J}\) are extended by adding a “pseudo-difference” operator \(\overset{.}-\) which is the dual of intuitionistic implication. Cut-elimination and decidability are proved for the extended systems \({\mathbf L}{\mathbf J}^{\overset{.}-}\) and \({\mathbf L}{\mathbf D}{\mathbf J}^{\overset{.}-}\), and a simply consistent but \(\omega\)-inconsistent Set Theory with Unrestricted Comprehension Schema based on \({\mathbf L}{\mathbf D}{\mathbf J}\) is sketched.

MSC:
03B20 Subsystems of classical logic (including intuitionistic logic)
03F05 Cut-elimination and normal-form theorems
03E70 Nonclassical and second-order set theories
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Curry, H. B., Foundations of Mathematical Logic , Dover, New York, 1976. · Zbl 0396.03001
[2] Czermak, J., “A remark on Gentzen’s calculus of sequents,” Notre Dame Journal of Formal Logic , vol. 18 (1977), pp. 471–474. · Zbl 0314.02026
[3] Gentzen, G., “Investigations into logical deduction,” The Collected Papers of Gerhard Gentzen , edited by M. E. Szabo, North-Holland, Amsterdam, 1969. · Zbl 0209.30001
[4] Glivenko, V., “Sur quelques points de la logique de M. Brouwer,” Académie Royale de Belgique, Bulletins de la classe des sciences , ser. 5, vol. 15 (1929), pp. 183–188. · JFM 55.0030.05
[5] Goodman, N. D., “The logic of contradiction,” Zeitschrift für mathematische Logik und Grundlagen der Mathematik , vol. 27 (1981), pp. 119–126. · Zbl 0467.03019
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.