Gödel's incompleteness theorem shows that there are sentences that are undecideable, that is they nor their negation can be proved.
This theorem operates purely syntactically or formally, that it doesn't use a model. No semantics are involved.
Now a formal proof is a finite string of inferences. What happens if this condition is dropped - that is use an infinite number of inferences? To make sense of this one has to use a theory of the infinite, because the inferences are ordered one should use the ordinal theory and not the cardinal.
Is there an infinite ordinal for which all sentences become decidable?
Is this essentially how Gentzen's proof of the consistency of PA works - which can only mean that all sentences are decidable?
What can this mean when proofs are actually finite inferences?