There is exist tradition to formulate axiom schemes such as induction, comprehension or replacment in a way like "for each formula $\phi(y,\overline{x})$ with free variables $y$ and $\overline{x}=x_1,...,x_n$ we have $\forall \overline{x} ( \text{text of axiom scheme which include } \phi(y,\overline x))$". To not be vague, let take as archetypical example comprehension scheme for second order arithmetics from ncatlab article.

$ \forall \overline m \forall \overline X \exists Z \forall n (n \in Z \leftrightarrow \phi(n,\overline m, \overline X))$

I choose that example because I don't know it is equivalent to axiom without parameters or not, whenever equivalence to $ZFC$ or first order $PA$ to versions without parameters is classical result. I understand that apriori allowing parameters could increase expressible power of our system, but I don't understand why we not allowing not only $\Pi_1$ parameters but parameters of all type like, for example, next $\Sigma_3$ axiom scheme

$\exists \overline m_1 \exists \overline X_1 \forall \overline m_2 \forall \overline X_2 \exists \overline m_3 \exists \overline X_3 \exists Z \forall n (n \in Z \leftrightarrow \phi(n,\overline m_1, \overline X_1, \overline m_2, \overline X_2, \overline m_3, \overline X_3))$

it seems for me like it could increase our expressible power a lot, so, why it is not traditional?

  • 1
    $\begingroup$ @MauroALLEGRANZA You are right it was mistyping. I am fix it $\endgroup$ – kp9r4d Mar 13 at 12:33
  • 1
    $\begingroup$ What does it mean for a parameter to be $\Pi_1$? $\endgroup$ – Asaf Karagila Mar 13 at 12:45
  • 1
    $\begingroup$ I'm not sure to understand what kind of "flexibility" are you thinking about... Consider the simple case $∀m∃Z∀n(n∈Z ↔ ϕ(n,m))$; the schema means that, for fixed $\phi$, we have a "collections" of sets $Z_m$, one for each value of the parameter $m$. $\endgroup$ – Mauro ALLEGRANZA Mar 13 at 12:57
  • $\begingroup$ If we instead use $∃$ what we get is $∃m∃Z∀n(n∈Z ↔ ϕ(n,m))$ that means that - for the specific value of $m$ that satisfies the formula - we have a single set $Z$. $\endgroup$ – Mauro ALLEGRANZA Mar 13 at 12:58
  • $\begingroup$ @AsafKaragila It means that it have form $\forall \text{param} (\text{axiom scheme})$ as analogy to arithmetical hierarchy of formulas. $\endgroup$ – kp9r4d Mar 13 at 13:00

Your Answer

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

Browse other questions tagged or ask your own question.