Re: SUO: RE: Re: Peirce's MS 514
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.
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).
-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