Reference Constructions in the Single-conclusion Proof Logicстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 18 июля 2013 г.
Аннотация:We propose an extension of the
propositional proof logic language by the second-order variables
denoting the reference constructors (like ``the formula which is
proven by $x$''). The proof logic in this weak second-order
language is axiomatized via the calculus
${\sf FLP}_{\mbox{\scriptsize\it ref}}$\,, the
{\em (Functional) Logic of Proofs with References}. It is supplied with the
formal arithmetical semantics: we prove that ${\sf FLP}_{\mbox{\scriptsize\it ref}}$ is
sound with respect to arithmetical interpretations and is a
conservative extension of propositional single-conclusion proof
logic ${\sf FLP}$. Finally, we demonstrate how the language
of ${\sf FLP}_{\mbox{\scriptsize\it ref}}$
can be used as a scheme language for
arithmetic and provide the corresponding proof conversion method.