論文の概要: Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

• arxiv url: http://arxiv.org/abs/2609.36279v2
• Date: Thu, 01 Oct 2026 16:36:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-03 01:19:23.515413
• Title: Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes
• Title（参考訳）: ノミナルな証明:ゲーデルのオントロジー論、その浅義の埋め込み、そしてモナトシェフトノートのオープンな疑問
• Abstract要約: Benzmller と Scott's Notes on Gdel's and Scott's variants of the Onlogical argument (2025) において、高階のモジュラー論理の浅い埋め込みはモジュラー対象言語を超えて到達する。 ノートが証明した全てのステートメントは、手書きとマシンチェックで書かれたオブジェクト言語294の内部に証明を持っているが、名目上は使用していない。 すべての定理はIsabelle/HOLで、独立してLean 4で検証されます。
• 参考スコア（独自算出の注目度）: 0.10152838128195468
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzmüller and Scott's Notes on Gödel's and Scott's variants of the ontological argument (2025), reaches beyond the modal object language of the arguments: its property quantifiers range over terms that may also express nominals and satisfaction operators of hybrid logic, and a proof using one proves a theorem of the embedding that need not be one of the modal logic. That the framework affords this is not new, and whether a result is one of the modal logic can be settled in two ways: by replaying it in an explicit proof calculus, done by hand for chosen theorems, or by analysing the proofs the embedding itself produces, done here mechanically, for every result at once. Every statement the Notes prove has a proof inside the object language: 294 written out by hand and machine-checked, none using a nominal. The proofs the Notes themselves give instantiate no nominal either; what the detector flags there are terms a prover substituted. The three questions the Notes leave open are settled too, without nominals, but the conjunction axiom has to be emended: generalised in the Notes to Gödel's "any number of summands", it covers the conjunction of no properties, and of one; the empty one alone settles all three, and the two together yield what a separate axiom of Gödel's is for. This article restricts the conjunction axiom to at least two different conjuncts, the reading Gödel's footnote suggests, and the questions are settled again, by proofs that turn on the argument rather than a degenerate instance. The restriction holds of the object language only: with a nominal the axioms make the accessibility relation the identity and the readings coincide. Every theorem is verified in Isabelle/HOL and independently in Lean 4; the countermodels are Nitpick's, certified by the build.
• Abstract（参考訳）: 古典的高階論理における高階モジュラー論理の浅い埋め込みは、ベンツミュラー(英語版)やスコットのゲーデルのノート(英語版)(2025年)やスコットのオントロジ論法(英語版)(英語版)の変種(英語版)(Notes on Gödel's and Scott's variants of the ontoological argument)で使用され、議論のモジュラー対象言語を超えて到達する:その性質の定量化は、ハイブリッド論理の名声や満足度演算子を表わすことができる用語の範囲に及び、一方を用いた証明は、モジュラー論理の1つではない埋め込みの定理を証明する。 フレームワークがこれを新しいものではなく、結果がモジュラー論理の1つであるかどうかを2つの方法で解決することができる: 明示的な証明計算でそれを再生することで、選択された定理に対して手作業で行うか、あるいは、埋め込み自体が生成する証明を機械的にここで機械的に、一度に全ての結果に対して行うかである。 ノートが証明したすべてのステートメントは、オブジェクト言語の内部で証明されている。 ノート自体の証明は、名目上も示さず、検出器のフラグは、証明者が代用した用語である。 ノートからゲーデルの「任意の数のサマンド」へのノートに一般化され、財産の連結を網羅し、1つが空のものだけで3つ全てを解決し、2つが共にゲーデルの別々の公理を成す。 この記事は、接続公理を少なくとも2つの異なる共役に制限し、ゲーデルの脚注が示唆し、これらの疑問は退化インスタンスではなく議論をオンにする証明によって再び解決される。 名目上の公理により、アクセシビリティーはアイデンティティと読み取りを一致させる。 すべての定理はIsabelle/HOLで、独立してLean 4で検証されます。

関連論文リスト

• Gödel's and Scott's Variants of the Ontological Argument in Lean 4 [0.10152838128195468]
  ポートは30個のLean 4加群で構成され、1つはIsabelle/HOL理論に従って、セクション構造、宣言順序、全ての公理、定義、補題、定理の名前を保持する。 イザベル/HOLの開発が証明した全てのことは、グデルの1970年の公理の不整合を含む、再び証明される。
  論文  参考訳（メタデータ） (2026-09-14T17:10:19Z)
• Revealed Rationality: Label-Free Evaluation and Regularization from Representation Theorems [0.0]
  行動が特定の公理を満たすという決定論の定理は、それが十分に定義された目的によって合理化できる場合に限る。 このことは、'構造がラベルのない評価とLLMやその他のAIシステムの正規化のための潜在的に有用な基盤を提供する場合に限る、と私は論じます。
  論文  参考訳（メタデータ） (2026-08-05T16:21:18Z)
• ARCHE: A Novel Task to Evaluate LLMs on Latent Reasoning Chain Extraction [70.53044880892196]
  本稿では、複雑な推論引数を標準推論パラダイムの組み合わせに分解し、Reasoning Logic Tree (RLT) という形で分解しなければならない、ARCHE(Latent Reasoning Chain extract)という新しいタスクを紹介する。 この作業を容易にするために,我々は,1,900以上の参照と38,000の視点を含む70のNature Communicationsの記事から得られた新しいベンチマークであるARCHE Benchをリリースする。 ARCHE Bench上での10のLLMの評価では、モデルがREAとECのトレードオフを示しており、完全な標準推論チェーンを抽出することはできません。
  論文  参考訳（メタデータ） (2025-11-16T07:37:09Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• Reasoning is about giving reasons [55.56111618153049]
  高い精度の3つの一般的な推論データセットにおいて、自然言語の引数の論理構造を同定し、抽出できることが示される。 我々のアプローチは、自然言語の引数の論理構造に依存するあらゆる推論形式をサポートする。
  論文  参考訳（メタデータ） (2025-08-20T07:26:53Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• MetaLogic: Logical Reasoning Explanations with Fine-Grained Structure [129.8481568648651]
  複雑な実生活シナリオにおけるモデルの論理的推論能力を調べるためのベンチマークを提案する。 推論のマルチホップ連鎖に基づいて、説明形式は3つの主成分を含む。 この新たな説明形式を用いて,現在のベストモデルの性能を評価した。
  論文  参考訳（メタデータ） (2022-10-22T16:01:13Z)
• Certain and Uncertain Inference with Indicative Conditionals [0.3437656066916039]
  我々は、真理条件と自然言語条件の確率の3値意味論を開発する。 いずれのフレームワークにおける推論の3価表現と確率表現の体系的対応を示す。 その結果は、条件推論の妥当性を分析するために有益に適用できる条件のセマンティクスと指示の統一的な説明である。
  論文  参考訳（メタデータ） (2022-07-17T20:06:00Z)
• AGM Belief Revision, Semantically [1.7403133838762446]
  最小限の変化のパラダイムを実装した信念修正演算子の汎用的モデル理論的特徴付けを確立する。 我々の特徴づけはすべてのタルスキア論理、すなわち古典的なモデル理論のセマンティクスを持つ全ての論理に適用できる。
  論文  参考訳（メタデータ） (2021-12-27T07:53:21Z)
• On abstract F-systems. A graph-theoretic model for paradoxes involving a falsity predicate and its application to argumentation frameworks [0.0]
  F-システム(F-systems)は、他の文の虚偽を述語する文をモデル化できるダイグラフである。 本稿では,表現された文が表現される言語の特徴をすべて抽象化するF-systemsモデルを提案する。
  論文  参考訳（メタデータ） (2020-05-14T15:07:11Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。