I am considering writing ''$\Pi^{n}_{i_{0},...,i_{n-1}}$-comprehension'' as abbreviation for ''$\Pi^{0}_{i_{0}}$-comprehension plus ... plus $\Pi^{n-1}_{i_{n-1}}$-comprehension'' in the context of an nth-order logic. Is there precedence for such a notation?
$\begingroup$
$\endgroup$
4
-
2$\begingroup$ Wouldn't this be redundant? In any reasonable system, AFAIK, $\Pi^{m+1}_a$-comprehension implies $\Pi^m_b$-comprehension for any $m, b, a$. Or am I missing something? $\endgroup$– Noah SchweberCommented Apr 19, 2015 at 3:47
-
$\begingroup$ That could be. What is the proof? $\endgroup$– Frode Alfson BjørdalCommented Apr 19, 2015 at 3:54
-
$\begingroup$ @Noah S Why would it be unreasonable to have a third order system which only allows $\Pi^{1}_{1}$-comprehension and $\Pi^{2}_{1}$-comprehension? It seems to me that we need not stipulate that the instances of $\Pi^{2}_{1}$-comprehension allowed in the logic comprise all instances of $\Pi^{1}_{n}$-comprehension for $n\geq 1$. I do not see a problem with having such weaker logical systems. $\endgroup$– Frode Alfson BjørdalCommented Apr 21, 2015 at 21:11
-
$\begingroup$ Because every $\Pi^1_n$ formula is $\Delta^2_0$, the comprehension schemes are ordinarily nested. I suppose you could view the latter as "improper" instances of the former scheme. But, to try to make the comprehension schemes disjoint, how would you separate the "properly" $\Pi^2_1$ instances of comprehension from the "improper" ones (making up words). That seems to involve more than just syntactic analysis, while the ordinary definition of the schemes is syntactic. For example, if $\phi$ is $\Pi^1_n$ and $\psi(X^2)$ is logically valid we might consider $(\exists X^2)[\psi(X) \land \phi]$. $\endgroup$– Carl MummertCommented Apr 25, 2015 at 13:16
Add a comment
|