Greg Restall on Nostr: npub13g2ev…3m4y3 It’s a sweet result, and the undecidability proof is not an easy ...

npub13g2ev73ec8ylfdf5pazc2dwhsaaxhtrxxqc86ct7n2hg4epyyxgqu3m4y3 (npub13g2…m4y3) It’s a sweet result, and the undecidability proof is not an easy one. The result is highly sensitive to how the logic is formulated: the set of theorems of the Anderson–Belnap logic R[→,∧,∨] is not recursive. But if you weaken the logic slightly, by removing the constraint that [∧,∨] distribute, and consider the logic they call LR, in the same family of connectives, then the logic is decidable.

That decidability result for LR is a lot of fun: the logic has a simple sequent calculus presentation, without weakening, but with contraction. Getting control of contraction when engaging in proof-search in the cut-free calculus is not straightforward, but there's a sweet argument (amounting to Dickson’s Lemma, it turns out) that any search is finite.

Mike Dunn and I went through the details of these results in our handbook chapter, here <https://consequently.org/writing/rle/>;