Sort of, though I was thinking of this quote from Rafael Harth’s post below:
However, if the theory of A is complete, then it is also decidable! This is so because:
If A is complete, for each sentence F, either F or ¬F is valid. Thus, either F or ¬F is internally provable. (Gödel’s completeness theorem.)
Therefore, we can write a procedure that, given any sentence F, searches for internal proofs for
F and ¬F in parallel and outputs ‘YES’ and ‘NO’, respectively, if it finds one. Since one of them is always internally provable, this always works.
I was trying to think of an answer to how this could work, or alternatively how this couldn’t work.
Sort of, though I was thinking of this quote from Rafael Harth’s post below:
I was trying to think of an answer to how this could work, or alternatively how this couldn’t work.
Based off that passage, I don’t see Rafael Harth’s argument works either.