Functionality in the Basic Logic of Proofs

TitleFunctionality in the Basic Logic of Proofs
Publication TypeTechnical Reports
Year of Publication1993
AuthorsArtemov, S, Strassen, T
AbstractThis report describes the elimination of the injectivity restriction for functional arithmetical interpretations as used in the systems $\mathcal{PF}$ and $\mathcal{PFM}$ in the Basic Logic of Proofs. An appropriate axiom system $\mathcal{PU}$ in a language with operators ``$x$ is a proof of $y$'' is defined and proved to be sound and complete with respect to all arithmetical interpretations based on functional proof predicates. Unification plays a major role in the formulation of the new axioms.