For the sake of discussion I would like to clarify that I regard those 'structures' that might be described by different themes of abstract mathematics as the objects that are to be considered either platonic or not. So, platonism in regards to the abstract structures, not necessarily the instantiations of those structures (ie: the example 'P.D.E structure' could be represented equally well with either categories or sets as the lifeblood of each respective formulation). So I think I am in agreement as to the grouping of features into 'invented' that you detailed earlier, which leaves the pattern still independent.
I think you do actually touch upon a related source of my disturbance (the primary one being, why does the abstract have literally any utility at all?), but perhaps i can re-phrase it as thus: One can engage in quantum mechanics, and it can often be the case that one encounters the only solution to a problem in QM is by using C* algebras or the other abstract analysis ideas. We can talk of using abstraction as a means of modelling the physical universe, but I do not believe that entails that that abstraction in question should even be likely to have utility (indeed, I think the opposite!). Summing it up after following your lead, 'why is it necessary that to produce a GOOD simulation of the physical universe, you require the existence of non-physical entities like those routinely encountered in mathematics?'
I am not well-versed enough in theoretical computer science to comment upon church-turing machines. I do not mind having a look, but as a default setting I remain doubtful that they will satisfy me, or dissolve my quandary sufficiently, as they can be interpreted via abstract concepts in their formation.
I like this mode of thinking, and its angle is something I haven't considered before. How would you interpret/dissolve the kind of question I posed in the answer to Pattern in the comments below?
'My point is the process of maths is (to a degree) invented or discovered, and under the invented hypothesis, where one would adhere to strict physicalist-style nominalism, the very act of predicting that the solutions to very real problems are dependent on abstract insight is literally incompatible with that position, to the point where seeing it done, even once, forces you to make some drastic ramifications to your own ontological model of the world.'
In addition, I am versed in rudimentary category theory, and wouldn't a presupposition of having abstraction as natural transformation presuppose the existence of abstraction to define itself? This may be naive of me, or perhaps I have not grasped your subtlety, but using an abstract notion like natural transformation to define abstraction seems circular to me.
This is actually similar to a kind of reasoning i have undertaken, but I want to ask you what you make of the fact that such high level abstraction even has any kind of utility at all. Say one day we as all physicalists (assumption on my part) all sit down (in present day mind, but without any knowledge of abstract maths), and we do the same type of physical formal kind of thinking that Newton or Leibniz undertook and developed calculus, which gives us the underpinning of most of modern applied mathematics. We then see how the kind of geometrical reasoning we have employed is able to tap into the 'world logic' (for want of a better phrase). If I were to come up to you, describe how we can obtain an enormous amount of world logic insight by some utterly far removed and esoteric notions concerning topological spaces, sobolev spaces and understanding complex abstract interactions in banach spaces (or what have you), why would you, as a physicalist, take that seriously? ie: you can believe there is more work to be done, but that it is very very unlikely to come from understanding concepts that have little or (very often) NOTHING to do with the real world. (indeed this can go quite far, see: https://ncatlab.org/nlab/show/differential+equation)
The core of what I've been struggling with is to produce a sufficient response that dissolves that question satisfactorily, and although there must be a connection between mathematics and neural structures (there is a good amount of literature as to this, echoing your own thoughts), I feel like this question is actually quite far removed from that even being the case or not.
With your point b) we can recognise it has order within itself, but then when it comes to that next step, that seeing what structures work on top of it, that process is either (very broadly speaking) an act of creation by the person (leaving out the nature of that act, lets consider it neural) or we simply have insight into another category of the world (platonic), and then we ask the question: 'If it is neural, why SHOULD this extra addition work? Reality has no means of simply abiding by logical structure or bending itself to fit into abstract reasoning. But now, given that it does work, how are we to interpret the nature of our two choices?'
My point is the process of maths is (to a degree) invented or discovered, and under the invented hypothesis, where one would adhere to strict physicalist-style nominalism, the very act of predicting that the solutions to very real problems are dependent on abstract insight is literally incompatible with that position, to the point where seeing it done, even once, forces you to make some drastic ramifications to your own ontological model of the world.
If I've messed anything up, or if you feel I haven't seen your point, any response would be appreciated.
The goal is mainly to understand its relation to proof assistants, I have experience with it before as a purely logical study but i haven't tried to see it in this new context for myself. This book looks excellent though, thank you for your recommendation
I appreciate the great feedback from all of you, thank you :) I do have another quick question, but it's of a lower priority. As of right now, I currently hold no degree. I've always been kind of Interested in the MIRI workshops, but I've always been nervous about signing up to one because: 1. I'm not sure if a degree would be necessary to keep up with the level of work people are to be involved in at the workshop and 2. In case my first point turned out to be true, I certainly wouldn't want a student who had no real formal (I've still learning computability and logic and have started to branch out into set theory and similarly related fields) experience in the kind of Math MIRI deals with to be a nuisance to people trying to get some work done by asking them questions all the time. So here is my question stated in full 'Would I be allowed to participate in a MIRI workshop, given that I have no degree as of right now, and could this factor be to the detriment of others there?' Again, a lower priority question, but any comments or thoughts from users would be welcomed graciously :)
I would also like to know the answer to this question.
A quick comment, for the segment on tiling agents, on the MIRI site the recommended reading (not counting any MIRI papers) is 'a mathematical introduction to logic' by Enderton. But on this page, it instead recommends Chang and Keislers Model theory. Can this be taken to mean that both works are important recommended reading? Are they both of equal worth or should (or rather, could) one be prioritised over the other?
Don't worry it no trouble :) Thank you, I see your reasoning more clearly now, and my thought of circularity is no longer there for me. Also I see the mental distinction between compression models and platonic abstracts.