This is another way of saying all these same sort of things
https://en.wikipedia.org/wiki/Curry%E2% ... espondence
In other words, the Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects. I refer to finite string transformations by an algorithm.

From the published Incompleteness Theorem Proof
http://www.liarparadox.org/godel-1931_F ... _Basis.pdf
The chain of symbolic manipulations in the calculus corresponds to

and represents the chain of deductions in the deductive system.

Curry, Haskell 1977. Foundations of Mathematical Logic. New York: Dover Publications, 45
Then the elementary statements which belong to {T} we shall call the elementary theorems of {T}; we also say that these elementary statements are true for {T}. Thus, given {T}, an elementary theorem is an elementary statement which is true. A theory is thus a way of picking out from the statements of {E} a certain subclass of true statements…

When we combine all that together we get finite strings that have been assigned the semantic value of Boolean true as the complete set of true premises. Truth preserving finite string transformations representing deductive inference and conclusions that are necessarily true because the argument is deductively sound.

The above shows how the whole notion of analytical True(X) can be one-and-the-same-thing as a theorem of a formal system, thus eliminating incompleteness. Also the formal system can be the entire body of analytical truth.

Copyright 2020 Pete Olcott