Category Theory
Zulip Server
Archive

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.


Stream: learning: questions

Topic: Logic and Set Theory


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.