@mudri
Sort of. ZFC + "There is an inaccessible cardinal" implies you have a set that satisfies ZFC and is well founded.
It's more general and subtle than just that though. A measurable cardinal gives you a nontrivial elementary embedding of V into a well founded class, for example.
(5/7) Let's say you want to follow the simpler "PA is consistent because it is sound" route. Simply implementing the natural numbers isn't enough; you need to be able to define an inductive type for arithmetical sets as well! https://en.wikipedia.org/wiki/Arithmetical_set In general for other arithmetics, you'll need to be able to do induction over the sets of things it inducts over. (For example, in full second order arithmetic you'd need induction over second order arithmetical sets of numbers.)
(7/7) Oh yeah, and optionally, you can help me with an experiment.
To help resolve the problem @MartinEscardo pointed out at https://mathstodon.xyz/@MartinEscardo/109552785927789702, I suggest the following:
- To follow this thread, follow the #MathInduction tag (#Induction is a cooking tag)
- When posting in this thread, if you're trying out the experiment, add #MathInduction to your post and make sure the visibility is public (not unlisted). You could include other tags that are relevant to your post too.
Ma(th)sdon doesn't foster the same amount of interaction as twitter. Most conversations go silent very quickly here compared to there. (I don't want to go back to twitter. I just want more interaction and discussion.)
(6/7) This is why the Burali-Forti paradox pops up in many different approaches to foundations (including type theory); if you can do induction over your own induction, you can often prove yourself consistent.
(1/7) Mathematical induction is in some sense the most powerful mathematical technique.
I don't simply mean that it's really useful; I mean that meta-mathematically it often underpins the strength of a foundation. This is the main insight from ordinal analysis.
In addition, many famous theorems from "everyday" mathematics are logically equivalent to induction principles of various strengths. This is the main insight of reverse mathematics.
(4/7) As an example, consider the consistency of PA. This can be proven with epsilon_0 induction. But we don't need to think about Von Neumann ordinals. In type theory, being able to create an inductive type for the Cantor normal form (a tree like notation for ordinals below epsilon_0) is sufficient to prove PA consistent. https://en.wikipedia.org/wiki/Cantor_normal_form
(3/7)
- Large cardinal axioms in #SetTheory are often equivalent to asserting that there exists *well-founded* models with various properties, which gives you access to more induction.
- In Predicative Arithmetic by Edward Nelson (https://web.math.princeton.edu/~nelson/books.html) it's shown that by severely weakening induction and then considering what numbers still satisfy inductive properties, you can get a system that might be acceptable in #ultrafinitism.
(2/7) Note that this induction is not just about Von Neumann ordinals. It takes different shapes in different foundations:
- In #arithmetic it is just natural number induction (although there are different forms of even this induction)
- In #TypeTheory, induction is provided by inductive types. The stronger the type formers, the more induction you get.
The King