Generalizing inference systems by coaxioms

TL;DR

This paper introduces a generalized inference system with coaxioms, enabling flexible reasoning on non-well-founded data types and extending classical fixed point semantics beyond traditional inductive and coinductive interpretations.

Contribution

It proposes a novel inference system framework incorporating coaxioms, allowing fixed points that are neither least nor greatest, thus broadening the scope of formal reasoning.

Findings

Extends classical inference systems to include coaxioms.

Supports fixed points beyond least and greatest, enabling new reasoning strategies.

Provides a unified framework for inductive, coinductive, and mixed interpretations.

Abstract

After surveying classical results, we introduce a generalized notion of inference system to support structural recursion on non-well-founded data types. Besides axioms and inference rules with the usual meaning, a generalized inference system allows coaxioms, which are, intuitively, axioms which can only be applied "at infinite depth" in a proof tree. This notion nicely subsumes standard inference systems and their inductive and coinductive interpretation, while providing more flexibility. Indeed, the classical results can be extended to our generalized framework, interpreting recursive definitions as fixed points which are not necessarily the least, nor the greatest one. This allows formal reasoning in cases where the inductive and coinductive interpretation do not provide the intended meaning, or are mixed together.