RE: SUO: RE: Re: Peirce's MS 514
Dear Chris M,
Thank you for this exposition. It is very enlightening.
I have a few questions.
>
> 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.
>
> > 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.
MW: I'm still not quite there with entailment. Could you give an
example please?
>
> 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.
MW: Well that answers one question I had - why KIF has no concept of
entailment.
>
> > >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.
MW: Again, could you give an example please?
>
> From this, the incompleteness of higher-order logic can be shown to
> follow: there is no complete proof procedure for higher-order
> languages.
MW: Does this mean that higher order languages depend on arithmetic?
If so why doesn't a first order language?
> 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).
>
> -chris
>
> --
>
> Christopher Menzel # web: philebus.tamu.edu/~cmenzel
> Philosophy, Texas A&M University # net: chris.menzel@tamu.edu
> College Station, TX 77843-4237 # vox: (979) 845-8764
>
Regards
Matthew
===============================================================
Matthew West http://www.matthew-west.org.uk/
Principal Consultant Shell Visiting Professor
Operations & Asset Management The Keyworth Institute
Shell Services International The University of Leeds
http://www.shellservices.com/ http://www.keyworth.leeds.ac.uk/
H3229, Shell Centre, London, SE1 7NA, UK.
Tel: +44 207 934 4490 Fax: 7929 Mobile: +44 7796 336538
===============================================================