Reasoning Around Paradox with Grounded Deduction

TL;DR

This paper introduces grounded deduction, a novel logical framework inspired by Kripke semantics, enabling reasoning around paradoxes like 'L := not L' without inconsistency, by using dynamic typing premises.

Contribution

Grounded deduction is a new approach that allows direct expression of recursive and paradoxical definitions while maintaining consistency through dynamic typing.

Findings

Permits expression of recursive and paradoxical definitions

Prevents paradoxes from causing inconsistency

Offers a pragmatically usable alternative to classical logic

Abstract

How can we reason around logical paradoxes without falling into them? This paper introduces grounded deduction or GD, a Kripke-inspired approach to first-order logic and arithmetic that is neither classical nor intuitionistic, but nevertheless appears both pragmatically usable and intuitively justifiable. GD permits the direct expression of unrestricted recursive definitions -- including paradoxical ones such as 'L := not L' -- while adding dynamic typing premises to certain inference rules so that such paradoxes do not lead to inconsistency. This paper constitutes a preliminary development and investigation of grounded deduction, to be extended with further elaboration and deeper analysis of its intriguing properties.