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.
Notification Bot (Mar 23 2024 at 20:12):A message was moved here from #learning: questions > Axiomatizing Glymour’s Theory of Bootstrap Confirmation by Julius Hamilton.
John Baez (Mar 24 2024 at 17:49):It doesn't take that long to learn the ZFC axioms once you understand the framework of classical first-order logic, which is very much worthwhile. I agree with Jean-Baptiste that it's not worth learning how large amounts of math can be formalized in ZFC... unless that's what you're interested in. I did it as a kid but I've forgotten most of the details.
John Baez (Mar 24 2024 at 17:58):First-order logic is based on a naive set theory which is not formalized.
It's good to be pretty careful about this. Proofs in first-order logic rely only on simple rules for manipulating finite strings of symbols. They don't require concepts of "set" or "membership". We say it's purely syntactic.
On the other hand there are many important metatheorems - that is, theorems about first-order logic - that are phrased in the language of set theory. In other words, we can use set theory, either naive or axiomatic, to reason about the syntax of first-order logic.
Also the concept of 'model' of a set of axioms in first-order logic relies on set theory. This can be seen as another aspect of metamathematics.
The most important metamathematical result about classical first-order logic is the soundness and completeness result saying that a sentence is provable from some axioms iff it is valid - i.e., satisfied in every model of those axioms. Provability is a purely syntactic notion, while validity is semantic.
Todd Trimble (Jun 11 2024 at 10:52):Julius wrote
but somehow, Stephen Wolfram found a way to reduce it to a single operation (NAND / Sheffer Stroke), called the Wolfram axiom
The history of the Sheffer stroke shows clearly that Wolfram was not the first to propose NAND as functionally complete. Peirce knew it, for example, although he didn't publish his finding.
The axiom itself, not the operator (often denoted by ), is . If I'm understanding it correctly, the other identities for Boolean algebras can be derived from this (and the substitution rule for equality). Which, I admit, is an interesting and curious fact, a kind of completeness theorem. Wolfram didn't prove this himself; it is one of 25 candidate equations he identified as possibly being a single axiom for Boolean algebras in terms of NAND, and other people showed it in fact works. See the article https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_algebra.
(Is it universally called the "Wolfram axiom", outside of Wolfram's MathWorld? I forget what exactly was said in the conversation I was in the other day during my visit to Tallinn, where we were talking about people naming concepts after themselves.)
On the other hand, if compelled to refer to him, I would be all too happy to occasionally refer to the Sheffer stroke as the "Wolfram ego stroke". :-P
Morgan Rogers (he/him) (Jun 11 2024 at 10:58):For some reason this discussion was split between two topics which I have now recombined; I had made a similar comment earlier @Todd Trimble :)
Todd Trimble (Jun 11 2024 at 11:02):Thanks for bringing it to attention, Morgan. At least I learned something new from all this. :-)
John Baez (Jun 11 2024 at 11:18):I know Matt Cook, whom Wolfram sued for violating a nondisclosure agreement and giving a talk about a mathematical discovery he made while employed by Wolfram.
Todd Trimble (Jun 11 2024 at 11:25):Yeah, it's pretty disgusting.
Wolfram is doing the rounds these days on the public intellectual circuit, promoting his new book which unveils the true meaning and explanation of the second law of thermodynamics. In terms of cellular automata, I think. (Here's a video: https://www.youtube.com/watch?v=c-RO3vM10Ok) But I guess that would be a topic for another stream.