SUO: Re: Critique Of Non-Functional Reason
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
As a rule, "usage varies".
It's just my guess that any group that wants to standardize others
is going to have to learn a number of different languages, natural
and technical, and to accommodate various perspectives. This will
take language-independent ways to describe important concepts and
distinctions -- which does not mean escaping language but working
over many diverse ways of expressing things.
John F. Sowa wrote:
>
> Seth Russell wrote:
>
> > Now what exactly was wrong with using implies?
>
> There are three symbols that are commonly used in books and papers
> on logic. They represent different, but related, notions of what
> it means to say "if p then q" in English:
>
> 1. The symbol => (also written as a horseshoe) represents
> material implication, sometimes called implication.
Many folks make a big deal about the distinction between the "connectives",
which have a generic type SC^k -> SC, and the "statemnts about statements",
which result from an operation of type SN^k -> SC, where SN is the type of
a statement name. For them, arrows and horseshoes signify the connective
called a "conditional", whereas "implies" marks a predicate, a relation,
or a statement about statements.
> 2. The symbol |- (with no gap between the vertical and horizontal
> lines) represents provability.
Some people use this for "truth table" truths, which they consider to
be "proof-theoretic" in a trivial sense of being purely syntactically
checkable. Other people consider truth tables to be "model-theoretic"
and point to the fact that they used to be called "semantic tableaux".
And who ever said that proof-theoretic and model-theoretic had to be
mutually exclusive ideas, even in intension, in their boundary cases?
Also, "|-", with nothing on the left, is used for assertion, the way
that an axiom is a limit case of provability.
> 3. The symbol |= (also with no gap) represents semantic entailment,
> also called entailment.
The word "entailment" is reserved by many for "relevance logic".
The model-theoretic "|=" is also standardly called "consequence".
Standards vary. And most of these verbal distinctions get kicked in the
the cropper as soon as you translate them between other natural languages.
A "standard" presentation of model theory:
| C.C. Chang & H.J. Keisler, 'Model Theory',
| North-Holland, Amsterdam, Netherlands, 1973.
http://suo.ieee.org/ontology/msg03246.html
http://suo.ieee.org/ontology/msg03247.html
http://suo.ieee.org/ontology/msg03248.html
http://suo.ieee.org/ontology/msg03249.html
http://suo.ieee.org/ontology/msg03250.html
http://suo.ieee.org/ontology/msg03251.html
http://suo.ieee.org/ontology/msg03252.html
http://suo.ieee.org/ontology/msg03254.html
Jon Awbrey
> Following is a brief explanation taken from Chapter 5 of my book
> on knowledge representation.
>
> John Sowa
> ______________________________________________________________________
>
> The three operators =>, |-, and |= represent different ways of
> formalizing _if-then_: => is a Boolean operator that appears in
> ordinary formulas of logic; |- and |= are _metalevel operators_
> that appear in statements about logic. Semantic entailment is more
> fundamental than provability because it derives the truth of formulas
> from facts about the world (or some model of the world). Provability
> depends on the rules of inference of a particular version of logic,
> and those rules must be justified in terms of entailment.
>
> For classical first-order logic, the distinction between |- and |=
> can be ignored because soundness and completeness guarantee that they
> are equivalent. For other versions of logic, however, they must be
> carefully distinguished. Kurt Goedel (1931) proved the _incompleteness_
> of higher-order logic by finding propositions entailed by |= that are
> not provable by |-. Nonmonotonic logic, which is discussed in Chapter
> 6, is not even sound. Instead of preserving truth, the nonmonotonic
> rules of inference preserve only the weaker property of consistency:
> all true statements must be consistent, but not all consistent
> statements are true.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤