zfc inductive predicates

Stream: general

[Huỳnh Trần Khanh]

I read random stuff in random PDFs on the internet and it seems that the Knaster–Tarski theorem is the way to construct inductive predicates in ZFC... I can't understand that theorem though. am I right that the Knaster–Tarski theorem is needed to construct inductive predicates in ZFC? and how can I construct them then?

[Eric Wieser]

I'm not sure how good a fit this type of question is for #general, since this doesn't really sound like a topic about lean. In future #maths _might_ be a better fit, as might #Type theory. Maybe I'm wrong though.

[Horatiu Cheval]

Somewhat tangential to your question, but maybe you will find interesting. As far as I understand there is a deep connection between fixed points and inductives, but I do not fully grasp it and am not qualified to explain. But I remember finding the accepted answer to this stackexchange question quite enlightening at some point regarding the basics of this relation.

[Horatiu Cheval]

Not zfc-theoretic, but it shows the intuition of how lists can be defined as a least fixed point, in the Knaster Tarski way

[Mario Carneiro]

I don't often apply the Knaster-Tarski theorem directly, because it's wrapping a fairly trivial construction: the intersection of a collection of sets. Just like the example I gave earlier about defining $\omega$ as the intersection of all sets closed under zero and successor to get what amounts to the inductive type generated by zero and successor, if you have some collection of constructors for an inductive predicate, you just define what it means for a predicate to be closed under those rules and take the intersection of all of them to get the least fixed point.

[Mario Carneiro]

The Knaster-Tarski theorem is basically showing the general conditions under which you can expect a similar result. For example you don't need it to be the intersection of sets, it can be the infimum in any complete lattice. Intersection of sets is by far the most common case though. You also need the "universe" to be a fixed point; this usually follows in concrete applications by some kind of type correctness condition. For example, if I am defining the provability relation, it's a subset of formulas, so the "universe" is the set of all formulas, and since all my rules say that if such and such formula is provable then so is this other formula, so naturally the rules never escape the bounds of the set of all formulas.

[Mario Carneiro]

Here's the metamath proof, which is quite short and self contained.

[Patrick Thomas]

I found a discussion using the Knaster–Tarski fixpoint theorem in relation to inductively defined sets in Appendix 1 of "Handbook of Practical Logic and Automated Reasoning" by John Harrison. I would like to find a more rigorous proof and discussion, especially in regard to how inductive rules are formally defined. Would someone have a good reference?

[Patrick Thomas]

That is, how is the definition of a set by inductive rules formalized in ZFC, and how is the Knaster-Tarski fixpoint theorem used to prove that the set exists?