Applying Second-Order Quantifier Elimination in Inspecting G\"odel's Ontological Proof

• URL: http://arxiv.org/abs/2110.11108v1
• Date: Thu, 21 Oct 2021 12:50:23 GMT
• Title: Applying Second-Order Quantifier Elimination in Inspecting G\"odel's Ontological Proof
• Authors: Christoph Wernhard
• Abstract summary: Formula macros are used to structure complex formulas and tasks. G"odel's ontological proof and variations are formalized and analyzed with automated tools.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In recent years, G\"odel's ontological proof and variations of it were formalized and analyzed with automated tools in various ways. We supplement these analyses with a modeling in an automated environment based on first-order logic extended by predicate quantification. Formula macros are used to structure complex formulas and tasks. The analysis is presented as a generated type-set document where informal explanations are interspersed with pretty-printed formulas and outputs of reasoners for first-order theorem proving and second-order quantifier elimination. Previously unnoticed or obscured aspects and details of G\"odel's proof become apparent. Practical application possibilities of second-order quantifier elimination are shown and the encountered elimination tasks may serve as benchmarks.

Related papers

• Multi-Agent Procedural Graph Extraction with Structural and Logical Refinement [66.51979814832332]
  model formulates procedural graph extraction as a multi-round reasoning process with dedicated structural and logical refinement.<n>Experiments demonstrate that model achieves substantial improvements in both structural correctness and logical consistency over strong baselines.
  arXiv  Detail & Related papers  (2026-01-27T04:00:48Z)
• SIGMA: Scalable Spectral Insights for LLM Collapse [51.863164847253366]
  We introduce SIGMA (Spectral Inequalities for Gram Matrix Analysis), a unified framework for model collapse.<n>By utilizing benchmarks that deriving and deterministic bounds on the matrix's spectrum, SIGMA provides a mathematically grounded metric to track the contraction of the representation space.<n>We demonstrate that SIGMA effectively captures the transition towards states, offering both theoretical insights into the mechanics of collapse.
  arXiv  Detail & Related papers  (2026-01-06T19:47:11Z)
• HalluZig: Hallucination Detection using Zigzag Persistence [0.1687274452793636]
  We introduce a new paradigm for hallucination detection by analyzing the dynamic topology of model's layer-wise attention.<n>Our core hypothesis is that factual and hallucinated generations exhibit distinct topological signatures.<n>We validate our framework, HalluZig, on multiple benchmarks, demonstrating that it outperforms strong baselines.
  arXiv  Detail & Related papers  (2026-01-04T14:55:43Z)
• "You Are An Expert Linguistic Annotator": Limits of LLMs as Analyzers of Abstract Meaning Representation [60.863629647985526]
  We examine the successes and limitations of the GPT-3, ChatGPT, and GPT-4 models in analysis of sentence meaning structure. We find that models can reliably reproduce the basic format of AMR, and can often capture core event, argument, and modifier structure. Overall, our findings indicate that these models out-of-the-box can capture aspects of semantic structure, but there remain key limitations in their ability to support fully accurate semantic analyses or parses.
  arXiv  Detail & Related papers  (2023-10-26T21:47:59Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  We propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability.
  arXiv  Detail & Related papers  (2023-10-16T08:42:39Z)
• Restoration-Degradation Beyond Linear Diffusions: A Non-Asymptotic Analysis For DDIM-Type Samplers [90.45898746733397]
  We develop a framework for non-asymptotic analysis of deterministic samplers used for diffusion generative modeling. We show that one step along the probability flow ODE can be expressed as two steps: 1) a restoration step that runs ascent on the conditional log-likelihood at some infinitesimally previous time, and 2) a degradation step that runs the forward process using noise pointing back towards the current gradient.
  arXiv  Detail & Related papers  (2023-03-06T18:59:19Z)
• Mutual Exclusivity Training and Primitive Augmentation to Induce Compositionality [84.94877848357896]
  Recent datasets expose the lack of the systematic generalization ability in standard sequence-to-sequence models. We analyze this behavior of seq2seq models and identify two contributing factors: a lack of mutual exclusivity bias and the tendency to memorize whole examples. We show substantial empirical improvements using standard sequence-to-sequence models on two widely-used compositionality datasets.
  arXiv  Detail & Related papers  (2022-11-28T17:36:41Z)
• Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought [10.524051272257614]
  Large language models (LLMs) have shown remarkable reasoning capabilities given chain-of-thought prompts. We present a new synthetic question-answering dataset called PrOntoQA, where each example is generated as a synthetic world model. This allows us to parse the generated chain-of-thought into symbolic proofs for formal analysis.
  arXiv  Detail & Related papers  (2022-10-03T21:34:32Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)
• Sequential Learning of the Topological Ordering for the Linear Non-Gaussian Acyclic Model with Parametric Noise [6.866717993664787]
  We develop a novel sequential approach to estimate the causal ordering of a DAG. We provide extensive numerical evidence to demonstrate that our procedure is scalable to cases with possibly thousands of nodes.
  arXiv  Detail & Related papers  (2022-02-03T18:15:48Z)
• 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)
• Generating Fact Checking Explanations [52.879658637466605]
  A crucial piece of the puzzle that is still missing is to understand how to automate the most elaborate part of the process. This paper provides the first study of how these explanations can be generated automatically based on available claim context. Our results indicate that optimising both objectives at the same time, rather than training them separately, improves the performance of a fact checking system.
  arXiv  Detail & Related papers  (2020-04-13T05:23:25Z)
• Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic [0.0]
  PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It supports a workflow based on documents that intersperse macro definitions, invocations of reasoners, andformatted natural language text.
  arXiv  Detail & Related papers  (2020-02-24T16:09:10Z)

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

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.