Atlas home || Conferences | Abstracts | about Atlas

First St.Petersburg Days of Logic and Computability
May 26-29, 1999
Steklov Institute of Mathematics
St. Petersburg, Russia

Organizers
Evgeny Dantsin, Gennadii Davydov, Dima Grigoriev, Eduard Karavaev, Nickolai Kossovskii, Vladimir Lifschitz, Maurice Margenstern, Yuri Matiyasevich (chairman), Grigori Mints, Vladimir Orevkov, Anatol Slissenko, Maxim Vsemirnov

View Abstracts
Conference Homepage

Nonaxiomatizability of first order logics of proofs
by
Tatiana Yavorskaja (Sidon)
Moscow State University

The idea to study properties of the proof predicate ``p is a proof of a formula F'' by means of propositional logic extended by a bynary proof operator p:F belongs to S. Artemov. He formulated and studied propositional systems of Logic of Proofs all of which turned to be decidable. We study the possibility to axiomatize properties of proof predicates in the first order language.

We consider the language L that is obtained by extending the usual predicate language by functional variables for recursive functions on proofs and operational symbol p:F for proof predicate. Formulas in the language L are defined in the standard way with the only additional clause. If F is a formula, g is a functional variable of arity n and x1, x2, ... , xn are individual variables then (g(x1, x2, ... , xn)): F is a formula.

Arithmetical interpretation *=(Prf, f) of the language L in the arithmetical language consists of the arbitrary proof predicate Prf and the evaluation f of functional variables and atomic formulas of L by provably recursive arithmetical terms and arithmetical formulas resp. We suppose that * commutes with substitution of free variables and boolean connectives, and
(g(x1, ... , xk): A(y1, ... , yn))* = Prf(f(g)(x1, ... , xk), A*(
×
y
 
1 
 , ... ,
×
y
 
n 
 ) ).

Being given an arithmetical theory U and a class of proof predicates K we define first order logic of proofs QLPK(U) as the set of principles that are provable in U under all interpretations based on proof predicates from K.

It is shown that for each proof predicate Prf the logics QLPPrf(TA) and QLPPrf(PA) that correspond to truth arithmetic and Peano arithmetic respectively are not recursively axiomatizable. The presise lower bounds for the complexity of these logics are obtained. We also consider the case of interpretations that assign constant functions to all functional symbols and prove that the corresponding logics remain undecidable thow the bounds of complexity may differ.

Date received: March 1, 1999

Copyright © 1999 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cacs-12.