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

[Tennant, Neil]

Harvey writes
______

Please give an example in a common real world mathematica situation, without resorting to any technical notions from proof theory, of what exactly you are flagging and what you are not.
______

For those new to this exchange, 'flagging' means 'disallowing in one's logical formalizations of mathematical reasoning'. Harvey thinks that the system of Core Logic (or its classicized extension) that I recommend for the natural formalization of mathematical reasoning might prevent certain mathematical proofs (which are usually not fully formalized) from being formalized at all.

But this is simply not the case. For any mathematical proof of A from X, there is a core version of it, whose premises are drawn from X (but not necessarily exhausting X), and whose conclusion is A (or #). Now, if X is a set of axioms in a branch of mathematics that one is morally certain is consistent, the latter possibility (i.e., the conclusion of the core proof being #) is ruled out. So, one is left with: for any proof of a mathematical theorem A from mathematical axioms X, there is a core version proving A from some subset of X.

So Core-ification of informal mathematical proofs is hardly going to 'flag' anything! Rather, Core-ification is going to be the most natural way of formalizing the essence of any stretch of mathematical reasoning. The 'added extras' (of EFQ, etc.) available in the standard Gentzen-Prawitz systems of intuitionistic and classical logic need never be used. They just contribute to proof-formalizing bloat, which can mask what is really going on.

What I raised earlier as a possible kind of 'proof pathology' is that standard formalizations of mathematical proofs might *miss* the opportunity to spot that the real result to be had, but one which is hidden behind the accumulation of cuts and thinnings, is a logically stronger one than the one that can be unreflectingly read off from the overall, *standardly* formalized, proof. In Core Logic, once all the cut-free, thinning-free stretches of reasoning have been formalized, they can all be put together, and an 'overall logical result' (a core proof) computed therefrom. That is, one will compute a core proof of *some subsequent* of the sequent standardly proved. This subsequent might involve subsetting down only on the left, i.e. on the antecedent of the sequent in question. But it *might* also involve subsetting down on the right!---that is, discovering that the accumulated premise-set is actually inconsistent, *on the basis of the reasoning already accomplished, but not, in the standard setting, properly reflected upon*.

Thus Harvey's request-challenge that I come up with some mathematica-style proof (or one from Mizar) that would be 'flagged' by the core logician is not germane to the discussion. Let me rather put the challenge the other way round.

If Mizar were based on Core Logic, it would still be able to prove every mathematical theorem from whatever mathematical axioms are being used, on the assumption that the latter are consistent. But in producing only Core proofs, Mizar would frequently be making great epistemic gains, which it might not be making at present. Such gains would arise in situations where one had a proof P of a lemma A from axioms X, and a proof P' of a theorem from A and further axioms Y; and one wanted to 'put those proofs P, P' together' to get a proof of theorem A from axioms X,Y.

(i) On the assumption that X,Y is consistent, you would compute a core proof [P,P'] of A from some subset of X,Y. If that subset is a proper subset of X,Y then you will have made epistemic gain---realizing that not all of the axioms apparently used are really needed for the overall proof.

(ii) If, however, X,Y is *inconsistent*, then in putting the two proofs together and computing the overall proof [P,P'], you might well come up with a core proof of # from X,Y. Thus you will have enjoyed another important kind of epistemic gain---realizing that your newly accumulated proofs form a proof whose overall set of premises is inconsistent.

This would be a 'writ large' case analogous to the degenerate case of having a core proof P of A:AvB  and a core proof P' of AvB,~A:B, and computing [P,P'] to be a core proof of A,~A:# --- rather than a core proof of A,~A:B. There is no core proof of the latter sequent.

Neil Tennant


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150831/4d92ed23/attachment.html>