Accession Number:

ADA364528

Title:

Operations on Proofs That Can be Specified by Means of Modal Logic

Descriptive Note:

Technical rept.

Corporate Author:

CORNELL UNIV ITHACA NY CENTER FOR FOUNDATIONS OF INTELLIGENT SYSTEMS

Personal Author(s):

Report Date:

1999-02-01

Pagination or Media Count:

23.0

Abstract:

Explicit modal logic was first sketched by Goedel as the logic with the atoms t is a proof of F. The complete axiomatization of the Logic of Proofs LP was found in 4 see also 6, 7, and 21. In this paper we establish a sort of a functional completeness property of proof polynomials which constitute the system of proof terms in LP. Proof polynomials are built from variables and constants by three operations on proofs . application, proof checker, and choice. Here constants stand for canonical proofs of simple facts, namely instances of propositional axioms and axioms of LP in a given proof system. We show that every operation on proofs that 1 can be specified in a propositional modal language, and 2 is invariant with respect to the choice of a proof system is realized by a proof polynomial.

Subject Categories:

  • Theoretical Mathematics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE