You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Julius Hamilton (Nov 16 2024 at 17:26):The issue of choosing some concepts as “primitives”, and others as constructed from primitives by rules, is a subject I wish to study in its own right, rather than leaving as a background assumption in some theory.
A common presentation of logic and formal systems includes the concept of “terms”, as well as “function symbols”, and the notion of “application” of a function symbol to terms. For example, here is how one paper regarding a certain term-rewriting algorithm begins:
Implicitly, it seems like there are already a number of “mental concepts” being used here, to present some of this information.
We are told there is something called “terms”, and something called “function symbols”. This, alone, already seems to imply that:
Even those rudimentary concepts probably contain more structure than one might initially realize. This may become more evident when one tries to “formalize”, or at least “analyze”, those concepts in turn.
For example: a “type” of a “thing” is something that stands in relation to a given thing; is associated with it. But, is a “type of a thing” itself also a “thing”? Is “thing” the most general mental concept possible, which anything conceivable or expressible is one of? Or, in this scenario, is “thing” a special type, and there are other concepts which “stand above” “thing” - properties, qualities, conditions of/on things? One could say that “the notion of ‘type’” is itself a “thing”, just by virtue of me being able to talk about it. One could also say that “thing” is a type, given that everything that exists (apparently) is of some type - at minimum, the type of “thing”.
Given these issues, I have recently started trying to define fundamental mathematical concepts in terms of “mental concepts”, rather than thinking there is some “canonical formal system” which I can formalize everything in.
I believe one of the most essential mental concepts is “putting two things together”. I have actually considered calling this “the axiom of reification”, which says something like “if you have two things, you can put them together, and that itself counts as ‘a thing’”.
Is this a good way to “get off the ground”, to define “the application of a function symbol to a term”? We might conceive of “application” in numerous ways. For example, it could just be seen as string concatenation, where we literally take a symbol “” and put it in front of a string of symbols “”. In set theory, it seems to me that “putting two things together” would be forming the set pairing the two things. If we needed them to be ordered, we could form the ordered pair.
But a lot of the time, if we try to use pre-existing theoretical frameworks to formalize something so “primitive”, I think we might be putting the cart before the horse, and it will only introduce more problems, more things to be formalized.
I think the most barebones aspect of what we are calling “function application”, in this context, is just “putting two things together”. It does not matter “in what order they are packaged together” (as in, an ordered pair like ); so long as whoever is “perceiving” this theory can mentally differentiate which element has which role (this symbol is the function symbol, this is the first argument to the function, this the second one, etc.) (To be extra nuanced: even though the arguments to the function carry information about their “order” relative to the function, they way we “store” this information does not itself have to be “ordered”.)
Is this a good way to avoid a bottomless chain of formalization? That the “application of a function symbol to terms” is just a pure mental concept, prior to any mathematical theories of sets, pairing, unions, functions, products, types, etc., which just says “putting them together”?
Ryan Wisnesky (Nov 17 2024 at 03:40):it's turtles all the way down. you pick your object language, pick your meta language, and then start proving theorems or writing programs. anything else is philosophy,
Rich Hilliard (Nov 17 2024 at 16:26):Regarding "putting two things together" you might find MERGE in generative linguistics of interest. See: https://arxiv.org/abs/2305.18278 and related papers by same authors.