[FOM] EFQ and Tennant's consistency

[Arnon Avron]

On Thu, Sep 10, 2015 at 02:03:39AM +0000, Tennant, Neil wrote:
> 
> Arnon Avron writes
> 
> "In his postings Neil maintains that ~p & p |- q is [an] invalid inference
> that mathematicians never use, while ~p |- p->q is valid."
> 
> I don't think I've actually said that mathematicians 'never use' 
> EFQ or any of its obvious equivalents; 

Well, On Mon, Aug 31, 2015 at 02:20:33AM +0000, you wrote:

> In Core Logic, *there is no rule of EFQ*. 
> That's because mathematicians NEVER (NEED TO) USE IT!

OK. There were these two words *(NEED TOO)* in brackets. So we now 
agree at least that these brackets should be deleted. Do we?

 And of course the claim that mathematicians 'never use' EFQ is right
from one trivial point of view: When mathematicians reach a 
real contradiction in their theory they do not apply EFQ for inferring
new theorems. In fact they stop applying *all* rules of inference, and
instead start thinking how to fix the theory in which they work. Even Cantor
needed to invent the difference between "absolute infinity" and 
"ordinary infinity" in order to be able to continue his research
on set theory, after he had discovered contradictions in it.
My point was that mathematicians use EFQ a lot in proofs from
set of assumptions (whether consistent or inconsistent - something
they might not be sure about)  in the form of inferring A->B from ~A,
a form that for every mathematician is completely equivalent
to EFQ. I truly cannot imagine a mathematician ("except
for logicians making jokes" in the words of Anderson and Belnap),
who infers that A implies B on the basis of some assumptions
(no matter what), but has any hesitations in using it later 
for inferring B once he proves or assumes A (what is the point 
of inferring A->B if one is not allowed to use it??) 

> 
> Arnon writes further
> 
> "The latter [i.e., ~p |- p->q] is justified by [Neil] (in the classical case, I guess)
> by the truth table of the material implication (and that of negation
> is needed too, right?)."
> 
> No. First, it is well known that for the intuitionist/constructivist, 
> the truth tables are acceptable, row by row, reading from left to right 
> (that is, from the status of the constituent propositions to the 
> status of the compound in question). 

Sorry, Neil. At this point it seems that we are not speaking the same 
language. In what sense are the truth tables "acceptable"?
What is this mysterious "status" of the propositions? And what
does the "status" of A have to do with (the "status" of?) ~A if
the truth table of negation is not used here?? And why is the use of the 
truth table of -> legitimate  for justifying inferences, while that of 
~ is not???

> The core logician, who is a constructivist seeking to ensure 
> relevance of premises of proofs to their conclusions, need 
> not 'think classically' at all in accepting the truth tables. 
> Secondly, that part of the modified rule of ->I in Core Logic 
> that permits one to conclude P->Q upon deriving # from P makes 
> no appeal at all to the truth table for any connective other than ->.

Maybe so, but this is not *relevant* to the issue.
We were not talking about this, but on the inference of
A->B from ~A, which you say is available in core logic, and you 
explicitly justified (at least for "classical core logic")
on the basis of the *truth-table for ->*.

Concerning this, I should tell you that it seems obvious
to me that you are confusing here the right order of things.
Mathematicians do not really think of -> in terms of its truth-table.
They all think about it in terms of the two rules of ND (i.e.
the deduction theorem in its two directions). Unless they
are intuitionists, they have learned to
*accept* the "truth-table" of implication as a faithful interpretation  
of the implication they use, because 
they have found out that it indeed reflects what they do. However,
they would have never *started* with the truth-table of ->, and
then use it to see what basic rules for -> they should use. 
Thus everyone who ever taught students of math or cs that ~A |- A->B
(or the corresponding lines of the truth-table for ->) knows that 
to practically *all* students this seems at first "a fairy tale of logicians" 
(as Anderson and Belnap describe it in their book on Entailment), 
and they do not believe that mathematicians really use this principle. 
This is the reason why when I teach  our course of Discrete Math (which starts
with the fundamentals of logic, continues to set theory, and
then to combinatorics and graph theory) I point out (when I
reach this subject) to the students
that the fact (which they have no problem with) that the
empty set is a subset of every other set can be explained
*only* on the basis of the principle ~A |- A->B. Only at that
point this principle, along with EFQ and the truth table of ->,
stopped to look to them funny and useless.
> 
> Arnon asks rhetorically
> 
> "... how exactly is the validity of ~p |- p->q forced by the truth-tables of -> and ~?"
> 
> But rather than waiting for the Core logician's answer, he rushes to provide a conjectured one himself:
> 
> "Answer: it is because according to these truth table every model of ~p is also
> a model of p->q. In other words: because the set of models of ~p is a subset of the
> set of models of p->q."
> 
> For the record: I simply don't see the justification as proceeding 
> along such lines at all. Arnon's talk of models is his, not mine. 
> For me, the justification is carried out entirely within an inferentialist framework. I look at the four rows of the truth table for ->, and note 
> that in the two rows where the antecedent is false, 

How can a justification in terms of the truth-table of -> be
"entirely within an inferentialist framework"?? To me this seems a
contradiction in terms! And what is the connection between 
"the antecedent is false" and the inference of something from 
(the truth of?) ~P, if you are 
not relying on the truth table of ~ (or at least the relevant line of it)?

> the whole conditional is true. So the inference to P->Q from 
> possession of a refutation of P is immediate 

Why?? (And please try to make your answer  look coherent to people 
who understand notions and claims in the conventional way, like me. You should
take into account that by just avoiding the use of the word "model" 
you do  not make yet your answers to questions
like this  really different from what I had written
in my previous posting!) 

Note also that to me, 
the inference of Q from possessions of a proof of P and a refutation of P 
is no less immediate (on the basis of the truth-table for ~)
than your inference of P->Q from  possession of a refutation of P
(on the basis of the truth-table for ->).

> *and relevant*. One does not even need a step of negation 
> introduction (to get ~P), before proceeding immediately to the 
> conclusion P->Q. And one need not entertain any qualm on the basis 
> of the allegation that one might be making a classical semantic 
> assumption to the effect that the consequent has to be either 
> true or false!  Even if the consequent lacks a truth value, 
> the falsity of the antecedent should suffice for the truth of 
> the conditional, since it suffices both when the consequent is 
> true, and when the consequent is false.

I apologize again, but obviously I fail to understand what you are trying
to say here, because to me it seems essentially the same as what I had said,
only put in different words... 

Arnon