[FOM] Use of Ex Falso Quodlibet (EFQ) (or ECQ)

[Timothy Y. Chow]

Alan Weir wrote:

> To put it another way, if Neil actually convinced working mathematicians 
> (say by persuading them that the epistemic gain, in spotting 
> inconsistent systems, outweighed the additional time and effort)  to go 
> over their informal proofs and desist from sending them forward for 
> publication if they suspected they could not be normalised according to 
> Core Logic rules, that would be a major change in practice. Perhaps more 
> feasibly, if there really does emerge a time when informal proofs are 
> standardly written up in a form which can be processed for automated 
> checking before being accepted in journals that would be a big revision 
> in practice; but an additional revisionary move would be to design Core 
> Logic automated provers and checkers and make them the sentinels for 
> good journals.

I like the idea that maybe the debate is just whether Neil Tennant is 
being "revisionary" or not.

On the other hand, I am not sure that deciding whether Tennant is being 
"revisionary" is any easier than explicating the precise relationship 
between informal and formal proof (and you have agreed that the latter is 
a difficult problem).

It's true that forcing mathematicians to review their proofs to see if 
they can be formalized in a certain way would be revisionary, but only 
because current practice works entirely on the informal level, and *any* 
introduction of formal proof (Core Logic or otherwise) would be 
revisionary.

As for proof assistants, by the time they get good enough to act as 
sentinels, they may be even better than Tennant is at finding tricks for 
eliminating what might naively appear to be instances of "illegitimate" 
reasoning and replacing them with derivations that obey this or that 
strict system of rules.

My feeling is that the only really definitive indication of 
revisionariness is the labeling of interesting *theorems* as incorrectly 
stated or even false.  In the absence of such, it seems to me that the 
question of whether a new proposed logic is "revisionary" will be a fuzzy 
one.

Tim