TY - CONF
T1 - The Logic of the Gödel Proof Predicate
T2 - Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, Brno, Czech Republic, August 24–27, 1993, Proceedings
Y1 - 1993
A1 - Sergei Artemov
A1 - Tyko Strassen
ED - Georg Gottlob
ED - Alexander Leitsch
ED - Daniele Mundici
AB - We discuss the logics of the operators ``$p$ is a proof of $A$'' and ``$p$ is a proof containing $A$'' for the standard Gödel proof predicate in Peano Arithmetic. Decidabillty and arithmetical completeness of these logics are proved. We use the same semantics as for the Provability Logic where the operator ``$A$ is provable'' is studied.
JF - Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, Brno, Czech Republic, August 24–27, 1993, Proceedings
T3 - Lecture Notes in Computer Science
PB - Springer
VL - 713
ER -