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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 1999
Accession Number
ADA364528

Entities

People

  • S. N. Artemov

Organizations

  • Cornell University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Arithmetic
  • Artificial Intelligence
  • Decoding
  • Information Operations
  • Intelligent Systems
  • Language
  • Mathematics
  • Military Research
  • Notation
  • Polynomials
  • Recursive Functions
  • Semantics
  • Specifications
  • Standards
  • Symbols
  • Universities

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Mathematical Modeling and Probability Theory.