I didn't. The OP did. He said that Gödel's incompleteness theorem is "erroneous." That theorem bears directly on set theory. The OP needs to either retract his claim or else take responsibility for its logical consequences.
Refuting Incompleteness and Undefinability
Re: Refuting Incompleteness and Undefinability
Re: Refuting Incompleteness and Undefinability
I didn't. The OP did. He said that Gödel's incompleteness theorem is "erroneous." That theorem bears directly on set theory. The OP needs to either retract his claim or else likewise assert (and be prepared to defend) its logical consequences.
Last edited by wtf on Sun Mar 24, 2019 7:30 am, edited 2 times in total.
Re: Refuting Incompleteness and Undefinability
double post sorry
Re: Refuting Incompleteness and Undefinability
The OP's proof is also explicitly in a Curry-Howard system using type theory.
So clearly the OP is in a Type-theoretic paradigm talking ABOUT the ZFC paradigm.
You are speaking different languages.
Godel speaks about axiomatic systems. I am pointing out that the identity axiom is unprovable in a Curry-Howard system
for all a in A: a = a <==== DOES NOT HALT for ANY infinite set
There is a conceptual misalignment between set-theorists and type-theorists on the semantics of "provability".
"provable" means "decidable" in a Curry-Howard system.....
Re: Refuting Incompleteness and Undefinability
There is some further conceptual/linguistic misalignment.
Here is a Curry-Howard system that quite literally contains a contradiction: https://repl.it/repls/WoodenCostlyModel
Code: Select all
$toggle = true
def a
$toggle = ( not $toggle )
end
a and not a
=> true
c = a
c and not c
=> false In a Gödelian conception - it's inconsistent by definition. It contains a contradiction ( a & ¬ a )
In a Constructivist/Curry-Howard conception - It's consistent because it computes. There exists a Mathematical object such that "a and not a" is True, and a different Mathematical object such that "c and not c" is false.
Problem? Yep! The problem of time
- Speakpigeon
- Posts: 987
- Joined: Sat Nov 11, 2017 3:20 pm
- Location: Paris, France, EU
Re: Refuting Incompleteness and Undefinability
OK, why choose this means of publication? I would expect most mathematicians to poo-poo this medium...PeteOlcott wrote: ↑Sat Mar 23, 2019 9:15 pm I have received many comments on my work over the years. I have finally (just barely) gained enough mathematical maturity that logicians are starting to take me seriously. I publish on Researchgate and PhilPapers. ResearchGate only permits members with actual published works
PeteOlcott wrote: ↑Sat Mar 23, 2019 9:15 pm To translate the essence of my ideas into laymen's terms all of conceptual truth is anchored in expressions of language (such as English statements and the well-formed formula of formal languages) that are defined to be true. Some mathematicians such as Haskell Curry understand that mathematical axioms are defined to be true.
Yes, I broadly agree with that.
I broadly agree.PeteOlcott wrote: ↑Sat Mar 23, 2019 9:15 pm The only way that we know that a {cat} is a kind of {animal} is that this is defined as a basic fact. It turns out that all of analytical truth works this same way. I refer to analytical truth because some truth depends on sensations for the sense organs and can thus not be fully expressed using words. The actual taste of strawberries is an example.
As I see it, the only actual knowledge we have is subjective. I know pain whenever I am in pain etc. The rest can only be believed. Thus, all truths about the material world can only be putative. And then, as you seem to suggest here, truth can only be a computation from assumed possible cases, with as a result some formulas necessarily true by definition of logical constants or from assumptions.
Yes, the notion of a semantic separate from the syntax is something I only discovered recently and I thought it was definitely not a good idea.PeteOlcott wrote: ↑Sat Mar 23, 2019 9:15 pm Nearly all logicians maintain two separate representations to analyze semantics. I show that this is unnecessary and and makes things much more complicated than they really need to be. We can express and analyze any and all semantics entirely syntactically without any separate assignment of meaning over and above the conventional meaning of the logical operators and the axioms specified in the formal language.
I tried to find a justification of this but I don't believe there is, so, if you have a link...
Yes. That"s what I thought reading your piece.PeteOlcott wrote: ↑Sat Mar 23, 2019 9:15 pm The consequence of my work would be that the Tarski Undefinability Theorem, Gödel's 1931 Incompleteness Theorem, Turing's 1931 Halting Problem proof and many other undecidable decision problems would be shown to be erroneous. The other key consequence of this work is that truth conditional semantics will finally be anchored in a formal correct notion of truth. This is a key missing piece of all artificial intelligence research.
I haven't yet looked at the details and I'm not a mathematician, but so far I agree with all your points.
My pet peeve is the principle of explosion, which I find intuitively just moronic and I can't understand how gown-up mathematicians could countenance it. I worked out myself two different proofs (not for publication) but your "semantic proof" about going to the grocery store is equally convincing.
I look forward to looking into the details of what you say.
EB
Re: Refuting Incompleteness and Undefinability
Speakpigeon wrote: ↑Sun Mar 24, 2019 12:02 pm My pet peeve is the principle of explosion, which I find intuitively just moronic and I can't understand how gown-up mathematicians could countenance it.
You sure didn't spare your accusations, insults and character assassination attempts in the thread where I contradicted the LNC.
The principle of explosion is what it is.
The root cause of ALL contradictions is semantic overloading https://en.wikipedia.org/wiki/Semantic_overload
The moment you re-use a symbol, ANY symbol (even = ) to mean more than one thing in one context - you have committed an "error". Explosion follows.
There is just no way to escape this problem. We have a finite alphabet, finite vocabulary, finite set of symbols with which to express our meaning. Finite set of operators. At some point you are just going to overload the meaning of a symbol. You are going to make errors! To aim for consistency is pure, harmful idealism. Perfect is the enemy of good enough!
The way you deal with it is para-consistent logic in a computational framework. The system does not explode because contradictions are recognized, and handled in a discriminating fashion. Some contradictions are trivial, some are critical.
Our brain is really, REALLY good at Exception handling: https://en.wikipedia.org/wiki/Exception_handling
So we, humans don't need consistency.
-
PeteOlcott
- Posts: 1597
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Refuting Incompleteness and Undefinability
Minimal Type Theory (formally specified at the end of my paper) is higher order logic with types, thus a kind of type theory.Logik wrote: ↑Sun Mar 24, 2019 6:58 amWhy have you chosen set theory and not type theory for your mathematical foundation?PeteOlcott wrote: ↑Sat Mar 23, 2019 9:15 pm Nearly all logicians maintain two separate representations to analyze semantics.
Re: Refuting Incompleteness and Undefinability
Apologies, that question was aimed at "wtf". I was merely using your quote as a demonstration of his own choice to represent semantics in set theory AND in English.PeteOlcott wrote: ↑Sun Mar 24, 2019 3:38 pmMinimal Type Theory (formally specified at the end of my paper) is higher order logic with types, thus a kind of type theory.Logik wrote: ↑Sun Mar 24, 2019 6:58 amWhy have you chosen set theory and not type theory for your mathematical foundation?PeteOlcott wrote: ↑Sat Mar 23, 2019 9:15 pm Nearly all logicians maintain two separate representations to analyze semantics.
To which he replied:
More evidence for my claim that set theorists and type theorists are speaking cross-paradigms.
I, myself, find it to be an uphill battle to speak to Mathematicians coming from a Computer Science background.
IF you accept the consequences of the Curry-Howard isomorphism there is no difference between the two fields.
Any and all distinctions are just linguistic/nomenclature divergence from having worked in silos for so long.
-
PeteOlcott
- Posts: 1597
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Refuting Incompleteness and Undefinability
My last reply seems to have gotten lost. I also agree that the principle of explosion is semantically unsound.Speakpigeon wrote: ↑Sun Mar 24, 2019 12:02 pm Yes. That"s what I thought reading your piece.
I haven't yet looked at the details and I'm not a mathematician, but so far I agree with all your points.
My pet peeve is the principle of explosion, which I find intuitively just moronic and I can't understand how gown-up mathematicians could countenance it. I worked out myself two different proofs (not for publication) but your "semantic proof" about going to the grocery store is equally convincing.
I look forward to looking into the details of what you say.
EB
I do not want to digress into talking about this until all of my current points are fully addressed.
Relevance logic seems to address the principle of explosion quite well.
My main point is that it impossible for truth and provability to ever diverge because truth
is ONLY verified as a formal proof to theorem consequences:
∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))
When this above formula is accepted as the correct formalization of Truth,
then Tarski and Gödel are both refuted.
-
PeteOlcott
- Posts: 1597
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Refuting Incompleteness and Undefinability
I have always approached these things from a philosophy of logic perspective.Speakpigeon wrote: ↑Sun Mar 24, 2019 12:02 pmOK, why choose this means of publication? I would expect most mathematicians to poo-poo this medium...PeteOlcott wrote: ↑Sat Mar 23, 2019 9:15 pm I have received many comments on my work over the years. I have finally (just barely) gained enough mathematical maturity that logicians are starting to take me seriously. I publish on Researchgate and PhilPapers. ResearchGate only permits members with actual published works
When I finally learned enough formal logic to unequivocally express what I mean,
this was rejected by logicians as just simply not the way that we do it.
Logicians take conventional wisdom as the foundatal basis of all of their work and
never question the legitimacy of this foundation.
Previously I could never find any people interested in the philosophy of logic
foundations that could begin to understand any aspect of predicate logic. Now
that I finally totally understand these ideas myself I can bridge the gap between
the math and plain English. I added a laymen's section to the second paper of
my original post.
- Speakpigeon
- Posts: 987
- Joined: Sat Nov 11, 2017 3:20 pm
- Location: Paris, France, EU
Re: Refuting Incompleteness and Undefinability
OK, that may be something we could disagree about. I understand truth to be essentially another name for whatever it is we believe. We believe it's night, then we say it's true it's night. Logic then is merely the syntactic relation between our beliefs. We can't verify our beliefs anyway, but it's clearly a good idea to have "coherent" beliefs so our brain evolved to make sure we do, up to a point. Truth still as a value for each of us. There are things you can say that are true, just because there are things you know, like how you feel and whether you're hungry or pissed off. But that's not enough to discuss with each other and that's not enough even to think the world around you. So you need logic to think up the world around you, and also, secondarily, to exchange with other people "linguistically", something which has only become very important since perhaps 10,000 to 40,000 years ago. The point here is that logic is first a mental process evolved by natural selection over more than 525 million years and an intuitive capability we all have, and only secondarily a formal system, which as such is a part of nearly all human languages. As I understand it, the formal system we use is only a partial expression of the mental capability we have. Logic comes first, formalisation comes second, and then maybe not quite the thing. Still, this gives us a number of "logical truths" we all think are true, although we can choose not to, just because logical truths are formal logic, ergo part of language, and that we can invent and say pretty much anything. Our intuitive brain couldn't, though. This explains for example how mathematicians could choose, after Russell, to move away from their own logical intuition. Basically, mathematical logic is mathematics, not logic.PeteOlcott wrote: ↑Sun Mar 24, 2019 4:02 pm My last reply seems to have gotten lost. I also agree that the principle of explosion is semantically unsound.
I do not want to digress into talking about this until all of my current points are fully addressed.
Relevance logic seems to address the principle of explosion quite well.
My main point is that it impossible for truth and provability to ever diverge because truth
is ONLY verified as a formal proof to theorem consequences:
∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))
When this above formula is accepted as the correct formalization of Truth,
then Tarski and Gödel are both refuted.
So, I agree with your definition of truth here, but only insofar as it is conceived as "formal truth", which of course goes without saying given the way it is defined. My point, though, is that we may want to keep in mind that this "formal truth" isn't quite truth as our brain intuit it.
In effect, your definition makes truth dependent on the formal system. There's no other way for formal truth but, again, that ain't really truth either.
My brain says he feels good about that.
EB
- Speakpigeon
- Posts: 987
- Joined: Sat Nov 11, 2017 3:20 pm
- Location: Paris, France, EU
Re: Refuting Incompleteness and Undefinability
PeteOlcott wrote: ↑Sun Mar 24, 2019 5:01 pm I have always approached these things from a philosophy of logic perspective. When I finally learned enough formal logic to unequivocally express what I mean, this was rejected by logicians as just simply not the way that we do it.
I take it you're aware that it's not only mathematicians. Basically, early 20th century mathematical logic has defined what is logic for the rest of the world, from mathematicians themselves to computer scientists to philosophers. There's nearly no writing today on logic proper. It's always mathematical logic, i.e. mathematics, not logic, be it from mathematicians, computer scientists or philosophers (i.e. doing analytical philosophy). To read something on logic proper, you have to read old books, from Aristotle to perhaps the 1920's.
PeteOlcott wrote: ↑Sun Mar 24, 2019 5:01 pm Logicians take conventional wisdom as the foundatal basis of all of their work and never question the legitimacy of this foundation.
My take is that although Russell had a few reservations about his system, those have been lost through the passage of successive generations of mathematicians. So, the young ones have zero idea that what they're doing isn't really logic at all. They're not even trying to solve the problems. All they're doing is build new developments from what they think they know, without realising the foundations are just crap.
Please notice also how logical intuition has been systematically discredited. According to them, it's just not reliable. My take on this is that they've been traumatised by the paradoxes Russell discovered and then by Gödel's theorem. There has been a sort of crisis of confidence, leading them to make truth relative and to go all formal. Again, formal truth can only be formal, but I know I'm in pain whenever I'm pain so truth isn't fundamentally formal. It's formal only insofar as it is formal truth, i.e. as we have to use it as part of linguistic communication with other people and as necessary assumed truth in our mental representation of the world.
OK, I'll look at that but the maths maybe beyond my abilities to assess.PeteOlcott wrote: ↑Sun Mar 24, 2019 5:01 pm Previously I could never find any people interested in the philosophy of logic foundations that could begin to understand any aspect of predicate logic. Now that I finally totally understand these ideas myself I can bridge the gap between the math and plain English. I added a laymen's section to the second paper of my original post.
EB
Re: Refuting Incompleteness and Undefinability
John is John. ( A = A ⇔ True )Speakpigeon wrote: ↑Sun Mar 24, 2019 6:38 pmOK, I'll look at that but the maths maybe beyond my abilities to assess.PeteOlcott wrote: ↑Sun Mar 24, 2019 5:01 pm Previously I could never find any people interested in the philosophy of logic foundations that could begin to understand any aspect of predicate logic. Now that I finally totally understand these ideas myself I can bridge the gap between the math and plain English. I added a laymen's section to the second paper of my original post.
EB
Jane is Jane ( B = B ⇔ True )
John is human. ( A = C ⇔ True)
Jane is human. ( B = C ⇔ True)
John is Jane.( A = B ⇔ False)
The above are NOT "claims". They are propositions. Facts.
They violate any and all Aristotelian sensibilities for transitivity because set-theorists will INSIST that "John is human" is translated into formal logic as John ∈ Humans. While at the same time they will also claim that "John is Jane" does NOT translate to John ∈ Jane
This is the semantic dualism Pete is pointing out. The verb 'is' means many things.
The PROOF for these propositions is in this code: https://repl.it/repls/TintedDefiantInstruction
The verb "is" (represented by the logical symbol "=" ) is semantically overloaded. Its meaning is context-specific and inferred in the __eq__ function of the Human class.
English is a para-consistent logic.
- Arising_uk
- Posts: 12259
- Joined: Wed Oct 17, 2007 2:31 am
Re: Refuting Incompleteness and Undefinability
But you don't have to use '=' for 'is'?Logik wrote:...
The verb "is" (represented by the logical symbol "=" ) is semantically overloaded. Its meaning is context-specific and inferred in the __eq__ function of the Human class.
...