Proof Search Algorithm in Pure Logical Framework

TL;DR

This paper presents a proof search algorithm for the Russell system, a pure logical framework, proving its correctness and completeness, ensuring it finds all valid proofs without relying on specific formal calculi.

Contribution

It introduces a novel proof search algorithm for Russell, demonstrating its correctness and completeness within a pure logical framework.

Findings

Algorithm is correct and complete

It finds all valid proofs within Russell

Ensures only valid proofs are generated

Abstract

By a pure logical framework we mean a framework which does not rely on any particular formal calculus. For example, Metamath is an instance of a pure logical framework. Another example is the Russell system (https://github.com/dmitry-vlasov/russell). In this paper, we describe the proof search algorithm used in Russell. The algorithm is proved to be correct and complete, i.e. it gives only valid proofs and any valid proof can be found (up to a substitution) by the proposed algorithm.