User talk:Prime.mover

From ProofWiki
Jump to navigation Jump to search
I like conversations to make sense. So I respond here to messages left for me.
If I leave a message on your talk page, I will expect to find your response there, not here. Many thanks.

User talk:Prime.mover Archives

Archive 1: 23 July 2008 to 13-June-2011
Archive 2: 13-June-2011 to 26-Nov-2011
Archive 3: 27-Nov-2011 to 29-Apr-2012
Archive 4: 29-Apr-2012 to 07-Mar-2013
Archive 5: 07-Mar-2013 to 21-Oct-2014
Archive 6: 22-Oct-2014 to 06-Nov-2016
Archive 7: 21-Nov-2016 to 01-Mar-2020


A Possible Next Direction

I was planning on starting on a project for a website/wiki about proofs, but if I could just incorporate some things into this website that would also work, and probably make things much easier.

Something that I would like to see, which this website does to some extent, is the breaking down of complex mathematical topics all the way down to the simplest axioms(regardless of which they are, and one could use multiple systems) and explicitly stating every step of the way. If one has the time, why not boil down a complex theorem as far down as it can go? Is that not basically the essence of proof anyhow?

One idea is that you could use flowcharts to state every pre-established concept that the proof makes use of. With this someone could also take a famous proof that they might find interesting, and then easily find the exact path(s) of what concepts, theorems, etc. are necessary to understand before they attempt to understand the proof in question.

Attached is one 'proof of concept' I was going for with the Pythagorean Theorem from Book I of Euclid's Elements(currently excluding definitions). In this case I didn't flesh out any proposition that already had been fleshed out somewhere else in the image.


Of course, it doesn't have to be in this exact format. With a website one can use hyperlinks, or make the individual branches collapsible, or use other tricks to make things more convenient.

This site already does make use of links in many proofs, which is great. The basic framework is already pretty much here, I just think it could be expanded upon and/or organized further. There wouldn't need to be a flowchart or a similar map for every proof, but wouldn't it make things more accessible/easier to understand?--Alexelam (talk) 04:25, 8 April 2021 (UTC)

The philosophy that you have described is exactly what the $\mathsf{Pr} \infty \mathsf{fWiki}$ manifesto states. In theory, every proof can (ultimately) be broken down into a chain of definitions and axioms, all the way back to ZFC and (in the case of geometry) Euclid.
There are very likely to be instances of where we have not gone all the way back to axioms, for example, for advanced proofs using basic arithmetic. Reminding the user of the rigorous definition of real addition based on abstract algebraical constructs in field theory backed up by the ZFC construction of the natural numbers is probably overkill -- but the structure to support has already been put in place on $\mathsf{Pr} \infty \mathsf{fWiki}$ (it was one of the first things we did). The philosophy is indeed already there.
I see your diagram for Pythagoras's Theorem but it's too small, and when I try to embiggen it, I find that the contents of the nodes have lost their definition. However, I suspect that there are repeated instances of the most basic axioms and definitions. I can totally see where you are coming from, but it might be more profitable to use a directed acyclic graph structure. (Fun fact: by strange coincidence, I was in the process of implementing one of those for a project in my day job while at the same time reading Stephenson's "Anathem". The significance of this would become apparent to a reader of at least the appendices of that literary work.) --prime mover (talk) 05:24, 8 April 2021 (UTC)

The file is an SVG so it should retain its definition, if you just click on it and then again at the file page. But you are right that there are redundancies, which is partly why I wasn't sure if links(or color coding) would work better or not. I didn't think of the acyclic graph idea, which is pretty good. I suppose that what I was going for was more of a UI reworking than a philosophical one, at least for proofwiki.
For now I'll probably just make a couple of them and try to add them as an image to the theorem's page.
I personally would like to see some worked examples of ZFC, for as much discussion as it gets, but I get that most people don't need that much rigor. Of course not every proof needs to go all the way back, if it's simply linking up with what has been established on another page.
--Alexelam (talk) 06:19, 8 April 2021 (UTC)
For it to be useful, such a diagram should be immediately comprehended by a single glance. I would gather that such a diagram should be designed first and foremost as an aid to understanding rather than an exercise in ingenuity, and so the user should not need to zoom in as though scanning it through a microscope. In my past career as a software engineer, I had great experience with documentation which did little to aid the understanding of a function, consisting of such tree-diagrams, and (beyond bulking out the bumph in order to bamboozle a client into believing we had provided the documentation required) it never actually did the job of explaining how it worked.
And, as I said above, if you've got multiple instances of the same node in a given tree, it really is not a tree. A proof is not in general a tree. It is a directed acyclic graph. IMO this is a vitally important concept which is vanishingly rarely emphasised in the mathematical discipline of proof theory. The latter is almost universally taught informally with a considerable amount of intuitive reliance on the concept of "circularity" without ever once indicating what that actually means.
Now none of the above paragraph is actually implemented in $\mathsf{Pr} \infty \mathsf{fWiki}$, mainly because I have not encountered a reliable primary source which discusses the matter properly -- it is just something that is acquired in the mind of the student by gradual osmosis. We have gone no further down the road of philosophical logic than the basic axioms of natural deduction, and sufficient faltering steps towards establishing some framework of mathematical logic, so the field here is wide open for someone who a) understands sufficient about this field as to be able to communicate it lucidly, and b) has adequately embraced the philosophy of this site as to be able to transfer that understanding to a suite of pages on $\mathsf{Pr} \infty \mathsf{fWiki}$ that present it. --prime mover (talk) 06:41, 8 April 2021 (UTC)