>>13660422>Definitions don't all have to be formulated in a strict formal system.You do you, I'm not gonna argue you should be more concise with your background if you don't like
>Too strong? Too strong for what?Too strong as in including subsets of N which we don't even know are decidable. Again, I'm not pushing this conservatism on anyone, so I'm not gonna argue more for that
>To me they seem two sides of the same coin.Yeah pretty much. I think in complexity theory the \Sigma side is the more "positive" phrasing, namely unbounded search without giving a time bound, but with certainty that till you certainly find something for the positive cases. (E.g. you can dovetail algorithms and computably generate the subset of N defined as all the numbers for which the "3x+1" collatz function applications eventually end in 1. Those searches will give us all such numbers even if it may be the case that there's counter-examples, or uncomputable n's.)
I think historically \Sigma_1 and the induction principle for it is just where computability theorists and complexity theorists see the theory diverge into the less computable realm / oracles / set theory like comprehension.
As opposed to the pic in
>>13660421, pic related is what you get if you adopt some weak choice ("for every infinitely big tree there exists an infinite path").
Clearly this has some important mathy theorems, so it's not like you should stop at RCA0. But you can be explicit about your assumptions beyond it too.
Or you just adopt ZFC, I don't care, do what you want. I'm off for today.
