Fugu-MT 論文翻訳(概要): Incompleteness for stably consistent formal systems

論文の概要: Incompleteness for stably consistent formal systems

arxiv url: http://arxiv.org/abs/2001.07592v7
Date: Mon, 15 Aug 2022 16:37:50 GMT
ステータス: 処理完了
システム内更新日: 2023-01-08 00:28:40.131928
Title: Incompleteness for stably consistent formal systems
Title（参考訳）: 安定に一貫した形式システムに対する不完全性
Authors: Yasha Savelyev
Abstract要約: まず、人間の実際の一貫性性を反映した安定な一貫性の数学的概念を部分的に展開する。次に、第1および第2のG"odel不完全性定理を安定に1,2$一貫性のある形式系に一般化する。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We first partly develop a mathematical notion of stable consistency intended to reflect the actual consistency property of human beings. Then we give a generalization of the first and second G\"odel incompleteness theorem to stably $1,2$-consistent formal systems. Our argument in particular re-proves the original incompleteness theorems from first principles, using Turing machine language to (computably) construct our "G\"odel sentence" directly, in particular we do not use the diagonal lemma, nor any meta-logic, with the proof naturally formalizable in set theory. In practice such a stably consistent formal system could be meant to represent the mathematical output of humanity evolving in time, so that the above gives a formalization of a famous disjunction of G\"odel, obstructing computability of intelligence.
Abstract（参考訳）: まず、人間の実際の一貫性特性を反映した安定一貫性という数学的概念を部分的に発展させた。次に、第一および第二の g\"odel incompleteness theorem を、安定的に1,12$一貫性のある形式系に一般化する。我々の議論は、チューリング機械言語を用いて(計算可能)直接「g\"odel sentence」を構築するために、第一原理から元の不完全性定理を再証明する。実際には、安定的に一貫した形式体系は、時間とともに進化する人類の数学的アウトプットを表現することを目的としており、上記のことは、知性の計算可能性を妨げる有名なG\"odelの解離の形式化を与える。

関連論文リスト

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文参考訳（メタデータ） (2024-10-21T08:04:21Z)
Towards Generalizable and Faithful Logic Reasoning over Natural Language via Resolution Refutation [24.584926992534346]
本稿では,GFaiR(Generalizable and Faithful Reasoner)という新しいフレームワークを提案する。解法の難解化は、推論規則を拡張し、矛盾による証明の原理を採用することによって、全ての一階論理推論問題を解く能力を持つ。我々のシステムは、単純なシナリオでパフォーマンスを維持しながら、複雑なシナリオで最先端のパフォーマンスを達成することで、これまでの作業より優れています。
論文参考訳（メタデータ） (2024-04-02T06:28:44Z)
Normative Conditional Reasoning as a Fragment of HOL [0.0]
本稿では(参照に基づく)条件付き規範推論の機械化について論じる。我々の焦点は条件付き義務のためのAqvistのシステムEとその拡張である。フレームワークの2つの可能性について検討する。
論文参考訳（メタデータ） (2023-08-21T12:47:30Z)
A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
論文参考訳（メタデータ） (2023-06-29T18:35:41Z)
Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文参考訳（メタデータ） (2023-01-05T17:56:00Z)
Quantum Mechanics as a Theory of Incompatible Symmetries [77.34726150561087]
古典確率論が非互換変数を持つ任意の系を含むように拡張可能であることを示す。非互換な変数を持つ確率的システム(古典的あるいは量子的)が不確実性だけでなく、その確率パターンにも干渉することを示す。
論文参考訳（メタデータ） (2022-05-31T16:04:59Z)
NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
論文参考訳（メタデータ） (2022-05-25T17:01:18Z)
Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文参考訳（メタデータ） (2021-11-23T17:49:00Z)
Sequent-Type Calculi for Systems of Nonmonotonic Paraconsistent Logics [2.627046865670577]
シーケント型証明システムにおいて、最小の矛盾に基づく非単調パラ一貫性論理の族に対する一様公理を導入する。パラドックスの3値最小矛盾論理と、アリエリとアヴロンによる4値パラドックス推論関係について、シークエント型計算を提供する。
論文参考訳（メタデータ） (2020-09-22T00:49:52Z)
Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文参考訳（メタデータ） (2020-09-07T19:50:10Z)
Towards Concise, Machine-discovered Proofs of G\"odel's Two Incompleteness Theorems [3.222802562733787]
我々は、特異な論理に容易に適応したり、新たな推論プロセスを統合するように設計された、自動定理のための新しいフレームワークMATRを提案する。我々はMATRの高レベル設計と実装の詳細について説明する。次に、G"odelの不完全性定理の証明に適した形式化されたメタロジックを記述し、MATRにおける我々のメタロジックを用いて、第一不完全性定理と第二不完全性定理の両方の証明を半自動生成する進捗について報告する。
論文参考訳（メタデータ） (2020-05-06T03:29:34Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。