Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 18 июля 2013 г.
Аннотация:It is known that the propositional logics of proofs are decidable
whereas the predicate case is nonaxiomatizable at all -- the
natural definition of a predicate proof logic gives a theory
which is not recursively enumerable. We propose an
extension of the propositional proof logic language by the second order
variables denoting the reference constructors
(like ``the formula which is proved by $x$''). The proof logic in
this weak second order language is axiomatized via the calculus
${\cal FLP}_{ref}$, the {\em Logic of Proofs with References}.
The decidability, arithmetical soundness and arithmetical
completeness of ${\cal FLP}_{ref}$ are established.
${\cal FLP}_{ref}$ gives a flexible proof-theoretical interface
for arithmetic. We show how the
${\cal FLP}_{ref}$-language can be used as a scheme
language for both arithmetical lemmas and arithmetical inference rules
specification (a rule can be specified by a formula too). The
${\cal FLP}_{ref}$-provability gives the complete admissibility test
for arithmetical inference rules provided the rules are in the scope of the
specification method.