SUO: Re: Propositions
John F. Sowa wrote:
>
> Pat and Jon,
>
> JS>>> I used the word "statement" to avoid getting into details
> >> > about the distinction between a "statement" and a "proposition".
> >> > But as I have said in my KR book (Ch. 5) and many email notes,
> >> > I prefer to define a proposition as an equivalence class of
> >> > statements in multiple languages. With such a definition,
> >> > you can talk about entailment in a form that factors out as
> >> > much of the notation as you like. (The larger the equivalence
> >> > class, the smaller the dependence on any particular notation.)
>
> JS>>> This kind of factoring is especially important for the SUO,
> >> > since we must deal with multiple languages, including CGs,
> >> > DAML, OIL, SQL, RDF, UML, and versions of controlled natural
> >> > languages, such as ACE or Aristotelian syllogisms.
>
> PH>> Interesting idea, and I agree important. But to give it flesh
> >> you need to say what the equivalence relation is, relative to
> >> which the equivalence classes are defined; and that in turn
> >> seems to require some way to compare the semantic content
> >> of expressions from different languages. If they are
> >> all interpreted in the same structures one could see
> >> how this would go -- equivalent expressions denote
> >> the same things in all interpretations -- but the
> >> more general construction eludes me.
>
> In Ch 5, I defined the notion of a "meaning-preserving
> translation", either within a single language or among
> multiple languages. The simplest example is identity,
> but I define a more interesting class of transformations:
>
> http://www.bestweb.net/~sowa/logic/meaning.htm
>
> That file has the nicely formatted version.
> The plain text version is attached below.
>
> JA> This is exactly the sort of problem that
> > Category Theory was invented to solve:
>
> I agree, and I was thinking of category theory, but I didn't
> want to overburden the KR book with too much formalism that I
> didn't intend to apply in detail. However, category theory
> is so general that the really interesting questions are often
> in the details of what kinds of transformations are appropriate
> for any given application.
>
> With that caveat, I agree that there are a lot of interesting
> possibilities for using category theory. Joe Goguen & Co. have
> been using "institution theory" for related purposes:
>
> http://citeseer.nj.nec.com/384650.html
>
> "Abstract: Institutions formalize the intuitive notion
> of logical system, including both syntax and semantics."
>
> Following is the plain text version of the HTML file cited above.
>
> John Sowa
>
> ---------------------------------------------------------------
>
> Meaning-Preserving Translations
>
> by John F. Sowa
>
> Informally, different statements in different languages can 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.
>
> According to Peirce (1905), "The meaning of a proposition is itself a
> proposition. Indeed, it is no other than the very proposition of which it
> is the meaning: it is a translation of it." Mathematically, Peirce's
> informal statement may be formalized by defining a proposition as an
> equivalence class of sentences that can be translated from one to another
> while preserving meaning. Some further criteria are necessary to specify
> what kinds of translations are considered to "preserve meaning." Formally,
> a meaning-preserving translation f from a language L1 to a language L2 may
> be defined as a function that satisfies the following constraints:
>
> * Invertible. The translation function f must have an inverse function g
> that maps sentences from L2 back to L1. For any sentence s in L1, f(s)
> is a sentence in L2, and g(f(s)) is a sentence in L1. All three
> sentences, s, f(s), and g(f(s)) are said to express the proposition p.
>
> * Proof preserving. When a sentence s in L1 is translated to f(s) in
> L2 and back again to g(f(s)) in L1, the result might not be identical
> to s. But according to the rules of inference of language L1, each
> one must be provable from the other: s|-g(f(s)), and g(f(s))|-s.
> Similarly, f(s) and f(g(f(s))) must be provable from each other by
> the rules of inference of language L2.
>
> * Vocabulary preserving. When s is translated from L1 to L2 and back to
> g(f(s)), the logical symbols like ∀ and the syntactic markers
> like commas and parentheses might be replaced by some equivalent.
> However, the same content words or symbols that represent categories,
> relations, and individuals in the ontology must appear in both
> sentences s and g(f(s)). 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.
>
> * Structure preserving. When s and g(f(s)) are mapped to Peirce Normal
> Form (with negation ~, conjunction &, and the existential quantifier
> ∃ as the only logical operators), they must contain exactly
> the same number of negations and existential quantifiers, nested in
> semantically equivalent patterns.
>
> These four criteria ensure that the sentences s and g(f(s)) are highly
> similar, if not identical. If s is the sentence "Every farmer who owns a
> donkey beats it", then the sentence g(f(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 are provably equivalent, they have the same
> content words, and they have the same structure when expressed with only
> &, ~, and ∃.
>
> Attempts to apply formal definitions to natural languages are fraught
> with pitfalls, exceptions, and controversies. To avoid such problems, the
> definition of meaning-preserving translation may be restricted to formal
> languages, like CGs and KIF. The sample sentence in Figure 5.12 could be
> defined as part of a formal language, controlled English, which happens
> to contain many sentences that look like English. Yet even for formal
> languages, the four criteria require further explanation and justification:
>
> * Invertible. The functions f and g are not exact inverses, since
> g(f(s)) might not be identical to s. To ensure that f 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.
>
> * Proof preserving. Preserving provability is necessary for meaning
> preservation, but it is not sufficient. It is a weak condition that
> allows all tautologies to be considered equivalent, even though the
> proof of equivalence might take an exponential amount of time.
> Informally, the test to determine whether two sentences "mean the
> same" should be "obvious." Formally, it should be computable by an
> efficient algorithm -- one whose time is linearly or polynomially
> proportional to the length of the sentence.
>
> * Vocabulary preserving. Two sentences that mean the same should talk
> about the same things. The sentence Every cat is a cat is provably
> equivalent to Every dog is a dog, even though one is about cats and
> the other is about dogs. Even worse, both of them are provably
> equivalent to a sentence about nonexistent things, such as Every
> unicorn is a unicorn. An admissible translation could make some
> changes to the syntactic or logical symbols, as in the sentence If
> something is a cat, then it is a cat. It might replace the word cat
> with domestic feline, but it should not replace the word cat with dog
> or unicorn.
>
> * Structure preserving. Of all the logical operators, conjunction &
> is the simplest and least controversial, while negation ~ introduces
> serious logical and philosophical problems. Intuitionists, for
> example, deny that ~~p is identical to p. 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. Computationally, ~~p and p have different
> effects on the binding of values to variables in Prolog, SQL, and many
> expert systems. The constraints on quantifiers and negations help
> ensure that formulas in the same equivalence class have the same
> properties of decidability and computational complexity.
>
> These 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.
>
> Examples of Meaning-preserving Translations. To illustrate the issues,
> consider meaning-preserving translations between two different notations
> for first-order logic. Let L1 be predicate calculus with Peano's symbols
> &, ∨, ~, ->, ∃, and ∀, and let L2 be predicate
> calculus with Peirce's symbols +, x, -, -<, Σ, and Π.
> Then for any formulas or subformulas p and q in L1,
> let f produce the following translations in L2:
>
> * Conjunction. p&q => pxq.
>
> * Disjunction. p∨q => -(-px-q).
>
> * Negation. ~p => -p.
>
> * Implication. p->q => -(px-q).
>
> * Existential quantifier. (∃x)p => Σx p.
>
> * Universal quantifier. (∀x)p => -Σx -p.
>
> The sentences generated by f use only the operators x, -, and
> Σ, but the inverse g is defined for all operators in L2:
>
> * Conjunction. pxq => p&q.
>
> * Disjunction. p+q => p∨q.
>
> * Negation. -p => ~p.
>
> * Implication. p-<q => p->q.
>
> * Existential quantifier. Σx p => (∃x)p.
>
> * Universal quantifier. Πx p => (∀x)p.
>
> The functions f and g meet the criteria for meaning-preserving
> translations: they are invertible, proof preserving, vocabulary preserving,
> and structure preserving. Furthermore, the proof of equivalence can be
> done in linear time by showing that two sentences s and t in L1 map to
> the same form with the symbols &, ~, and ∃.
>
> The functions f and g in the previous example show that it is possible to
> find functions that meet the four criteria. They don't map any sentences
> to the same equivalence class unless they can be said to "preserve
> meaning" in a very strict sense, but they leave many closely related
> sentences in different classes: permutations such as p&q and q&p;
> duplications such as p, p&p, and p&p&p; and formulas with renamed
> variables such as (∃x)P(x) and (∃y)P(y). To include more
> such sentences in the same equivalence classes, a series of functions
> f1, f2, ..., can be defined, all of which have the same inverse g:
>
> 1. Sorting. The function f1 makes the same symbol replacements as f,
> but it also sorts conjunctions in alphabetical order. As a result,
> p&q and q&p in L1 would both be mapped to pxq in L2, which would be
> mapped by g back to p&q. Therefore, f1 groups permutations in the
> same equivalence class. Since a list of N terms can be sorted in
> time proportional to NlogN, the function f1 takes just slightly
> longer than linear time.
>
> 2. Renaming variables. The function f2 is like f1, but it also renames
> the variables to a standard sequence, such as x1 ,x2 , ... . For
> very long sentences with dozens of variables of the same type, the
> complexity of f2 could increase exponentially. A typed logic can
> help reduce the number of options, since the new variable names
> could be assigned in the same alphabetical order as their type
> labels. For the kinds of sentences used in human communications,
> most variables have different types, and the computation time for
> f2 would be nearly linear.
>
> 3. Deleting duplicates. After f1 and f2 sort conjunctions and rename
> variables, the function f3 would eliminate duplicates by deleting
> any conjunct that is identical to the previous one. The deletions
> could be performed in linear time.
>
> For the kinds of sentences that people speak and understand,
> the total computation time of all three functions would be
> nearly linear. Although it is possible to construct sentences
> whose computation time would increase exponentially, those
> sentences would be hopelessly unintelligible to humans.
> What is unnatural for humans would be inefficient for
> computers.
>
> This series of functions shows how large numbers of closely related
> sentences can be reduced to a single canonical form. If two sentences
> express the same proposition, their canonical forms, which can usually
> be calculated efficiently, would be the same. The function f2 has the
> effect of reducing sentences to Peirce Normal Form (PNF) -- the result
> of translating a sentence from predicate calculus to an existential graph
> and back again. 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." When translated to L2 by f3 and back to L1 by g, it has
> the following Peirce Normal Form:
>
> * ~((~(p & ~r) & ~(q & ~s)) & ~(~(p & q) & ~(r & s)) ).
>
> This form is not as readable as the original, but it serves as the
> canonical representative of an equivalence class that contains 864
> different, but highly similar sentences. The function f3, which deletes
> duplicates, can reduce an infinite number of sentences to the same form.
> Such transformations can factor out the differences caused by the choice
> of symbols or syntax.
>
> To account for synonyms and definitions, another function f4 could be used
> to replace terms by their defining lambda expressions. 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, f4 should only expand definitions without
> recursions, direct or indirect. Since the definitions may introduce
> permutations, duplications, and renamed variables, f4 should expand
> the definitions before performing the reductions computed by f3.
> Without recursion, the expansions would take at most polynomial time.
>
> Meaning in Natural Languages. When functions like the fi series are
> extended to natural languages, they become deeply involved with the
> problems of syntax, semantics, and pragmatics. In his early work on
> transformational grammar, Noam Chomsky (1957) hoped to define
> transformations as meaning-preserving functions. But the transformations
> that moved phrases and subphrases had the effect of changing the scope of
> quantifiers and the binding of pronouns to their antecedents:
>
> * Every cat chased some mouse.
> => Some mouse was chased by every cat.
>
> * We do your laundry by hand; we don't tear it by machine.
> => We don't tear your laundry by machine; we do it by hand.
>
> To account for the implications of such transformations,
> Chomsky (1982) developed his theory of government and binding,
> which replaced all transformations by a single operator called
> move-α and a set of constraints on where the phrase α
> could be moved. In his most recent minimalist theory, Chomsky (1995)
> eliminated movement altogether and formulated the principles of grammar
> as a set of logical constraints. With that theory, both language generation
> and interpretation become constraint-satisfaction problems of the kind discussed
> in Section 4.6. The common thread running through these theories is Chomsky's search
> for a syntax-based characterization of the meaning-preserving translations.
>
> AI-based computational linguistics has also involved a search for
> meaning-preserving translations, but with more emphasis on semantics
> and pragmatics than on syntax. Roger Schank (1975), for example, developed
> his conceptual dependency theory as a canonical representation of meaning
> with an ontology of eleven primitive action types. Although Schank was
> strongly opposed to formalization of any kind, his method of reducing
> a sentence to canonical form could be viewed as a version of function f4.
> In his later work (Schank & Abelson 1977; Schank 1982), he went beyond
> the sentence to higher-level structures called scripts, memory organization
> packets (MOPs), and thematic organization packets (TOPs). These structures,
> which have been implemented in framelike and graphlike versions of EC logic,
> address meaning at the level of paragraphs and stories. Stuart Shapiro and
> his colleagues have implemented versions of propositional semantic networks,
> which support similar structures in a form that maps more directly to logic
> (Shapiro 1979; Shapiro & Maida 1982; Shapiro & Rappaport 1992). Shapiro's
> propositional nodes serve the same purpose as Peirce's ovals and McCarthy's
> contexts.
>
> Besides the structural forms of syntax and logic, the meaning-preserving
> translations for natural languages must account for the subtle interactions
> of many thousands of words. The next two sentences, for example, were
> adapted from a news report on finance:
>
> * The latest economic indicators eased concerns that inflation is
> increasing.
>
> * The latest economic indicators heightened concerns that inflation is
> increasing.
>
> The first sentence implies that inflation is not increasing, but the second
> one implies that it is. The negation, which is critical for understanding
> the sentences, does not appear explicitly. Instead, it comes from an
> implicit negation in the meaning of the noun concern: if some agent x has
> a concern about y, then x hopes that some bad event does not happen to y.
> The concern is eased when the bad event is less likely to occur, and the
> concern is heightened when the bad event is more likely to occur. In the
> normal use of language, people understand such sentences and their implications.
> For a computer to understand them, it would require detailed definitions of the
> words, background knowledge that rising inflation is bad for the economy, and
> the reasoning ability to combine such information. Doug Lenat and his group
> in the Cyc project have been working since 1984 on the task of encoding and
> reasoning with the millions of rules and facts needed for such understanding.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
John,
This very interesting to me, but I am trying
to work in recursed spite of a headache today,
and so I am looking forwared to returning to ut
in detail when the pain stops. I have of course
been specializing on the purely alpha level aspects
of this, and so it is probably best if I limit my
observations to what I know. Just off the top
of my head -- to coin a poignant phrase --
think about the sixteen "propositions",
that is, abstract truth functions on
two boolean vraiables, in the lattice
of the implication ordering. This is
the object domain. Then think about
all the various and sundry notational
schemes that you have seen for signing
these elements of this object structure.
The "logical equivalence classes" (LEC's)
of "sentences" (propositional expressions)
in each language then "reconstruct" over the
syntactic domain the structure of the object
domain. What sorts of factors would enter into
your chosing one language over another for this?
The degree of clutter in the LEC's, the difficulty
of getting to the canonical representatives of LEC's,
and so on, are factors that weigh against a particular
language. In this regard, Peirce's Alpha is pretty good,
while most of the languages that we still teach students are
a positive impediment to logical representation and reasoning.
Nuf Fer Now,
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤