Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss

Daniil Kozhemiachenko

TL;DR

This work addresses proving-system efficiency in finite-valued Łukasiewicz logics by generalizing proof-simulation techniques from Frege systems to logics without the deduction theorem, notably through disjunction elimination rules. It constructs augmented Frege-like systems for ${\hbox{\sf\L}}_3$ and extends the simulations to all finite-valued ${\hbox{\sf\L}}_k$, providing upper bounds on speed-ups relative to proof steps and lengths, and establishing polynomial simulations of natural deduction and hypersequent calculi by Frege systems. The results show that near-linear (and occasionally inverse-Ackermann-type) bounds hold for translations between systems, illustrating robust inter-derivability even without the deduction theorem. The work advances understanding of proof complexity in non-classical logics and suggests directions for extending these bounds to broader logics and infinite-valued cases, with implications for automated reasoning in Łukasiewicz frameworks.

Abstract

In this paper, we present a~generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems that augment Avron's Frege system for Łukasiewicz three-valued logic with nested and general versions of the disjunction elimination rule, respectively. For these systems we provide upper bounds on speed-ups w.r.t.\ both the number of steps in proofs and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics.

Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss

TL;DR

This work addresses proving-system efficiency in finite-valued Łukasiewicz logics by generalizing proof-simulation techniques from Frege systems to logics without the deduction theorem, notably through disjunction elimination rules. It constructs augmented Frege-like systems for and extends the simulations to all finite-valued , providing upper bounds on speed-ups relative to proof steps and lengths, and establishing polynomial simulations of natural deduction and hypersequent calculi by Frege systems. The results show that near-linear (and occasionally inverse-Ackermann-type) bounds hold for translations between systems, illustrating robust inter-derivability even without the deduction theorem. The work advances understanding of proof complexity in non-classical logics and suggests directions for extending these bounds to broader logics and infinite-valued cases, with implications for automated reasoning in Łukasiewicz frameworks.

Abstract

In this paper, we present a~generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems that augment Avron's Frege system for Łukasiewicz three-valued logic with nested and general versions of the disjunction elimination rule, respectively. For these systems we provide upper bounds on speed-ups w.r.t.\ both the number of steps in proofs and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics.
Paper Structure (10 sections, 24 theorems, 54 equations)

This paper contains 10 sections, 24 theorems, 54 equations.

Table of Contents

  1. Introduction
  2. 3-valued Łukasiewicz logic: semantics and proof systems
  3. Main results
  4. Simulation of the disjunction elimination rule in classical logic
  5. Simulation of the disjunction elimination rule in ${\hbox{\sf\L}}_3$
  6. Simulation of natural deduction and hypersequent calculus
  7. Generalisation to finite-valued Łukasiewicz logics
  8. Semantics and proof systems
  9. Simulations of the general and nested disjunction elimination rules for ${\hbox{\sf\L}}_k$
  10. Conclusion and future work

Key Result

Theorem 3.1

There is a constant $c$ such that if $B$ is inferred in a Frege system from $A$ in $n$ steps, then $A\supset B$ has Frege proof in $c\cdot n$ steps.

Theorems & Definitions (47)

  • Definition 2.1
  • Definition 2.2: $\mathcal{H}{\hbox{\sf\L}}\mathsf{uk}$ Avron1991
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5: ${\hbox{\sf\L}}_{3_\vee}$
  • Definition 2.6: ${\hbox{\sf\L}}_{3_{n\vee}}$
  • Definition 2.7
  • Theorem 3.1: Bonet and Buss BonetBuss1993
  • Theorem 3.2: Bonet and Buss BonetBuss1993
  • Theorem 3.3: Bonet and Buss BonetBuss1993
  • ...and 37 more