John F. Sowa

Abstract.  Informally, sentences in different languages may mean “the same thing.” Formally, that “thing,” called a proposition, represents abstract, language-independent, semantic content. As an abstraction, a proposition has no physical embodiment that can be written or spoken. Only its statements in particular languages can be expressed as strings of symbols. To bring the informal notion of proposition within the scope of formal treatment, this paper proposes a formal definition:  a proposition p shall be defined as an equivalence class of sentences in some formal language L under some meaning-preserving translation (MPT) defined over the sentences of L. For any equivalence class p and model M, all the sentences in p shall have the same vocabulary, structure, and truth value. This paper defines a series of six MPTs ƒ0,...,ƒ5. For most purposes, ƒ4 and ƒ5 are the most useful.

Note:  This paper is a revised excerpt from Section 4 of Worlds, Models, and Descriptions. See that article for references and further discussion. There is also a PDF version of this paper.

A proposition should represent the language-independent meaning of a sentence, but “language independence” and “meaning” are two notoriously difficult notions to formalize. Stalnaker (1976) proposed that the proposition expressed by a sentence should be defined as the set of possible worlds in which the sentence is true. That definition, however, is too coarse grained:  it causes all mathematical theorems to collapse into a single proposition. Fermat’s last theorem, for example, doesn’t mean the same as 2+2=4, and it’s much harder to prove. Peirce had a better definition:  a proposition corresponds to a collection of equivalent sentences with their partial interpretants (CP 5.569).

To avoid the details of Peirce’s theory of interpretants, a proposition shall be defined as an equivalence class of sentences that preserve truth, vocabulary, and structure under some meaning-preserving translation (MPT). For simplicity, this paper will restrict the definition to some version of first-order logic. An MPT from the sentences of a first-order language L1 to the sentences of a first-order language L2 shall be a function ƒ that satisfies the following four constraints:

  1. Invertible. The translation function ƒ must have an inverse function g that maps sentences from L2 back to L1. For any sentence s in L1, ƒ(s) is a sentence in L2, and g(ƒ(s)) is a sentence in L1 but not necessarily s itself. To ensure that ƒ is defined for all sentences in L1, the language L2 must be at least as expressive as L1. If L2 is more expressive than L1, then the inverse g might be undefined for some sentences in L2. In that case, the language L2 would express a superset of the propositions of L1.

  2. Truth preserving. Although the sentences s and g(ƒ(s)) might not be identical, both must have exactly the same truth conditions:  for any model M of the language L1, M⊨s if and only if Mg(ƒ(s)). Preserving truth is necessary, but not sufficient:  the condition is too coarse to distinguish 2+2=4 from Fermat’s last theorem; and its computation may be intractable or even undecidable. Ideally, the test to determine whether two sentences “mean the same” should be “obvious.” Formally, it should be computable by an efficient algorithm — one whose computation time is linearly or at worst polynomially proportional to the length of the sentence.

  3. Vocabulary preserving. When s is translated from L1 to L2 and back to g(ƒ(s)), the syntax might be rearranged, but the words or symbols that represent proper names and ontology must appear in both sentences s and g(ƒ(s)). For example, the sentence Every cat is a cat should not be considered to have the “same meaning” as Every dog is a dog or Every unicorn is a unicorn, since the first is about cats, the second is about dogs, and the the third is about nonexistent things. This criterion could be relaxed to allow terms to be replaced by synonyms or definitions, but arbitrary content words or predicates must not be added or deleted by the translations. An admissible MPT might replace the word cat with domestic feline, but it should not replace the word cat with dog or unicorn.

  4. Structure preserving. When s and g(ƒ(s)) are mapped to a canonical form that uses only negation ~, conjunction ∧, and the existential quantifier ∃ as the logical operators, they must contain computationally equivalent patterns of negations and quantifiers:  i.e., the decidability, provability, and computational complexity of both sentences must be the same. (Formally, the functions ƒ1 through ƒ4, which are defined below, specify what patterns are considered computationally equivalent.) The short justification for this approach is that conjunction is the simplest and least controversial of all the Boolean operators, while negation introduces serious philosophical and computational problems, which are inherited by other operators that require a negation in their definition. Intuitionists, for example, deny that ~~p should be considered provably equivalent to p. Computationally, ~~p and p have different effects on the binding of values to variables in Prolog, SQL, and other systems. For relevance logic, Anderson and Belnap (1975) disallowed the disjunctive syllogism, which is based on ∨ and ~, because it can introduce extraneous information into a proof.
These four conditions impose strong constraints on translations that are said to preserve meaning. They ensure that the content words or predicates remain identical or synonymous, they preserve the logical structure, and they prevent irrelevant content from being inserted. If s is the sentence Every farmer who owns a donkey beats it, then the sentence g(ƒ(s)) might be If a farmer x owns a donkey y, then x beats y. Those sentences use different logical and syntactical symbols, but they have the same truth conditions, they have the same content words, and they have the same structure when expressed with only ∧, ~, and ∃.

In general, an MPT is defined as a function that translates sentences from one language to another, but for many applications L1 and L2 may be the same language. Any MPT ƒ defined over a single language L partitions the sentences of L into a set of equivalence classes called propositions. A series of six MPTs ƒ0, ..., ƒ5 are defined below, which have the following properties:

As an abbreviation, the sentence s is said to state the proposition p if and only if s is contained in the equivalence class p.

For any language L, the simplest MPT ƒ0 is the identity function:  for every sentence s in L, ƒ0(s)=s. This translation satisfies all four criteria for an MPT, since ƒ0 is its own inverse, it preserves truth, vocabulary, and structure, and it is very easy to compute. Its primary drawback is that it fails to group sentences into useful classes:  every sentence in L is the canonical sentence of a proposition in which there are no other sentences.

In order to group sentences into larger equivalence classes, the MPT ƒ1 translates every sentence to a canonical sentence that uses only the three logical symbols ∧, ~, and ∃. The inverse of ƒ1 is ƒ0 itself. The details for defining ƒ1 will vary with the syntax of every version of FOL, but to illustrate the method, let L be a conventional infix notation for FOL with the two quantifiers represented by the symbols ∃ and ∀, with negation represented by ~, and with conjunction, disjunction, material implication, and equivalence represented by the symbols ∧, ∨, ⊃, and ≡. The translation of any sentence or subsentence s of L to its canonical form ƒ1(s) is defined recursively:

  1. If s is an atom (i.e., any relation symbol applied to its arguments), the result is s unchanged:
    ƒ1(s)  ⇒  s

  2. If s consists of a prefix operator (negation or quantifier) applied to a subsentence u, the result is the transformed operator applied to the translation of u:
    ƒ1(~u)  ⇒  ~ƒ1(u)

    ƒ1((∃x)u)  ⇒  (∃x1(u)

    ƒ1((∀x)u)  ⇒  ~(∃x)~ƒ1(u)

  3. If s consists of a dyadic operator (∧, ∨, ⊃, or ≡) applied to two subsentences u and v, the result is a transformation of the operator applied to the translations of u and v:
    ƒ1(uv)  ⇒  ƒ1(u) ∧ ƒ1(v)

    ƒ1(uv)  ⇒  ~(~ƒ1(u) ∧ ~ƒ1(v))

    ƒ1(uv)  ⇒  ~(ƒ1(u) ∧ ~ƒ1(v))

    ƒ1(uv)  ⇒  (~(ƒ1(u) ∧ ~ƒ1(v))) ∧ (~(ƒ1(v) ∧ ~ƒ1(u)))

The function ƒ1 satisfies the criteria for an MPT:  it has an inverse ƒ1; it preserves truth because every step of the translation expands one operator according to its definition in terms of ∧, ~, and ∃; it leaves the content words and symbols unchanged; and it preserves the structure of a sentence when mapped to ∧, ~, and ∃. For any sentence s, ƒ1(s) is a unique canonical sentence of the equivalence class defined by ƒ1:  every sentence in L that is mapped to that canonical sentence states the same proposition. For all logical operators except ≡, the time to convert any sentence to the canonical sentence is linear. If a sentence contains a large number of equivalences, the translation time may be exponentially proportional to the number of equivalences. Such sentences, however, are extremely rare; when people write pqr, they usually intend it as the conjunction pq and qr, which merely doubles the translation time.

The function ƒ1 would classify sentences of the form pq and qp in different equivalence classes because its definition does not reorder any of the subsentences. To group such sentences in the same equivalence class, the function ƒ2 makes the same symbol replacements as ƒ1, but it also sorts conjunctions in lexical order according to some encoding, such as Unicode. As a result, arbitrary permutations of conjunctions map to the same canonical sentence and are grouped in the same equivalence class. Since disjunctions are defined in terms of of conjunctions, the sentences pq and qp would also be in the same class. Since a list of N terms can be sorted in time proportional to NlogN, the function ƒ2 would take just slightly longer than linear time.

Ideally, sentences that differ only in the names assigned to their bound variables, such as (∃x)P(x) and (∃y)P(y), should also be grouped together. Therefore, the function ƒ3 should rename the variables to a fixed sequence, such as x1, x2 , .... That renaming must be done before conjunctions are sorted; the simplest method would be to move all quantifiers to the front by mapping every sentence to prenex normal form and then naming the variables in the order in which they appear. The function ƒ3 would first convert sentences to prenex normal form and rename variables, then it would perform the translation method of ƒ1 and sort conjunctions according to the method of ƒ3.

The function ƒ3 is not yet an ideal MPT because it would assign sentences of the form u, uu, and uu to different equivalence classes. To group such sentences together, the function ƒ4 would perform exactly the same translations as ƒ3 followed by one additional step:  deleting duplicate conjunctions. Since ƒ3 has already sorted conjunctions in lexical order, the deletion can be performed in linear time just by checking whether any conjunct is identical to the one before it; if so, it would be deleted from the result. This process would delete duplicate disjunctions since the method of ƒ1 would have already mapped disjunctions to combinations of conjunctions and negations.

For most purposes, the function ƒ4 is a good MPT for grouping sentences that “say the same thing.” As an example, consider the following sentence, which Leibniz called the Praeclarum Theorema (splendid theorem):

((pr) ∧ (qs)) ⊃ ((pq) ⊃ (rs))
This formula may be read If p implies r and q implies s, then p and q imply r and s. The function ƒ3 would translate it to the following canonical sentence:
~((~(p ∧ ~r) ∧ ~(q ∧ ~s)) ∧ ~(~(pq) ∧ ~(rs)) )
This sentence is not as readable as the original, but it serves as the canonical representative of an equivalence class of ƒ3 that contains 864 different, but highly similar sentences. The function ƒ4, which deletes duplicate conjuncts, can relate infinitely many sentences to the same form. Such transformations factor out accidental differences caused by the choice of symbols or syntax.

To account for synonyms and definitions, another function ƒ5 could be used to replace a word or relation such as cat with its definition as domestic feline. If recursions are allowed, the replacements and expansions would be equivalent in computing power to a Turing machine; they could take exponential amounts of time or even be undecidable. Therefore, ƒ5 should only expand definitions without recursions, direct or indirect. Definitions of this form are common in database systems, in which a fixed set of relations are privileged, and virtual relations may be defined in terms of the privileged relations. With such restrictions, any sentence that uses virtual relations could always be expanded to a form that only uses relations in the privileged set. Therefore, the function ƒ5 would first expand all virtual relations to the privileged set before performing the translations defined for ƒ4. Since no recursion is involved, the expansions would take at most polynomial time.

In summary, an open-ended number of meaning-preserving translations could be defined. For ease of computing, an MPT that determines a unique canonical form for any proposition in at worst polynomial time is recommended. If no definitional mechanisms are available in the given language L, MPT ƒ4 is recommended. If L supports nonrecursive definitions, ƒ5 could be used.

Last Modified: