Révision 155 CharacterizingPH/qpvbc.tex
| qpvbc.tex (revision 155) | ||
|---|---|---|
| 275 | 275 |
\item Arithmetic including both safe and sharply bounded normal quantification. (for sequences) |
| 276 | 276 |
\item (if time) allow both bounded and safe quantifiers? |
| 277 | 277 |
\end{enumerate}
|
| 278 |
|
|
| 279 |
|
|
| 280 |
|
|
| 281 |
FCA: |
|
| 282 |
\[ |
|
| 283 |
\exists f^\safe . \forall \vec u ; \vec x . |
|
| 284 |
\left( |
|
| 285 |
\exists y^\safe . A(\vec u ; \vec x , y) \ciff A(\vec u ; \vec x , f^\safe(\vec u ; \vec x)) |
|
| 286 |
\right) |
|
| 287 |
\] |
|
| 288 |
(with typing information) |
|
| 289 |
This could be enough with open induction if we introduce ranks later? Yup, seems like a good idea. Can then make into a real `open' theory. |
|
| 278 | 290 |
\end{document}
|
Formats disponibles : Unified diff