when you think about it, formal systems are weird.

Many [programming languages], such as Pascal and LISP, look quite different from one another in style and structure. Can some algorithm be programmed in one of them and not the others? Of course not -- we can compile LISP into Pascal and Pascal into LISP, which means that the two languages describe exactly the same class of algorithms. So do all other reasonable programming languages. The widespread equivalence of computational models holds for precisely the same reason. Any two computational models that satisfy certain reasonable requirements can simulate one another and hence are equivalent in power...

-- Sipser, Introduction to the Theory of Computation

When we talk about mathematical ideas, we often say that we're "discovering" them, as if they were always there just waiting for us, and that when I talk about Turing Machines or differential calculus or set theory, I mean the same thing that yourusername means... but why? Rationalists of different stripes have long held maths to be a fundamental thing-in-reality -- but if you were going to be an empiricist about it, how do you account for this whole math thing? Hume (patron saint of hard empiricists) calls apodictic-type knowledge "consequences of names" but even that presupposes that there's such a thing as "consequence" when it comes to thinking about things. Is there such a thing as "what you must think, if you think"?

Are all of these things just implications of some hardwired logic bits that humans have in their brains, or is it a property of the world? Or is it that we learn to do the same sort of reasoning as other humans from having the particular wetware that we do and interacting with a reasonably-similar environment? Is it conceivable that another intelligent species (in a different kind of environment, I suppose) would come up with a different sort of reasoning where they would find the math that we think up illogical?

Particularly, the λ-calculus and the TM describe exactly the same sort of computation -- where did we get that computation from in the first place, and why were those cats Church and Turing just waiting to describe it with their different computational models?

Discuss. eponis and realitycalls particularly, this is me looking at you.