Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reasoning Around Paradox with Grounded Deduction

Bryan Ford

TL;DR

This paper proposes grounded deduction (GD), a Kripke-inspired logic for first-order logic and arithmetic that combines unrestricted recursive definitions with typed premises to prevent paradoxes. GD weakens the law of excluded middle while preserving practical deduction techniques, enabling definitions like $L\equiv\neg L$ and other self-referential constructs without explosion, and it treats judgments as terms to unify truth and computation. The work develops a formal GD system (propositional and predicate calculus, with natural number arithmetic), a restricted GA (Grounded Arithmetic) fragment, and a computational interpretation via BSOS, PCF, and PPF, together with a denotational semantics and reflective reasoning concepts (Gödel coding, REM). It then sketches the relationship to primitive recursive arithmetic, the potential for real numbers and Cantor-like constructions under grounding, and avenues for further exploration, including meta-logical considerations and the prospects for extending GD toward richer foundational frameworks. Overall, the approach aims to offer a robust, paradox-tolerant foundation for mathematics and computation that preserves practical reasoning while carefully managing self-reference and infinite dependencies.

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.

Reasoning Around Paradox with Grounded Deduction

TL;DR

This paper proposes grounded deduction (GD), a Kripke-inspired logic for first-order logic and arithmetic that combines unrestricted recursive definitions with typed premises to prevent paradoxes. GD weakens the law of excluded middle while preserving practical deduction techniques, enabling definitions like and other self-referential constructs without explosion, and it treats judgments as terms to unify truth and computation. The work develops a formal GD system (propositional and predicate calculus, with natural number arithmetic), a restricted GA (Grounded Arithmetic) fragment, and a computational interpretation via BSOS, PCF, and PPF, together with a denotational semantics and reflective reasoning concepts (Gödel coding, REM). It then sketches the relationship to primitive recursive arithmetic, the potential for real numbers and Cantor-like constructions under grounding, and avenues for further exploration, including meta-logical considerations and the prospects for extending GD toward richer foundational frameworks. Overall, the approach aims to offer a robust, paradox-tolerant foundation for mathematics and computation that preserves practical reasoning while carefully managing self-reference and infinite dependencies.

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.
Paper Structure (111 sections, 103 equations, 3 figures, 4 tables)

This paper contains 111 sections, 103 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Pythagoras visits Epimenides
  3. The paradoxes in classical and alternative logics
  4. Introducing grounded deduction (GD)
  5. Propositional deduction in GD
  6. Boolean truth values
  7. Type judgments and inference rules
  8. Proof by contradiction in GD
  9. Judgments as terms
  10. Logical negation $\neg$
  11. Definitions, self-reference, and paradox
  12. Using definitions
  13. First-class definitions versus metalogical abbreviations
  14. The Liar Paradox
  15. Logical conjunction $\land$ and disjunction $\lor$
  16. ...and 96 more sections

Figures (3)

  • Figure 1: An impossibility triangle for logic. We may desire our logical reasoning to be (fully) consistent, to give us (unrestricted) use of the law of excludded middle or LEM, and to give us (unrestricted) recursive definition capability. It appears we must compromise at least one of these desires, however.
  • Figure 2: A decision diagram illustrating a choice among three type disciplines: agnostic types, coded types, or disjoint types.
  • Figure 3: Working use of a system of logic $L_0$ to reason about ordinary objects such as numbers and sets.