Propositions

John F. Sowa

Abstract.  Informally, different statements 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 is defined as an equivalence class of sentences in some formal language L under some meaning-preserving translation (MPT) defined over the sentences of L. This paper defines a series of six MPTs f₀,...,f₅ and recommends f₄ as the most useful for most purposes.

Meaning-preserving translations can be defined for any kind of language, but for simplicity, this paper will restrict the definition to first-order logic or some subset of FOL. Formally, a meaning-preserving translation from the sentences of a first-order language L₁ to the sentences of a first-order language L₂ is any function f that satisfies the following four constraints:

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

2. Truth preserving. Although the sentences s and g(f(s)) might not be identical, both must have exactly the same truth conditions:  for any model M of the language L₁, M|=s if and only if M|=g(f(s)). Preserving truth is necessary for meaning preservation, but it is a weak condition that groups too many sentences in the same equivalence classes. For example, Fermat's last theorem and the sentence "2+2=4" are true in every model of Peano's axioms, but it would be absurd to say that they are synonymous. 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 L₁ to L₂ and back to g(f(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(f(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(f(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 f₁ through f₄, 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₁ and L₂ may be the same language. Any MPT f defined over a single language L partitions the sentences of L into a set of equivalence classes called propositions. A series of six MPTs f₀, ..., f₅ are defined below, which have the following properties:

• Each MPT f_i is its own inverse:  g_i = f_i.

• Every equivalence class p in the partition of L determined by f_i contains exactly one canonical sentence c.

• For every sentence s in p, f_i(s) = c and g_i(f_i(s)) = c.

• Any two sentences s₁ and s₂ of L are contained in the same equivalence class if and only if f_i maps both of them to the same canonical sentence c:  f_i(s₁) = c and f_i(s₂) = c.

For any language L, the simplest MPT f₀ is the identity function:  for every sentence s in L, f₀(s)=s. This translation satisfies all four criteria for an MPT, since f₀ 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 f₁ translates every sentence to a canonical sentence that uses only the three logical symbols ∧, ~, and ∃. The inverse of f₁ is f₀ itself. The details for defining f₁ 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 f₁(s) is defined recursively:

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

   f₁(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:

   f₁(~u)  ⇒  ~f₁(u)

   f₁((∃x)u)  ⇒  (∃x)f₁(u)

   f₁((∀x)u)  ⇒  ~(∃x)~f₁(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:

   f₁(u ∧ v)  ⇒  f₁(u) ∧ f₁(v)

   f₁(u ∨ v)  ⇒  ~(~f₁(u) ∧ ~f₁(v))

   f₁(u ⊃ v)  ⇒  ~(f₁(u) ∧ ~f₁(v))

   f₁(u ≡ v)  ⇒  (~(f₁(u) ∧ ~f₁(v))) ∧ (~(f₁(v) ∧ ~f₁(u)))

The function f₁ 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 f₂ makes the same symbol replacements as f₁, but it also sorts conjunctions in lexical order according to some encoding, such as Unicode. As a result, arbitrary permuations of conjunctions map to the same canonical sentence and are grouped in the same equivalence class. Since disjuctions are defined in terms of of conjunctions, the sentences p∨q and q∨p would also be in the same calss. Since a list of N terms can be sorted in time proportional to NlogN, the function f₂ 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 f₃ should rename the variables to a fixed sequence, such as x₁, x₂ , .... 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 f₃ would first convert sentences to prenex normal form and rename variables, then it would perform the translation method of f₁ and sort conjunctions according to the method of f₃.

The function f₃ 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 f₄ would perform exactly the same translations as f₃ followed by one additional step:  deleting duplicate conjunctions. Since f₃ 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 f₁ would have already mapped disjunctions to combinations of conjunctions and negations.

For most purposes, the function f₄ 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))

~((~(p ∧ ~r) ∧ ~(q ∧ ~s)) ∧ ~(~(p ∧ q) ∧ ~(r ∧ s)) )

To account for synonyms and definitions, another function f₅ 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, f₅ 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 f₅ would first expand all virtual relations to the privileged set before performing the translations defined for f₄. 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 f₄ is recommended. If L supports nonrecursive definitions, f₅ could be used.

Last Modified: