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 (Mar 21 2024 at 17:49):(work in progress. Please allow me a moment to improve the presentation. Thanks.)
There was recently a Philosophy Stack Exchange post about Glymour’s theory of bootstrap confirmation, and it serves as an exercise for me in trying to formulate a mathematical theory completely down to certain axioms.
The theory assumes certain concepts like probability, permutations, functions, real numbers, and “a set of individuals”.
Material set theories are arguably completely adequate for pure mathematics. They succeed in defining all mathematical objects as some specific arrangement of sets in a universe of sets.
Structural set theories aim to preserve the same relationships between structures in material set theory, but they just get rid of the philosophical problem that material set theory seems to imply that the world is actually made of something called “sets”. However, maybe it did take some labor to reformulate set theory so that the same relationships emerge, but the objects of the theory “lack internal structure”. I need to specifically see for myself what this looks like.
I’ll probably read this article now: https://ncatlab.org/nlab/show/fully+formal+ETCS
My motivation is trying to understand how people use mathematics to talk about things in “the real world”. Even in a structural set theory, if we assume the existence of an “abstract constant set”, does this behave meaningfully when one says, “in this context, I use that abstract set to signify the set of all animals”?
Glymour’s theory of bootstrap confirmation makes use of some concepts like the real numbers, functions, n-tuples, subsets, and set intersection. Even working in a material set theory like ZFC, I would love some back and forth conversation with someone in understanding how to define these things in ZFC. I have so many questions at the same time, it’s hard to express one without going down a bottomless loop of new questions.
I am still trying to fundamentally grasp what ZFC truly is.
I have come to understand many logicians accept the idea of “primitive notions”, which are ideas, concepts, rules, symbols, etc., that you simply take for granted in attempting to build your theory.
First order logic is a very common logic for defining mathematics in (and a good standard place to start, before trying alternative ideas). First order logic assumes the existence of an alphabet of symbols, and it also takes as primary the idea of constants, unary functions (predicates), binary functions (relations), quantification over variables which range over a “domain of discourse”, free variables (I think), and the equality symbol (which is a binary function, but which has some special rules, I think). Common unary functions would be a negation symbol. Common binary functions would be an implication symbol. The important thing is that these symbols can only attain definition because we have an equality symbol. I think I read Mike Shulman write on Stack Exchange that all logics, abstractly seen, are essentially equivalence classes imposed on the elements of a freely generated monad. (I really like that idea, anyway). So, technically, there are many kinds of unary and binary functions we could supply the logic with, defined in terms of what their output is “equal to”. Some of those systems have varying logical properties like completeness, consistency, soundness, decidability, etc (I do not understand any of those properties as well as I would like yet, and I also really want to know the abstract version of those properties, ie on the aforementioned free monad of “words” in an “alphabet”).
I am not sure, but I wonder if the reason you include constant symbols is just to be able to name things. I’m not sure. I know we need to be able to define new functions if we want to conveniently express more complex mathematical ideas starting from these simpler elements.
I read that a more general term for a “first order logic” (since that refers to a very specific one), is a “first order theory”. This emphasizes more abstractly (I think) that you basically have some symbol-manipulating rules, but the key thing I think is that you have variables that can be substituted with values. It is “first order” because whatever is responsible for doing the substitution in those variables (functions) can not be substituted itself. When you allow there to be variables which range over functions, that is a second order theory. I think it is impossible to express the idea of infinity in a zero order theory, because you would have to write an infinite number of expressions. A first order theory allows you to encapsulate an idea of infinity in finite symbols - for example, a successor function implies the existence of infinite terms. I do not know if a first order theory can express an idea of infinity larger than the cardinality of the natural numbers.
First order logic is called a “specification language” because what the variables refer to is left completely open.
Model theory tries to study the relationship between a specification language (a syntax) like FOL, and some actual thing that language is supposed to be describing. For some reason, model theory has generally selected set theory as that structural phenomenon. It is that relationship or duality between a syntax (FOL) and a semantics (set theory) that enables a number of famous concepts like incompleteness, soundness, etc. These are relationships between the syntax and the semantics. Apparently, there is some way that you could use the set theory side to imply the existence of certain sets, which FOL could not, through its syntactic formation rules, derive a corresponding expression to describe it. This is the basic idea of Gödel’s incompleteness theorem, but I do not really understand it. I am especially unclear on the set theory side.
I believe conventional set theory also has to have some “primitive notions” in order to get started. For example, the Von Neumann cumulative hierarchy is when you just keep taking successive sets of the previous generation of sets. Set theory wanted to try to describe essential properties of that universe of sets, in first order logic. Eventually, they succeeded in formulating the 9 axioms of ZFC.
The nine axioms are somewhat curious to me. For example, I believe the first two - regularity and extensionality - are sort of like “constraints”, if you think about it. They do not tell you a conditional truth about the existence of certain sets, like, “if this particular set exists, then so would this other one”. They just state “static”, universal properties of all the sets in that universe V: no set contains itself, and we do not allow multiple “instances” of the same set (in other words, when we refer to some set by its set structure, there will never be any doubt about if we are making assertions about one instance of it over another).
I think the rest of the axioms are more like “generating” axioms. Of course, they are also “static truths”, in the sense above: “if two sets exist, then their pairing exists too” is a true condition which can be checked and confirmed for all the sets in V. That said, it still seems like they give you alternative instructions in how you could generate V (the von Neumann hierarchy / universe) as opposed to Von Neumman’s generating rule. I guess I would like to know: does ZFC describe V, or can ZFC generate V? Could there be an algorithm which enumerates all the axioms of ZFC? The generating axioms would be used to generate new sets. The “constraint” axioms would perhaps be used to eliminate any sets generated that violated the condition?
My guess is no - I read there are actually countably infinite models of ZFC, I think, which is a very, very mind blowing idea. I’m wondering if this implies that ZFC is a set of axioms we work with because there are some proofs about it having the right properties, but nobody ever said it was “the ultimate theory of sets”. For example, there are axioms you can swap out, which are probably equivalent (Zorns lemma vs the Axiom of Choice). This to me opens the question of if there are possibly radically different formulations of all the axioms of ZFC? Ie, has anyone ever tried to get rid of say, the axiom of regularity, and found some other axiom they could use instead to achieve the same result? (I know about non-well-founded set theories coming from people like Quine and Susan Haack, but I’m talking about how many unique formulations we know of that provably describe the same set universe - or, the same class of universes (since ZFC describes a class of universes, right?)).
From there, I just wanted to know how to define the elements of Glymour’s theory, rigorously, in that set theory. I know about Dedekind’s construction of the reals, but I need to learn way more basic things first like how addition is defined.
I am also curious if there is a way to express that Glymour’s theory is the set of all enumerated sentences from an enlarged set of axioms - ZFC, but restricted to only the sentences the are derived from certain starting concepts, like the real numbers, the factorial function, etc.
Notification Bot (Mar 21 2024 at 18:03):A message was moved here from #learning: questions > Defining a basic mathematical theory (Glymour’s bootstrap... by Julius Hamilton.
Julius Hamilton (Mar 21 2024 at 19:53):I’ve learned a ton of stuff about the above that I’ll need to digest. The enumerated sentences of FOL form a cylindrical algebra. There are various zeroth order logics whose expressions are equivalent to algebraic structures, such as a Boolean algebra or a heyting algebra. A Boolean algebra is commonly expressed in terms of 3 operations (conjunction, disjunction, negation), but somehow, Stephen Wolfram found a way to reduce it to a single operation (NAND / Sheffer Stroke), called the Wolfram axiom. Emil Post classified all the zeroth order theories I think, in what’s called Post’s lattice. Scott Aaronson and others recently published a classification of a different class of operations, “reversible bit operations”. One way to know if multiple distinct operations are necessary to express an algebraic structure (I think) is checking if they are “functionally complete”. The Sheffer stroke alone is functionally complete. A set of operations is functionally complete if it is not montonic, affine, self-dual, truth-preserving, or falsity-preserving. I’m trying to digest all this and reformulating the above.
Morgan Rogers (he/him) (Mar 22 2024 at 09:27):Julius Hamilton said:
Stephen Wolfram found a way to reduce it to a single operation (NAND / Sheffer Stroke), called the Wolfram axiom.
The single operation is NAND, and apparently all of the axioms of a BA can be combined into a single equation which uses only NAND, although Wolfram's own website is the only one to call it the "Wolfram axiom" and he wasn't actually the one to prove that it worked.
Eric M Downes (Mar 22 2024 at 11:19):The reduction of boolean functions to NAND (or NOR) gates is noteworthy in that it requires non-associativity. A single generator in a magma can carry more information than a monoid of the same size in a way it would be nice to make explicit.
The rest of my comment is an aside on ETCS, as you mentioned perhaps learning it.
I highly recommend Lawvere and Roseburgh Sets for Mathematics for learning ETCS, I've gotten and continue to get a lot out of it.
https://www.amazon.com/Sets-Mathematics-F-William-Lawvere/dp/0521010608/
to see if you'd like it take a look at Tom Leinster's preprint
https://arxiv.org/abs/1212.6543
Maybe you can save the details until after you have a decent familiarity with ETCS, because the prood style requires thinking carefully in terms of isomorphisms and equivalences, but you might also want to be aware of HoTT. This (from Mike Shulman) is the most concise argument in favor of HoTT of which I'm aware, and he touches on ETCS, material vs. structural.
https://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html
And more in depth: https://arxiv.org/pdf/1703.03007.pdf