Size Relationships in Abstract Cyclic Entailment Systems

TL;DR

This paper introduces a formal framework for cyclic proof systems, focusing on size relationships of models in entailments, which aids in program verification by ensuring models are smaller relative to consequents.

Contribution

It provides an abstract definition of cyclic entailment systems and establishes conditions for model size comparisons within these systems.

Findings

Models are always smaller when interpreted with respect to the consequent.

A new condition on proof objects guarantees size relationships in entailments.

The framework supports reasoning about infinite proofs in a finite manner.

Abstract

A cyclic proof system generalises the standard notion of a proof as a finite tree of locally sound inferences by allowing proof objects to be potentially infinite. Regular infinite proofs can be finitely represented as graphs. To preclude spurious cyclic reasoning, cyclic proof systems come equipped with a well-founded notion of 'size' for the models that interpret their logical statements. A global soundness condition on proof objects, stated in terms of this notion of size, ensures that any non-well-founded paths in the proof object can be disregarded. We give an abstract definition of a subclass of such cyclic proof systems: cyclic entailment systems. In this setting, we consider the problem of comparing the size of a model when interpreted in relation to the antecedent of an entailment, with that when interpreted in relation to the consequent. Specifically, we give a further condition on proof objects which ensures that models of a given entailment are always 'smaller' when interpreted with respect to the consequent than when interpreted with respect to the antecedent. Knowledge of such relationships is useful in a program verification setting.