[FOM] 603: Removing Deep Pathology 3 Harvey Friedman Tue Aug 25 10:24:45 EDT 2015

[Harvey Friedman]

I definitely remember many cases when teaching baby set theory, especially,
when a proof of a claim C splits into cases, where by this often convenient
proof method, the cases are all laid out, say often 4 cases (sometimes 2
sometimes other powers of 2). The prover knows that they have divided up
the work in a trivially understandable and comprehensive way in order to
avoid errors and confusions. Then under one or more of the trivial cases,
the statement of the case itself is cited to contradict (or quickly
contradict) something we already know or have assumed, and therefore the
case is dispatched as "inapplicable" or whatever, and the desired
conclusion C is considered secured under that case.
​ After the claim is secured in all of the cases, the claim is considered
secured (relative of course to any assumptions made ahead of the split into
cases).​


Superficially, this seems to be the kind of thing that people actually do
and teach, and like, which you are negatively flagging. E.g., I think that
common ways of proving the distributive laws for pairwise union and
intersection, and maybe De Morgan laws, are often done this way.

If this is right, then we have to evaluate
​exactly
 what you are depriving us of.

​ALSO, do we get any benefit from a Tenant approved proof as opposed to
simply a proof? In constructively/intuitionism, we definitely do. ​

​Harvey Friedman​

On Sun, Aug 30, 2015 at 8:47 PM, Neil Tennant <neilpmb at yahoo.com> wrote:

> 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/20150830/b3f54069/attachment-0001.html>