zbMATH — the first resource for mathematics

Towards a proof system for admissibility. (English) Zbl 1116.03304
Baaz, Matthias (ed.) et al., Computer science logic. 17th international workshop CSL 2003, 12th annual conference of the EACSL, 8th Kurt Gödel colloquium KGC 2003, Vienna, Austria, August 25–30, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40801-0/pbk). Lect. Notes Comput. Sci. 2803, 255-270 (2003).
Summary: In the author’s paper “On the admissible rules of intuitionistic propositional logic” [J. Symb. Log. 66, No. 1, 281–294 (2001; Zbl 0986.03013)] a basis for the admissible rules of intuitionistic propositional logic IPC was given. Here we strengthen this result by presenting a system ADM that has the following two properties. \(A\vdash_{\mathsf{ADM}}B\) implies that \(A\) admissibly derives \(B\). ADM is complete in the sense that for every formula \(A\) there exists a formula \(A\vdash_{\mathsf{ADM}}\Lambda_A\) such that the admissibly derivable consequences of \(A\) are the (normal) consequences of \(\Lambda_A\). This work is related to and partly relies upon research by Ghilardi on projective formulas.
For the entire collection see [Zbl 1019.00011].

03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI