[FOM] 603: Removing Deep Pathology 3 Harvey Friedman Tue Aug 25

[Tennant, Neil]

I thank Harvey for taking note of my question about possible pathologies in (certain) proofs.

The question of providing formalized proofs that do not trade illicitly on irrelevancies is an interesting one.

In the vast majority of cases, I believe, it doesn't happen. Mathematicians (whether constructivist or non-constructivist) almost always reason relevantly. This is why standard intuitionistic and classical logic are unnecessarily bloated, in containing the First Lewis Paradox (A, not-A; so, B). Rules of natural deduction (or sequent calculus) can be stated for the connectives and quantifiers in such a way that (i) such irrelevancies cannot be proved (hence cannot be exploited), and (ii) there is no loss of completeness. For deductive reasoning in constructive mathematics, the logical system that does this is Core Logic. For deductive reasoning in classical mathematics, the logical system that does this is Classical Core Logic.

For each of the two species of mathematical reasoning, it is the corresponding core system that most faithfully regiments informal proofs as formal ones.

Now, the kind of proof-pathologies that *might* still arise in mathematics would be ones where various different proofs, using different sets of axioms, were joined together via cuts into one big proof of the 'overall result'---say, some mathematical theorem being shown to be a consequence of some big union of the various axiom-sets involved. It may be that the accumulation of smaller proofs to form the bigger proof masks the fact that the theorem actually follows from a significantly proper subset of the overall set of axioms. It could also be the case (an extremely improbable one, I grant) that the overall set of axioms is actually inconsistent, AND that this is something that could be gleaned from all the smaller proofs and the way they have been put together, if only one had the proof-theoretic methods to discover the fact.

The nice feature of the core systems is that they do provide such methods. And the methods are effective ones. If one has a core proof P of A from X, and a core proof P' of B from A,Y, then a core proof [P,P'] can be computed, which proves some subsequent of X,Y:{B}. This allows the possibility that for certain subsets X',Y' of X,Y respectively, the proof [P,P'] is of the sequent X',Y':#  (where # is absurdity).

Much more likely, though, is that [P,P'] will prove some sequent of the form X',Y':B. Still, if either of the axiom-set containments (X' in X; Y' in Y) is proper, this represents an epistemic gain, or logical advance: one will have found that not all those axioms in X,Y were needed for one's theorem B.

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150831/b7579c3d/attachment-0001.html>