Re: SUO: RE: Re: Peirce's MS 514
Chris,
I agree with your "niggling points" as I do with Pat's
"quibbles". (Which is bigger, a niggle or a quibble?)
I just had a niggle-quibbles about notation, since I believe
that it is possible to talk about propositions in a notation
independent way (at least with respect to a specified set of
notations).
>John wrote:
>
>> Matthew West wrote:
>>
>> >I'm glad you posted this, because I have been puzzled by the
>> >difference between inference (provability) and entailment
>> >for some time.
>> >
>> >Below you give the difference by:
>> >
>> >> 1. Provability: p is said to be _provable_ from A in some
>> >> logical system L iff there are rules of inference that
>> >> allow p to be derived by performing some operations on
>> >> the statements of A to generate the statement p.
>> >>
>> >> 2. Entailment: p is said to be _semantically entailed_ by
>> >> A iff in any state of affairs (or universe of discourse,
>> >> or possible world) for which all the statements of A are
>> >> true, the statement p is also true.
>> >
>> >Well I can see some difference, and that entailment should be
>> >stronger, but I don't really understand the difference.
>>
>> The basic point is that semantic entailment depends on the
>> subject matter, but provability depends on your choice of
>> notation for logic and the rules of inference associated with
>> it.
>
>Niggling point: entailment depends on notation as well, since it is
>always some set of statements in some notation (some language) that
>entails some other sentence in that notation.
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.)
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.
>> Provability can be defined in terms of the syntax of the notation,
>> but entailment depends on the semantics of whatever subject is under
>> consideration.
>
>Right. In a little more detail, a statement S is provable from a set
>of statements M iff there is a proof of S from M, where such a proof
>(in classical logic) is just a finite sequence of sentences S1, ...,
>Sn, where each Si is either an axiom of the proof procedure, a member
>of M, or is warranted by some rule of inference like Modus Ponens. A
>proof is thus a finite, purely syntactic object whose legitimacy can
>be checked mechanically (assuming that there is a mechanical test for
>membership in your set M). Note that there is no notion of *meaning*
>involved in the concept of a proof.
>
>By contrast, S is entailed by M iff any interpretation of the language
>of S and M that makes all of the members of M true also makes S true;
>again, iff any way of assigning meanings to the nonlogical expressions
>of S and the members of M that makes the members of M true also makes
>S true. Note that there is no notion of inference rules or mechanical
>checking involved in the concept of entailment. It is a purely
>semantic notion.
>
>The concepts of provability and entailent are thus, conceptually,
>completely different. It is therefore a rather wondrous thing that
>the two can be shown (by means of soundness and completeness proofs)
>to match up exactly in first-order logic: M entails S iff S is
>provable from M.
>
>> >Presumably there are cases where something can be proved through
>> >inference, but is not entailed.
>
>Such a system would be useless in classical logic; soudness is a
>minimum criterion that any classical system must meet, as the point of
>a proof theory is to mirror entailment as far as possible. As John
>notes, there may be more flexible, nonclassical logics where this does
>not hold.
>
>> With his famous incompleteness theorem, Kurt Goedel proved that
>> higher-order logic is not complete: there are true statements
>> of arithmetic that are not provable.
>
>Though this holds as much for first-order as for higher-order systems
>of arithmetic. Indeed, the incompleteness of higher-order logics can
>be shown to follow from the incompleteness of first-order arithmetic.
>But note that there are two quite different notions of completeness at
>work here that it is important to distinguish. John defined the
>notion of the completeness of a *proof procedure* for a language
>relative to some semantic theory for the language. Goedel's notion of
>completeness has to do with *theories* (i.e., sets of sentences is
>some language). Say that a theory T is *negation-complete* iff, for
>any sentence S of the language of T, either S is provable from T or ~S
>is provable from T. What Goedel showed is that every attempt to
>axiomatize arithmetic is bound to fail; any (decidable) set of axioms
>in the language of arithmetic that you propose, i.e., any (decidable)
>theory in that language, will either be inconsistent or will not be
>negation-complete -- i.e., there will be some sentence S of the
>language of arithmetic such that neither S nor ~S is provable from
>your theory. (Actually, this form of Goedel's theorem, due to Rosser,
>is slightly stronger than Goedel's original theorem.) Your theory
>will, in particular, as John notes, fail to prove some sentence that
>expresses a truth of arithmetic.
>
>From this, the incompleteness of higher-order logic can be shown to
>follow: there is no complete proof procedure for higher-order
>languages. In particular, for any proposed proof procedure for a
>higher-order language, there will always be sentences S of the
>language that are logically valid (i.e., true in every interpretation
>of the language) but which are not theorems (i.e., are not provable
>from the axioms of the proof procedure).
John