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 (May 05 2024 at 12:07):Working through Ebbinghaus 2021, would enjoy some supplementary conversation.
2F436725-4B4D-4992-B307-1642795B593C.jpg
One thing I have yet to feel comfortable with is why first order logic is standardly presented with exactly those groups of symbols: variables, constants, functions, relations, logical operators, quantifiers, equality, and punctuation.
I have been thinking it becomes more obvious if you formulate the same thing in type theory.
“Constants” I believe are terms from any number of atomic types. Thus we begin with the idea of a multi-sorted theory. The only specific type we need is the binary type (to express truth values).
I don’t think variables are necessary; they are more like implicit. They are not a type.
Everything else is definable in terms of function types and the product type. For example, logical symbols like and are functions .
I’m wondering if there is a concept of “subtypes”, and I’m wondering how we might define quantifiers.