Premium
Glivenko like theorems in natural expansions of BCK‐logic
Author(s) -
Cignoli Roberto,
Torrens Torrell Antoni
Publication year - 2004
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.200310082
Subject(s) - mathematics , negation , intuitionistic logic , congruence relation , many valued logic , intermediate logic , negation as failure , discrete mathematics , pure mathematics , algebra over a field , propositional calculus , autoepistemic logic , calculus (dental) , multimodal logic , linguistics , artificial intelligence , medicine , philosophy , dentistry , computer science , description logic
The classical Glivenko theorem asserts that a propositional formula admits a classical proof if and only if its double negation admits an intuitionistic proof. By a natural expansion of the BCK‐logic with negation we understand an algebraizable logic whose language is an expansion of the language of BCK‐logic with negation by a family of connectives implicitly defined by equations and compatible with BCK‐congruences. Many of the logics in the current literature are natural expansions of BCK‐logic with negation. The validity of the analogous of Glivenko theorem in these logics is equivalent to the validity of a simple one‐variable formula in the language of BCK‐logic with negation. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)