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 (Apr 03 2024 at 16:07):I would like to formulate some broad questions to help me focus my investigation.
A simple formulation of the natural numbers in some n-order language is a single constant symbol c, a (constant) first-order function symbol from a constant c to a function f, and a single second-order function F from a function to a function. This generates a theory whose terms include f(c), F(f(c)), F(F(c)), and F(F(F(f(c)))).
“Addition” is a binary function that can be defined inductively. Addition of any term x and initial term f(c) is x. The inductive rule expresses the interaction between the successor function F and the addition function A, which is simple: it commutes. The successor of a term, plus a term, is equivalent to a term plus a term, and then the successor. This lets us generate the theorem that A(f(c), F(f(c))) = F(A(f(c), f(c)) = F(f(c)). I had never thought about addition before this way, and I find it pretty fascinating.
Skipping way ahead since this is what I want to think more about today.
I know at least the natural numbers have been expressed as a category-theoretic diagram, as Lawvere’s “natural numbers object”. Is there a clear method for expressing any “numbers system” as a commutative diagram? (Is there a “category of numbers systems”?) Especially the real numbers: what is their diagram, and what does it tell us are the “essential features” defining any “real-numbers object”?
I mainly ask since I am curious about the notion of “uncountability”. Intuitively, both the rational numbers and the real numbers have the property that we could “zoom in on some interval forever”, with an infinitude of smaller sub-intervals. Yet, there is a formula establishing a bijection between sets of natural numbers and sets of rational numbers. The existence of real numbers is implied when we include operations like exponentiation. I know about the diagonal argument, but I need to brush up on how certain axioms added to a theory enable that. I read that Lawvere formulated the diagonal argument categorically.
I am most interested in what properties, as a graph (since a category is a type of graph), the real numbers have, so I can understand “what they are” better - topologically, geometrically.
I am also curious about the Von Neumann cumulative hierarchy. There must be some mistake in here: ZFC can construct real numbers. The Von Neumann universe is a model of ZFC. But the Von Neumann hierarchy is generated by a simple recursive algorithm involving power sets and unions. Generation K+1 = Union (Power Set (Union (Generation K)), Union (generation 0 to K-1)). Then, how could there not be a bijection between sets of natural numbers and sets of reals? The reals are contained in the successive generations of V; and the generations are countable and sequential.
Thank you :pray:
Joshua Meyers (Apr 03 2024 at 17:53):A simple formulation of the natural numbers in some n-order language is a single constant symbol c, a (constant) first-order function symbol from a constant c to a function f, and a single second-order function F from a function to a function. This generates a theory whose terms include f(c), F(f(c)), F(F(c)), and F(F(F(f(c)))).
What's the purpose of ? Why not just have be zero and be successor? Also if takes functions as input, your terms are ill-formed because you are putting terms into rather than functions.
Joshua Meyers (Apr 03 2024 at 17:57):I know at least the natural numbers have been expressed as a category-theoretic diagram, as Lawvere’s “natural numbers object”. Is there a clear method for expressing any “numbers system” as a commutative diagram? (Is there a “category of numbers systems”?) Especially the real numbers: what is their diagram, and what does it tell us are the “essential features” defining any “real-numbers object”?
There is a lot of work in this direction, such as "models of a (Lawvere) theory", "algebras of a monad", and other approaches as well. The real numbers are not as simple to express this way since they can't be presented by finitary operations -- you also need supremum or some equivalent, but I'm sure CTists have thought about it. I'll let someone else give more details if they want.
Joshua Meyers (Apr 03 2024 at 17:59):I am most interested in what properties, as a graph (since a category is a type of graph), the real numbers have, so I can understand “what they are” better - topologically, geometrically.
To speak correctly, a category is not a type of graph, it is a graph with extra structure. That is, the data of a category is a graph AND some additional operations on it. Just like a group is not a type of set, it is a set with extra structure.
Joshua Meyers (Apr 03 2024 at 18:04):There must be some mistake in here:
Here is the mistake:
Generation K+1 = Union (Power Set (Union (Generation K)), Union (generation 0 to K-1)).
You have to know about successor ordinals vs. limit ordinals in order to understand the Von Neumann cumulative hierarchy. Your formula only works for successor ordinals, in which case it is overkill, you could just write Gen succ(K) = powerset(Gen K).
and the generations are countable and sequential.
They are not countable, they are indexed by the ordinals, which are vast (so big that they are not even a set).
Julius Hamilton (Apr 03 2024 at 18:07):Joshua Meyers said:
What's the purpose of $F$? Why not just have $c$ be zero and $f$ be successor?
That is the presentation I’ve generally seen, but when I try to re-express the theories I’ve been exposed to authentically, where I fully understand each step, I find new questions/issues emerging. I was trying to define in terms of how I have commonly seen the “signatures” of languages, in logic. I felt it to be a problem that a first-order successor function has to quantify over zeroth-order terms (in order to “succeed” the initial element, zero), but its codomain is on the first-order ‘level’. It has to be - it is recursive.
On the other hand, I could leave “” out, and declare a single initial function , along with successor function , where I suppose is the “first order domain of discourse” (I’m not sure how this is commonly denoted).
But then, my definitions start on the first-order level. But I kind of imagined that there is something wrong with a logical universe where there is a first-order function, but no existing terms it can act on. So, I had to supply it with a single value “c”, so that we can get definition “down to the bottom”.
I also saw Ryan Wiznesky’s “initial model” on Nat4 in CQL, which had an interesting convention I don’t understand - in his inductive definition in CQL, the zero element is a function without a domain, which he called the “constant function type”: zero: successor (or something, I need to double-check.)
Julius Hamilton (Apr 03 2024 at 18:08):I really appreciate you taking the time to respond and augmenting my understanding on these topics. I plan to respond in full. Thank you.
Ryan Wisnesky (Apr 03 2024 at 19:14):the idea that a constant is simply a 0-ary function is a common one, not CQL specific. In a product category, a constant would have domain 1, that is, domain unit, domain terminal object: zero : 1 -> Nat, succ: Nat -> Nat. In a cartesian multi-category, which is technically what CQL is using and is strongly related to product categories, a constant would have a domain with 0 objects. In coq for example you can write "Axiom infinity : Nat" or "Axiom infinity : unit -> Nat" and they behave indistinguishably.
Joshua Meyers (Apr 03 2024 at 21:55):That is the presentation I’ve generally seen, but when I try to re-express the theories I’ve been exposed to authentically, where I fully understand each step, I find new questions/issues emerging. I was trying to define in terms of how I have commonly seen the “signatures” of languages, in logic. I felt it to be a problem that a first-order successor function has to quantify over zeroth-order terms (in order to “succeed” the initial element, zero), but its codomain is on the first-order ‘level’. It has to be - it is recursive.
It's good that you are trying to re-express the theories you've been exposed to authentically, where you fully understand each step. Unfortunately, I don't understand this sentence: "I felt it to be a problem that a first-order successor function has to quantify over zeroth-order terms (in order to “succeed” the initial element, zero), but its codomain is on the first-order ‘level’." What is the problem exactly?
Joshua Meyers (Apr 03 2024 at 21:55):Also, you write "That is the presentation I've generally seen". I've never seen such a thing before, can you give a reference?
Julius Hamilton (Apr 04 2024 at 17:29):I meant that your presentation is the standard one - a constant element , and a successor function .
I’ll try to zoom out a bit to explain the context of my thinking.
In model theory, the very first thing you see defined is the “language”. The language is a collection of symbols. However, the symbols must be grouped into kinds.
A symbol can be a constant or a variable, and they are suggested to take values in “a domain of discourse”, .
The most important property of a variable is that it can be substituted by another expression. Variables permit the use of string-rewriting rules, which allow us to derive new expressions.
A bare variable does not refer to a specific element in , but it potentially does. A variable is restricted to a collection of values it can take.
To enable the substitution of a variable with an expression, I guess we need to specify a rule - under what conditions can it be replaced - and with what.
A rule could be very arbitrary, like, “the symbol can be substituted by any of the following symbol strings: ‘abcdefg’, ‘:::::!’, ‘qwertyuiop’”.
A rule can have more conditional logic, like a “lookahead” feature, which says something like, “if the current symbol is x, and the next symbol is c, then you can replace x with c”.
I think this is related to Turing machines and the Chomsky hierarchy, and I need to think more about it.
My hope is that we can find a more precise way to define what the “order” of a symbol is. I wonder if it is the number of consecutive substitutions possible.
In logic, there is a traditional distinction between things like ‘natural deduction’ and ‘Hilbert-style axioms’. They are both sets of rules for rewriting expressions, but natural deduction has more rules, and Hilbert-style systems have as few as possible. A Hilbert-style system has more symbolic expressions (‘axioms’) at the outset.
This was my thinking process for why I expressed with three symbols, not two:
The natural numbers (if they do not have any operations) are defined by a single idea, which is ‘next-ness’. We only have to assert i) there is something, ii) there is the ability to claim “next”, for any something, and iii) claiming “next” for something, is itself something. So we have:
something, next(something), next(next(something)), next(next(next(something))), and one could continue.
Coming back to how I have seen “languages” defined in model theory. In principle, the “something” could be either a constant or a variable. The “next” action is a unary function. All that means is that we have a first-order constant symbol . In this case, if the symbol is followed by a zero-order symbol , we consider the concatenation as a “symbolic” unit in its own right. But is symbol zero-order, or first?
I think this answers my own question. I may have mistakenly thought had to return a first-order symbol. I am having difficulty remembering why I thought my previous way was necessary. It probably doesn’t matter, and I want to move onto to the next parts of the above.
Julius Hamilton (Apr 04 2024 at 17:33):I think I will think about a formal parser for axiomatizing arithmetic next; since I want these foundations before trying to define Lawvere theories and real numbers.
Spencer Breiner (Apr 04 2024 at 17:50):Julius Hamilton said:
A symbol can be a constant or a variable, and they are suggested to take values in “a domain of discourse”, .
I would say this is putting the cart in front of the horse. A variable is a syntactic entity, so it doesn't depend in any way on the domain of discourse, which is a semantic entity (I'll call it for "universe"). Rather, once we have fix a model/interpretation of the logical language, which includes specifying , then takes values in . Similarly, a constant does not refer to a specific element, except relative to a particular interpretation.