Related papers: Incompleteness for stably consistent formal systems

Related papers

No Universal Hyperbola: A Formal Disproof of the Epistemic Trade-Off Between Certainty and Scope in Symbolic and Generative AI [0.0]
We disprove a conjectured artificial intelligence trade-off between certainty and scope in the universal hyperbolic product form.<n>We show, first, that when the conjecture is instantiated with prefix (self-delimiting, prefix-free) Kolmogorov complexity, it leads to an internal inconsistency, and second, that when it is instantiated with plain Kolmogorov complexity, it is refuted by a constructive counterexample.
arXiv Detail & Related papers (2025-12-21T20:04:40Z)
An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction [8.21204701022347]
This paper proposes a novel automated theorem generation theory and tool.<n>It defines and proves, for the first time, a new logical structure known as rectangular standard contradiction.<n>To implement this theory, an efficient template-based ATG algorithm is designed.
arXiv Detail & Related papers (2025-11-06T06:03:54Z)
A Unified Formal Theory on the Logical Limits of Symbol Grounding [0.65268245109828]
We show that meaning within a formal system must arise from a process that is external, dynamic, and non-algorithmic.<n>We extend this limitation to systems with any finite, static set of pre-established meanings.
arXiv Detail & Related papers (2025-09-24T05:40:08Z)
Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory [0.0]
This paper contributes to the Alpay Algebra by demonstrating that the stable outcome of a self referential process is identical to the unique equilibrium of an unbounded revision dialogue between a system and its environment.<n>By unifying concepts from fixed point theory, game semantics, ordinal analysis, and type theory, this research establishes a broadly accessible yet formally rigorous foundation for reasoning about infinite self referential systems.
arXiv Detail & Related papers (2025-07-25T13:12:55Z)
Immutability Does Not Guarantee Trust: A Formal and Logical Refutation [0.0]
We define immutability as the cryptographic persistence of historical states in an append-only data structure.<n>We demonstrate that immutability neither entails nor implies correctness, fairness, or credibility.
arXiv Detail & Related papers (2025-07-08T09:35:52Z)
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
arXiv Detail & Related papers (2025-06-05T03:16:08Z)
DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
arXiv Detail & Related papers (2025-05-29T17:59:39Z)
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation. For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
arXiv Detail & Related papers (2024-10-21T08:04:21Z)
Towards Generalizable and Faithful Logic Reasoning over Natural Language via Resolution Refutation [24.584926992534346]
We propose a novel framework, named Generalizable and Faithful Reasoner (GFaiR), which introduces the paradigm of resolution refutation. Resolution refutation has the capability to solve all first-order logic reasoning problems by extending reasoning rules and employing the principle of proof by contradiction. Our system outperforms previous works by achieving state-of-the-art performances in complex scenarios while maintaining performances in simple scenarios.
arXiv Detail & Related papers (2024-04-02T06:28:44Z)
Normative Conditional Reasoning as a Fragment of HOL [0.0]
We discuss the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. We consider two possible uses of the framework.
arXiv Detail & Related papers (2023-08-21T12:47:30Z)
A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
We propose a hybrid system capable of solving arithmetic problems that require compositional and systematic reasoning over sequences of symbols. We show that the proposed system can accurately solve nested arithmetical expressions even when trained only on a subset including the simplest cases.
arXiv Detail & Related papers (2023-06-29T18:35:41Z)
Connecting classical finite exchangeability to quantum theory [69.62715388742298]
Exchangeability is a fundamental concept in probability theory and statistics. We show how a de Finetti-like representation theorem for finitely exchangeable sequences requires a mathematical representation which is formally equivalent to quantum theory.
arXiv Detail & Related papers (2023-06-06T17:15:19Z)
Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. We introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover.
arXiv Detail & Related papers (2023-01-05T17:56:00Z)
Quantum Mechanics as a Theory of Incompatible Symmetries [77.34726150561087]
We show how classical probability theory can be extended to include any system with incompatible variables. We show that any probabilistic system (classical or quantal) that possesses incompatible variables will show not only uncertainty, but also interference in its probability patterns.
arXiv Detail & Related papers (2022-05-31T16:04:59Z)
NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
Theorem proving in natural mathematical language plays a central role in mathematical advances and education. We develop NaturalProver, a language model that generates proofs by conditioning on background references. NaturalProver is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time.
arXiv Detail & Related papers (2022-05-25T17:01:18Z)
Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
We build a rule-based system that can reason with natural language input but without the manual construction of rules. We propose MetaQNL, a "Quasi-Natural" language that can express both formal logic and natural language sentences. Our approach achieves state-of-the-art accuracy on multiple reasoning benchmarks.
arXiv Detail & Related papers (2021-11-23T17:49:00Z)
Sequent-Type Calculi for Systems of Nonmonotonic Paraconsistent Logics [2.627046865670577]
We introduce uniform axiomatisations for a family of nonmonotonic paraconsistent logics based on minimal inconsistency in terms of sequent-type proof systems. We provide sequent-type calculi for Priest's three-valued minimally inconsistent logic of paradox, and for four-valued paraconsistent inference relations due to Arieli and Avron.
arXiv Detail & Related papers (2020-09-22T00:49:52Z)
Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
arXiv Detail & Related papers (2020-09-07T19:50:10Z)
Towards Concise, Machine-discovered Proofs of G\"odel's Two Incompleteness Theorems [3.222802562733787]
We present MATR, a new framework for automated theorem proving explicitly designed to easily adapt to unusual logics or integrate new reasoning processes. We explain the high-level design of MATR as well as some details of its implementation. We then describe a formalized metalogic suitable for proofs of G"odel'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.
arXiv Detail & Related papers (2020-05-06T03:29:34Z)

This list is automatically generated from the titles and abstracts of the papers in this site.