Re: SUO: RE: Re: Peirce's MS 514
>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,
They should be precisely the same strength, in an ideal world.
>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. Provability can be defined in terms of the syntax of the
>notation, but entailment depends on the semantics of whatever
>subject is under consideration.
That isnt *quite* right. Both of them depend on what nowadays would
be called the 'namespace', ie the set of relation and individual
names used. Strictly speaking one can only define entailment or
provability with respect to a given vocabulary (called the
'signature' of the language in logic). [Only a technical quibble.]
The common example of the need for care over the choice of namespace
is that of Skolem functions, which are 'new' function symbols are
introduced to replace existential quantifiers, so that one can replace
(forall (?x) (exists (?y) (R ?x ?y))
with
(forall (?x)(R ?x (fun ?x)))
These are almost the same in meaning, if you think about it, but the
first does not entail the second because the second one uses a symbol
which isnt in the namespace of the first one.
> >Presumably there are cases where something can be proved through
> >inference, but is not entailed. Could you give an example of
> >that please?
That would be an invalid inference. For example if you were to have
an inference rule that said that if P isn't provable, then infer
not-P (often called negation by failure), then your system of rules
could prove things that are not entailed (relative to the usual
logical interpretations. You can give a different notion of
interpretation relative to which it would be entailed, however.
Entailment is always relative to the semantics you are assuming the
notation to have.)
There are plenty of examples of the opposite, where something is
entailed but some system of rules is unable to make the inferential
connection. Those systems of rules would be incomplete (relative to
the semantics in question). For example, most description logics are
seriously incomplete with respect to ordinary first-order semantics;
prolog is incomplete, since it cannot draw inferences involving
non-Horn clauses, and so on.
>.....
>First-order logic has the very nice property of being both
>sound and complete: everything that is provable is also true
>by semantic entailment, and everything that is semantically
>entailed is also provable.
>
>With his famous incompleteness theorem, Kurt Goedel proved that
>higher-order logic is not complete:
John, you might have pointed out that it was also K. Goedel who
proved the first-order completeness theorem.
Pat
---------------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola, FL 32501 (850)202 4440 fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes