[FOM] Faithful Formalisation

[Alan Weir]

Timothy Y. Chow, (FOM Vol. 153 Issue 30) finds my suggestion that faithful formalizations should contain no content not in the original informal proof surprising. Tim writes:

>Can we infer that there is a clear sense in which a formal ZFC proof of any theorem of a paper with a Mathematics Subject Classification number other than 03Exx (set theory) will not be faithful to the original proof, because the latter brings in content from branches of mathematics other than set theory?<

I think I'll try to bite the bullet here. Where Tim says:

>any formalization of any theorem surely starts with a very small set of basic concepts, but then by the above criterion, it will be hopeless to "faithfully represent" any theorem of algebraic topology or microlocal analysis or p-adic representation theory<

I'd say that minimising basic concepts (or, but this tends to pull in the opposite direction, minimising the number of axioms), obviously has benefits- logicians went wild for that at the start of the 20th Century- but is not the key in faithful formalisation. The faithful formalisation should attempt to formalise the branch of algebraic topology or p-adic representation theory using the proper concepts of the theory  as primitives and capture the structure of the proof, filling in the gaps with inference steps used by the practitioners. To be sure, this was one thing Rav was sceptical of, he complained that no one had axiomatised matrix theory, for example, though I would be surprised if that was too difficult. So maybe the project would break down there at the stage of setting out axioms (or basic inference rules) implicitly assumed in the informal proofs in that area. But that seems to me what one would have to do if one was formalising a proof in algebraic topology, say, rather than one in set theory.

(From my very limited knowledge of  algebraic topology, presentations usually involve some use of set theory in the conceptual toolkit. A formalisation would need to provide axioms or rules strong enough for the set theory used but one might also, for example, take some of the concepts notions such as 'function' or 'vector space' as primitive and try to axiomatise, or provide inference rules governing them, if the informal proofs in that discipline simply take various steps involving those notions for granted, as they often seem to do, and rarely define them or analyse them any further.)

Now of course there is a separate question: can we interpret algebraic topology, or p-adic representation theory or arithmetic, in set theory? Can we interpret all mathematics, including category theory, in set theory? That's an interesting question as is the question whether we can interpret all maths in category theory or in homotopy type theory with univalent foundations or whatever. There doesn't seem to me to be any compelling reason why all of maths should be interpretable in One Big Theory, certainly not in a Unique Big Theory, but it is obviously interesting to inquire after this. But this seems to me to be a different issue from whether informal proofs can be formalised and whether, and in what sense, formalizations are faithful to the proof itself. If one was formalising two different informal proofs of the same result, one of which used topological methods and the other didn't, surely one and the same formal proof couldn’t be equally faithful to both?

Alan Weir

Roinn na Feallsanachd/Philosophy
Sgoil nan Daonnachdan/School of Humanities
Oilthigh Ghlaschu/University of Glasgow
GLASGOW G12 8QQ
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150908/a76434ea/attachment-0001.html>