[triska]

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.

[soberhoff]

Sorry, I was out of town for a while.

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.

[triska]

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:

https://en.wikipedia.org/wiki/Craig%27s_theorem

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.

[soberhoff]

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.

[triska]

"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.

[soberhoff]

I don't agree with that definition of "effectively axiomatized". Granted, that's what Wikipedia says here: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... But the reference given doesn't check out. Franzén's 2005 book Gödel's Theorem doesn't say anything about effective axiomatization on page 112. He does however give the following definition in his lecture notes at: https://books.google.de/books?id=Wr51DwAAQBAJ&pg=PA138#v=one...

"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.

[triska]

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!