Logic translation is the process of representing a text in the formal language of a logical system. If the original text is formulated in ordinary language then the term natural language formalization is often used. An example is the translation of the English sentence "some men are bald" into first-order logic as ${\displaystyle \exists x(M(x)\land B(x))}$.^[a] The purpose is to reveal the logical structure of arguments. This makes it possible to use the precise rules of formal logic to assess whether these arguments are correct. It can also guide reasoning by arriving at new conclusions.

Many of the difficulties of the process are caused by vague or ambiguous expressions in natural language. For example, the English word "is" can mean that something exists, that it is identical to something else, or that it has a certain property. This contrasts with the precise nature of formal logic, which avoids such ambiguities. Natural language formalization is relevant to various fields in the sciences and humanities. It may play a key role for logic in general since it is needed to establish a link between many forms of reasoning and abstract logical systems. The use of informal logic is an alternative to formalization since it analyzes the cogency of ordinary language arguments in their original form. Natural language formalization is distinguished from logic translations that convert formulas from one logical system into another, for example, from modal logic to first-order logic. This form of logic translation is specifically relevant for logic programming and metalogic.

A major challenge in logic translation is determining the accuracy of translations and separating good from bad ones. The technical term for this is criteria of adequate translations. An often-cited criterion states that translations should preserve the inferential relations between sentences. This implies that if an argument is valid in the original text then the translated argument should also be valid. Another criterion is that the original sentence and the translation have the same truth conditions. Further suggested conditions are that a translation does not include additional or unnecessary symbols and that its grammatical structure is similar to the original sentence. Various procedures for translating texts have been suggested. Preparatory steps include understanding the meaning of the original text and paraphrasing it to remove ambiguities and make its logical structure more explicit. As an intermediary step, a translation may happen into a hybrid language. This hybrid language implements a logical formalism but retains the vocabulary of the original expression. In the last step, this vocabulary is replaced by logical symbols. Translation procedures are usually not exact algorithms and their application depends on intuitive understanding. Logic translations are often criticized on the grounds that they are unable to accurately represent all the aspects and nuances of the original text.

Definition

A logic translation is a translation of a text into a logical system. For example, translating the sentence "all skyscrapers are tall" as ${\displaystyle \forall x(S(x)\to T(x))}$ is a logic translation that expresses an English language sentence in the logical system known as first-order logic. The aim of logic translations is usually to make the logical structure of natural language arguments explicit. This way, the rules of formal logic can be used to assess whether the arguments are valid.^[1]

Understood in a wide sense, a translation is a process that associates expressions belonging to a source language with expressions belonging to a target language.^[2] For example, in a sentence-by-sentence translation of an English text into French, English sentences are linked to their French counterparts. The hallmark of logic translations is that the target language belongs to a logical system.^[3] Logic translations differ from regular translations in that they are mainly concerned with expressing the logical structure of the original text and less with its concrete content. Regular translations, on the other hand, take various additional factors into account pertaining to the content, meaning, and style of the original expression.^[4] For this reason, some theorists, like Peregrin and Svoboda, have argued that it is not a form of translation. They tend to use other terms, such as "formalization", "symbolization", and "explication".^[5] This opinion is not shared by all logicians and some, like Mark Sainsbury, argue that successful logic translations preserve all the original meaning while making the logical structure explicit.^[6]

Discussions on logic translations usually focus on the problem of expressing the logical structure of ordinary language sentences in a formal logical system. The term also covers cases where the translation happens from one logical system into another.^[7]

Basic concepts

Various basic concepts are employed in the study and analysis of logic translations. Logic is interested in correct reasoning, which happens in the form of inferences or arguments. An argument is a set of premises together with a conclusion.^[8] An argument is deductively valid if it is impossible for its conclusion to be false if all its premises are true.^[9] Valid arguments follow a rule of inference, which prescribes how the premises and the conclusion have to be structured.^[10] A prominent rule of inference is modus ponens, which states that arguments of the form "(1) p; (2) if p then q; (3) therefore q" are valid.^[11] An example of an argument following modus ponens is: "(1) today is Sunday; (2) if today is Sunday then I don't have to go to work today; (3) therefore I don't have to go to work today".^[12]

There are different logical systems for assessing which arguments are valid.^[13] For example, propositional logic only focuses on inferences based on logical connectives, like "and" or "if...then". First-order logic, on the other hand, also includes inferential patterns belonging to expressions like "every" or "some". Extended logics cover further inferences, for example, in relation to what is possible and necessary or regarding temporal relations.^[14]

This means that logical systems usually do not capture all inferential patterns. This is relevant for logic translation since they may miss patterns for which they were not intended. For example, propositional logic can be used to show that the following ordinary language argument is correct: "(1) John is not a pilot; (2) John is a pilot or Bill is a poet; (3) therefore Bill is a poet". However, it fails to show that the argument "(1) John is a pilot; (2) therefore John can aviate" is correct since it is unable to capture the inferential relation between the terms "Pilot" and "can aviate".^[15] If a logical system is applied to cases beyond its limited scope, it is unable to assess the validity of natural language arguments. The advantage of this limitation is that the vagueness and ambiguity of natural language arguments are avoided by making some of the inferential patterns very clear.^[16]

Formal logical systems use precise formal languages to express their formulas and inferences. In the case of propositional logic, letters like ${\displaystyle A}$ and ${\displaystyle B}$ are used to represent simple propositions. They can be combined into more complex propositions using propositional connectives like ${\displaystyle \land }$ to express that both propositions are true and ${\displaystyle \lor }$ to express that at least one of the propositions is true. So if ${\displaystyle A}$ stands for "Adam is athletic" and ${\displaystyle B}$ stands for "Barbara is athletic", then the formula ${\displaystyle A\land B}$ represents the claim that "Adam is athletic, and also Barbara is athletic".^[17] First-order logic also includes propositional connectives but introduces additional symbols. Uppercase letters are used for predicates and lowercase letters stand for individuals. For example, if ${\displaystyle A}$ stands for the predicate "is angry" and ${\displaystyle e}$ represents the individual Elsa, then the formula ${\displaystyle A(e)}$ expresses the proposition "Elsa is angry". Another innovation of first-order logic is the use of quantifiers like ${\displaystyle \exists }$ and ${\displaystyle \forall }$ to represent the meanings of terms like "some" and "all".^[18]

Types

Logic translations can be classified based on the source language of the original text. For many logic translations, the original text belongs to a natural language, like English or French. In this case, the term "natural language formalization" is often used.^[19] For example, the sentence "Dana is a logician and Dana is a nice person" can be formalized into propositional logic using the logical formula ${\displaystyle L\land N}$.^[20] A further type of logic translation happens between two logical systems. This means that the source text is composed of logical formulas belonging to one logical system and the goal is to associate them with logical formulas belonging to another logical system.^[21] For example, the formula ${\displaystyle \Box A(x)}$ in modal logic can be translated into first-order logic using the formula ${\displaystyle \forall y(R(x,y)\to A(y))}$.^[22]

Natural language formalization

Natural language formalization is a form of semantic parsing^[b] that starts with a sentence in natural language and translates it into a logical formula.^[3] Its goal is to make the logical structure of natural language sentences and arguments explicit.^[25] It is mainly concerned with their logical form while their specific content is usually ignored.^[26] Logical analysis is a closely related term that refers to the process of uncovering the logical form or structure of a sentence.^[27] Natural language formalization makes it possible to use formal logic to analyze and evaluate natural language arguments. This is especially relevant for complex arguments, which are often difficult to evaluate without formal tools. Logic translation can also be used to look for new arguments and thereby guide the reasoning process.^[28] The reverse process of formalization is sometimes called "verbalization". It happens when logical formulas are translated back into natural language. This process is less nuanced and discussions concerning the relation between natural language and logic usually focus on the problem of formalization.^[29]

The success of applications of formal logic to natural language requires that the translation is correct.^[30] A formalization is correct if its explicit logical features fit the implicit logical features of the original sentence.^[31] The logical form of ordinary language sentences is often not obvious since there are many differences between natural languages and the formal languages used by logicians.^[32] This poses various difficulties for formalization. For example, ordinary expressions frequently include vague and ambiguous expressions. For this reason, the validity of an argument often depends not just on the expressions themselves but also on how they are interpreted.^[33] For example, the sentence "donkeys have ears" could mean that all donkeys (without exception) have ears or that donkeys typically have ears. The second translation does not exclude the existence of some donkeys without ears. This difference matters for whether a universal quantifier can be used to translate the sentence. Such ambiguities are not found in the precise formulations of artificial logical languages and have to be solved before translation is possible.^[34]

The problem of natural language formalization has various implications for the sciences and humanities, especially for the fields of linguistics, cognitive science, and computer science.^[35] In the field of formal linguistics, for example, Richard Montague provides various suggestions for how to formalize English language expressions in his theory of universal grammar.^[36] Formalization is also discussed in the philosophy of logic in relation to its role in understanding and applying logic.^[37] If logic is understood as the theory of valid inferences in general then formalization plays a central role in it since many of these inferences are formulated in ordinary language. Logic translation is needed to link formal systems of logic to arguments expressed in ordinary language.^[38] A related claim is that all logical languages, including highly abstract ones like modal logic and many-valued logic, have to be "anchored in the structures of natural language".^[39] One difficulty in this regard is that logic is usually understood as a formal science, but a theory of its relation to empirical matters pertaining to ordinary languages goes beyond this purely formal conception.^[40] For this reason, some theorists like Georg Brun identify a pure branch of logic and contrast it with applied logic, which includes the problem of formalization.^[41]

Some theorists draw the conclusion from these considerations that informal reasoning takes precedence over formal reasoning. This would imply that formal logic can only succeed if it is based on correct formalization.^[42] For example, Michael Baumgartner and Timm Lampert hold that "there are no informal fallacies" but only "misunderstanding of informal arguments expressed by inadequate formalizations".^[43] This position is rejected by Jaroslav Peregrin and Vladimír Svoboda, who argue that informal reasoning is not always accurate and may be corrected through the application of formal logic.^[44]

An alternative to formalization is to use informal logic, which analyzes the cogency of natural language arguments in their original form. This has many advantages by avoiding the difficulties associated with logic translations but it also comes with various drawbacks. For example, informal logic lacks the precision found in formal logic for distinguishing between good arguments and fallacies.^[45]

Examples

For propositional logic, the sentence "Tiffany sells jewelry, and Gucci sells cologne" can be translated as ${\displaystyle T\land G}$. In this example, ${\displaystyle T}$ represents the claim "Tiffany sells jewelry", ${\displaystyle G}$ stands for "Gucci sells cologne", and ${\displaystyle \land }$ is the logical conjunction corresponding to "and". Another example is the sentence "Notre Dame raises tuition if Purdue does", which can be formalized as ${\displaystyle P\to N}$.^[46]

For predicate logic, the sentence "Ann loves Ben" can be translated as ${\displaystyle L(a,b)}$. In this example, ${\displaystyle L}$ stands for "loves", ${\displaystyle a}$ stands for Ann and ${\displaystyle b}$ stands for Ben.^[47] Other examples are "some men are bald" as ${\displaystyle \exists x(M(x)\land B(x))}$,^[48] "all rivers have a head" as ${\displaystyle \forall x(R(x)\to H(x))}$,^[49] "no frogs are birds" as ${\displaystyle \forall x(F(x)\to \lnot B(x))}$,^[50] and "if Elizabeth is a historian, then some women are historians" as ${\displaystyle H(e)\to \exists x(W(x)\land H(x))}$.^[51]

Problematic expressions

For various natural language expressions, it is not clear how they should be translated and the right translation may differ from case to case. The vagueness and ambiguity of ordinary language, in contrast to the precise nature of logic, is often responsible for these problems. For this reason, it has proven difficult to find a general algorithm to cover all cases of translation.^[52] For example, the meaning of basic English expressions like "and", "or", and "if...then" can vary from context to context. The corresponding logical operators in symbolic logic (${\displaystyle \land }$, ${\displaystyle \lor }$, ${\displaystyle \to }$), on the other hand, have very precisely defined meanings. In this regard, they only capture some aspects of the original meaning.^[53]

The English word "is" poses another such difficulty since it has many meanings. It can express existence (as in "there is a Santa Claus"), identity (as in "Superman is Clark Kent"), and predication (as in "Venus is a planet"). Each one of these meanings is expressed differently in logical systems like first-order logic.^[54] Another difficulty is that quantifiers are often not explicitly expressed in ordinary language. For example, the sentence "emeralds are green" does not directly state the universal quantifier "all", i.e. "all emeralds are green". However, some sentences with a similar structure, such as the "children live next door", imply the existential quantifier "some", i.e. "some children live next door".^[55]

A closely related problem is found in some valid natural language arguments whose most obvious translations are invalid in formal logic. For example, the argument "(1) Fury is a horse; (2) therefore Fury is an animal" is valid but the corresponding argument in formal logic from ${\displaystyle H(f)}$ to ${\displaystyle A(f)}$ is invalid. One solution is to add to the argument an additional premise stating that "all horses are animals". Another is to translate the sentence "Fury is a horse" as ${\displaystyle H(f)\land A(f)}$. These solutions come with new problems of their own.^[56] Further problematic expressions are definite descriptions, conditional sentence, and attributive adjectives, as well as mass nouns and anaphora.^[57]

Translation between logics

A further type of logic translation takes place between logical systems. A translation between two logical systems can be defined in a formal sense as a mathematical function. This function maps sentences of the first system to sentences of the second system while obeying the entailment relations between the original sentences. This means that if a sentence entails another sentence in the first logic, then the translation of the first sentence should entail the translation of the second sentence in the second logic. This way, a translation from one logic to another represents the formulas, proofs, and models of the first logic in terms of the second.^[58] This is sometimes referred to as conservative translation. It contrasts with rough translation, which only maps the sentences of the first logic to sentences of the second logic without regard to their entailment relations.^[59]

A preliminary of logic translations is that there is not one logic but many logics.^[60] These logics differ from each other concerning the languages they use as well as the rules of inference they see as valid. For example, intuitionistic logic differs from classical logic since it rejects certain rules of inference, such as the double negation elimination. This rule states that if a sentence is not not true, then it is true, i.e. that ${\displaystyle A}$ follows from ${\displaystyle \lnot \lnot A}$.^[61] One way to translate intuitionistic logic into non-intuitionistic logic is by using a modal operator. This is based on the idea that intuitionistic logic expresses not just what is true but what is knowable. For example, the formula ${\displaystyle \lnot p}$ in intuitionistic logic can be translated as ${\displaystyle K\lnot p}$ where ${\displaystyle K}$ is a model operator expressing that the following formula is knowable.^[62]

Another example is the translation of modal logic to regular predicate logic. Modal logic contains additional symbols for possibility (${\displaystyle \diamond }$) and necessity (${\displaystyle \Box }$) not found in regular predicate logic. One way to translate them is to introduce new predicates, such as the predicate R, which indicates that one possible world is accessible from another possible world. For example, the modal logic expression ${\displaystyle \lfloor \diamond p\rfloor _{\iota ))$ (it is possible that p is true in the actual world) can be translated as ${\displaystyle \exists vR(\iota ,v)\land \lfloor p\rfloor _{v))$ (there exists a possible world that is accessible from the actual world and p is true in it).^[63]

Translations between logics are relevant for metalogic and logic programming. In metalogic, they can be used to study the properties of logical systems and the relations between them.^[64] In logic programming, they make it possible for programs limited to one type of logic to be applied to many additional cases. With the help of logic translations, programs like Prolog can be used to solve problems in modal logic and temporal logic even though Prolog does not natively support these logical systems.^[65] A closely related issue concerns the question of how to translate a formal language like Controlled English into a logical system. Controlled English is a controlled language that limits grammar and vocabulary with the goal of reducing ambiguity and complexity. In this regard, the advantage of Controlled English is that every sentence has a unique interpretation. This makes it possible to use algorithms to translate them into formal logic, which is generally not possible for natural languages.^[66]

Criteria of adequate translations

Criteria of adequate translations specify how to distinguish good from bad translations. They determine whether a logical formula accurately represents the logical structure of the sentence it translates. This way, they help logicians decide between competing translations of the same sentence.^[67] Various criteria are discussed in the academic literature.^[68] According to various theorists, like Peregrin and Svoboda, the most basic criterion is that translations should preserve the inferential relations between sentences. This principle is sometimes called the criterion of syntactic correctness or the criterion of reliability.^[69] It stipulates that if an argument is valid in the original text then the translated argument is also valid.^[70] One difficulty in this regard is that the same sentence may form part of several arguments, sometimes as a premise and sometimes as a conclusion. A translation of a sentence is only correct if in all or nearly all these cases, the inferential relations are preserved.^[71] According to the view of holism, this implies that one cannot evaluate sentence translations individually. This position holds that the correctness of a translation of one sentence depends on how other sentences are translated to ensure correspondence in the inferential relations. This view is rejected by atomists, who claim that the correctness of sentence translations can be assessed individually.^[72]

A closely related criterion focuses on the truth conditions of sentences.^[73] A truth condition of a sentence is what the world must be like for that sentence to be true.^[74] This criterion states that for adequate translations, the truth conditions of the original sentence are identical to the truth conditions of the translated sentence. The mere fact that the sentence and its translation have the same truth value is not sufficient. Instead, it implies that whenever one is true, the other is also true, i.e. they have to have the same truth value in all possible circumstances.^[75] This criterion is not universally accepted and it has been criticized based on the claim that logical formulas do not have truth conditions. According to this view, the symbols they use are meaningless by themselves and only have the purpose of expressing the logical form of a sentence without implying any concrete content.^[31] Another problem with this approach is that all tautologies have the same truth conditions: they are true independently of the circumstances. This would imply that any tautology is a correct translation of any other tautology.^[76]

Besides these core criteria, various additional criteria are often discussed in the academic literature. Their goal is usually to exclude bad translations that nonetheless comply with the other criteria. For example, according to the first two criteria, the sentence "it rains" could be formalized as ${\displaystyle p}$ or as ${\displaystyle \lnot \lnot \lnot \lnot \lnot \lnot p}$. The reason is that both formulas have the same truth conditions and the same inferential patterns. However, the second formula is a bad translation. One additional criterion is that translations should not include symbols that do not correspond to expressions in the original sentence. According to it, the translation of "it rains" should not include the symbol for logical negation (${\displaystyle \lnot }$) since a corresponding expression is not found in the original sentence.^[77]

Another criterion holds that the order of symbols in the translation should reflect the order of the expressions in the original sentence. For example, the sentence "Pete went up the hill and Quinn went up the hill" should be translated as ${\displaystyle p\land q}$ and not as ${\displaystyle q\land p}$.^[77] A closely related criterion is the principle of transparency, which states that translations should aim to be similar to the original expression. This concerns, for example, that a translation reflects the grammatical structure of the original sentence as closely as possible.^[78] The principle of parsimony states that simple translations (i.e. logical formulas that use as few symbols as possible) are to be preferred.^[79] One way to test whether a formalization is correct is to translate it back into natural language and see if this second translation matches the original.^[80]

The problem of the criteria of adequate translations is often not discussed in detail in introductions to logic. One reason for this is that some theorists, like Herbert E. Hendry, see logic translation as an art or an intuitive practice. According to this view, it is based on a practical skill learned from experience with many examples and guided by some rough rules of thumb. This outlook implies that there are no strict rules of adequate formalization. Critics of this idea argue that without clear criteria of adequate translations it is very difficult to decide between competing formalizations of the same sentence.^[81]

Translation procedures

Various logicians have proposed translation procedures employing several steps to arrive at correct translations. Some only constitute rough guidelines to help translators in the process while others consist of detailed and effective procedures covering all the steps needed to arrive at a translation. In either case, they are usually not exact algorithms that could be blindly followed but rather tools to simplify the process.^[82]

Preparatory steps may be taken within natural language before the actual translation starts. An initial step is often to understand the meaning of the original text, for example, by analyzing the claims made in it. This includes identifying which arguments are made and whether a claim acts as a premise or as a conclusion.^[83] At this stage, a common recommendation is to paraphrase the sentences to make the claims more explicit, remove ambiguities, and highlight their logical structure. For example, the sentence "John Paul II is infallible" could be paraphrased as "it is not the case that John Paul II is fallible".^[84] This can involve identifying truth-functional connectives, like "and", "if...then", or "not", and decomposing the text accordingly. Each of the units analyzed this way is an individual claim that is either true or false.^[85] A closely related step is to group the individual expressions into logical units and classify them according to their logical role. In the sentence above, for example, "is fallible" is a predicate and the expression "it is not the case that" corresponds to the logical connective for negation.^[86]

Once these preparations are done, some theorists, like Peregrin and Svoboda, recommend translation into a hybrid language. Such hybrid expressions already contain a logical formalism but retain regular names for predicates and proper names. For example, the sentence "All rivers have heads" could be translated as ${\displaystyle \forall x((River(x))\to HasHead(x))}$. The idea behind this step is that the regular terms still carry their original meaning and thereby make it easier to understand the formulas and to see how they relate to the original text. The natural language vocabulary is usually not precisely defined and therefore lacks the exactness demanded by formal logic.^[87] As a last step, these regular terms are then replaced by logical symbols. For the expression above, this would result in the formula ${\displaystyle \forall x((R(x))\to H(x))}$. This way, the connection to the ordinary language meanings is cut. The formulas become a purely formal expression of the logical structure of the original text and any specific content is removed.^[88]

The formalization of a full argument consists in several steps since the argument is made up of several propositions.^[89] Once the translation is complete, the formal tools of the logical system, such as its rules of inference, can be employed to assess whether the argument is valid.^[90]

Criticism

Criticism of logic translations is primarily focused on the limitations and the range of valid applications, as well as the way they are discussed in academic literature. Logic translation is a widely accepted and utilized process in logic and other fields, even among theorists who criticize aspects of it.^[91] In some cases, individual logic translations are criticized based on the claim that they are unable to accurately represent all the aspects and nuances of the original text. For example, logical vocabulary is usually unable to capture things like sarcasm, indirect insinuation, or emphasis. In this regard, many aspects of the meaning of the original expression that go beyond truth value, validity, and logical structure are frequently ignored.^[92] On the level of informal inferences, there are various expressions that cannot easily be represented using the precise but limited languages of formal logic.^[93] For these reasons, it is sometimes controversial whether a specific logic translation is correct. When a logic translation is used to defend the conclusion of a natural language argument, one way to undermine such a defense is to claim that the logic translation is incorrect. This implies that insights gained from the formal logical analysis do not carry any weight for the original argument.^[90]

Another type of criticism is not directed at logic translations themselves but at how they are discussed in many standard works and courses of logic. In this regard, theorists like Georg Brun, Peregrin, and Svoboda argue that such works do not provide a proper discussion of the role and limitations of logic translations. Instead, it is claimed that they merely treat this topic as a side note. They may provide a few examples but their main focus is on the formal systems themselves. This way, there is no in-depth discussion of how these systems are applied to ordinary arguments.^[94]