Description: We give the definitions  for Form 230 (\( L^{1} = HOD\))  from Myhill/Scott [1971]

Content:

We give the definitions  for Form 230 (\( L^{1} = HOD\))  from Myhill/Scott [1971].

Definition:

  1. \(DF^{0}(A)\) is the set of all subsets of  \(A\)  definable by first order formulas in \(\langle A,\in _{A}\rangle \) using parameters from \(A\), i.e., \(DF^{0}(A)\) is all sets of the form \(\{ x \in  A :\Phi^{(A)}(x,a_{0},\ldots a_{n-1}) \}\) where \(\Phi \) is a formula of the type described above, \(a_{0}, \ldots ,a_{n-1}\) are in \(A\) and \(\Phi ^{(A)}\) means all variables range over \(A\).
  2. Gödel's constructible sets are defined by \(L^{0}_{\alpha }=\bigcup^{}_{\beta <\alpha }DF^{0}(L^{0}_{\beta })\)  and\(L^{0} =\bigcup^{}_{\alpha \in \hbox{On}}L^{0}_{\alpha }\).
  3. \(DF^{1}(A)\)  consists  of  all  sets  of  the  form \(\{x\in A:\Phi (x,a_{0},\ldots ,a_{n-1}) \}\)  where \(a_{0}, \ldots , a_{n-1}\)are in \(A\) and the quantifiers are restricted to \(A\) or \({\cal P}(A)\).
  4. \(L^{1}_{\alpha } = \bigcup^{}_{\beta <\alpha }DF^{1}(L^{1}_{\beta})\) and \(L^{1} = \bigcup^{}_{\alpha\in\hbox{On}}L^{1}_{\alpha}\).
  5. \(HOD\) is the class of hereditarily ordinal definable sets.

Howard-Rubin number: 82

Type: Definitions

Back