arXiv subjects

Christoph Benzmüller

Publications and source records attributed to Christoph Benzmüller.

At least 19 recordsLinked to original sources

arXiv2026

Gödel's and Scott's Variants of the Ontological Argument in Lean 4

This paper presents a complete, structure-preserving port to Lean 4 of the Isabelle/HOL dataset accompanying Benzmüller and Scott's study of Gödel's modal ontological argument and Scott's variant of it. The port comprises 30 Lean 4 modules, one per Isabelle/HOL theory, retaining the section structure, the declaration order and the name of every axiom, definition, lemma and theorem; a comparison tool certifies all 548 statements identical. Everything the Isabelle/HOL development proves is proved again, including the inconsistency of Gödel's 1970 axioms, the repaired Gödel variants, Scott's variant, modal collapse, monotheism and the ultrafilter property of the positive properties; five statements the original leaves unreplayed after an automated prover had found a proof, one of which it then postulates, are proved as well. The 45 remaining unproved statements are exactly those the original refutes by nitpick (35) or leaves open (10); they are anonymous sorrys on which nothing depends. Two features of Lean 4 shape the result. It has neither a sledgehammer nor a model finder, so the one-line automated proofs become explicit proof terms and the 72 nitpick invocations are recorded as documentation. And #print axioms reports the postulates each proof consumes, giving for every result an upper bound on the modal logic it requires: Scott's necessary-existence theorem and modal collapse need only symmetry of the accessibility relation (logic KB); the essence and monotheism lemmas and the possible existence of a God-like being need no frame condition (the latter with the one exception the original records, the mixed-quantifier setting); and the inconsistency of Gödel's 1970 axioms needs none either. The development depends on no library beyond Lean 4's core; sources, comparison tools and two Isabelle cross-check sessions are included as ancillary files.

cs.LO↗

arXiv2026

A Comment on Modal Collapse and Ultrafilters in Gödel's Ontological Argument

Gödel's ontological argument is modal by design. Possibility and necessity are among its central concerns, and connected interpretation decisions -- extensions or intensions for the positive properties, constant or varying quantifier domains, the choice of modal logic, etc. -- subtly shape the argument and, in particular, whether the modal collapse is implied or not. It is tempting to abstract the modality away and to read the positive properties as merely forming an ultrafilter -- which, however, may replace Gödel's argument with a perhaps more manageable alternative that may have little to do with Gödel's original intention. In this spirit, Odifreddi and Gomes argue that modal collapse is an intrinsic structural feature of any theory that characterises positive properties as an ultrafilter and identifies God as its principal generator. This comment shows, with machine-verified counterexamples, that the structural claim is false: what drives the collapse is primarily not the filter structure but the rigidity of positivity -- itself a thoroughly modal condition. Moreover, two claims of Odifreddi and Gomes are corrected: one on the derivability of Gödel's Theorem IV, one on the extensionality of positivity. All results are machine-checked in Isabelle/HOL.

math.LO↗

arXiv2026

First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

We extend, in Isabelle/HOL, the deep-and-shallow embedding methodology of our prior work from propositional to first-order modal logic (FML) with constant-domain Kripke semantics. Three embeddings of FML into classical higher-order logic (HOL) are provided side by side: a deep embedding, a heavyweight maximal-shallow embedding, and a lightweight minimal-shallow embedding. The minimal-shallow embedding is presented as an Isabelle/HOL locale, parametrised by an accessibility relation, a world-indexed interpretation, a universe of worlds, and a variable assignment; the locale form admits a global faithfulness theorem, stating that quantifying over all minimal-shallow interpretations recovers exactly deep validity. A central technical contribution is a mechanisation, for FML under constant-domain Kripke semantics, of the (countable) downward Löwenheim-Skolem theorem, which underpins the automation of our faithfulness proof between the deep and minimal-shallow embeddings. Deploying it inside an extension of the minimal-shallow locale resolves the surjectivity problem that arises against an uncountable domain of individuals -- where the locale's variable assignment, having countable domain V = nat, cannot be surjective onto the domain -- and thereby yields faithfulness over the full domain. Since prior work treats only the propositional fragment, we develop here the substitution machinery (free/bound-variable predicates, the fresh-variable function, capture-avoiding substitution, alphabetic renaming, the substitutability predicate, the substitution lemma, and size-based induction principles) needed for the first-order quantifiers.

cs.AI↗

arXiv2026

Neuro-Symbolic Verification of LLM Outputs for Data-Sensitive Domains (extended preprint)

LLMs deployed in high-stakes domains face fundamental reliability challenges: hallucinations, inconsistencies, and privacy vulnerabilities introduce unacceptable risks where errors carry legal, financial, or safety consequences. This paper presents a hybrid verification architecture combining formal symbolic methods with neural semantic analysis to provide complementary guarantees for LLM-generated content. This architecture employs logical reasoning for input verification, leveraging completeness properties to provide decidable guarantees on structured requirements. For output validation, embedding-based semantic similarity detects contextual hallucinations where formal methods lack expressiveness. This separation is realized in a parallel, actor-based pipeline, addressing limitations of prompt-based self-verification approaches, which inherit the distributional biases that produce hallucinations. The proposed architecture and type-aware verification method are validated with HAIMEDA, a real-world medical device damage assessment reporting system developed through Action Design Research. Evaluation shows hallucination detection rates of over 83% for structured entities and 72% for semantic fabrications, with a 30% reduction in report creation time, demonstrating that neuro-symbolic architectures can provide principled safeguards for LLM deployment in data-sensitive domains.

cs.AI↗

arXiv2026

Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)

This position statement looks back on two decades of work on shallow embeddings of non-classical logics in classical higher-order logic (HOL), a line of research that expanded into a range of logic embeddings in HOL and inspired the LogiKEy logic-pluralistic knowledge representation and reasoning methodology. This paper advances the case for logical pluralism at object-logic level within a unifying meta-logical framework such as LogiKEy, grounding the argument in computational metaphysics. More broadly, it advocates principled support for logical pluralism in modern proof assistants, and cautions against logical imperialism -- the rigid adoption of a single foundational logic for large-scale theory developments -- which impedes the interdisciplinary reuse that LogiKEy is designed to enable.

cs.LO↗

arXiv2025

Faithful Logic Embeddings in HOL -- Deep and Shallow

Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embeddings. The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic. However, this approach is conceptual in nature and not limited to this simple logic context.

cs.LO↗

arXiv2025

Logical Modalities within the European AI Act: An Analysis

The paper presents a comprehensive analysis of the European AI Act in terms of its logical modalities, with the aim of preparing its formal representation, for example, within the logic-pluralistic Knowledge Engineering Framework and Methodology (LogiKEy). LogiKEy develops computational tools for normative reasoning based on formal methods, employing Higher-Order Logic (HOL) as a unifying meta-logic to integrate diverse logics through shallow semantic embeddings. This integration is facilitated by Isabelle/HOL, a proof assistant tool equipped with several automated theorem provers. The modalities within the AI Act and the logics suitable for their representation are discussed. For a selection of these logics, embeddings in HOL are created, which are then used to encode sample paragraphs. Initial experiments evaluate the suitability of these embeddings for automated reasoning, and highlight key challenges on the way to more robust reasoning capabilities.

cs.AI↗

arXiv2024

Script-Based Dialog Policy Planning for LLM-Powered Conversational Agents: A Basic Architecture for an "AI Therapist"

Large Language Model (LLM)-Powered Conversational Agents have the potential to provide users with scaled behavioral healthcare support, and potentially even deliver full-scale "AI therapy'" in the future. While such agents can already conduct fluent and proactive emotional support conversations, they inherently lack the ability to (a) consistently and reliably act by predefined rules to align their conversation with an overarching therapeutic concept and (b) make their decision paths inspectable for risk management and clinical evaluation -- both essential requirements for an "AI Therapist". In this work, we introduce a novel paradigm for dialog policy planning in conversational agents enabling them to (a) act according to an expert-written "script" that outlines the therapeutic approach and (b) explicitly transition through a finite set of states over the course of the conversation. The script acts as a deterministic component, constraining the LLM's behavior in desirable ways and establishing a basic architecture for an AI Therapist. We implement two variants of Script-Based Dialog Policy Planning using different prompting techniques and synthesize a total of 100 conversations with LLM-simulated patients. The results demonstrate the feasibility of this new technology and provide insights into the efficiency and effectiveness of different implementation variants.

cs.CL↗

arXiv2024

Normative Conditional Reasoning as a Fragment of HOL

We report on the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. Our mechanization is achieved via a shallow semantical embedding in Isabelle/HOL. We consider two possible uses of the framework. The first one is as a tool for meta-reasoning about the considered logic. We employ it for the automated verification of deontic correspondences (broadly conceived) and related matters, analogous to what has been previously achieved for the modal logic cube. The equivalence is automatically verified in one direction, leading from the property to the axiom. The second use is as a tool for assessing ethical arguments. We provide a computer encoding of a well-known paradox (or impossibility theorem) in population ethics, Parfit's repugnant conclusion. While some have proposed overcoming the impossibility theorem by abandoning the presupposed transitivity of ''better than'', our formalisation unveils a less extreme approach, suggesting among other things the option of weakening transitivity suitably rather than discarding it entirely. Whether the presented encoding increases or decreases the attractiveness and persuasiveness of the repugnant conclusion is a question we would like to pass on to philosophy and ethics.

cs.LO↗

arXiv2024

Solving Quantified Modal Logic Problems by Translation to Classical Logics

This article describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to both typed first-order and higher-order logic in the TPTP language using an embedding approach, and solved using first-order resp. higher-order logic ATP systems and model finders. Additionally, the results from native modal logic ATP systems are considered, and compared with the results from the embedding approach. The findings are that the embedding process is reliable and successful when state-of-the-art ATP systems are used as backend reasoners, The first-order and higher-order embeddings perform similarly, native modal logic ATP systems have comparable performance to classical systems using the embedding for proving theorems, native modal logic ATP systems are outperformed by the embedding approach for disproving conjectures, and the embedding approach can cope with a wider range of modal logics than the native modal systems considered.

cs.LO↗

arXiv2024

Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection

Many European citizens become targets of the Kremlin propaganda campaigns, aiming to minimise public support for Ukraine, foster a climate of mistrust and disunity, and shape elections (Meister, 2022). To address this challenge, we developed ''Check News in 1 Click'', the first NLP-empowered pro-Kremlin propaganda detection application available in 7 languages, which provides the lay user with feedback on their news, and explains manipulative linguistic features and keywords. We conducted a user study, analysed user entries and models' behaviour paired with questionnaire answers, and investigated the advantages and disadvantages of the proposed interpretative solution.

cs.CL↗

arXiv2023

A Simplified Variant of Gödel's Ontological Argument

A simplified variant of Gödel's ontological argument is presented. The simplified argument is valid already in basic modal logics K or KT, it does not suffer from modal collapse, and it avoids the rather complex predicates of essence (Ess.) and necessary existence (NE) as used by Gödel. The variant presented has been obtained as a side result of a series of theory simplification experiments conducted in interaction with a modern proof assistant system. The starting point for these experiments was the computer encoding of Gödel's argument, and then automated reasoning techniques were systematically applied to arrive at the simplified variant presented. The presented work thus exemplifies a fruitful human-computer interaction in computational metaphysics. Whether the presented result increases or decreases the attractiveness and persuasiveness of the ontological argument is a question I would like to pass on to philosophy and theology.

cs.LO↗

arXiv2023

PapagAI:Automated Feedback for Reflective Essays

Written reflective practice is a regular exercise pre-service teachers perform during their higher education. Usually, their lecturers are expected to provide individual feedback, which can be a challenging task to perform on a regular basis. In this paper, we present the first open-source automated feedback tool based on didactic theory and implemented as a hybrid AI system. We describe the components and discuss the advantages and disadvantages of our system compared to the state-of-art generative large language models. The main objective of our work is to enable better learning outcomes for students and to complement the teaching activities of lecturers.

cs.AI↗

arXiv2023

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation

This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization of the notion of elementary topoi. Additionally, we formalize symmetrical monoidal closed categories expressing the denotational semantic model of intuitionistic multiplicative linear logic. Next to these meta-logical-investigations, we contribute to building an Isabelle category theory library, with a focus on ease of use in the formalization beyond category theory itself. This work paves the way for future formalizations based on category theory and demonstrates the power of automated reasoning in investigating meta-logical questions.

cs.LO↗

arXiv2023

Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint

Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a theorem prover for DHOL.

cs.LO↗

arXiv2023

Automated multilingual detection of Pro-Kremlin propaganda in newspapers and Telegram posts

The full-scale conflict between the Russian Federation and Ukraine generated an unprecedented amount of news articles and social media data reflecting opposing ideologies and narratives. These polarized campaigns have led to mutual accusations of misinformation and fake news, shaping an atmosphere of confusion and mistrust for readers worldwide. This study analyses how the media affected and mirrored public opinion during the first month of the war using news articles and Telegram news channels in Ukrainian, Russian, Romanian and English. We propose and compare two methods of multilingual automated pro-Kremlin propaganda identification, based on Transformers and linguistic features. We analyse the advantages and disadvantages of both methods, their adaptability to new genres and languages, and ethical considerations of their usage for content moderation. With this work, we aim to lay the foundation for further development of moderation tools tailored to the current conflict.

cs.CL↗

arXiv2022

Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers

This paper reports on an exploration of Boolos' Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos' and related examples now seems to be within reach of higher-order ATPs.

math.LO↗

arXiv2022

Mathematical Proof Between Generations

A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time this has been a topic for experts in specialized communities. However, mathematical proofs have become increasingly sophisticated, stretching the boundaries of what is humanly comprehensible, so that leading mathematicians have asked for formal verification of their proofs. At the same time, major theorems in mathematics have recently been computer-verified by people from outside of these communities, even by beginning students. This article investigates the gap between the different definitions of a proof and possibilities to build bridges. It is written as a polemic or a collage by different members of the communities in mathematics and computer science at different stages of their careers, challenging well-known preconceptions and exploring new perspectives.

math.HO↗