XPost: comp.theory, sci.math

On 12/15/23 11:39 AM, olcott wrote:

*The philosophical foundation of analytic knowledge*

Analytic knowledge is the set of expressions of formal or natural
language that are connected to the semantic meanings that make them
true.

Thus when we construe provability broadly within the Curry-Howard isomorphism, we understand that unprovable (within this body of
human knowledge BOHK) simply means untrue.

Where does Curry-Howard say unprovable is untrue, my understanding is it
says unprovable is uncomputable/undecidable as it maps computation to
proof, (and says nothing about "true")

*I now prove that such a system cannot be incomplete in the Gödel sense* *There are two mutually exclusive possibilities*

(a) The BOHK can prove every instance of (formal system /expression)
pair that cannot be proved making the BOHK complete.

"The Body of Human Knowledge" is not a "System of Logic" so can't
actually prove anything, it is a collection of "facts".

Thus, you have made a category error.

(b) The BOHK cannot prove some instances of (formal system /expression)
pairs cannot be proved, thus humans have no way to know that they cannot
be proved.

But we don't need to know WHAT isn't provable, just that some things ARE unprovable.

The Body of Human Knowledge knows sets of questions that we know one
answer or the other is true, but we have no way of knowing which one is
the true answer, thus it needs to admit the possibility of being incomplete.

The BOHK cannot possibly be incomplete in the Gödel sense. It is either complete in the Gödel sense or its incompleteness cannot be shown.

Nope. Invalid logic.

Note, systems do not need to "know" they are incomplete to be
incomplete. In fact, in Godel's proof, the system F doesn't know it is incomplete, its incompleteness is only shown it the meta system derived
from it. You are just showing your lack of understanding of how systems
work.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)