Truth Predicate of Inductive Definitions and Logical Complexity of Infinite-Descent Proofs

TL;DR

This paper investigates the logical complexity of proof systems for inductively defined relations, establishing that provability in the infinite-descent proof system LKID-omega is (Pi-1-1)-complete, linking it to the complexity of validity in standard models.

Contribution

It extends the understanding of the logical complexity of LKID-omega, showing its provability problem is (Pi-1-1)-complete and connecting it to the validity of inductive definitions in standard models.

Findings

Provability in LKID-omega is (Pi-1-1)-complete.

Validity of inductive definitions in standard models is equivalent to validity in standard term models.

Extended the truth predicate of omega-languages to inductive definitions using arithmetical coding.

Abstract

Formal reasoning about inductively defined relations and structures is widely recognized not only for its mathematical interest but also for its importance in computer science, and has applications in verifying properties of programs and algorithms. Recently, several proof systems of inductively defined predicates based on sequent calculus including the cyclic proof system CLKID-omega and the infinite-descent proof system LKID-omega have attracted much attention. Although the relation among their provabilities has been clarified so far, the logical complexity of these systems has not been much studied. The infinite-descent proof system LKID-omega is an infinite proof system for inductive definitions and allows infinite paths in proof figures. It serves as a basis for the cyclic proof system. This paper shows that the logical complexity of the provability in LKID-omega is (Pi-1-1)-complete. To show this, first it is shown that the validity for inductive definitions in standard models is equivalent to the validity for inductive definitions in standard term models. Next, using this equivalence, this paper extends the truth predicate of omega-languages, as given in Girard's textbook, to inductive definitions by employing arithmetical coding of inductive definitions. This shows that the validity of inductive definitions in standard models is a (Pi-1-1) relation. Then, using the completeness of LKID-omega for standard models, it is shown that the logical complexity of the provability in LKID-omega is (Pi-1-1)-complete.