The body of analytic knowledge cannot be incomplete in the Gödel sense
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
analytic knowledge BOAK) simply means untrue.
[b]I now prove that such a system cannot be incomplete in the Gödel sense
There are two mutually exclusive possibilities:[/b]
(a) The BOAK can prove every instance of (formal system /expression)
pair that cannot be proved making the BOAK complete.
(b) The BOAK cannot prove some instances of (formal system /expression)
pairs cannot be proved, thus humans have no way to know that they cannot
be proved.
[b]The BOAK cannot possibly be incomplete in the Gödel sense. It is either
complete in the Gödel sense or its incompleteness cannot be shown.[/b]
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
analytic knowledge BOAK) simply means untrue.
[b]I now prove that such a system cannot be incomplete in the Gödel sense
There are two mutually exclusive possibilities:[/b]
(a) The BOAK can prove every instance of (formal system /expression)
pair that cannot be proved making the BOAK complete.
(b) The BOAK cannot prove some instances of (formal system /expression)
pairs cannot be proved, thus humans have no way to know that they cannot
be proved.
[b]The BOAK cannot possibly be incomplete in the Gödel sense. It is either
complete in the Gödel sense or its incompleteness cannot be shown.[/b]
Comments (50)
https://en.wikipedia.org/wiki/Ontology_(information_science) is an inheritance hierarchy {tree of knowledge} model of the current world using Richard Montague meaning postulates of formalized natural language.
All of the basic facts of the model of the current world are stipulated to be necessarily true, thus are the axioms of BOAK. The only other source of expressions of BOAK are deductions from these axioms.
Possibly false assumptions are not allowed. Only facts and deductions from facts are allowed. If a person disagrees that a cat is an animal then they are wrong in the same sense as disagreeing with arithmetic. 2 + 3 = 5 if you disagree then you are necessarily incorrect.
Yet the way that truth actually works is that unprovable literally means untrue within any finite formal system such as the BOAK. The whole notion of undecidability is a misconception.
I have been very diligently studying these things for two decades. I have written many papers.
What I mean by axiom is any expression of language that has been stipulated to be true. That cats are animals is stipulated to be true. Infinite proofs do not derive knowledge because they never reach their conclusion.
Every expression of the language of BOAK can be proved in BOAK, or it is simply untrue within BOAK.
This is the (expression of language / BOAK formal system) pair.
Quoting tim wood
This does not apply to BOAK.
Quoting tim wood
He never showed that there are expressions that are unprovable but true in the system.
He showed that G is unprovable in F and provable (thus true) in meta-mathematics.
This
If there is no truth-maker in formal system F making G true in F then G is simply untrue in F.
We never misconstrue this as F is incomplete.
Quoting tim wood
It seems utterly ridiculous to me that people still fail to understand that the liar paradox is simply not a truth bearer. Is this sentence true or false: "What time is it?"
(Obviously neither because it is a question and not a statement).
OK, this means an uncountable collection of "axioms". How could you organize these axioms in such a fashion they represent a data set in CS? What is axiom #1 ?
Some time back we had a promising theory of everything that started with the premise all facts could be catalogued within a program. But when asked "how?", things began to fade.
(a) Formal system BOAK (b) Every expression of the language of BOAK can be proved in
(a) and (b) is the pair.
Quoting PL Olcott
Quoting tim wood
(1) Cats are animals is an axiom of BOAK.
(2) Any unprovable expressions in the language of BOAK are simply untrue.
Because it is the {body of analytical knowledge} every expression is BOAK is true.
(3) Every axiom is stipulated to be true and every expression deduced from axioms is true.
Mendelson represents theorems this way ?C, in other words C is provable from axioms, thus according to Haskell Curry that makes it true. https://www.liarparadox.org/Haskell_Curry_45.pdf
Quoting tim wood
That is its mistake. Every analytic truth must have an analytic truthmaker connection to the formalized set of semantic meanings that make it true. When this provability semantic connection is missing then the expression is simply untrue. That G is unprovable in F merely means that G is untrue in F it does not actually means that F is incomplete.
Since this is generically the way that analytic truth really works mathematics is not free to override this.
The body of all current analytical general knowledge is not only countable it is finite.
They would be organized as a knowledge ontology inheritance hierarchy.
https://en.wikipedia.org/wiki/Ontology_(information_science)
The Cyc project has already done this on a massive scale.
https://en.wikipedia.org/wiki/Cyc
The Cyc project has {Thing} at the root of its knowledge tree.
Quoting jgill
It is basically the model of the current world plugged into a knowledge ontology inheritance hierarchy.
Thats because somewhere along the line you have things you know without knowing how you know them. We cant explain explaining. The epistemic buck has to stop somewhere.
A far cry from listing all facts (axioms).
Quoting PL Olcott So, the system of axioms is constantly increasing. Proof it is finite at a particular time?
Quoting PL Olcott "True" by what measures? What of potential inferences not realized?
Season's Greetings
I don't know how I came up with that wording.
Every expression of the BOAK is either stipulated to be true (AKA axioms) or deduced from these axioms. Unprovable simply means untrue, thus undecidable cannot possibly exist.
We know that dogs are animals and thus not fifteen story office buildings only because of the meanings of the words {dog} and {fifteen story office buildings} that have been stipulated. Unless these meanings are stipulated the words {dog} and {fifteen story office buildings} remain meaningless.
The body of analytic truth is only true on the basis of the connection of terms to the meanings that make the expression true. The lack of such a connection simply makes the expression untrue. Undecidability cannot possibly occur.
No the BOAK is a knowledge ontology inheritance hierarchy having the same structure as the Cyc project. Unlike a mere dictionary the requires a human mind, the knowledge ontology connections create a human mind. The term {human} may have as many connections as there are millimeters to the nearest star.
All of the general knowledge known to humans derives that {sheep cannot live on Mars} on the basis that sheep must have an atmosphere that Mars does not provide. This same knowledgebase would also know that the atmosphere that sheep require could be artificially provided, thus the question: "Can sheep live on Mars?" is a different question than "Can sheep possibly live on Mars?"
Every single detail of all of the general knowledge known to humans is in the BOAK. Can sheep live on Mars? is not general knowledge thus must be derived on the basis of general knowledge.
It is deduction from true premises. The formal system required must have a human level of comprehension directly hard-wired into it. It must know every slight nuance of the meaning of every word. The word {human} may have a full definition that makes a book light years tall.
Some {humans} go to Universities. {Universities} teach from books. {Books} have knowledge. The knowledge that {Books} have is {the text of every book ever written}.
It in not probable that sheep need air to breath therefore it is not inductive inference. Inductive inference only deals with probabilities it never deals with certainties. The meaning of the words {Sheep} and {Mars} conclusively proves that sheep cannot survive in the Mars atmosphere.
"the conclusion of a deductive argument is certain given the premises are correct; in contrast, the truth of the conclusion of an inductive argument is at best probable, based upon the evidence given."
https://en.wikipedia.org/wiki/Inductive_reasoning
Not undecidability. Rather potential facts. I know my Corgi could not understand analytic geometry, and that is a general assumption for Corgis. But there is the faint possibility that one will come along and understand the math. Then that fact becomes a member of the set of "axioms" in your system. But it is not at present. Thus your system continues to grow, and with each new axiom there is the possibility of contradicting a previously established axiom. So, when you ponder Godel what system are you talking about?
My question remains: show how exactly all axioms can be listed for reference. What is axiom #1?, #2?, . . .
It is currently known that humans are the only life on the Earth that can understand analytic geometry.
Listing all the axioms make fill a book light years deep. The Cyc project spent 1000 labor years on this.
But Godel was speaking of a small finite collection of axioms, not an axiomatic system that continues to increase without end. At what point does one initiate the drawing of conclusions? Tacking on the axiom of choice took math into new dimensions, as did infinity axioms. BOAK seems bewildering rather than enlightening, imo.
And subsequent discussion has been confused on other crucial points.
In the following, the context is formal theories.
/
A theory is a set of sentences closed under provability.
A theory has a language. For any language L, there are models for L.
For any model M for a language L, every sentence in L is either true or false, and not both, in M.
A model M for the language L for a theory T is a model of T if and only if every theorem of T is true in M.
A theory T is consistent if and only if there is no sentence S in the language for T such that both S and the negation of S are theorems of T.
A theory T is inconsistent if and only if T is not consistent.
A theory T is consistent if and only if there is an M that is a model of T.
A theory T is inconsistent if and only if there is not M that is a model of T.
A theory T is complete if and only if, for every sentence S in the language L for T, either S is a theorem of T or the negation of S is a theorem of T.
A theory T is incomplete if and only if T is not complete.
The Godel-Rosser incompleteness theorem is: If a theory T is recursively axiomatizable, sufficiently arithmetic, and consistent, then T is incomplete.
A formula is valid if and only if it is satisfied by all models and assignments for the variables.
The Godel completeness theorem (not to be confused with the incompleteness theorem) is that if a formula P is valid then P is derivable in the pure first order predicate calculus.
The soundness theorem is that if a formula P is derivable in the pure first order predicate calculus then P is valid.
There is a particular model of PA (first order Peano arithmetic) that we call "the standard model of arithmetic". Since there are sentences in the language for PA such that neither the sentence nor its negation is a theorem of PA, there are sentences that are true in the standard model that are not theorems of PA. Moreover, the particular sentence G (that we call "the Godel sentence") is proven outside of PA to be true in the standard model.
/
No recursively axiomatizable theory has an uncountable number of axioms. Theories with an uncountable number of axioms are not a consideration regarding the incompleteness theorem. Indeed, a language for a formal theory has only a countable number of symbols, thus only a countable number of expressions, thus only a countable number of formulas, thus only a countable number of sentences, thus there can be only a countable number of axioms in any axiomatization of the theory.
/
For any model M, there is the theory T whose theorems are all and only the sentences true in M. It was Tarski who proved "the undefinability of truth" theorem, which says that the set of sentences true in the standard model for the language of arithmetic is not definable in the language of arithmetic. For example, there is no formula in the language for PA that is true of all and only the Godel numbers of sentences true in the standard model of arithmetic.
/
The incompleteness theorem may be proved finitistically and contructivistically. While the proof is complicated, its methods are reducible to the basic reasoning of arithmetic by finite operations on single, discrete token objects. Thus, if the proof is considered dubious, then so is the basic reasoning of arithmetic on single, discrete token objects, which is to say that if the proof is considered dubious, then even the most basic arithmetic should be considered dubious.
/
To reiterate regarding this thread:
(1) The incompleteness theorem does not pertain to any set that includes informal expressions. And the incompleteness theorem does not pertain to sets of expressions other than those of recursively axiomatized, sufficiently arithmetic, and consistent theories.
(2) Sentences are not true or false in theories or systems. Rather sentences are true or false in models.
(3) No recursively axiomatizable theory has an uncountable number of axioms.
Not a finite set of axioms, rather a countably infinite set of axioms. However, indeed, not an uncountable set of axioms as was incorrectly claimed by a poster earlier in this thread.
The key change is the unprovable in BOAK simply means untrue in the BOAK, thus cannot means that BOAK is incomplete. BOAK is merely the actual body of general analytical knowledge as of now.
The BOAK can perform every arithmetic and logical operations, thus qualifies for Gödels Incompleteness. Knowledge specified in natural language has been formalized using Montague Grammar.
Quoting TonesInDeepFreeze
My system fully integrates the model directly within the formal system such that the system can perform deductive inference on the basis of semantics.
Quoting TonesInDeepFreeze
I have changed this.
(Incomplete(L) ? ?x ? Language(L) ((L ? x) ? (L ? ¬x)))
becomes
(¬TruthBearer(L,x) ? ?x ? Language(L) ((L ? x) ? (L ? ¬x)))
Incompleteness utterly ceases to exist.
[b]True(L,x) ? (L ? x)
False(L,x) ? (L ? ¬x)[/b]
Quoting TonesInDeepFreeze
Thus step (3) of Tarski's proof is rejected as a false assumption:
https://liarparadox.org/Tarski_275_276.pdf
(3) x ? Provable if and only if x ? True. // derived from (1) and (2)
Tarski's proof makes no false assumptions, no matter whatever incoherent ersatz pseudo formulations a crank on the Internet wishes to cook up.
I hoped you would chime in. :cool:
Quoting PL Olcott
That is Tarski's line (3) that says that expression of language x is only true if x cannot be proven.
It seems that Tarski is saying: If Y is true and X follows from Y then X is not true.
I am not talking about Montague grammar per say. I am talking about some system like Montague Grammar that can explain every detail about human general knowledge such that a machine acquires a fully human level of understanding. The Cyc Project has been doing this for decades. It is known as a knowledge ontology inheritance hierarchy. Not words and a list of meanings. A knowledge tree having an enormous number of connections to and from each unique sense meaning of every word.
And, for the third time: The incompleteness theorem pertains only to recursively axiomatizable theories.
If I don't comment to further replies, it's because meaningful discussion is not possible, and engagement is a waste of time, with a person who refuses to properly inform himself on the subject matter.
Here is Tarski saying exactly that: "(3) x ? Pr if and only if x ? Tr"
The exact same thing is on the bottom of the first page of Tarski's actual text:
https://liarparadox.org/Tarski_275_276.pdf
Which means x is not an element of Provable if and only if x is an element of True.
I apologize for not making this 100% perfectly clear in my prior replies.
The body of all analytical knowledge includes every recursively axiomatizable theory as a subset.
A set of statements that includes a proper subset that is a recursive set is not thereby itself a recursive set. And it is howlingly ridiculous to cite some set of statements that includes all recursive axiomatizations, such such a set is patently inconsistent. Claims about "every recursively axiomatizable theory" in a larger theory then with implications for incompleteness is howlingly ridiculous ignorance.
But as a free speech hawk, I do applaud The Philosophy Forum for not ejecting such patently misinformational postings even though that restraint comes at the price of contributing that much further to the degradation of sincere discussion on such topics.
This is pages from his paper. I have taken them to be
the actual proof of the undefinability theorem.
https://liarparadox.org/Tarski_275_276.pdf
What do you think that they mean?
This sure seems to be talking about undefinability to me
From page 276
For every deductive science in which arithmetic is contained
it is possible to specify arithmetical notions which, so to speak,
belong intuitively to this science, but which cannot be defined
on the basis of this science.
Unless you can describe this vague notion as it might appear in a computer program - that is to say a list with #1, #2, . . . - I can't get beyond it to the conclusions you draw. @TonesInDeepFreeze is recognized as a go-to source on these kinds of subjects.
He seems to be disagreeing with Tarski.
https://en.wikipedia.org/wiki/Ontology_(information_science) is how the knowledge is stored.
It is easiest to simply imagine that all the [general] things known to humans that can be written down in language have already been written down. Now we have the {body of analytic knowledge}.
So if listed, the listing might have to be refined as new knowledge is accrued. Still way to vague for me, but others may feel differently. I admire your tenacity on the subject.
It is simply the ordinary and common body of general knowledge known to mankind. It could be updated or static. Once the notions of {analytic truthmaker} is understood it is easy to see how this conquers Tarski Undefinability and Gödel's 1931 incompleteness. An expression of language either has an {analytic truthmaker} or it is untrue. Undecidable is no longer an option.