One thing that seemed a bit surprising to me, especially in light of the paper's strong focus on computation, is that the assumption that the axiomatization is effective is only mentioned in a footnote, and even there it is not explained but we are told to "don't worry about it" if we don't know what that means.
Yet, the code pieces in the paper make critical use of this assumption in that they assume that we can decide (with an algorithm) whether or not a string is a proof. This only works if the axioms are recursive.
So, maybe you could consider adding a short explanation about this to the paper?
Every time I said "either/or" I was making use of the law of the excluded middle. But I didn't add a detailed disclaimer explicitly highlighting this fact either. Should I have? I think it's okay to just take some things for granted.
Though, I admit that I have never spent much thought on non-effective axiomatizations. So I'm open to be educated.
The proofs you present are entirely constructive and work without appealing to the law of the excluded middle! As was also pointed out by Gödel himself about his proofs, they are obtained in an "intuitionistically unobjectionable manner".
When you say "either/or" in the paper, you make case distinctions that are intuitionistically non-contentious, i.e., you say "either F ⊢ G, then contradiction, so F ⊬ G, or F ⊬ G, then contradiction etc.", but the point is that G is explicitly constructed, so this is intuitionistically acceptable.
In contrast, the other assumption I mentioned is used in the paper and in fact essential for its proofs.
I agree in the cases where I argue "suppose, then..." But there are instances where I argue "either this is the case, or this is not the case." Unless there are multiple laws of the excluded middle, that's an application of it.
In any case, that was merely an example. The central point I was making doesn't depend on this.
In the paper, it is assumed — per footnote 1 — that the formal systems under discussion are effectively axiomatized. I assume this means that their theorems are recursively enumerable, is this correct? If so, then this means that determining whether a string is a proof may only be semi-decidable, and may not halt for strings that are not proofs.
However, as I mentioned, in the remainder of the paper, it appears to me that you assume that the theorems are not only recursively enumerable, but in fact recursive. For example, in the proof of Theorem 4 on page 5, the lines stating "if s is a proof ..." seem to assume that this check always terminates, requiring assumptions that the original proof does not and therefore weakening the obtained result.
In my opinion, adding a short explanation about how this can be salvaged (it can!), or at least precisely specifying what is assumed, could improve the presentation.
I'm only assuming that checking whether "does s prove S?" is a recursive property. That's not the same as demanding "is S provable?" to be recursive.
Upon reflection I agree that effective axiomatization isn't actually that difficult to explain. So I've changed the footnote to say: "For the purpose of this discussion every formal system is effectively axiomatized by definition. This basically just boils down to the fact that proofs are computer checkable."
I was initially worried that this might raise the question what non-effective axiomatizations are all about. That's not a can of worms I want to open. But I think this should be fine.
Thank you for adding this! Still, it is not so straight-forward to conclude, from just the premise that the system is effectively axiomatized (i.e., its theorems are recursively enumerable), that "does s prove S" is a recursive property.
In my opinion, if the assumption is that "proofs are computer checkable" (i.e., "does s prove S" is a recursive property, which is what is required in the paper), then it would be good to either state that as the key assumption, or state for example that this follows via Craig's theorem from the assumption that the system is effectively axiomatized:
Interestingly, from this theorem it follows that such a system can be re-axiomatized so that "S is a theorem" is even a primitive recursive property. In fact, when Gödel wrote "rekursiv" around 1930, he meant the class of functions that we now call primitive recursive. Because of Craig's theorem, we know that primitive recursive, recursive, and recursively enumerable can be used interchangeably in the definition of effective axiomatization, but without such a theorem, it would be a leap to conclude one from the other.
I don't see why there's a theorem required here. Let our formal system be effectively axiomatized. Then by definition its axioms are a recursive set. So I can just check a proof by starting at the top and verifying that every line is either an axiom or follows from a line above via an inference rule. Both of these two checks are recursive. Hence, proof checking is recursive.
Also, the Wikipedia article doesn't say that Craig's Theorem proves recursively enumerable axiomatizations equivalent to (primitive) recursive axiomatizations. I would find it very surprising if this was a consequence. It only says that a recursively enumerable set of formulas (e.g. the provable sentences in Peano arithmetic, not merely its axioms) can be given a (primitive) recursive axiomatization. That's a very much weaker claim.
"Let our formal system be effectively axiomatized. Then by definition its axioms are a recursive set."
"effectively axiomatized" means that the theorems are recursively enumerable. It does not immediately follow that the axioms are a recursive set. However, by Craig's theorem, we can then re-axiomatize so that the axioms are a recursive set, even a primitive recursive set!
You are of course right about the consequences: In the post above, I meant to say that due to this theorem, it makes no difference whether we require the axioms to be recursively enumerable, recursive, or primitive recursive. But still, without this theorem, it would be a leap to conclude from "the system is effectively axiomatized" that "s
is a proof of S" is recursive.
"If T is effectively axiomatized, in the sense that there is an algorithm for deciding whether or not a given sentence is an axiom of T,..."
In Computability: Turing, Gödel, Church and Beyond Martin Davis even makes the definition "T is axiomatizable if it has an axiom set that is computable" on page 42.
And that's also the definition Shoenfield gives on page 125 of Mathematical Logic.
Besides, "effective" has always been a synonym for "computable", "recursive", or "decidable" whenever I've encountered it in this context.
Also, I must insist that "it makes no difference whether we require the axioms to be recursively enumerable, recursive, or primitive recursive." is not what Craig's Theorem says. This is dangerously close to claiming that recursively enumerable sets are recursive which is plainly untrue. If recursively enumerable axioms (not just recursively enumerable theorems) are indeed interchangeable with recursive axioms, then I'd like to hear more about that.
Yes, you are right: This is not what Craig's theorem says! It is enough to assume that the theorems are recursively enumerable. From this, it follows that there is an axiomatization where the axioms are recursive.
The key point is that I would find it a worthwhile addition to the paper to somehow make clear that "s proves S" is assumed to be decidable. Since you have done this: Thank you!
One thing that seemed a bit surprising to me, especially in light of the paper's strong focus on computation, is that the assumption that the axiomatization is effective is only mentioned in a footnote, and even there it is not explained but we are told to "don't worry about it" if we don't know what that means.
Yet, the code pieces in the paper make critical use of this assumption in that they assume that we can decide (with an algorithm) whether or not a string is a proof. This only works if the axioms are recursive.
So, maybe you could consider adding a short explanation about this to the paper?