Why use incorrect quantifier rules in predicate logic?
Wolfgang Schwarz
Some axiomatic systems of predicate logic (e.g. Mendelson,
Kutschera/Breitkopf, and Hodges' in the Handbook of Philosophical
Logic) contain incorrect rules of inference such as
A -> B => A -> \forall x B(t/x)
provided that t does not occur in A
or
A => \forall x A(t/x)
These rules are incorrect in deductions from assumptions. That's why in
systems containing them the Deduction Theorem and the definition of
"correctness" have to be restricted.
Can anyone explain to me why these authors don't just add another
proviso to their incorrect rules, thereby making them correct (as some
other authors do), e.g.:
A -> B => A -> \forall x B(t/x)
provided that t does not occur in A nor in any assumption
of the current deduction.
Are there any advantages of using the incorrect rules, or is there an
historical explanation of their usage?
(The reason why I'm asking is that I have to convince somebody to use
correct rules in the introductory logic book he's writing. He agrees that
the incorrect rules aren't nice, as it is difficult to explain why e.g.
Fa & -Fa should be derivable from Fa & -Fb. But since he learned logic
from books using incorrect rules, he's afraid that they might after all
be essential for something we just don't see.)
Thanks for your help.
wo.
David C. Ullrich
<wolf...@umsu.de> wrote:
>Hello,
>
>Some axiomatic systems of predicate logic (e.g. Mendelson,
>Kutschera/Breitkopf, and Hodges' in the Handbook of Philosophical
>Logic) contain incorrect rules of inference such as
>
>A -> B => A -> \forall x B(t/x)
A better notation for this might be
A -> B |- A -> \forall x B(t/x)
or
A -> B
_______________
A -> \forall x B(t/x)
> provided that t does not occur in A
And the rules are _not_ incorrect, _in_ the systems in
which they are rules.
>or
>
>A => \forall x A(t/x)
>
>These rules are incorrect in deductions from assumptions. That's why in
>systems containing them the Deduction Theorem and the definition of
>"correctness" have to be restricted.
>
>Can anyone explain to me why these authors don't just add another
>proviso to their incorrect rules, thereby making them correct (as some
>other authors do), e.g.:
Because there _are_ no "assumptions" in the systems under
consideration. The rules you say are "incorrect" would be incorrect
in a different sort of deduction system, one that _has_ a notion
of "current assumption". But adding a condition about the assumptions
in a system where there's no such thing as an assumption would
be incoherent.
>A -> B => A -> \forall x B(t/x)
> provided that t does not occur in A nor in any assumption
> of the current deduction.
>
>Are there any advantages of using the incorrect rules, or is there an
>historical explanation of their usage?
>
>(The reason why I'm asking is that I have to convince somebody to use
>correct rules in the introductory logic book he's writing. He agrees that
>the incorrect rules aren't nice, as it is difficult to explain why e.g.
>Fa & -Fa should be derivable from Fa & -Fb. But since he learned logic
>from books using incorrect rules, he's afraid that they might after all
>be essential for something we just don't see.)
Why not start by explaining to us what's incorrect about these rules?
For example, a wff that can be proved, but which is not actually
valid. (If there is no such example then it's hard to see what's
"incorrect"...)
>Thanks for your help.
>
>wo.
******************
David C. Ullrich
Wolfgang Schwarz
Hi,
Thanks for your reply.
> >Can anyone explain to me why these authors don't just add another
> >proviso to their incorrect rules, thereby making them correct (as some
> >other authors do), e.g.:
>
> Because there _are_ no "assumptions" in the systems under
> consideration. The rules you say are "incorrect" would be incorrect
> in a different sort of deduction system, one that _has_ a notion
> of "current assumption". But adding a condition about the assumptions
> in a system where there's no such thing as an assumption would
> be incoherent.
[...]
> Why not start by explaining to us what's incorrect about these rules?
Okay, sorry if I wasn't clear enough on this point.
It is certainly possible to use the turnstile "|-" only as a provability
predicate, and not to talk about deducibility from given premises at
all. In such a system, the rule
UG) A
__________________
\forall x A(t(x)
is unobjectionable, because "|- A" really does imply "|- \forall x
A(t/x)". This is not the kind of system I meant to be talking about. I
was thinking of systems where the turnstile expresses a (two-place)
relation of deducibility, in which "S |- A" means "A can be deduced from
(the set of sentences) S". More precisely,
DED) S |- A iff there is a finite sequence of sentences ending with "A"
each of which is either an axiom, or an element of S, or can be
derived from previous sentences by an application of a rule.
Now this is what I meant by "correct" (maybe I should have said "sound"):
COR) A rule is correct iff whenever a sentence A can be derived from
other sentences B_1,...,B_n by an application of that rule, then
B_1,...,B_n |= A.
In this sense (UG) is not correct, because it allows the derivation of
"\forall x F(x)" from "Fa":
1. Fa
2. \forall x F(x)
From here, there are several possible ways to get a sound axiomatic system:
1) Restrict (UG) by adding as a proviso that the substituted term t
must not occur in the premises of the deduction.
2) Reject (DED) by redefining "|-", as follows:
DED') S |- A iff there is a finite sequence of sentences ending
with "A" each of which is either an axiom, or an element
of S, or can be derived from previous sentences by an
application of a rule, and in no case is the rule (UG)
applied to a sentence that contains a term which also
occurs in S.
3) Keep (DED), but redefine "sound", as follows:
SOU') The system P is sound iff whenever S |-_P A then S |= A,
provided that in the deduction of A from S in P, the rule
(UG) isn't applied to a sentence that contains a term
which also occurs in S.
I've seen instances of all three possibilities.
So finally, here is my question again: Why do some authors use (2) or
(3) rather than (1)? The redefinitions of "|-" and "sound" look quite ad
hoc to me. The same holds for the reformulation of the Deduction Theorem
that is necessary in both cases. And, as I tried to say in my original
posting, it is difficult to justify or explain the usage of a rule that
obviously allows the derivation of falsehoods from truths. (The only
explanation or justification is then to point at the soundness of the
entire system, together with (DED') or (SOU').)
Best,
wo.
David C. Ullrich
That's correct, it isn't. But nobody claims that it _is_
correct in this sense, in this setting! You started by asking
why people used incorrect rules - they're _not_ incorrect
in the setting in which they're claimed to be valid rules.
>because it allows the derivation of
>"\forall x F(x)" from "Fa":
> 1. Fa
> 2. \forall x F(x)
>
>From here, there are several possible ways to get a sound axiomatic system:
>
>1) Restrict (UG) by adding as a proviso that the substituted term t
> must not occur in the premises of the deduction.
>
>2) Reject (DED) by redefining "|-", as follows:
>
> DED') S |- A iff there is a finite sequence of sentences ending
> with "A" each of which is either an axiom, or an element
> of S, or can be derived from previous sentences by an
> application of a rule, and in no case is the rule (UG)
> applied to a sentence that contains a term which also
> occurs in S.
>
>3) Keep (DED), but redefine "sound", as follows:
>
> SOU') The system P is sound iff whenever S |-_P A then S |= A,
> provided that in the deduction of A from S in P, the rule
> (UG) isn't applied to a sentence that contains a term
> which also occurs in S.
>
>I've seen instances of all three possibilities.
>
>So finally, here is my question again: Why do some authors use (2) or
>(3) rather than (1)?
I don't know. I _suspect_ that the following may be a reason:
An unmodified UG seems nice, simple, elegant. (It can lead
to confusion if someone thinks that P(x) logically implies
Ax P(x), but someone who gets that idea gets it straight
pretty quick or there's no hope - in fact |-P(x) _does_
imply |- Ax P(x), which is all UG says.)
Now, it's true that UG doesn't work so well with
S|-P. But (I think???) there's no problem with
unrestricted UG for S|-P as long as there are no
free variables anywhere in S, and it seems to me
that that's the case that's typically of interest in
mathematics.
>The redefinitions of "|-" and "sound" look quite ad
>hoc to me. The same holds for the reformulation of the Deduction Theorem
>that is necessary in both cases. And, as I tried to say in my original
>posting, it is difficult to justify or explain the usage of a rule that
>obviously allows the derivation of falsehoods from truths. (The only
>explanation or justification is then to point at the soundness of the
>entire system, together with (DED') or (SOU').)
>
>Best,
>wo.
******************
David C. Ullrich
G. Frege
>
> 1) Restrict (UG) by adding as a proviso that the substituted term t
> must not occur in the premises of the deduction.
>
Yes.
>
> I've seen instances of all three possibilities.
>
Well, this may be so... but actually, GENTZEN (who was one of the inventors of
the calculus of natural deduction) had:
AE: Wenn Fa für 'beliebiges a' bewiesen ist, so gilt AxFx. Die
Voraussetzung, dass a "ganz beliebig" ist, lässt sich genau so
ausdrücken: Fa darf von keiner Annahme abhängen, in welcher die
Gegenstandsvariable a vorkommt. [...]"
(Gerhard Gentzen, Untersuchungen über das logische Schließen I)
In a modern adoption of Gentzen's system we find:
UI (Universal Quantifier Introduction)
[...] given A(e), we may derive (v)A(v) as conclusion, provided that
e occurs in no assumption on which A(e) depends. (...)
(E. J. Lemmon, Beginning Logic)
>
> So finally, here is my question again: Why do some authors use (2) or
> (3) rather than (1)?
>
I have no idea...
(Hence I stay with Gentzen and Lemmon... ;-)
F.
William Elliot
> Kutschera/Breitkopf, and Hodges' in the Handbook of Philosophical
> Logic) contain incorrect rules of inference such as
>
> A -> B => A -> \forall x B(t/x)
> provided that t does not occur in A
>
> or
>
> A => \forall x A(t/x)
>
> These rules are incorrect in deductions from assumptions. That's why in
> systems containing them the Deduction Theorem and the definition of
> "correctness" have to be restricted.
>
> Can anyone explain to me why these authors don't just add another
> proviso to their incorrect rules, thereby making them correct (as some
> other authors do), e.g.:
>
> A -> B => A -> \forall x B(t/x)
The rule of inference is
If S |- A, then S |- for all x, A(t/x)
provided no free x occures in any of the statements of S and no free
occurance of t in A, falls within the scope of a quantifer of x within A,
namely the substitution t/x causes no confusion of variables within A.
Wolfgang Schwarz
Hi again,
First, quick replies to the other answers in this thread:
Gottlob, I've never seen a system of Natural Deduction with rules of the
kind I misleadingly called "incorrect". I've only seen this in axiomatic
(Hilbert-Frege style) systems.
William, I think "provided no free x occures in any of the statements of
S" in your formulation is redundant. Did you mean "t" rather than "x"?
Then your suggestion amounts to the "correct", restricted version of
(UG) which I, too, favour. My question is why some authors don't use it.
"David C. Ullrich" wrote:
> >In this sense (UG) is not correct,
>
> That's correct, it isn't. But nobody claims that it _is_
> correct in this sense, in this setting!
Sure. I'm sorry to have caused this confusion. I should have said from
the beginning that a) I mean "correct" in this technical sense, and b) I
don't want to suggest that anything is formally wrong with systems that
use "incorrect" rules. My only complaint is a lack of elegance and perspicuitiy.
> >So finally, here is my question again: Why do some authors use (2) or
> >(3) rather than (1)?
>
> I don't know. I _suspect_ that the following may be a reason:
> An unmodified UG seems nice, simple, elegant. (It can lead
> to confusion if someone thinks that P(x) logically implies
> Ax P(x), but someone who gets that idea gets it straight
> pretty quick or there's no hope - in fact |-P(x) _does_
> imply |- Ax P(x), which is all UG says.)
If that was all UG says, it would be unusable in deductions from
assumptions, and the resulting system would be incomplete, I think
(unless of course there is another version of UG allowed in deductions
from assumptions). To get a strongly complete axiomatic system, in which
S |- A whenever S |= A (rather than just a weakly complete system in
which |- A whenever |= A), there has to be a rule to get to S |- Ax P(x)
from S |- P(x) in certain contexts.
I agree that the unmodified UG looks nicer, simpler and more elegant.
But the necessary reformulations of the Deduction Theorem and the
redefinition of "|-" are so obviously inelegant that I can't really
believe that it's desire for elegance that motivates the unrestricted UG.
> Now, it's true that UG doesn't work so well with
> S|-P. But (I think???) there's no problem with
> unrestricted UG for S|-P as long as there are no
> free variables anywhere in S, and it seems to me
> that that's the case that's typically of interest in
> mathematics.
I agree that the case where free variables occur in the premises of a
deduction might well be considered untypical or even meaningless. But
this certainly doesn't hold for constants. If the language in question
contains constants, like "0", the unrestricted UG only works well, i.e.
without a redefinition of "|-" and DT, if no set of premises ever
contains a constant.
Best,
wo.
David C. Ullrich
Is that so? You may well be right, but I don't see what the problem
with constants is.
Um, maybe the UG I have in mind is not the one you have in mind.
Take an example: Say 0 is a constant symbol, and S consists of
the axiom Ax(x+0 = x). So something like
[i]
S|-y+0=y
S|-Ay(y+0=y)
is no problem. _Are_ you maybe talking about a version of UG
that would allow something like the following?
[ii]
S|-y+0=y
S|-Ax(y+x=y).
_If_ something like [ii] is the problem you have in mind: Well
of course [ii] is wrong, and so if we have a version of UG that
allows [ii] it needs to be modified. But I wasn't aware that
anyone ever meant to allow anything like [ii] in the first
place when they say UG! (I could be wrong about that...
_if_ something like [ii] is actually included in some people's
"UG" then I agree that _that's_ "incorrect".)
Wolfgang Schwarz
hi,
> is no problem. _Are_ you maybe talking about a version of UG
> that would allow something like the following?
>
> [ii]
> S|-y+0=y
> S|-Ax(y+x=y).
exactly. Of course the free y is irrelevant: the systems I have in mind
need not allow open formulas in conclusions or premises.
> _If_ something like [ii] is the problem you have in mind: Well
> of course [ii] is wrong, and so if we have a version of UG that
> allows [ii] it needs to be modified. But I wasn't aware that
> anyone ever meant to allow anything like [ii] in the first
> place when they say UG!
It's definitely allowed in two (German) logic books I know (by
Kutschera/Breitkopf and Beckermann) I'll look up the passages in
Mendelson and Hodges again. Maybe they really only allow your variant
[i] of UG.
wo.
Wolfgang Schwarz
hello,
> > _If_ something like [ii] is the problem you have in mind: Well
> > of course [ii] is wrong, and so if we have a version of UG that
> > allows [ii] it needs to be modified. But I wasn't aware that
> > anyone ever meant to allow anything like [ii] in the first
> > place when they say UG!
>
> It's definitely allowed in two (German) logic books I know (by
> Kutschera/Breitkopf and Beckermann) I'll look up the passages in
> Mendelson and Hodges again. Maybe they really only allow your variant
> [i] of UG.
They do. And since Beckermann just copied the system from
Kutschera/Breitkopf, my question seems to be about the motivation of
Kutschera/Breitkopf only. Looking at systems that only allow the [i]
variant, I think I can even see now what might have happened when
Kutschera and Breitkopf built their system: They didn't want to allow
open formulas (with free variables) among the relata of |-. But since
almost all axiomatic systems allow open formulas (does anyone know
why?), they had to modifiy these systems, which they did by just
treating all individual constants like variables are treated in many
ordinary systems.
Thanks for putting me on a track that seems right.
wo.
David C. Ullrich
<wolf...@umsu.de> wrote:
>
>hello,
>
>> > _If_ something like [ii] is the problem you have in mind: Well
>> > of course [ii] is wrong, and so if we have a version of UG that
>> > allows [ii] it needs to be modified. But I wasn't aware that
>> > anyone ever meant to allow anything like [ii] in the first
>> > place when they say UG!
>>
>> It's definitely allowed in two (German) logic books I know (by
>> Kutschera/Breitkopf and Beckermann) I'll look up the passages in
>> Mendelson and Hodges again. Maybe they really only allow your variant
>> [i] of UG.
>
>They do.
Well fine then. This explains a lot - I had no idea until two posts
ago that [ii] was part of what you were including in UG.
(At least I didn't _think_ I'd ever seen such a thing - turns out
the Alzheimer's hasn't quite got me yet<g>.)
>And since Beckermann just copied the system from
>Kutschera/Breitkopf, my question seems to be about the motivation of
>Kutschera/Breitkopf only. Looking at systems that only allow the [i]
>variant, I think I can even see now what might have happened when
>Kutschera and Breitkopf built their system: They didn't want to allow
>open formulas (with free variables) among the relata of |-. But since
>almost all axiomatic systems allow open formulas (does anyone know
>why?),
Don't know. Of course they seem very natural in "natural deduction
systems", where they do model how people actually _do_ reason
about things: In actual life, if you want to prove that all even
numbers have a certain property you say this:
Let n be even.
Something(n)
Something(n)
Something(n)
Conclusion(n)
Hence every even number satisfies Conclusion,
as opposed to this:
For every even number n, Something(n)
For every even number n, Something(n)
For every even number n, Something(n)
For every even number n, Conclusion(n)
(I once had a student who wrote English proofs the
second way - drove me crazy, took me the longest
time to get him to say "Assume n is even."...)
So in a natural deduction system open formulas
seem very natural, and allow us to model the way
we actually do prove things. But why they're included
in un-natural ("Hilbert-style"?) systems I don't know.
>they had to modifiy these systems, which they did by just
>treating all individual constants like variables are treated in many
>ordinary systems.
>
>Thanks for putting me on a track that seems right.
>
>wo.
******************
David C. Ullrich
William Elliot
> William, I think "provided no free x occures in any of the statements of
> S" in your formulation is redundant. Did you mean "t" rather than "x"?
> Then your suggestion amounts to the "correct", restricted version of
> (UG) which I, too, favour. My question is why some authors don't use it.
>
Indeed. The actual formulation is
S |- A implies S |- Ax.A
provided no free x in any formula of S.
So if for some quirk, it's needed to change the variable use
Ax.A <-> At.A(x/t)
provided the subsitution causes no confusion of variables.
I've never had occasion to twist those two separate notions
into a single step. The auther may have garbbled the mix.
Have you considered reading a different more reknown author,
perhaps one of the classical authors of symbolic logic?