Abstract.Informally, sentences in different languages may mean “the same thing.” Formally, that “thing,” called aproposition, 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 propositionpshall be defined as an equivalence class of sentences in some formal languageLunder somemeaning-preserving translation(MPT) defined over the sentences ofL. For any equivalence classpand modelM, all the sentences inpshall 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 **L**_{1}
to the sentences of a first-order language **L**_{2}
shall be a function ƒ that satisfies the following four constraints:

*Invertible*. The translation function ƒ must have an inverse function*g*that maps sentences from**L**_{2}back to**L**_{1}. For any sentence*s*in**L**_{1}, ƒ(*s*) is a sentence in**L**_{2}, and*g*(ƒ(*s*)) is a sentence in**L**_{1}but not necessarily*s*itself. To ensure that ƒ is defined for all sentences in**L**_{1}, the language**L**_{2}must be at least as expressive as**L**_{1}. If**L**_{2}is more expressive than**L**_{1}, then the inverse*g*might be undefined for some sentences in**L**_{2}. In that case, the language**L**_{2}would express a superset of the propositions of**L**_{1}.*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**L**_{1}, M⊨*s*if and only if**M**⊨*g*(ƒ(*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.*Vocabulary preserving*. When*s*is translated from**L**_{1}to**L**_{2}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*.*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.

In general, an MPT is defined as a function that translates sentences
from one language to another, but for many applications
**L**_{1} and **L**_{2} 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:

- Each MPT
*f*is its own inverse:_{i}*g*=_{i}*f*._{i} - Every equivalence class
*p*in the partition of**L**determined by*f*contains exactly one_{i}*canonical sentence**c*. - For every sentence
*s*in*p*,*f*(_{i}*s*) =*c*and*g*(_{i}*f*(_{i}*s*)) =*c*. - Any two sentences
*s*_{1}and*s*_{2}of**L**are contained in the same equivalence class if and only if*f*maps both of them to the same canonical sentence_{i}*c*:*f*(_{i}*s*_{1}) =*c*and*f*(_{i}*s*_{2}) =*c*.

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:

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

_{1}(*s*) ⇒*s* - 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*) ⇒ (∃*x*)ƒ_{1}(*u*)ƒ

_{1}((∀*x*)*u*) ⇒ ~(∃*x*)~ƒ_{1}(*u*) - 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}(*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 N*log*N, 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 *x*_{1}, *x*_{2} , ....
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):

((This formula may be readp⊃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 ƒp∧ ~r) ∧ ~(q∧ ~s)) ∧ ~(~(p∧q) ∧ ~(r∧s)) )

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: