Computer Science Logic and 8th Kurt Gödel Colloquium
R. Iemhoff: Towards a proof system for admissibility
Welcome and News
Host Institutions
Calls and Deadlines
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint this page
An interesting meta-mathematical property of intuitionistic propositional logic IPC is the existence of non-derivable admissible rules for this logic. Some years ago it was shown that a certain class of rules, so-called Visser's rules, form a basis for the admissible rules of IPC. Intuitively this means that all the admissible rules of IPC can be obtained from Visser's rules via derivability in IPC. Here we strengthen this result by presenting a system ADM that consists of Visser's rules and a finite number of simple rewriting rules, such that for every formula A the system ADM derives a formula B such that the the admissibly derivable consequences of A are the (normal) consequences of B. Note that this result implies that V is a basis for the admissible rules of IPC. However, it is stronger in the sense that it provides more information about the admissibility relation.
© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04 Valid HTML 4.01! Valid CSS! Debian