Towards Concise, Machine-discovered Proofs of Gödel's Two Incompleteness Theorems
This work addresses the challenge of automating complex reasoning tasks in formal logic, which could benefit researchers in AI and automated theorem proving, though it appears incremental as it builds on existing methods with a new framework.
The authors tackled the problem of automated theorem proving by introducing MATR, a flexible framework designed to adapt to various logics and integrate new reasoning processes, and demonstrated its utility by semi-autonomously generating proofs of Gödel's First and Second Incompleteness Theorems using a formalized metalogic.
There is an increasing interest in applying recent advances in AI to automated reasoning, as it may provide useful heuristics in reasoning over formalisms in first-order, second-order, or even meta-logics. To facilitate this research, we present MATR, a new framework for automated theorem proving explicitly designed to easily adapt to unusual logics or integrate new reasoning processes. MATR is formalism-agnostic, highly modular, and programmer-friendly. We explain the high-level design of MATR as well as some details of its implementation. To demonstrate MATR's utility, we then describe a formalized metalogic suitable for proofs of Gödel's Incompleteness Theorems, and report on our progress using our metalogic in MATR to semi-autonomously generate proofs of both the First and Second Incompleteness Theorems.