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⌜κ⌝ → ⊥

κ, κ ⊢ ⊥ (from transparency and →E)
κ ⊢ ⊥ (contraction — the only non-trivial step)
⊢ κ (→I)
⊢ ⊥ (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.

Symbol	Unicode	Name	Meaning
κ	U+03BA	Kappa / Curry sentence	T⌜κ⌝ → ⊥
⊢	U+22A2	Right tack / Turnstile	Consequence over multiset contexts
→	U+2192	Rightwards arrow / Conditional	Detachable; φ → (φ → ψ) does not give φ → ψ
⊥	U+22A5	Up tack / Falsum	What Curry would deliver
Γ	U+0393	Gamma / Context	Multiset whose multiplicities matter
⌜	U+231C	Top left corner / Quasi-quotation	Opens a name of a sentence
⌝	U+231D	Top right corner / Quasi-quotation	Closes a name of a sentence
ω	U+03C9	Omega	Index in IKTω; also the ω-rule at issue
φ	U+03C6	Phi	Schematic sentence
ψ	U+03C8	Psi	Schematic sentence
T	—	Truth predicate	Fully transparent
IKTω	—	Zardini's system	Contraction-free with naive T
ST	—	Strict-Tolerant	The rival that drops cut instead

Metatheory. Non-triviality for the naive theories is proved by cut elimination, which is why the noncontractive route keeps cut: it is the instrument of the proof rather than a casualty of it. Zardini's IKTω combines a contraction-free base with fully transparent truth rules and is shown non-trivial by that argument (2011); Grišin (1982) and Petersen (2000) established the corresponding result for unrestricted comprehension, and Terui (2004) showed that naive comprehension over light affine logic is not merely non-trivial but has exactly the polynomial-time computable functions as its provably total ones. Dropping contraction separates φ → (φ → ψ) from φ → ψ, which is the step Curry's derivation requires and the step Russell's requires too, so both fail for one reason. The route has known casualties: IKTω has been shown to be ω-inconsistent (Fjellstad), so whether a naive noncontractive theory survives the addition of ordinary arithmetic is the open question. ST and IKTω are the two developed structural options — one drops cut, the other contraction — and each retains every connective and the full T-schema.

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 drop.

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 mathematical induction without a repair. The consistent contraction-free theories are correspondingly weak — over light affine logic the provably total functions reach only polynomial time, far short of the arithmetic the naive theory was meant to accommodate. The repairs, whether stable fragments or controlled contraction, reinstate the rule exactly where it is wanted and still need an account of why the paradoxical instances fall outside that does not merely list them. And the ω-inconsistency of IKTω shows the difficulty is not hypothetical: the naive rules and the standard model of arithmetic do not sit together, so either standard models or the unrestricted truth rules must go — the concession the approach was designed to avoid.