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.
Verity Scheel (Jan 07 2021 at 17:39):I am not a logician, and I only know the basics of model theory, so this is just an idea I’ve been ruminating on, but:
What if we humans are the initial model of logic? (Alternatively, it is whatever physics drive the computational mechanisms of our universe and brains.)
My understanding is that model theory concerns deriving new models of logic from old ones, and this process can be considered transitive in some sense. In particular, if we build models in a metatheory, and then we pick some models of the metatheory (within some metametatheory), we get some models of the theory within the metametatheory.
But where could this process stop? What do the (meta^n)-theories all have in common?
Well, us. We are what they all have in common.
In particular, they all rely on our abilities of reason (constrained by the computational limits of our brain and the physics of the universe) to construct things. And even though our brain can only deal with finite things directly, we get to build models that appear infinite from the inside by virtue of the structure of logic and our capacity for imagination.
I think some introductions to logic rely on this already ... in particular I think I read an intro to either HoTT or elementary set theory where the author mentioned something to the effect of “Don’t worry about what particular metatheory is used to talk about these rules, it should be intuitive”.
Anyways, just some thoughts. I’m sure that someone’s said something about these matters before.
Idea: could we account for the error-prone nature of human reason (and the error-correcting codes, if you will, that we thus rely upon)? what about the social nature of research and teaching/learning? is our initial model really the collective collection of initial models that we hold individually, and thus is unbounded in some sense that it could continue to replicate forever (even though human life must eventually die out)?
P.S. apologies if I am abusing the term initial model, feel free to suggest more accurate terms
John Baez (Jan 07 2021 at 19:21):I think I read an intro to either HoTT or elementary set theory where the author mentioned something to the effect of “Don’t worry about what particular metatheory is used to talk about these rules, it should be intuitive”.
I think they can get away with this because almost mathematicians and computer scientists have been trained in a bunch of mathematical/logical conventions that allow them to read a book like this and understand it. I think someone without previous training would have a lot of trouble understanding such a book. And indeed, basic undergraduate courses on logic have to explain how mathematicians use words like "or", "implies", "assume", etc. Students often have a lot of trouble with this.
John Baez (Jan 07 2021 at 19:22):In short I don't think the "metatheory" used in math textbooks is the common property of all humans, only those who have undergone some training.
Morgan Rogers (he/him) (Jan 07 2021 at 20:44):Nick Scheel said:
Well, us. We are what they all have in common.
It seems like you're saying that humans are somehow the progenitors of logic, and that seems like a stretch, even if we're the first species that we know of to have formal expressions/languages for working with it.
John Baez (Jan 07 2021 at 21:27):I think people have some common ways of thinking and reasoning, but the "common core" is smaller than one might naively think if one spends a lot of time hanging out with 21st-century Westerner who have some education in math and science.
John Baez (Jan 07 2021 at 21:29):Lately psychologists have started noticing that most test subjects in psychology experiments are WEIRD: Western, educated, industrialized, rich and democratic.
James Wood (Jan 07 2021 at 21:58):Nick Scheel said:
I think I read an intro to either HoTT or elementary set theory where the author mentioned something to the effect of “Don’t worry about what particular metatheory is used to talk about these rules, it should be intuitive”.
I think there's a grain of truth to this in that the metatheory required for stating syntactic rules is usually very simple, and most metatheories you could think of agree. You start needing to worry about metatheory when you want to prove something about that system.
James Wood (Jan 07 2021 at 21:59):Perhaps a good place to look to examine the things “everyone agrees on” is Σ₁-validity.
Verity Scheel (Jan 07 2021 at 22:01):Thanks @James Wood, I think that’s most closely what I was trying to get at.
Verity Scheel (Jan 07 2021 at 22:14):I didn't mean to imply that logic exists because of humans, but just that if we are creating models in some metatheory we need to have enough tools available in that metatheory with which to craft our models, and so on, and so we must be conduct our reasoning in _some_ base system, and then build up more powerful theories and models inside of that base system
Verity Scheel (Jan 07 2021 at 22:16):The other thing I would compare it to is enrichment in CT: when you're working with “plain” categories, you can actually think of them as being -enriched, where is really the metatheory you're working in (modulo size issues). I think I am not articulating myself well enough here … :-/
Verity Scheel (Jan 07 2021 at 22:18):John Baez said:
And indeed, basic undergraduate courses on logic have to explain how mathematicians use words like "or", "implies", "assume", etc. Students often have a lot of trouble with this.
This is a good point. But I wonder how much basic logic students could figure out, given enough time? Could they take their intuitive usages of quasi-logical notions and formalize them? I suppose the process of formalization might be difficult to explain to them, if they weren't already exposed to it.
Edit: that is, how many of their mistakes are really mistakes, as opposed to discrepancies in how their understand logical concepts vs how those concepts have been rigorously defined.
Verity Scheel (Jan 07 2021 at 22:20):And point well taken about the biases of assuming levels of knowledge, and cultural biases, etc. … it is interesting that games (like card games, but also other types) provide an example of logical rules (to varying levels of formality) that I think most people have some exposure to.
John Baez (Jan 08 2021 at 00:26):Games are a great introduction to formal mathematics!
John Baez (Jan 08 2021 at 00:26):There are some amazing computer games these days that teach kids math... that are really games.