In Avigad's lecture notes, we are given a set $U$, a subset $B \subseteq U$, and some functions $f_{1}, \dots, f_{k}$. Furthermore, following Enderton (p. 22) say a set is inductive if it contains $B$ and is closed under the $f_{j}$'s and let $C^{*}$ be the intersection of all the inductive subsets of $U$. I want to fill out the missing part of showing that $C^{*}$ is also inductive.

Here is what I have to offer:

Let $$C^{*}:=\bigcap\{S \mid S \text{ is inductive}\}.$$ If we choose an arbitrary sequence that belongs to $C^{*}$ then this will surely be contained within a subset, say $B$ because of the fact that $C^{*}$ is the intersection of all inductive sets. Moreover, the set is closed for any function $f_{j}$. This is because each inductive set satisfy, by definition, the property of being closed under any arbitrary function and so when we take its intersection we have that any function $f_{j}$ maps within $C^{*}$. Therefore, $C^{*}$ is inductive.

I realize that this looks more of a sketch rather than an actual proof. However, I'm unable make any progress as to write it clearer, and so my question is: How would you formalize this?

  • $\begingroup$ The right hand side of your formula for $C^*$ doesn't make sense. There is no set $\{S \mid S$ is inductive$\}$ in ZFC. $\endgroup$ – kahen Sep 18 '13 at 19:59
  • $\begingroup$ That is one of the criticism you could raise against this problem - it is not acceptable to constructivists. $\endgroup$ – user94284 Sep 18 '13 at 20:03
  • $\begingroup$ I'd have written $\{S \subseteq U \mid S$ is inductive$\}$. Just to be completely clear that I'm not talking about something like $\mathbb{ON}$, the class of ordinals. $\endgroup$ – kahen Sep 18 '13 at 20:05
  • $\begingroup$ Fair enough, thanks! $\endgroup$ – user94284 Sep 20 '13 at 8:48

You have all of the ingredients and a clear informal statement of the proof. If you want to make it a bit more formal, you could do it like this:

Let $f_j$ be any of the functions. If $f_j$ is an $n$-ary function, let $\langle c_1,\ldots,c_n\rangle\in (C^*)^n$ be arbitrary. Let $S$ be any inductive subset of $U$. Clearly $\langle c_1,\ldots,c_n\rangle\in S^n$, so $f_j(c_1,\ldots,c_n)\in S$; since $S$ was arbitrary, $f_j(c_1,\ldots,c_n)\in S$ for each inductive $S\subseteq U$. Thus, $f_j(c_1,\dots,c_n)\in C^*$ for $j=1,\ldots,k$, and $C^*$ is inductive.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.