Principle of reiteration reflects structural continuity in logical proofs
The Proof-Theoretic Foundations of the Principle of Reiteration in Natural Deduction
Logic in Computer Science
Summary
This paper looks closely at a rule used in logical reasoning called the principle of reiteration, which allows repeating statements within proofs. The authors show that this rule isn’t a separate or new step in logic but comes from the way certain logical frameworks keep track of formulas step-by-step. By comparing two styles of logical proofs, they reveal that repetition is just a way to reuse and restore earlier parts of reasoning without adding new information. Essentially, repeating statements is built into the structure of logical arguments, not an independent rule.
What this means in practice
- •For logic system developers: Optimize proof-checking tools by recognizing reiteration as structural preservation, reducing redundancy in natural deduction implementations.
- •For formal verification engineers: Improve reasoning frameworks in software correctness tools by understanding reiteration’s role in maintaining proof dependencies without adding complexity.
A theory result. No direct application yet.
Authors
Khashayar Irani
Abstract
This paper investigates the proof-theoretic foundations of the principle of reiteration (R) in natural deduction, arguing that its legitimacy originates in the structural preservation of formulae within sequent calculus rather than in an independent logical rule. By examining singlesuccedent and multisuccedent sequent calculus, we demonstrate how logical operations transform principal formulae while preserving unaffected antecedent and succedent contexts. We subsequently analyse the schematic formulation of reiteration and compare natural deduction derivations with corresponding sequent calculus derivations. This comparison identifies two fundamental functions of reiteration, namely the reuse of previously employed formulae and the restoration of previously derived conclusions. We conclude that reiteration introduces no independent inferential content but explicitly represents the structural continuity of inferential dependencies already included into sequent calculus.