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:
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:
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(s) ⇒ s
ƒ1(~u) ⇒ ~ƒ1(u)
ƒ1((∃x)u) ⇒ (∃x)ƒ1(u)
ƒ1((∀x)u) ⇒ ~(∃x)~ƒ1(u)
ƒ1(u ∧ v) ⇒ ƒ1(u) ∧ ƒ1(v)
ƒ1(u ∨ v) ⇒ ~(~ƒ1(u) ∧ ~ƒ1(v))
ƒ1(u ⊃ v) ⇒ ~(ƒ1(u) ∧ ~ƒ1(v))
ƒ1(u ≡ v) ⇒ (~(ƒ1(u) ∧ ~ƒ1(v))) ∧ (~(ƒ1(v) ∧ ~ƒ1(u)))
The function ƒ1 would classify sentences of the form p∧q and q∧p 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 p∨q and q∨p 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, u∧u, and u∨u 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):
((p ⊃ r) ∧ (q ⊃ s)) ⊃ ((p ∧ q) ⊃ (r ∧ s))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)) ∧ ~(~(p ∧ q) ∧ ~(r ∧ s)) )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.