「‍」 Lingenic

Noncontractive Logic

(⤓.md ◇.md); γ ≜ [2026-07-17T120407.600, 2026-07-17T135416.643] ∧ |γ| = 3

Noncontractive Approaches to Paradox

Origin. Elia Zardini, "Truth without contra(di)ction" (Review of Symbolic Logic, 2011); Greg Restall's earlier observation that contraction drives Curry ("How to be Really Contraction Free", 1993); Petersen (2000) on naive comprehension without contraction; Mares and Paoli (2014) for the general substructural framing. The counterpart to the nontransitive answer: same problem, different structural rule.

Models. Curry's paradox does not need negation. From a sentence κ saying "if κ then ⊥", contraction alone derives ⊥ — and contraction is the rule that lets a premise used twice be counted once. Drop it, and the derivation stops. The truth predicate is fully transparent, the connectives are classical, and what fails is the licence to reuse an assumption.

Formalism.

Curry's derivation: κ := T⌜κ⌝ → ⊥

  1. κ, κ ⊢ ⊥ (from transparency and →E)
  2. κ ⊢ ⊥ (contraction — the only non-trivial step)
  3. ⊢ κ (→I)
  4. ⊢ ⊥ (from 2, 3) Delete line 2 and nothing follows.

The structural rule: Γ, A, A ⊢ B ───────────── contraction Γ, A ⊢ B Without it, contexts are multisets whose multiplicities matter, and κ used twice is not κ used once.

Zardini's IKTω: An affine-style relevant base with a transparent T. Naive truth rules: from φ infer T⌜φ⌝ and back. Consistent, and non-triviality is proved by a cut-elimination argument.

Naive comprehension (Petersen, Cantini): The same move for set theory: {x : φ(x)} with full comprehension, consistent over a contraction-free base. Russell's paradox needs contraction for the same reason Curry does.

Contrast with the nontransitive answer: ST keeps contraction, drops cut, is classical at the inference level. IKTω keeps cut, drops contraction, is substructural at the inference level. Both keep every connective and the full T-schema. The two are the two ways to be structurally revisionary about the same paradoxes.

Cost: Without contraction, φ → (φ → ψ) and φ → ψ come apart. Mathematical induction and ordinary reasoning that reuses hypotheses need repair. Zardini's answer: a distinguished "stable" fragment where contraction holds.

Symbols.

SymbolUnicodeNameMeaning
κU+03BACurry sentenceT⌜κ⌝ → ⊥
U+22A2ConsequenceOver multiset contexts
TTruth predicateFully transparent
IKTωZardini's systemContraction-free with naive T
U+22A5FalsumWhat Curry would deliver

Metatheory. Non-triviality for the naive theories is proved by cut elimination, which is why the noncontractive route keeps cut: it is the tool. That the same paradox family yields to either dropping cut or dropping contraction — and to nothing weaker in the object language — is the substructural literature's main claim, and it locates the paradoxes in the structural rules rather than in truth or in negation. Zardini's systems have been shown to have unexpected weaknesses (Fjellstad, and Zardini's own later corrections about ω-inconsistency in some versions), and whether a naive theory survives the addition of ordinary arithmetic is where the argument now sits.

Applies to. Curry's paradox and naive truth. Naive set theory with full comprehension. Substructural logic's application to foundations. The classification of paradox responses by which structural rule they spend.

Limitations. Losing contraction is expensive in a way losing weakening is not: ordinary mathematics reuses hypotheses constantly, and a logic in which φ → (φ → ψ) does not give φ → ψ cannot support induction without a repair. The repairs — stable fragments, controlled contraction — reintroduce the rule where it is needed and owe an account of why the paradoxical cases are excluded that does not simply name them. And the ω-inconsistency results against particular systems suggest the approach is harder to make good on than the Curry derivation alone implies.

© 2026 Lingenic LLC