PaperlayerView exact revision on arXiv

Source-linked AI summary

Non-Expansive Fuzzy Modal Logic Has Uniform Interpolation

Stefan Gebhart, Lutz Schröder, Paul Wild

arXiv:2610.32335v1cs.LO

TL;DR

Fuzzy modal logics face a trade-off between the limited expressiveness of Zadeh semantics and the computational cost of Łukasiewicz semantics, while interpolation is unavailable in both. This paper establishes uniform interpolation for non-expansive fuzzy modal logic using a sequent-calculus construction. Its interpolants have exponential size and can be computed in exponential time, matching the two-valued correspondent’s complexity.

  • Problem

    Zadeh and Łukasiewicz semantics present a trade-off between tractability and expressiveness, and both lack Craig interpolation even in basic propositional logic.

    Source: §1 · pp. 2–3

  • Method

    The paper constructs interpolants along proofs in a sequent calculus, first for threshold judgements and then for formulae using symbolic thresholds.

    Source: §1 · p. 3, §8 · p. 16

  • Results

    Non-expansive fuzzy modal logic has uniform interpolation, with interpolants of exponential size computable in exponential time, matching the two-valued correspondent.

    Source: §1 · p. 3, §8 · p. 16

  • Takeaways & Limitations

    Uniform interpolation supplies a property used in applications including modularization, information hiding, and summarization.

    Source: §1 · p. 3

    The normal-form adjustment construction may be undefined for trivially true or false target judgements, although those cases are trivial.

    Source: §4 · p. 8

Abstract

from arXiv · show

Fuzzy logics with truth values in the unit interval vary in their choice of propositional connectives and their semantics, ranging from just minimum and maximum as in Zadeh logics to truncated addition and subtraction as in {\L}ukasiewicz logics or their extensions with truth constants, known as Pavelka logics. In the more specific world of fuzzy modal logics, non-expansive fuzzy modal logic has recently been proposed as a sweet spot between {\L}ukasiewicz (more precisely, Pavelka) and Zadeh fuzzy modal logic; it restricts {\L}ukasiewicz propositional connectives to have one argument constant, equivalently extends the Zadeh propositional base with constant shift operators. It retains reasonable expressiveness both in practical terms and abstractly; in particular, it characterizes the standard notion of behavioural distance on fuzzy Kripke frames. At the same time, it allows for satisfiability checking in the same complexity as for its two-valued correspondent (the modal logic K, or the description logic ALC), in contrast to the notorious computational hardness of {\L}ukasiewicz modal logic. In the present work, we show that non-expansive fuzzy modal logic admits uniform interpolation, a key property in modularization, information hiding, summarization, and other applications that fails for both {\L}ukasiewicz (or Pavelka) and Zadeh modal logic.

1 Introduction

Fuzzy modal logics trade off the tractability of Zadeh semantics against the expressiveness and reasoning costs of Łukasiewicz semantics. The paper establishes uniform interpolation for non-expansive fuzzy modal logic, an intermediate logic whose reasoning complexity remains that of its two-valued correspondent.

1 Introduction

  • Zadeh semantics supports tractable reasoning but is close to classical semantics, whereas Łukasiewicz semantics offers desirable logical properties at substantially higher reasoning cost.For Łukasiewicz fuzzy ALC, the best known satisfiability upper bound is NExpTime, and general TBoxes make satisfiability undecidable.Source: §1 · p. 2
  • Non-expansive fuzzy modal logic is expressive for behavioural distance, with Hennessy–Milner- and van-Benthem-type characterizations.It lies syntactically between Zadeh fuzzy modal logic and rational Pavelka logic.Source: §1 · p. 2
  • Its propositional base restricts Łukasiewicz connectives to one truth-constant argument, equivalently adding constant shifts to the Zadeh base, while retaining PSpace plain satisfiability and ExpTime under global assumptions.Constant shifts can express dampening in the inheritance of properties.Source: §1 · p. 2
  • The paper establishes uniform interpolation for non-expansive fuzzy modal logic, presenting the first known interpolation result for a fuzzy modal logic.Uniform interpolants capture the strongest consequence free of a chosen atom, and interpolation has applications including summarization, modularization, and information hiding.Source: §1 · pp. 2–3
  • The construction first handles threshold judgements and then extends to formulae using symbolic thresholds, with an exponential interpolant-size bound.This contrasts with Zadeh and full Łukasiewicz semantics, where even basic propositional logic fails Craig interpolation; the paper also extends the failure to Pavelka logic.Source: §1 · p. 3
  • Earlier proof-theoretic methods addressed intuitionistic propositional and two-valued modal logics, but the authors report no prior positive fuzzy-modal interpolation result.Uniform interpolation of TBoxes in two-valued ALC may fail to exist and can have triply exponential size.Source: §1 · p. 3

2 Preliminaries on Fuzzy Logic and Interpolation

The preliminaries distinguish fuzzy semantics and consequence relations, then state the paper’s interpolation result for non-expansive fuzzy modal logic.

2 Preliminaries on Fuzzy Logic and Interpolation

  • Fuzzy propositional logics interpret formulae over unit-interval valuations, with Zadeh conjunction and disjunction as minimum and maximum and Łukasiewicz logic adding truncated arithmetic connectives.Pavelka logic extends Łukasiewicz logic with rational truth constants.Source: §2 · p. 4
  • Strong consequence compares truth values pointwise, unlike weak consequence, which only preserves truth value 1; Craig interpolation here concerns strong consequence.Both Zadeh and Łukasiewicz logic fail Craig interpolation under this definition, and the paper reports the same failure for Pavelka logic.Source: §2 · p. 4
  • The main result establishes Craig and uniform interpolation with respect to strong consequence for non-expansive fuzzy modal logic.Source: §2 · p. 4

3 Non-Expansive Fuzzy Modal Logic

Non-expansive fuzzy modal logic combines a Zadeh-like base with limited Łukasiewicz arithmetic and a fuzzy diamond modality. Its sequent framework uses threshold judgements to formalize truth-value comparisons.

3 Non-Expansive Fuzzy Modal Logic

  • The non-expansive propositional base lies between Zadeh and Pavelka bases and restricts Łukasiewicz-style shifts to constant arguments.The paper uses a unimodal presentation for readability; its modal version is also called non-expansive fuzzy ALC.Source: §3 · p. 5
  • Formulae are built from atoms, zero, negation, truncated subtraction by a constant, conjunction, and the diamond modality.Disjunction and box are defined by duality, and truncated addition by a constant is definable from negation and subtraction.Source: §3 · p. 5
  • The valuation interprets negation as one minus the formula value and conjunction as minimum, while the diamond combines transition weight and formula value by minimum.Source: §3 · p. 5
  • A threshold judgement compares a formula with a real bound using one of four strict or non-strict inequalities, and sequents are finite sets of judgements.A sequent is satisfied when at least one of its judgements is satisfied; validity and satisfiability quantify over fuzzy Kripke models and worlds.Source: §3 · p. 6
  • In the example using transition degrees as accessibility, the formula measures reachability of a nearly deadlocked state in one step.The deadlock degree is 1 − sup_z R(y,z), and the shift discounts successor values by up to 1/5.Source: §3 · p. 6

4 Normal Forms

The section introduces negation normal form and judgement adjustments as preprocessing tools for the sequent and interpolation calculi. Both preserve equivalence, with adjustments subject to edge-case conditions.

4 Normal Forms

  • Every formula has an equivalent negation-normal-form formula with linear syntactic size, preserving its atoms and modal depth.Negations occur only immediately before atoms; derived connectives, modal operators, and truth constants are treated as first-class citizens.Source: §4 · pp. 6–7
  • Judgement adjustments replace a comparison and bound with prescribed ones while preserving equivalence, enabling convenient combination and modal-rule application.The construction applies to strict or non-strict comparisons of matching strictness and increases formula size by at most four.Source: §4 · pp. 7–8
  • Adjustments may be undefined for trivial target judgements, but those undefined cases are always trivial and do not imply that no adjustment exists.The construction is defined whenever the target is not trivially true or false, subject to the stated source-judgement conditions for trivial targets.Source: §4 · pp. 7–8

5 A Sequent Calculus For Fuzzy Modal Logic

The authors introduce a sound and complete single-sequent calculus for non-expansive fuzzy modal logic, using Gentzen-style rules and accommodating graded accessibility in its modal rule.

5 A Sequent Calculus For Fuzzy Modal Logic

  • The calculus works with finite sets of threshold judgements and assumes negation-normal-form formulae and > or ≥ comparisons after linear preprocessing.These assumptions are made without loss of generality, with preprocessing increasing syntactic size by at most a constant factor.Source: §5 · pp. 8–9
  • The system retains a comparatively simple single-sequent Gentzen-style calculus, avoiding much of the extra proof-theoretic machinery used for full Łukasiewicz logics.It is obtained essentially by dualizing a tableau calculus for non-expansive fuzzy ALC [10].Source: §5 · p. 8
  • Propositional rules reflect connective semantics and handle valid or unsatisfiable judgements, while the □ rule accounts for graded accessibility.The □ rule's side condition bounds the comparison thresholds so a failing box judgement yields a suitable diamond judgement at the original world.Source: §5 · pp. 8–9
  • The calculus is sound and complete: a sequent has a derivation if and only if it is valid.Its rules are presented in Table 1.Source: Table 1 · p. 9, §5 · p. 10

6 Uniform Interpolation of Threshold Judgements

The section develops uniform post-interpolation for threshold judgements using a sequent-based computation of p-free complements. The construction yields post-interpolants of at most exponential size and preserves modal depth.

6 Uniform Interpolation of Threshold Judgements

  • The target is deductive uniform interpolation parametrized by lower bounds on truth values, rather than only truth-at-1 weak consequence.The section presents this as a generalized form of deductive uniform interpolation.Source: §6 · p. 10
  • The method reduces threshold-judgement interpolation to computing a p-free complement of a normalized judgement, which yields a post-interpolant.The construction uses N on the judgement and the complement's lower-bound form; post-interpolants for judgements extend to sequents by combining normalized judgements.Source: §6 · p. 11
  • The interpolation calculus computes a right-hand judgement equivalent to the p-free complement of its left-hand sequent, without introducing new atoms.Its rules parallel the sequent calculus, and their nondeterminism does not affect the result up to logical equivalence.Source: §6 · pp. 11–12, Table 2 · p. 12
  • For sequents whose judgements share one comparison operator, every computation tree returns a judgement equivalent to the sequent's p-free complement.The computation proceeds alongside proofs in the sequent calculus.Source: §6 · pp. 11–12
  • Every threshold judgement in non-expansive fuzzy modal logic has a post-interpolant, and each has one of at most exponential size.The result also applies to threshold judgements in the propositional fragment of non-expansive fuzzy ALC.Source: §6 · p. 13
  • The construction does not increase modal depth, and its exponential size bound remains exponential with binary-encoded rational parameters.The binary-encoding bound applies when numerical parameters are rational; the construction preserves their rationality.Source: §6 · p. 13

7 Uniform Interpolation

Section 7 constructs pointwise uniform interpolants by extending the threshold-judgement interpolation calculus to symbolic thresholds. The resulting interpolants are p-free strongest consequences, preserve modal depth, and have exponential size and computation time for rational inputs.

7 Uniform Interpolation

  • For every formula ϕ and atom p, ∃p.ϕ is p-free, is implied by ϕ in the pointwise order, and is its strongest p-free consequence.Any p-free ψ with |= ϕ ≤ ψ also satisfies |= ∃p.ϕ ≤ ψ.Source: §7 · p. 14
  • By duality, ∀p.ϕ is the greatest p-free formula below ϕ in the pointwise order.It is defined as ¬∃p.(¬ϕ).Source: §7 · p. 14
  • Symbolic thresholds extend the threshold-judgement calculus: the constructed U(Γ) is independent of threshold A, which appears only in the resulting judgement.Threshold side conditions are encoded with truth constants and truncated shifts.Source: §7 · p. 14
  • The result follows from a symbolic-threshold construction whose correctness proof compares it with the interpolation calculus on Γ−A.The invariant is proved by induction on the total syntactic size of formulae in Γ.Source: §7 · p. 15
  • The construction preserves modal depth, so pointwise uniform interpolation also holds for the propositional fragment of non-expansive fuzzy ALC.The formula construction derives from a negation-normal-form threshold judgement and its post-interpolant.Source: §7 · p. 15
  • Pointwise interpolants have syntactic size 2^O(|ϕ|), and rational input parameters retain an exponential size bound and yield an exponential-time computation.The construction uses addition, subtraction, clipping, and division by 2; rational parameters are encoded in binary.Source: §7 · pp. 15–16

8 Conclusions

The conclusion establishes uniform interpolation for non-expansive fuzzy modal logic, between Zadeh and Pavelka modal logic. Its interpolants have exponential size and are computable in exponential time; extensions to richer logics and model types remain future work.

8 Conclusions

  • Non-expansive fuzzy modal logic, between Zadeh and Pavelka modal logic, has uniform interpolation with exponential-size interpolants computable in exponential time.These bounds match those for its two-valued correspondent, modal logic K or description logic ALC; computation follows proofs in a sequent calculus dualizing a previous tableau calculus [10].Source: §8 · p. 16
  • Future work includes extending the result to fuzzy hybrid and first-order logics, varying model types to probabilistic models, and pursuing generic coalgebraic methods.The passage identifies quantitative probabilistic modal logics as one target.Source: §8 · p. 16

Failure of Craig Interpolation for Propositional Pavelka Logic

The section gives a propositional Pavelka counterexample showing that Craig interpolants need not exist for the pointwise order. The required interpolant would evaluate to q/2, but no rational Pavelka formula has that evaluation function.

Failure of Craig Interpolation for Propositional Pavelka Logic

  • The section introduces propositional Pavelka formulae using truth constants from [0,1] and propositional atoms.Their semantics is defined over fuzzy Kripke frames.Source: Failure of Craig Interpolation for… · p. 20
  • The proposed formulas satisfy ϕ(p,q) ≤ q/2 ≤ ψ(q,r) for all valuations, establishing |= ϕ ≤ ψ.An interpolant would have to depend only on q and lie between ϕ(p,q) and ψ(q,r).Source: Failure of Craig Interpolation for… · p. 20
  • The counterexample forces any q-only interpolant to evaluate to q/2, which no rational Pavelka formula can express.Such formulae have continuous piecewise-affine evaluation functions with integer slopes, so Craig interpolants—and therefore uniform interpolants—do not always exist.Source: Failure of Craig Interpolation for… · p. 20
  • For a finite set of formulae, jointly attainable truth-value vectors form a compact set, and each vector is realized at the root of a finite tree model.The proof proceeds by induction on modal depth and constructs finite trees with bounds depending only on the formula set.Source: Failure of Craig Interpolation for… · p. 20

Details for Section 4

The normalization rules produce negation normal form without increasing modal depth or duplicating subformulae, so the resulting formula has linear syntactic size.

Details for Section 4

  • Normalization removes double negations and pushes remaining negations inward without duplicating subformulae, yielding linear syntactic size.The rules preserve atoms and modal depth.Source: Details for Section 4 · p. 21

Details for Section 5

The proof details establish soundness and completeness of the sequent calculus, then justify the complement construction and its threshold-based extension. The construction preserves the required equivalence across positive thresholds.

Details for Section 5

  • The propositional rules are sound and invertible, while modal completeness reduces saturated sequents to valid modal premises through countermodel constructions.For the modal rule, a finite countermodel witnesses failure; completeness combines countermodels of modal premises using separate successors.Source: Details for Section 5 · pp. 21–22

Details for Section 6

  • The conjunction step builds its candidate complement from β1 and β2, then uses invertibility to show it remains a p-free complement.The proof applies the conjunction rule to ¬β and uses the complements of the two branches to close both resulting premises.Source: Details for Section 6 · pp. 22–23

Details for Section 7

  • The stated shift equivalence is preserved by both modalities, allowing modal adjustments to transfer between threshold A and threshold 0.5.The proof establishes preservation directly for boxes and by finite-model reasoning for diamonds.Source: Details for Section 7 · p. 24
  • The construction verifies U(Γ) ≥ A against the interpolation output on Γ − A for every positive threshold, by induction over formula size.The induction treats propositional and modal cases and establishes the invariant simultaneously for all positive A.Source: Details for Section 7 · pp. 24–26
Loading 2610.32335v1…