Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic

José Espírito Santo, Ralph Matthes, Luís Pinto

TL;DR

This work extends coinductive proof search (CoIPS) from implicational intuitionistic logic to the polarized propositional logic $LJP$, developing both coinductive and inductive representations of the proof-search spaces and establishing decision procedures for inhabitation, solvability, and finiteness. By proving the adequacy and compatibility of a coinductive solution-space term ${S}(\sigma)$ with its finitary counterpart ${F}(\sigma)$, the authors derive generic decidability results and meta-theoretic properties (e.g., disjunction, infinity) within a unified framework. They further show that $LJP$ provides full embeddings of two standard IPL proof systems, $LJT$ and $LJQ$, via negative and positive polarizations, enabling inheritance of results to full IPL with all connectives. Overall, the paper establishes $LJP$ as a versatile platform for understanding proof search across polarized and intuitionistic logics, delivering new decision procedures and extending CoIPS beyond implicational fragments.

Abstract

The approach to proof search dubbed "coinductive proof search" (CoIPS), and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. Inhabitation is taken in a generalized sense, because we also consider when a sequent has a solution, that is a (possibly infinite) run of bottom-up proof search which never fails to apply another inference rule. We provide a very general scheme whose instances are decision problems concerning solutions in LJP having algorithms through the inductive syntax. Polarized logic and LJP can be used as a platform from which proof search for other logics is understood. We illustrate this for the proof systems LJT and LJQ for intuitionistic logic, both equipped with all the connectives. For that we work out respectively a negative and a positive interpretation into LJP, which map formulas of the source logic into formulas in LJP of the said polarity; and this even at the level of the coinductive versions of the three involved proof systems. The interpretations are proved to be, not only faithful, but actually full embeddings, establishing a bijection between the solutions (resp. proofs) of a sequent and the solutions (resp. proofs) of its polarized interpretation. This allows the inheritance to the source systems of the decidability and other results previously obtained for LJP, thereby vastly generalizing the previous results of CoIPS, which were confined to LJT and implicational intuitionistic logic.

Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic

TL;DR

This work extends coinductive proof search (CoIPS) from implicational intuitionistic logic to the polarized propositional logic , developing both coinductive and inductive representations of the proof-search spaces and establishing decision procedures for inhabitation, solvability, and finiteness. By proving the adequacy and compatibility of a coinductive solution-space term with its finitary counterpart , the authors derive generic decidability results and meta-theoretic properties (e.g., disjunction, infinity) within a unified framework. They further show that provides full embeddings of two standard IPL proof systems, and , via negative and positive polarizations, enabling inheritance of results to full IPL with all connectives. Overall, the paper establishes as a versatile platform for understanding proof search across polarized and intuitionistic logics, delivering new decision procedures and extending CoIPS beyond implicational fragments.

Abstract

The approach to proof search dubbed "coinductive proof search" (CoIPS), and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. Inhabitation is taken in a generalized sense, because we also consider when a sequent has a solution, that is a (possibly infinite) run of bottom-up proof search which never fails to apply another inference rule. We provide a very general scheme whose instances are decision problems concerning solutions in LJP having algorithms through the inductive syntax. Polarized logic and LJP can be used as a platform from which proof search for other logics is understood. We illustrate this for the proof systems LJT and LJQ for intuitionistic logic, both equipped with all the connectives. For that we work out respectively a negative and a positive interpretation into LJP, which map formulas of the source logic into formulas in LJP of the said polarity; and this even at the level of the coinductive versions of the three involved proof systems. The interpretations are proved to be, not only faithful, but actually full embeddings, establishing a bijection between the solutions (resp. proofs) of a sequent and the solutions (resp. proofs) of its polarized interpretation. This allows the inheritance to the source systems of the decidability and other results previously obtained for LJP, thereby vastly generalizing the previous results of CoIPS, which were confined to LJT and implicational intuitionistic logic.

Paper Structure

This paper contains 25 sections, 42 theorems, 58 equations, 21 figures.

Table of Contents

  1. Introduction and Motivation
  2. Background on the system $\mathsf{LJP}$ of polarized propositional logic
  3. Coinductive approach to proof search in $\mathsf{LJP}$ - part I
  4. System $\mathsf{LJP}^\mathit{co}$
  5. System $\mathsf{LJP}^\mathit{co}_{\Sigma}$
  6. Representation of solution spaces as forests of $\mathsf{LJP}^\mathit{co}_{\Sigma}$
  7. A class of predicates on forests
  8. What we obtained so far
  9. Coinductive approach to proof search in $\mathsf{LJP}$ - part II
  10. System $\mathsf{LJP}^\mathsf{gfp}_{\Sigma}$
  11. Finitary representation of solution spaces
  12. Analysis of predicates on forests with the finitary system $\mathsf{LJP}^\mathsf{gfp}_{\Sigma}$
  13. Deciding problems on inhabitants and on solutions in the systems $\mathsf{LJP}$ and $\mathsf{LJP}^\mathit{co}$
  14. Applications to intuitionistic propositional logic with all connectives
  15. Systems $\mathsf{LJT}$, $\mathsf{LJT}^{co}$ and their negative embedding into polarized logic
  16. ...and 10 more sections

Key Result

Lemma 3.1

For any $T\in\mathsf{LJP}$, $\sigma(T)$ is valid in $\mathsf{LJP}$ iff $\sigma(T)$ is valid in $\mathsf{LJP}^\mathit{co}$.

Figures (21)

  • Figure 1: Roadmaps
  • Figure 2: Typing rules of $\mathsf{LJP}$
  • Figure 3: Solution spaces for $\mathsf{LJP}$
  • Figure 4: Dual pair of predicates $\mathbb{P}_{D}$ and $\overline\mathbb{P}_{D}$ for dual pair data $D=(\circledcirc,Q,\overline Q,\circledast)$
  • Figure 5: Predicates ${\sf exfin}$, ${\sf nofin}$, $\mathsf{finfin}$ and $\mathsf{inffin}$
  • ...and 16 more figures

Theorems & Definitions (114)

  • Example 2.1
  • Definition 3.1: Expressions
  • Definition 3.2: Co-proof terms
  • Definition 3.3: Typing system of $\mathsf{LJP}^\mathit{co}$
  • Lemma 3.1
  • Example 3.1
  • Example 3.2
  • Definition 3.4: Expressions
  • Definition 3.5: Forests
  • Definition 3.6: Membership
  • ...and 104 more