Fact-checked by Grok 2 weeks ago

Logic translation

Logic translation encompasses the process of representing natural language arguments in the formal language of a logical system, as well as mappings between different formal logical systems. In the latter sense, it is a formal mapping, or morphism, between logical systems that preserves the entailment relation, ensuring that if a set of formulas entails another in the source logic, their images under the translation entail the image of the target formula in the destination logic.^[1] This abstract notion applies without presupposing specific syntactic structures for sentences or the nature of logical consequence, encompassing both proof-theoretic approaches (based on deduction) and model-theoretic ones (based on satisfaction in structures).^[2] Such translations enable the embedding of one logic into another, facilitating comparisons of their expressive power and structural properties. The development of translations between logical systems emerged in the 1920s and 1930s through efforts to establish intertranslatability between classical logic and intuitionistic logic, with key contributions from mathematicians including Andrei Kolmogorov, Dmitri Glivenko, Kurt Gödel, and Gerhard Gentzen.^[2] These early works, such as Kolmogorov's double-negation embedding of classical propositional logic into intuitionistic logic, demonstrated how translations could preserve validity while highlighting differences in logical strength.^[1] In modern treatments, translations are often formalized using category theory or institutions, where they induce hierarchies of logical expressiveness (the ability to discriminate between non-equivalent formulas), consistency strength (the robustness of theorem sets), and sublogics (weaker variants within a given logic).^[2] Beyond historical foundations, logic translations play a crucial role in resolving paradoxes, such as those concerning whether a sublogic can fully express its parent logic, by refining definitions of conservativeness (where the converse preservation holds) and recoverability of connectives and quantifiers.^[1] For instance, conservative translations ensure no new theorems are introduced in the target logic beyond those derivable from the source, while surjective mappings allow reconstruction of source connectives like negation or implication.^[2] Applications extend to non-classical logics, including modal and dynamic logics, where translations aid in combining systems or verifying properties across frameworks.^[3]

Fundamentals

Definition

Logic translation refers to the process of mapping expressions from a source logic—such as propositional logic—to a target logical system, such as first-order logic, in a way that preserves the semantic content and inferential structure of the original expressions.^[4] This mapping ensures that the logical relationships, including entailments and valid inferences, are maintained across the systems, facilitating analysis, reasoning, and comparison without loss of meaning.^[4] Formally, a logic translation is defined as a structure-preserving mapping between the consequence relations of two logics, where if a set of formulas Γ entails a formula ϕ in the source logic (denoted Γ ⊢ ϕ), then the image of Γ under the translation entails the image of ϕ in the target logic (α(Γ) ⊢ α(ϕ)).^[5] This preservation of validity holds without requiring identical syntax between the source and target, as introduced in foundational works on translations between logics. Unlike mere interpretations, which assign truth values to formulas within a single model-theoretic framework to evaluate semantic satisfaction, logic translations emphasize syntactic-semantic equivalence by embedding one system's expressive power into another while conserving logical properties.^[6] The key components of a logic translation include the source logic, which provides the initial expressions to be mapped; the target logic, into which the expressions are transformed; and faithfulness conditions such as soundness (ensuring that valid source inferences remain valid in the target) and completeness (ensuring that target-valid inferences correspond to source-valid ones, often in conservative translations).^[7] These elements collectively enable the translation to function as a bridge for interoperability between diverse logical frameworks, supporting applications in philosophy, computer science, and linguistics.^[4]

Historical Development

The modern formalization of logic translation emerged in the early 20th century, influenced by foundational results in proof and model theory. Kurt Gödel's 1930 completeness theorem for first-order logic established that every semantically valid formula is provable, providing a semantic criterion for assessing the fidelity of translations between syntactic systems and their models.^[8] In the 1930s, Arend Heyting's formalization of intuitionistic logic spurred the creation of negative translations to embed classical logic into intuitionistic logic. Key contributions included Andrei Kolmogorov's 1925 double-negation embedding for propositional logic, Dmitri Glivenko's 1929 extension to predicate logic, and stronger embeddings by Gödel (1932) and Gerhard Gentzen (1933).^[9]^[10] These works preserved provability while highlighting differences, such as the rejection of the law of excluded middle in intuitionistic logic. This period marked a shift toward inter-system translations, using consequence relations to embed one logic conservatively into another. João Marcos's 2009 framework further abstracted logic translation as a morphism preserving consequence relations between logics, allowing rigorous comparisons of deductive strength across diverse systems like classical and paraconsistent logics.^[4] Post-2000 developments have deepened these foundations by integrating proof theory and category theory, facilitating translations between non-classical logics such as from intuitionistic to linear logic. Proof-theoretic methods, emphasizing cut-elimination and normalization, ensure translations maintain structural properties like resource sensitivity in linear logic embeddings.^[11] Category-theoretic approaches, including fibring, model logics as categories with functors as translations, enabling modular combinations of non-classical systems while preserving semantics and proofs.^[12]

Types of Logic Translation

Natural Language Formalization

Natural language formalization involves translating ambiguous, context-dependent statements from everyday language into precise expressions in formal logical systems, such as propositional or first-order predicate logic, to enable rigorous analysis and inference. This process requires careful identification of logical components within the sentence, including connectives (like "and," "or," "not"), predicates (properties or relations), quantifiers ("all," "some," "no"), and variables representing objects, while resolving inherent ambiguities in scope, reference, and implication.^[13] The formalization begins by parsing the sentence to extract its propositional structure for simple cases without quantification, assigning atomic propositions to basic assertions. For instance, the statement "It is raining and cold" can be formalized in propositional logic as P \land Q, where P denotes "It is raining" and Q denotes "It is cold," allowing evaluation of truth values based on the connectives. More complex sentences introduce predicates and quantifiers in first-order logic; the predicate "Man(x)" might represent "x is a man," and universal quantification applies to generalizations like "All men are mortal," rendered as \forall x (Man(x) \to Mortal(x)), capturing the implication that if something is a man, then it is mortal. Similarly, "Some birds fly" translates to \exists x (Bird(x) \land Flies(x)), asserting the existence of at least one entity satisfying both properties.^[13]^[13] Handling scope ambiguity is a key challenge, particularly with multiple quantifiers, where the order affects meaning. Consider "Every boy loves a girl": this can formalize as \forall x (Boy(x) \to \exists y (Girl(y) \land Loves(x, y))), meaning for each boy there exists (possibly different) girl he loves, or alternatively \exists y (Girl(y) \land \forall x (Boy(x) \to Loves(x, y))), implying there is one girl loved by all boys. The appropriate reading depends on contextual inference, often requiring paraphrasing the natural language sentence for clarity, such as rephrasing to "For every boy, there is some girl he loves" to disambiguate the wide scope of the existential quantifier.^[13] Definite descriptions, like "the king of France," pose further issues due to presuppositions of uniqueness and existence, which Russell addressed by analyzing them as scoped quantifiers rather than referring terms. In his theory of descriptions, the sentence "The king of France is bald" is formalized not as a simple predication but as an existential claim with uniqueness: there exists an x such that x is king of France, x is unique in that property, and x is bald, expressed as \exists x (KingOfFrance(x) \land \forall y (KingOfFrance(y) \to y = x) \land Bald(x)). This approach eliminates paradoxes arising from non-referring descriptions by treating them as incomplete symbols within the overall proposition.^[14] Propositional logic suits unquantified sentences for basic truth-functional analysis, while first-order logic extends to quantified statements, accommodating relations and generality essential for most natural language arguments.

Translation Between Logical Systems

Translation between logical systems refers to the construction of mappings that preserve the inferential relations and semantic properties of formulas from a source logic into a target logic, enabling the analysis of one system within another while maintaining key structural features such as validity and deducibility. These translations are essential for comparing logics, proving relative consistency, and exploring embeddings where a stronger or more expressive logic interprets a weaker one without loss of expressive power. For instance, translations often rely on semantic frameworks like Kripke models to define equivalence between source and target interpretations.^[15] A prominent example is the standard translation from propositional modal logic into first-order logic, grounded in Kripke semantics. Here, atomic propositions are treated as unary predicates, and the necessity operator \Box \phi (where \phi is translated to an open formula P(x)) becomes \forall y (R(x,y) \to P(y)), with R denoting the accessibility relation between worlds. The possibility operator \Diamond \phi correspondingly translates to \exists y (R(x,y) \land P(y)). This mapping embeds the entire modal language into a fragment of first-order logic, preserving truth in Kripke frames: a modal formula is valid if and only if its first-order counterpart is valid in all corresponding relational structures. The translation is sound and complete relative to this semantics, ensuring no loss or addition of validities. Negative translations provide a method for embedding classical logic into its intuitionistic subsystem, addressing the fact that classical logic extends intuitionistic logic by principles like the law of excluded middle and double negation elimination. The simplest such embedding is the double-negation translation, which maps a classical formula A to \neg \neg A; under this mapping, a formula A is a classical theorem if and only if \neg \neg A is an intuitionistic theorem, as established by Glivenko's theorem for propositional logic. More generally, the Gödel-Gentzen negative translation, introduced by Gödel in 1933 and refined by Gentzen in 1934, defines a recursive mapping g(A) for complex formulas: for atomic P, g(P) = \neg \neg P; for conjunction, g(A \land B) = g(A) \land g(B); for implication, g(A \to B) = g(A) \to g(B); and for disjunction, g(A \lor B) = \neg (\neg g(A) \land \neg g(B)). This translation satisfies g(A \leftrightarrow \neg \neg g(A)) intuitionistically and embeds classical predicate logic conservatively into intuitionistic logic, proving their equiconsistency. Fidelity conditions ensure that translations accurately reflect the source logic's structure in the target without distortion. Soundness requires that every theorem of the source logic maps to a theorem in the target logic. Faithfulness (or conservativity) demands that no new theorems are introduced in the target logic for the embedded language beyond those corresponding to source theorems. Completeness stipulates that every target theorem derivable from the image of the source corresponds to a source theorem. These properties collectively guarantee that the translation is a faithful embedding, preserving both provability and refutability; for example, in negative translations, they confirm that classical arithmetic is interpretable in intuitionistic arithmetic without collapse. Violations of faithfulness, such as introducing extraneous validities, would undermine the translation's utility for metatheoretic comparisons. Further examples illustrate translations across substructural logics. Intuitionistic logic, which permits contraction (reusing assumptions) and weakening (discarding assumptions), can be embedded into linear logic—a resource-sensitive system without unrestricted structural rules—by prefixing assumptions with the exponential modality !, which licenses controlled contraction and weakening. Specifically, an intuitionistic implication A \to B translates to !A \multimap B, where \multimap is linear implication; this allows multiple uses of A via the rules for !, recovering intuitionistic deducibility while respecting linear logic's resource constraints. The embedding is faithful, as intuitionistic theorems map precisely to linear theorems under this adjustment, without altering the constructive nature of proofs.^[11] Relevance logic, which enforces a relevance condition on implications to avoid paradoxes like the material conditional's detachment issues, can be related to classical logic through adjustments involving Ackermann's rule \gamma: from A \to B and A, infer B. This rule, admissible in systems like the relevance logic R, bridges the stricter relevance requirement with classical modus ponens by permitting inferences where the antecedent shares content with the consequent; translations incorporating \gamma effectively extend relevance systems toward classical deduction while preserving core validities in relational semantics. Such mappings highlight how adding structural rules like contraction recovers classical behavior from relevance-restricted frameworks.^[16]

Methodologies

Criteria for Adequate Translations

In logic translation, criteria for adequacy ensure that the mapping from a source logical system to a target system preserves essential properties such as validity, satisfiability, and inferential structure, thereby maintaining the intended meaning without introducing distortions or losses. These standards are crucial for evaluating translations between formal logical systems or from natural language to logic, distinguishing effective embeddings from mere syntactic mappings. Key criteria include soundness, completeness, faithfulness, and semantic fidelity, often supplemented by considerations of conservativeness, syntactic naturalness, and expressiveness preservation. Soundness requires that every theorem or valid formula in the source logic translates to a theorem or valid formula in the target logic, ensuring no invalid inferences are spuriously validated. Formally, for a translation σ from system L to L', if Γ ⊢L ϕ, then σ(Γ) ⊢{L'} σ(ϕ), preserving the consequence relation in one direction. This criterion guarantees that the translation does not amplify the expressive power of the source beyond its original deductive strength. In the context of modal logics, soundness is verified by ensuring that source validities hold in the target's Kripke frames after translation. Completeness, the converse of soundness, stipulates that every theorem in the target logic that corresponds to a source formula arises from a source theorem, preventing the target from validating unintended source-level inferences. Specifically, if σ(Γ) ⊢_{L'} σ(ϕ), then Γ ⊢_L ϕ, ensuring the translation captures all source-level entailments without omission. Strong completeness may not always hold for embeddings, as some translations preserve only a subset of the target's theorems, but it is essential for full equivalence in conservative settings. For instance, translations between intuitionistic and classical logics often aim for this to maintain proof-theoretic adequacy. Faithfulness combines soundness and completeness, requiring bidirectional preservation of the consequence relation: Γ ⊢L ϕ if and only if σ(Γ) ⊢{L'} σ(ϕ). This ensures the translation is an isomorphism on theorems, avoiding both over- and under-generation of validities. In semantic terms, faithfulness equates satisfiability: a source formula ϕ is satisfiable in L if and only if its image σ(ϕ) is satisfiable in L'. Conservative extensions further refine this by prohibiting new theorems in the target unless derivable from the source, formalized as σ(Γ) ⊢_{L'} ψ only if ψ is an image under σ of some source formula. Semantic fidelity emphasizes model-theoretic equivalence, where translations must respect the interpretive structures of the logics involved, such as Kripke frames for modal logics or Heyting algebras for intuitionistic logic. A translation is semantically faithful if source models M satisfy ϕ exactly when target models σ(M) satisfy σ(ϕ), preserving truth conditions across frames. For modal systems, this involves maintaining accessibility relations in Kripke semantics; for intuitionistic logics, it requires compatibility with Heyting algebra valuations, ensuring that implications and negations align without collapsing to classical Boolean structures. Additional metrics address practical and structural aspects. Syntactic naturalness evaluates whether the target formula introduces minimal complexity, such as avoiding excessive nesting or auxiliary symbols that obscure the source's structure, which is particularly relevant in natural language formalizations to retain readability. Expressiveness preservation ensures the target system captures all nuances of the source, including modalities or quantifiers, without reducing the logic's discriminatory power over models. For example, the standard translation from propositional modal logic to first-order logic achieves this by embedding necessity and possibility operators into quantified predicates while preserving frame correspondences.

Translation Procedures

Translation procedures in logic encompass both manual and algorithmic methods for converting expressions from natural language to formal logic or between different logical systems. These procedures ensure that the semantic content is preserved while adapting to the target formalism's syntax and inference rules. Manual approaches provide foundational steps for human translators, while algorithmic techniques enable automation, often leveraging computational linguistics and proof theory. Verification follows to confirm fidelity to adequacy criteria, such as soundness and completeness.

Manual Procedures

Manual translation from natural language to formal logic typically involves a structured sequence of steps to capture the underlying logical structure. First, identify the logical form by parsing the sentence to detect quantifiers (e.g., "all," "some"), connectives (e.g., "and," "or," "if-then"), and predicates, rewriting the sentence in a more explicit, quantified form such as Aristotelian patterns like "All Ps are Qs" corresponding to ∀x (P(x) → Q(x)). Second, assign symbols by defining predicates for properties or relations (e.g., Cat(x) for "x is a cat") and variables for entities, ensuring consistency across the translation. Third, resolve ambiguities using contextual cues, such as scope of quantifiers or referential dependencies; for instance, in "Every cat loves some dog," context determines whether the dog varies per cat (∀x (Cat(x) → ∃y (Dog(y) ∧ Loves(x,y)))) or is fixed. For translations between logical systems, manual procedures often rely on definitional extensions to embed one logic into another while preserving expressiveness. A common technique treats specialized operators, such as modal operators in modal logic, as predicates or relations in first-order logic; for example, the necessity operator □φ is extended definitionally to ∀y (R(x,y) → φ), where R is the accessibility relation and x the current world. This approach applies iteratively, expanding axioms and rules of the source logic into the target via explicit definitions to maintain provability.^[15]

Algorithmic Approaches

Algorithmic methods systematize translation through computational parsing and embedding functions, particularly for handling complex structures like quantifier scope. Tree-based parsing constructs a syntactic tree from the input, then applies lambda calculus to formalize meanings compositionally; for quantifier scope, lambda abstractions bind variables during tree traversal, as in Montague semantics where "every man runs" becomes λP.∀x (Man(x) → P(x)) applied to Run, resolving scope ambiguities by choice of binding order. This enables automated derivation of first-order logic forms from parse trees, with beta-reduction simplifying expressions post-parsing.^[17] Recent advancements incorporate large language models (LLMs) for natural language to first-order logic translation. For example, fine-tuned models like LogicLLaMA (a LLaMA-7B variant) achieve high accuracy in generating formal logical expressions from natural language inputs, handling ambiguities through contextual prompting and post-processing verification, as demonstrated in benchmarks up to 2024.^[18] For inter-system translations, embedding functions like the standard translation algorithm map modal formulas to first-order equivalents, especially effective in S5 where the equivalence relation on worlds allows a straightforward relational encoding: a formula φ becomes ST_x(φ), relativized to world x via predicates over world-individual pairs, ensuring the translation preserves validity across models.^[15]

Tools and Frameworks

Sequent calculi serve as frameworks for proof-preserving translations between logical systems by providing inference rules that maintain sequent structure across embeddings; for instance, translating classical to intuitionistic logic involves restricting right rules (e.g., no double negation elimination) while preserving left-sided inferences, ensuring that provable sequents in the source map to provable ones in the target.^[19] Category-theoretic functors offer abstract procedures for translations by modeling logics as categories of proofs or models, where a functor F: C → D preserves structure (e.g., composition of inferences) between source category C and target D; Lawvere's functorial semantics uses such functors to embed algebraic theories into Cartesian closed categories, facilitating translations that conserve logical operations like conjunction and implication.^[20]

Verification Steps

Post-translation verification ensures the procedure yields adequate translations by checking semantic equivalence. Model comparison involves defining logical relations between source and target models, verifying that satisfaction in one implies satisfaction in the other via transition pairs (e.g., a model morphism Ψ and comorphism Ξ); for example, in modal-to-FOL translations, relations like SC_ML confirm that modal models expand correctly to relational structures.^[21] Theorem proving automates this through type-checking in logical frameworks like Twelf, proving meta-theorems such as soundness (every source theorem translates to a target theorem) by encoding the translation and checking well-formedness.^[21] These steps align with adequacy criteria by confirming faithfulness in both directions where required.^[21]

Challenges and Applications

Problematic Expressions

In natural language, ambiguities pose significant challenges to logic translation, particularly scope ambiguities arising from quantifier interactions. For instance, the sentence "Every farmer who owns a donkey beats it" can be interpreted in two ways: one where the universal quantifier "every" takes wide scope over the existential "a donkey," implying that every farmer beats all donkeys they own, and another where the existential takes wide scope, suggesting that for every farmer who owns at least one donkey, that farmer beats their donkey. This ambiguity resists direct translation into first-order logic without additional mechanisms to resolve quantifier order, as classical formal systems typically require explicit scoping that natural language leaves implicit.^[22] Vagueness in natural language expressions further complicates translation, as predicates like "tall" lack precise boundaries, leading to borderline cases where neither truth nor falsity applies straightforwardly in bivalent logic. For example, determining whether someone is "tall" depends on context without a fixed threshold, such as 6 feet, making it impossible to assign a crisp truth value in standard logical frameworks. This sorites paradox—where incremental changes (e.g., adding one grain of sand) blur category membership—highlights how vagueness undermines the precision required for formalization.^[23] Presuppositions represent another hurdle, where certain expressions assume background conditions that, if unmet, render the statement infelicitous rather than false. Peter Strawson argued that definite descriptions, such as "the present king of France," presuppose the existence and uniqueness of the referent; thus, "The present king of France is bald" fails to have a truth value if no such king exists, contrasting with truth-conditional approaches. This view implies that logic translation must account for presupposition failure, which classical logic treats as mere falsity, potentially distorting semantic content.^[24] Logical mismatches between natural language and formal systems exacerbate these issues, especially with non-monotonic expressions in commonsense reasoning. Defaults, like assuming "birds fly" unless specified otherwise (e.g., penguins do not), introduce defeasible inferences that classical monotonic logic cannot capture, as adding information retracts prior conclusions rather than preserving them. Similarly, natural language tense and modality—such as "John might have gone" or past perfect constructions—lack direct analogs in basic first-order logic, requiring extensions like temporal operators or possible-worlds models to represent shifting temporal perspectives or hypothetical necessities.^[25]^[26] A prominent case study is the Russell-Strawson debate over the sentence "The present king of France is bald," which underscores presuppositional tensions in translation. Bertrand Russell's theory of descriptions analyzes it as an existential claim ("There exists exactly one present king of France, and he is bald"), rendering it false due to non-existence, thereby preserving bivalence in logic. Strawson countered that the sentence presupposes existence, leading to a truth-value gap upon failure, which better aligns with intuitive language use but challenges formal systems reliant on exhaustive truth assignments.^[14] Handling counterfactual conditionals provides another illustrative challenge, as in "If John had studied, he would have passed," which natural language evaluates based on hypothetical scenarios rather than actual ones. David Lewis's possible-worlds semantics addresses this by defining counterfactuals as true if the consequent holds in worlds closest to the actual one where the antecedent is true, ordered by similarity; however, this requires a non-classical framework that diverges from indicative conditionals, complicating uniform translation.^[27] Mitigation strategies include multi-valued logics to handle vagueness, such as fuzzy logic assigning degrees of truth (e.g., "tall" as 0.7 true for borderline heights), which allows graded interpretations without sharp cutoffs, though it introduces complexity in inference rules. Pragmatics extensions, incorporating context and speaker intent, further aid by resolving ambiguities beyond pure semantics, as in Gricean implicatures that clarify scope or presuppositions; yet, these approaches offer partial resolutions, as full equivalence between natural language flexibility and logical rigor remains elusive.^[28]^[29]

Modern Applications and Criticisms

In natural language processing, logic translation enables the conversion of user queries into formal representations for tasks like question answering, as demonstrated by the GeoQuery dataset, which pairs English questions with logical forms for geographic database queries.^[30] This approach has been integrated into AI reasoning systems using large language models (LLMs), particularly for translating natural language to linear temporal logic (LTL) in verification tasks, with benchmarks like VLTL-Bench evaluating performance across datasets from 2023 to 2025.^[31] Additionally, automated theorem proving leverages translations from first-order logic to description logics via the TPTP library, facilitating efficient solving of complex problems in reasoning systems.^[32] Philosophically, logic translation supports argument analysis in ethics by formalizing moral syllogisms to evaluate deontological and consequentialist claims, enhancing clarity in ethical debates.^[33] In law, it models legal arguments through logical structures, aiding in the reconstruction and critique of statutes and precedents.^[34] For quantum computing models, embedding non-classical logics, such as quantum logic, into formal systems captures superposition and entanglement phenomena beyond classical frameworks.^[35] Criticisms of logic translation highlight its overreliance on classical logic, which Quine argued fails to account for context-dependence in natural language and interpretation, potentially leading to inadequate translations since the 1950s.^[36] Computational intractability arises in expressive logics, where translating complex formulas becomes undecidable or NP-hard, limiting scalability for real-world applications.^[37] Recent LLM studies from 2024-2025 reveal instability in formal translations, where models produce inconsistent logical outputs under minor input perturbations, questioning their reliability for universal reasoning.^[38] Future directions emphasize hybrid neuro-symbolic systems that integrate LLMs with dedicated logic translators to mitigate instability and enhance robust reasoning, combining neural pattern recognition with symbolic verification.^[39]

References

[1]
https://doi.org/10.1007/s11787-009-0005-2
[2]
[PDF] What is a Logic Translation? - DFKI
We show how logic translations induce notions of logical expressiveness, consistency strength and sublogic, leading to an explanation of paradoxes that have ...
[3]
How to identify, translate and combine logics? - Oxford Academic
2 What is a logical framework? 3 What is a logic? 4 What is a logic translation? 5 What is a logic combination? 6 Related work. 7 Conclusion. Footnotes.
[4]
What is a Logic Translation? | Logica Universalis
Apr 21, 2009 · We show how logic translations induce notions of logical expressiveness, consistency strength and sublogic, leading to an explanation of ...
[5]
[PDF] Translations Between Logics Tutorial - cle.unicamp.br
The method of studying inter-relations between logical systems by the analysis of translations between them was originally introduced by Kolmogo-.
[6]
New Dimensions on Translations Between Logics | Logica Universalis
Apr 21, 2009 · We concentrate on three paradigms of translations between logics: (conservative) translations, transfers and contextual translations.
[7]
[PDF] On translating between logics - PhilSci-Archive
Jan 9, 2018 · That is, it would fall within the definition to offer one way of translating the formulae of L1 into those of L2 when considering the closure of ...
[8]
https://plato.stanford.edu/entries/goedel/
[9]
Ancient Logic - Stanford Encyclopedia of Philosophy
Dec 13, 2006 · Aristotle is the first great logician in the history of logic. His logic was taught by and large without rival from the 4th to the 19th ...
[10]
Kurt Gödel - Stanford Encyclopedia of Philosophy
Feb 13, 2007 · The main theorem of his dissertation was the completeness theorem for first order logic (Gödel 1929). Gödel's university years also ...
[11]
[PDF] On Various Negative Translations - People at MPI-SWS
The first such translation is due to Kolmogorov [19] in 1925. He observed that placing a double negation ¬¬ in front of every subformula turns a classically ...
[12]
Possible-translations semantics for some weak classically-based ...
Abstract. In many real-life applications of logic it is useful to interpret a particular sentence as true together with its negation.
[13]
Meaning-Preserving Translations of Non-classical Logics into ...
Abstract. In order to prove the validity of logical rules, one has to assume these rules in the metalogic. However, rule-circular 'justifications' are ...
[14]
Towards a stronger notion of translation between logics
In this survey we address the following question: Which logical properties a (strong) logic translation should preserve? ... between logics and between other ...
[15]
[PDF] First-Order Logic
Now we're going to see how first-order logic can be used to formalize a variety of real-world concepts and situations. We'll go through a bunch of examples ...
[16]
Modal Logic - Stanford Encyclopedia of Philosophy
Feb 29, 2000 · Modal logic is, strictly speaking, the study of the deductive behavior of the expressions 'it is necessary that' and 'it is possible that'.
[17]
Linear Logic - Stanford Encyclopedia of Philosophy
Sep 6, 2006 · ... intuitionistic logic, we can try to eliminate the contraction and weakening rules instead. In doing so, we are left with two different ...
[18]
[PDF] Greg Restall - RELEVANCE LOGIC
Both relevance logic and classical logic agree on the stan- dard 'normal form equivalences': commutation, association, idempotence,. Page 30. 30. J. MICHAEL ...
[19]
None
### Summary of Step-by-Step Procedures for Translating Natural Language into First-Order Logic
[20]
Montague Semantics - Stanford Encyclopedia of Philosophy
Nov 7, 2011 · Montague semantics is a theory of natural language semantics and of its relation with syntax. It was originally developed by the logician ...
[21]
[PDF] Efficient Translation of Sequent Calculus Proofs Into Natural ...
Translations of LK to natural deduction are as old as the proof systems them- selves. However these translations often focus on the preservation of provability,.
[22]
Category theory - Stanford Encyclopedia of Philosophy
Dec 6, 1996 · Definition (Lambek): A category is a deductive system in which the following equations hold between proofs: for all f : X → Y, g : Y → Z and h: ...
[23]
[PDF] Mechanically Verifying Logic Translations - KWARC
Aug 24, 2010 · Common tasks include verification of derivations, search for derivations, and proving meta-theorems about deductive systems. Logical frameworks ...
[24]
[PDF] Donkeys under discussion* | Semantics and Pragmatics
Nov 12, 2019 · Abstract Donkey sentences have existential and universal readings, but they are not often perceived as ambiguous.
[25]
Vagueness - Stanford Encyclopedia of Philosophy
Feb 8, 1997 · The direct bearers of vagueness are a word's full disambiguations such as 'tall for an eighteenth-century French man'. Words are only vague ...
[26]
Presupposition - Stanford Encyclopedia of Philosophy
Apr 1, 2011 · However, Strawson (1950) famously argued against Russell's theory by proposing that when a definite description fails to refer, the result can ...Characterizing Presupposition · The Frege-Strawson tradition · Accommodation
[27]
Non-Monotonic Logic - Stanford Encyclopedia of Philosophy
The term "non-monotonic logic" covers a family of formal frameworks devised to capture and represent defeasible inference, i.e., that kind of inference of ...
[28]
Temporal Logic - Stanford Encyclopedia of Philosophy
Nov 29, 1999 · Temporal Logic covers formal approaches to representing and reasoning about time and temporal information, often using a modal-logic style.
[29]
Descriptions - Stanford Encyclopedia of Philosophy
Mar 2, 2004 · ... Bertrand Russell's paper “On Denoting,” in 1905. Despite the apparent simplicity of definite and indefinite descriptions, the past 100+ ...
[30]
Counterfactuals - Stanford Encyclopedia of Philosophy
Jan 18, 2019 · Counterfactuals are conditionals concerning hypothetical possibilities. What if Martin Luther King had died when he was stabbed in 1958 ...Counterfactuals in Philosophy · Semantic Puzzles · Variably Strict Analyses: The...
[31]
Many-Valued Logic - Stanford Encyclopedia of Philosophy
Apr 25, 2000 · Many-valued logics are non-classical logics. They are similar to classical logic because they accept the principle of truth-functionality.Semantics · Systems of Many-Valued Logic · Applications of Many-Valued...
[32]
Pragmatics - Stanford Encyclopedia of Philosophy
Nov 28, 2006 · Pragmatics deals with utterances, by which we will mean specific events, the intentional acts of speakers at times and places, typically ...
[33]
[PDF] Learning to Transform Natural to Formal Languages
Abstract. This paper presents a method for inducing transformation rules that map natural-language sentences into a formal query or command language.
[34]
[PDF] Verifiable Natural Language to Linear Temporal Logic Translation
Jul 1, 2025 · VLTL-Bench introduces three new datasets which contain both raw and lifted versions of NL specifications, an AP-to-Condition dictionary, lifted ...
[35]
[PDF] Automated Theorem Proving by Translation to Description Logic
Description Logic Form (DLF) is the new TPTP syntax for DL. DLF was designed as a part of this research, and is described in Appendix A. 2 CNF to DL Translation.
[36]
14.3 Logic in Legal and Ethical Reasoning - Fiveable
Ethical reasoning involves different approaches like deontology and consequentialism. Moral syllogisms help analyze arguments and derive conclusions.
[37]
Law and logic: A review from an argumentation perspective
This article reviews legal applications of logic, with a particularly marked concern for logical models of legal argument.
[38]
Quantum Logic and Probability Theory
Feb 4, 2002 · Mathematically, quantum mechanics can be regarded as a non-classical probability calculus resting upon a non-classical propositional logic.
[39]
[PDF] Against Second-Order Logic: Quine and Beyond. Fraser MacBride
For this reason, Quine held that first-order logic is built into our canons of translation. Translation should 'Save the obvious' and since first-order logic is ...
[40]
Descriptive Complexity, Computational Tractability, and the Logical ...
Nov 9, 2020 · Consequently, second-order systems of logic are considered to be computationally intractable, and may therefore seem to be unfit to model human ...
[41]
Are LLMs Stable Formal Logic Translators in Logical Reasoning ...
Jun 5, 2025 · While effective in many tasks, these LLM-based translators often fail to generate consistent symbolic representations when the same concept ...Missing: studies 2024
[42]
Towards Improving the Reasoning Abilities of Large Language Models
Aug 19, 2025 · This paper comprehensively reviews recent developments in neuro-symbolic approaches for enhancing LLM reasoning. We first present a ...