[triska]

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.

[soberhoff]

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.

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