[FOM] The terrible EFQ: reply to Tenant--reply from Tennant

[Tennant, Neil]

Martin wrote:

______________

Neil evidently misunderstands me. These are not sequents. I'm not "uniformly substituting" anything. I'm noting a common pattern of proof used every day by working mathematicians. The letters A,B,C stand for any mathematical statements in formal or informal discourse. It would make a curious exception to say that A and B must be different.
______________

I took Martin to be treating A, B, C as placeholders for sentences in a formal language. But I would be happy to read them---as I think he is now saying one should---as metalinguistic variables ranging over sentences that can stand to each other in relations such as classical deducibility. So let's not talk any more about substitution of a formula for a placeholder; let us talk instead about instantiating sentential variables, which seems to be what Martin wants. (And please remember that 'sequent' in my earlier posting meant simply an argument, like X:A---a set of premises followed by an inference marker, followed by a sentential conclusion, which might be #. The exact interpretation of 'sequent' is actually neither here nor there. It's just the kind of thing that a proof aims to establish.)

The gravamen of my earlier reply remains unchanged and unrebutted. For Martin had earlier written:
_____________
"Suppose one knows that A and ~B are true and wishes to prove C.  A reductio ad absurdam proof might proceed by proving B from A and ~C. The principle involved can be rendered:
                                 if A,~C |- B, then A,~B |- C
Then the special case B=A gives
                                           A,~A |- C
This shows that to eliminate EFQ one must interdict a simple special case of an important general logical principle."
_____________

Martin says "The letters A,B,C stand for any mathematical statements in formal or informal discourse." So, we accord them that general interpretation, and inquire after the deducibility assumed --- A,~C |- B --- and the deducibility Martin says follows from that --- A,~B |- C. The turnstile abbreviates "there exists a proof of [conclusion] from [premises]". So Martin's principle is to be read as follows:

"If there is a proof of B from A,~C, then there is a proof of C from A,~B."
I then reasoned as follows, in acknowledging that we all have good grounds to accept this conditional metalinguistic assertion (if we accept Classical Reductio):

Suppose there is a proof of B from A,~C. As a natural-deduction schema,
we can picture this as follows:
     A, ~C
                  :
                 B

         That would mean that there would be a larger natural-deduction schema
         in classical logic, looking like this:

                             ___(1)
                         A, ~C
                            :
              ~B         B
              _________
                     #
                 _____(1)
                     C

[Now we proceed with due consideration for Martin's clarification of how
he meant A, B and C to be understood ...] So, for all sentences A, B and C
there would be a natural-deduction schema looking like the one just
displayed. Now, instantiating this generalization by taking A* for A, A* for B
and C* for C, there would be a natural-deduction schema in classical logic,
looking like this:
                    ___(1)
                         A*, ~C*
                            :
              ~A*        A*
              _________
                     #
                 _____(1)
                     C*

At this point one plugs this starred version into my earlier argument in my posting
[FOM] The still unbearable EFQ: Reply to Martin Davis ;
and one proceeds as I did before.

One points out exactly where the Core logician demurs from certain fundamental assumptions on which Martin rests his reasoning about the situation, reasoning that takes him (unconvincingly, to the Core logician) to the conclusion that EFQ somehow miraculously drops out as a special case of some quite general principle. It doesn't; so it's the general principle that's at fault. Not all instantiations (a.k.a. sentential substitutions for placeholders) preserve proofhood, for the Core logician.

Neil Tennant




-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150906/0af34fce/attachment.html>