From: Frederick Williams on
Christopher Menzel wrote:
>
> On 2010-06-19, George Greene <greeneg(a)email.unc.edu> wrote:
> > On Jun 19, 11:07� am, Frederick Williams
> ><frederick.willia...(a)tesco.net> wrote:
> >> "David C. Ullrich" wrote:
> >> > No, it is not true that FOL includes inference rules.
> >>
> >> [...]
>
> Now that's not true either, although I will not accuse you of lying
> about it. ;-) The other standard way of specifying a logic is model
> theoretic. That is, one specifies a language and a notion of an
> interpretation for the language in terms of which one defines a semantic
> notion of logical consequence. A corresponding deductive apparatus for
> such a logic may or may not be defined. In general, of course, it is
> impossible to provide a complete deductive apparatus for a given model
> theoretic logic -- consider standard second-order logic, for example.
> And, depending on one's purposes, there may not be any point in doing
> so.

I suppose David Ullrich might say that since he was writing of FOL in
particular that doesn't matter because for it the semantic notion and
the syntactic notion coincide. But still your point is well made.

In Fundamental Concepts of the Methodology of the Deductive Sciences (Ch
V of Logic, Semantics, Metamathematics), Tarski writes 'Every set of
sentences which contains all its consequences is called a _deductive
system_...'. So for him a deductive system is a set of a certain kind,
but one needs to know what the consequence relation is
>
> There is a well known collection of essays entitled _Model Theoretic
> Logics_, edited by Barwise and Feferman, that explores this notion of a
> logic in great technical detail.

About 15 years ago I didn't buy it because it was so expensive. Let's
just see what it costs now... Oh! 541.23 pounds sterling via Amazon.
Clearly I should have bought one then.

Anyway, I hope David Ullrich will return to the thread, because, though
I think he's right, I want to know if he's right for the reason I think
he's right!

--
I can't go on, I'll go on.
From: Chris Menzel on
On Sun, 20 Jun 2010 17:38:19 -0700 (PDT), George Greene
<greeneg(a)email.unc.edu> said:
> On Jun 20, 6:01 pm, Christopher Menzel <cmen...(a)philebus.tamu.edu>
> wrote:
>> On 2010-06-19, George Greene <gree...(a)email.unc.edu> wrote:
>> > One way to define ANY logic is by its inference rules.
>> > Even if these are not the totality of the definition, they are ALWAYS
>> > a CRUCIAL part of it.  
>>
>> Now that's not true either, although I will not accuse you of lying
>> about it. ;-)  The other standard way of specifying a logic is model
>> theoretic.
>
> The way you are about to describe IS NOT "other".
>
>> That is, one specifies a language and a notion of an interpretation
>> for the language in terms of which one defines a semantic notion of
>> logical consequence.
>
> ANY notion of logical consequence IS a rule of inference.

Oh, George, you character, you. It is a never ending source of
amusement how you regularly appeal to "global usage" and "standard
conventions" and then depart from such conventions with your own
idiosyncracies.

> To say that any wff is a logical consequence of some others IS TO SAY
> that it can BE INFERRED from them.

Actually, it isn't.

> If you have rules for determining what is a logical consequence OF
> what, then you have rules of inference.

Actually, you don't.

> The fact that they are defined semantically rather than syntactically
> (and are therefore what(GUFFAW), rules "of CONSEQUENCE" ?) DOES NOT
> STOP them from being rules of inference.

It is true that, while deductive systems in general and rules of
inference in particular are *typically* defined without any reference to
semantic notions, it is not in principle out of the question to do so.
(For example, IIRC, Boolos & Jeffrey defined the propositional base of
their system of predicate logic in the first couple of editions of
Computability and Logic simply to consist of all tautologies.) But your
general claim here is false. For a rule of inference in a formal,
deductive system (that is, the relation determined by the rule) has to
be decidable; there must be an effective procedure for checking whether
or not a statement S follows from the premises of the rule by means of
the rule. That is an essential part of the definition of a deductive
system. (Check, e.g., Enderton or Mendelson on this point if you want
confirmation.) In general, logical consequence isn't decidable and
hence cannot, in general, serve as a rule of inference.

>> A corresponding deductive apparatus for such a logic may or may not
>> be defined.  In general, of course, it is impossible to provide a
>> complete deductive apparatus for a given model theoretic logic --
>> consider standard second-order logic, for example.
>
> To the extent that the syntactic rules cannot be codified, the model-
> theoretic ones HAVE NOT BEEN specified.

You lost me there. Perhaps if you defined what it means to say a rule
is "codified" it might make sense.

> It is hardly relevant to say that X WOULD be a semantic consequence of
> Y when YOU CAN'T TELL whether it is, or not.
>
> The semantic definition IS NOT an alternative to the syntactic one.

Actually, it is.

>> And, depending on one's purposes, there may not be any point in doing
>> so.  
>
> If THOSE are one's purposes then there MOST CERTAINLY is "not any
> point" in EVEN *CALLING* the result "a logic"! CLUE:
> http://www.gwu.edu/~philosop/news_events/documents/Pedeferri1.pdf

Ah, so your "clue" is a single unpublished paper that seems to kinda
sorta support your claims. I don't really have the inclination to read
it carefully, but I'd want first to know what the author means by "the
complete deductive system for second order logic", since no such thing
can exist in any standard sense of "deductive system".

>> There is a well known collection of essays entitled _Model Theoretic
>> Logics_, edited by Barwise and Feferman, that explores this notion of a
>> logic in great technical detail.
>
> I'm sure, but this does not change the fact that if you cannot tell at
> least APPROXIMATELY what is a consequence of what, then you have
> completely defeated the purpose.

You should study the book to see what the various "purposes" are.

> Standard classical FOL is standard BECAUSE (among many other reasons)
> THERE IS a complete syntactic characterization of its semantic
> consequence relation. But to the extent that ANY semantic consequence
> relations ARE UNDERSTOOD, AT ALL, that understanding is CODIFIED
> *VIA*RULES*, EVEN when the rules are not explicitly syntactic or
> complete.

Sorry, but you're just making this stuff up.

From: George Greene on
On Jun 21, 2:24 pm, Chris Menzel <cmen...(a)remove-this.tamu.edu> wrote:
> On Sun, 20 Jun 2010 17:38:19 -0700 (PDT), George Greene

> > ANY notion of logical consequence IS a rule of inference.  
>
> Oh, George, you character, you.  It is a never ending source of
> amusement how you regularly appeal to "global usage" and "standard
> conventions" and then depart from such conventions with your own
> idiosyncracies.

I fully concur.
This is exactly what has happened here.
However, you still have a problem:
what you have said here IS NOT A REFUTATION of what I said.
The fact that global usage and standard conventions do not necessarily
conform to what I said here IS THEIR PROBLEM AND NOT mine!
This is arguably A DEFICIENCY IN the traditional usage.
This field IS ALWAYS having to come up with TECHNICAL TERMS,
BECAUSE the terms it chooses to use ALREADY HAD NATURAL LANGUAGE
DEFINTIONS from which THE FIELD NEEDS to DEPART in employing
the terms! This kind of departure IS ALWAYS objectionable and we
mute our objections routinely BECAUSE the "generally accepted" terms
are simply THE BEST WE CAN DO. We mute our objections "faute de
mieux",
for lack of anything better. This does not change the fact that the
natural language
meanings of the terms still exist and still matter, and it does not
change the
fact that revising their meanings when using technical terms is a
necessary EVIL.
It is something to be mitigated where possible.


> > To say that any wff is a logical consequence of some others IS TO SAY
> > that it can BE INFERRED from them.  
>
> Actually, it isn't.

Actually, it is. What I said was purely analytic.
It almost wouldn't bear belaboring, LET ALONE contradicting.
Imply and infer are just like that.


> > If you have rules for determining what is a logical consequence OF
> > what, then you have rules of inference.  
>
> Actually, you don't.

Actually, you do.
Gee, that was easy.
You are mis-perceiving YOUR OWN side of the debate here.
YOU are supposed to be taking the side that says, having defined
some notion of semantic consequence, your "definition" can still be
such
that there canNOT ACTUALLY BE "rules" for determining what is a
semantic
consequence of what. You can give a criterion but you can't
necessarily compute
whether any particular pair does or doesn't satisfy it.
But you are now reducing me to arguing your side AS WELL AS mine.
You are supposed to be able to tell WHAT the opposite of a position
is,
if you are going to presume to publicly contradict it.


> > The fact that they are defined semantically rather than syntactically
> > (and are therefore what(GUFFAW), rules "of CONSEQUENCE" ?) DOES NOT
> > STOP them from being rules of inference.
>
> It is true that, while deductive systems in general and rules of
> inference in particular are *typically* defined without any reference to
> semantic notions, it is not in principle out of the question to do so.

Here, you have COMPLETELY SWITCHED SIDES!
I DID NOT SAY that it was out of the question to define things
semantically!
What *I*SAID* was that EVEN when you define consequence semantically,
the fact that you are DEFINING something and giving CRITERIA AND
GUIDELINES
for when this or that is or is not a semantic consequence of that or
this, YOU ARE
GIVING AND USING *RULES* to do this!!
In the paragraph that follows, you are arguing a point that IS NOT
BEING disputed!
The issue was about non-standard usage of "rules of inference", NOT
about whether
semantic consequence happens! OF COURSE it happens! It happens EVEN
in
contexts (like standard classical FOL) where a complete syntactic rule-
structure
is concomitantly available! In all OTHER contexts, the semantic
consequence, far from needing
your defense, is NECESSARILY going to be PRIMARY!
NOBODY was disputing THAT!

> (For example, IIRC, Boolos & Jeffrey defined the propositional base of
> their system of predicate logic in the first couple of editions of
> Computability and Logic simply to consist of all tautologies.)  But your
> general claim here is false.  For a rule of inference in a formal,
> deductive system (that is, the relation determined by the rule) has to
> be decidable

I'm sorry, that is just arbitrary bullshit.
Think about it:
WHAT are you saying has to be decidable??

"The relation determined by the rule" ??
THIS IS SELF-contradictory! If the relation should turn out NOT to be
decidable,
then according to you here, the relation IS NOT associated with ANY
*RULE OF INFERENCE*.
In other words, THERE IS NO rule any more, so we CAN'T SAY "the
relation determined by the rule".
There has to be SOME PRIOR consequence relation.
You are basically saying that we can associate "a rule of inference"
with this relation if the
relation is decidable. To which the obvious retort would be, WHAT
relation??
HOW WAS THE RELATION EVEN SPECIFIED IN THE FIRST PLACE??
If the description of the relation WAS EVEN UNAMBIGUOUS, if you even
KNOW WHAT RELATION YOU ARE TALKING ABOUT, then RULES WERE INVOLVED.
You are trying to defend a standard usage here that I am simply not
obligated to
respect. If somebody has "specified a consequence relation" BY ANY
means,
but STILL can't tell what is a consequence of what, then there may be
something
interesting going on here, but it is hardly logic.

> Ah, so your "clue" is a single unpublished paper that seems to kinda
> sorta support your claims. I don't really have the inclination to read
> it carefully,

Oh, SHUT UP.
You don't NEED to read any ONE paper carefully to know that
"2nd-order logic IS NOT logic" is a thesis.
YOU COULD GOOGLE IT.
There are MANY CLUES AVAILABLE.
The mere existence of the meme refutes you.
From: Chris Menzel on
On Mon, 21 Jun 2010 12:11:51 -0700 (PDT), George Greene
<greeneg(a)email.unc.edu> said:
> On Jun 21, 2:24 pm, Chris Menzel <cmen...(a)remove-this.tamu.edu> wrote:
>> On Sun, 20 Jun 2010 17:38:19 -0700 (PDT), George Greene
>
>> > ANY notion of logical consequence IS a rule of inference.  
>>
>> Oh, George, you character, you.  It is a never ending source of
>> amusement how you regularly appeal to "global usage" and "standard
>> conventions" and then depart from such conventions with your own
>> idiosyncracies.
>
> I fully concur.
> This is exactly what has happened here.
> However, you still have a problem:
> what you have said here IS NOT A REFUTATION of what I said. The fact
> that global usage and standard conventions do not necessarily conform
> to what I said here IS THEIR PROBLEM AND NOT mine! This is arguably A
> DEFICIENCY IN the traditional usage. This field IS ALWAYS having to
> come up with TECHNICAL TERMS, BECAUSE the terms it chooses to use
> ALREADY HAD NATURAL LANGUAGE DEFINTIONS from which THE FIELD NEEDS to
> DEPART in employing the terms! This kind of departure IS ALWAYS
> objectionable and we mute our objections routinely BECAUSE the
> "generally accepted" terms are simply THE BEST WE CAN DO. We mute our
> objections "faute de mieux", for lack of anything better. This does
> not change the fact that the natural language meanings of the terms
> still exist and still matter, and it does not change the fact that
> revising their meanings when using technical terms is a necessary
> EVIL. It is something to be mitigated where possible.

Well, ok, but we're talking about concepts out of formal logic here.
I don't really care about whether the names for those concepts departs
from their natural language meanings. Perhaps they do and if it really
bothers you we can use different words. But my post only had to do with
those concepts, not with the suitability of their names.

>> > To say that any wff is a logical consequence of some others IS TO SAY
>> > that it can BE INFERRED from them.  
>>
>> Actually, it isn't.
>
> Actually, it is. What I said was purely analytic. It almost wouldn't
> bear belaboring, LET ALONE contradicting. Imply and infer are just
> like that.

It may be analytic in ordinary language, but what you say doesn't follow
if by "logical consequence" we mean model theoretic consequence and if
by "can be inferred" we mean provability in a deductive system (hence
one whose axioms and inference rules are decidable). That was my only
point.

>> > If you have rules for determining what is a logical consequence OF
>> > what, then you have rules of inference.  
>>
>> Actually, you don't.
>
> Actually, you do.

Not if "logical consequence" and "rules of inference" are understood
noted. If you are going to deny that, then you are either confused or
you simply have changed the subject (e.g., to the question of the
meanings of those expression in ordinary language).

> You are mis-perceiving YOUR OWN side of the debate here.

No, really, I'm not.

> YOU are supposed to be taking the side that says, having defined some
> notion of semantic consequence, your "definition" can still be such
> that there canNOT ACTUALLY BE "rules" for determining what is a
> semantic consequence of what.

Well, if I may, my "side" is that, a definition of semantic consequence
cannot, in general, of itself, serve as a rule of inference in a
deductive system, for the simple reason that (a) the semantic
consequence relation is not, in general, decidable and (b) the relation
determined by a legitimate rule of inference must be decidable. Note
that there isn't really a *side* here. This is just a simple fact of
basic mathematical logic.

> You can give a criterion but you can't necessarily compute whether any
> particular pair does or doesn't satisfy it. But you are now reducing
> me to arguing your side AS WELL AS mine. You are supposed to be able
> to tell WHAT the opposite of a position is, if you are going to
> presume to publicly contradict it.

This is terribly confusing. You said (or so it appeared) that if you
have a notion of logical (a.k.a‥, semantic) consequence, then you have a
rule of inference. I pointed out that, on standard understandings of
"logical consequence" and "rule of inference", that is false. I'm not
sure how things could be clearer.

>> > The fact that they are defined semantically rather than
>> > syntactically (and are therefore what(GUFFAW), rules "of
>> > CONSEQUENCE" ?) DOES NOT STOP them from being rules of inference.
>>
>> It is true that, while deductive systems in general and rules of
>> inference in particular are *typically* defined without any reference to
>> semantic notions, it is not in principle out of the question to do so.
>
> Here, you have COMPLETELY SWITCHED SIDES!

No, I totally haven't. I simply said a notion of logical consequence
does not *in general*, of itself, yield a rule of inference in a
deductive system. It *could* (although it would be unusual to specify a
deductive system in terms of logical consequence), so long as the notion
of consequence in question is decidable.

> What *I*SAID* was that EVEN when you define consequence
> semantically, the fact that you are DEFINING something and giving
> CRITERIA AND GUIDELINES for when this or that is or is not a semantic
> consequence of that or this, YOU ARE GIVING AND USING *RULES* to do
> this!!

But these "RULES" don't necessarily yield deductive rules of inference.
That is what you were suggesting in your earlier original post and that
is what I was correcting.

>> (For example, IIRC, Boolos & Jeffrey defined the propositional base of
>> their system of predicate logic in the first couple of editions of
>> Computability and Logic simply to consist of all tautologies.)  But your
>> general claim here is false.  For a rule of inference in a formal,
>> deductive system (that is, the relation determined by the rule) has to
>> be decidable
>
> I'm sorry, that is just arbitrary bullshit.
> Think about it:
> WHAT are you saying has to be decidable??
>
> "The relation determined by the rule" ??

Yes.

> THIS IS SELF-contradictory!

No, it really isn't. Here's an example: The rule Modus Ponens "B
follows from A and A->B" determines the relation consisting of all those
pairs of the form <{A,A->B},B>. That's a decidable relation. See? Not
contradictory. (And, actually, if we really want to get all abstract
and technical about it, the rule of inference just IS the relation in
question.)

> If the relation should turn out NOT to be decidable, then according to
> you here, the relation IS NOT associated with ANY *RULE OF INFERENCE*.
> In other words, THERE IS NO rule any more, so we CAN'T SAY "the
> relation determined by the rule".

Well, I should have thought the idea was clear enough, but let me spell
it out a little more. I can give you a "rule", a definition, that
determines all sorts of relations. But, once again, in order for such a
definition to count as a formal *rule of inference* in a deductive
system, the relation in question has to be decidable. Contrast the rule
MP above with the rule "B follows from A if B is true in every model in
which A is true". That determines the relation {<A,B> | {A} |= B}, and
that relation is not (in general) decidable. Hence, if the relation is
not decidable, that "rule" won't do as a rule of inference in a formal,
deductive system.

> There has to be SOME PRIOR consequence relation. You are basically
> saying that we can associate "a rule of inference" with this relation
> if the relation is decidable.

That is correct.

> To which the obvious retort would be, WHAT relation?? HOW WAS THE
> RELATION EVEN SPECIFIED IN THE FIRST PLACE??

Any number of ways. In my example above I specified it using standard
model theoretic notions. Isn't that obvious?

> If the description of the relation WAS EVEN UNAMBIGUOUS, if you even
> KNOW WHAT RELATION YOU ARE TALKING ABOUT, then RULES WERE INVOLVED.

In an informal sense of "rule" only.

> You are trying to defend a standard usage here that I am simply not
> obligated to respect.

I'm not *defending* it at all, I'm simply *using* it. If you wish to
depart from conventional usage, be my guest, but don't be surprised if
you say things that appear to be false or confused to others.

> If somebody has "specified a consequence relation" BY ANY means, but
> STILL can't tell what is a consequence of what, then there may be
> something interesting going on here, but it is hardly logic.

Well, the question of what deserves the honorific title "logic" is
perhaps an interesting question but it has nothing to do with what I've
been pointing out here, which is simply that there are two common,
non-equivalent ways of defining what a logic is: proof theoretic and
model theoretic.

From: George Greene on
On Jun 21, 2:24 pm, Chris Menzel <cmen...(a)remove-this.tamu.edu> wrote:
> >> There is a well known collection of essays entitled _Model Theoretic
> >> Logics_, edited by Barwise and Feferman, that explores this notion of a
> >> logic in great technical detail.

This is NOT any sort of SURPRISE.
Given that the most standard typical logic does in fact
HAVE A model theory (which is usually phrased in ZFC),
THE DEFAULT is for logics in general TO HAVE, NOT to lack,
a model theory. The default is for logics TO HAVE a semantics.
Typically, usually, BY DEFAULT, notions of logical consequence
IN GENERAL are going to be EXPECTED to be definABLE SEMANTICALLY,
in addition to whatever other ways may or may not be available.
THE QUESTION is going to be whether something syntactic (like
what YOU call "a rule of inference") is going to be definable in a way
that captures or "completely" covers the underlying semantic notion,
WHILE REMAINING tractable (or, as you claim, recursive).

Claiming this authority to banish things is over-claiming
REGARDLESS of standard parlance.
You can't banish all relations from "rule-of-inferencehood" that
happen not to be recursive (surely recursively ENUMERABLE would be
SUFFICIENT, since that is in fact what the theories resulting TURN OUT
TO BE,
when the axiom-sets themselves are recursive) while denying my
entitlement
to banish intractable consequence-relations from logic-hood-AT-ALL,
since
THE WHOLE PURPOSE of the endeavor is to in fact ascertain that some
later simpler things follow as consequences from earlier more
complicated ones.


MY point was that the underlying semantic consequence "relation",
ITSELF, HAS to be defined, specified, identified, or otherwise
articulated
IN SOME way, and THAT NECESSARILY involves RULES.


> > I'm sure, but this does not change the fact that if you cannot tell at
> > least APPROXIMATELY what is a consequence of what, then you have
> > completely defeated the purpose.
>
> You should study the book to see what the various "purposes" are.

I should study the book in any case, but I don't even care what THE
OTHER
purposes are. THIS purpose is an IMPORTANT enough purpose (indeed,
a foundationally important purpose; it in some sense subsumes
humanity's
ENTIRE INTELLECTUAL QUEST) that it deserves a term.

> > Standard classical FOL is standard BECAUSE (among many other reasons)
> > THERE IS a complete syntactic characterization of its semantic
> > consequence relation.  But to the extent that ANY semantic consequence
> > relations ARE UNDERSTOOD, AT ALL, that understanding is CODIFIED
> > *VIA*RULES*, EVEN when the rules are not explicitly syntactic or
> > complete.
>
> Sorry, but you're just making this stuff up.

THAT is NOT a refutation!

It's also excessive praise; I am hardly original or creative enough to
have
been the first person to have thought this.