Refuting Incompleteness and Undefinability

[Logik]

But you don't have to use '=' for 'is'?

It doesn't matter what symbol you choose. The "is" in English is semantically overloaded ( https://en.wikipedia.org/wiki/Semantic_overload ). It means different things in different contexts.

If you were to write an English-to-FOPL parser you will need a 1:M (1 to many) map between the English "is" and its various representations in FOPL.
Choosing the correct meaning of "is" from a 1:M map is trivial for a human brain, but it is an open problem in computer science.

https://en.wikipedia.org/wiki/Word-sense_disambiguation

[PeteOlcott]

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.

I yes this makes sense. I too come from a computer science background.

[PeteOlcott]

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.

OK, that may be something we could disagree about. I understand truth to be essentially another name for whatever it is we believe.

That would logically entail that the Earth really was flat when (before Pythagoras) there was a universal consensus that the Earth was flat.

[PeteOlcott]

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.

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.

That is why I only define truth as expressions of language that can be totally verified as true entirely on the basis of the meaning of their words.

https://www.britannica.com/topic/tautology
Tautology, in logic, a statement so framed that it cannot be denied
without inconsistency. Thus, “All humans are mammals” is held to
assert with regard to anything whatsoever that either it is a human
or it is not a mammal. But that universal “truth” follows not from
any facts noted about real humans but only from the actual use of
human and mammal and is thus purely a matter of definition.

This is the formal mathematical way of saying the same thing:
∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))

[PeteOlcott]

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.

OK, I'll look at that but the maths maybe beyond my abilities to assess.
EB

John is human. ( A = C ⇔ True)

The above English sentence can be formalized in Minimal Type Theory as a relation between logical constants.
{John} ∈ {Human}

[Logik]

The above English sentence can be formalized in Minimal Type Theory as a relation between logical constants.
{John} ∈ {Human}

"John is human" <==> {John} ∈ {Human}
"Jane is human" <==> {Jane} ∈ {Human}
"John is Jane" <=/=> {John} ∈ {Jane}

The problem is the semantic overloading of the verb "IS" which happens in English.

So if I am optimizing to maintain 1:1 relationship between my English and Type-theoretic grammar then I do this:

Override the __eq__ method to allow it to infer meaning from context.

Code: Select all

class Human(object):
  def __init__(self):
    pass
  
  # We are wildly inconsistent! 
  # We mean many different things by the English word "IS"!
  def __eq__(self, other):
    # Identity check
    if id(self) == id(other):
      return True
    # Type-equivalence
    elif other.__class__ == self.__class__:
      return False
    # Type-check
    return self.__class__ == other

Which then allows me to express

John == Human Returns: True
Jane == Human Returns: True
John == Jane: Returns False

As per https://repl.it/repls/TintedDefiantInstruction

[Speakpigeon]

OK, that may be something we could disagree about. I understand truth to be essentially another name for whatever it is we believe.

That would logically entail that the Earth really was flat when (before Pythagoras) there was a universal consensus that the Earth was flat.

No because a belief doesn't imply anything as to the reality of things.
We believe it's night, we say it's true it's night.
That's how we use the word "true".
EB

[Speakpigeon]

OK, that may be something we could disagree about. I understand truth to be essentially another name for whatever it is we believe.

That would logically entail that the Earth really was flat when (before Pythagoras) there was a universal consensus that the Earth was flat.

No because a belief doesn't imply anything as to the reality of things.
We believe it's night, we say it's true it's night.
That's how we use the word "true".
EB

[Speakpigeon]

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.

That is why I only define truth as expressions of language that can be totally verified as true entirely on the basis of the meaning of their words.

https://www.britannica.com/topic/tautology
Tautology, in logic, a statement so framed that it cannot be denied
without inconsistency. Thus, “All humans are mammals” is held to
assert with regard to anything whatsoever that either it is a human
or it is not a mammal. But that universal “truth” follows not from
any facts noted about real humans but only from the actual use of
human and mammal and is thus purely a matter of definition.

This is the formal mathematical way of saying the same thing:
∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))

But the notion of tautology is not synonymous with the ordinary notion of truth. If you mean tautology, then use the word "tautology". Don't do what mathematical logic does: redefine our vocabulary beyond recognition.
EB

[PeteOlcott]

OK, that may be something we could disagree about. I understand truth to be essentially another name for whatever it is we believe.

That would logically entail that the Earth really was flat when (before Pythagoras) there was a universal consensus that the Earth was flat.

No because a belief doesn't imply anything as to the reality of things.
We believe it's night, we say it's true it's night.
That's how we use the word "true".
EB

Then we use the word "true" in a way that we deceive ourselves thus incorrectly.
It truth and belief was actually the exact same thing then disagreement would be
logically impossible. The fact that contradictory statements cannot possibly be true
and contradictory beliefs exist proves that belief and truth are not the same.

[Speakpigeon]

No because a belief doesn't imply anything as to the reality of things.
We believe it's night, we say it's true it's night.
That's how we use the word "true".

Then we use the word "true" in a way that we deceive ourselves thus incorrectly.

We don't deceive ourselves since we really believe. What we believe about the material world is invariably and irredeemably false but that doesn't matter. It works.

It truth and belief was actually the exact same thing then disagreement would be logically impossible.

It's not the exact same thing. Belief implies say it's true. Not that it's true of reality.
And it's a fact we can't disagree with ourselves, whatever we believe.
However, since different people have different beliefs, the statements they see as true will be different.
Whatever someone else says may be contradictory to my beliefs. Something which is apparent enough on forums but also between logicians.

The fact that contradictory statements cannot possibly be true and contradictory beliefs exist proves that belief and truth are not the same.

Again, I didn't say they are the same thing. We have different beliefs so we disagree about truth. Two people can have contradictory beliefs and both will insist what they say as a result of their beliefs is true. I think you should find that Quine hold the same view, i.e. what matters is that we try to keep our set of beliefs logically consistent. I guess it's just our brain that requires it. Debate may provide opportunities to detect an inconsistency in your own beliefs, unless you're too dogmatic for that.
Please note this underpins the usual notion of proposition as being possibly true or possibly false. All logical calculus keeps these two possibilities alive except for premises and for the conclusion.
Truth isn't a logical concept. Truth is pre-logical. Then, to connect with it, any method of logic has to specify it's own formal expression of truth. But logical truth is not truth as we think of it. Logical truth is in effect a vehicle. The vehicle to preserve truth through logical calculation.
And so we can't do any different. We have to have a formal notion of truth. But we shouldn't confuse logical truth with our usual notion of truth, which is that whatever we believe, we say is true.
And the notion that logic is independent of any actual truth I think goes back to the Stoics, and it was absolutely crucial to the Scholastic. And this is in evidence in the fact that we recognise the notion of logical validity as independent of any actual truth. A bicycle is a large planet; All large planets are stupidly mortal; Therefore, a bicycle is stupidly mortal. Isn't that valid? Logic is all about validity, something I believe logicians have belatedly started to recognise.
EB

[PeteOlcott]

I understand truth to be essentially another name for whatever it is we believe.

It's not the exact same thing. Belief implies say it's true. Not that it's true of reality.

When you said : "truth to be essentially another name for whatever it is we believe."
you didn't mean what you said.

Logical propositions formalize the notion of truth, We use propositional attitudes to specify
beliefs. There is a humongous (sometimes life and death) difference between these two.

[wtf]

Logical propositions formalize the notion of truth, We use propositional attitudes to specify
beliefs. There is a humongous (sometimes life and death) difference between these two.

You claim to have falsified Gödel's incompleteness theorem. That theorem applies to ALL formal systems that can express elementary number theory, whether type theory or set theory or category theory or any other foundational approach. When I asked you to comment on the obvious consequences of your claim, you changed the subject and started a new thread.

Likewise you claim to have disproved Turing's proof of the unsolvability of the Halting problem; and when I asked you to point out the error in the proof, you did not do so. You did say you've been studying the proof for 15 years. Turing's beautifully simple proof is about an hour's worth of work for a CS undergrad: Five minutes to read it and fifty-five minutes to grok it. If you've studied the proof, point out the error. Become famous. You'll be overthrowing 83 years of orthodoxy in computer science.

I won't be joining the daily back and forth in this thread. I'll just say that if one claims to have overthrown two of the most fundamental results in math and computer science, one should be prepared to defend their ideas better than you have with me. Whether you do this now or later, you should at some point ask yourself if you really believe what you're claiming. You should reread my posts to get some specific points of departure for your research; specifically the work of Gödel and Cohen regarding independence proofs in set theory, and related modern developments.

@Logik has mentioned to me that I should be thinking of type theory and not set theory. But Gödelian incompleteness bears directly on set theory; and it's perfectly appropriate to point out the great claim that @PeteOlcutt is making; and the utter lack of a counterargument when challenged on this simple point. Anyone knowledgeable in math or computer science who hears your claims of overthrowing Gödel and Turing will ask you these same questions as I did.

Russell and Whitehead talked about set theory and so did Gödel. And frankly the idea that a great mind like Haskell Curry would endorse any of the utter nonsense in this thread is laughable.

[PeteOlcott]

When I asked you to comment on the obvious consequences of your claim, you changed the subject and started a new thread.

I don't know the consequences of my claim. It has taken all of my time on the single-minded focus for 22 years to simply make my claim and its proof clear enough to be understood.

In this thread I am only prepared to refute the Tarski Undefinability Theorem and this simplified refutation of the 1931 Incompleteness Theorem. ∃F ∈ Formal_Systems (∃G ∈ Language(F) (G ↔ ~(F ⊢ G))).

I have rewritten this paper dozens of times since yesterday to make it increasingly more clear based on all of the feedback.
Philosophy of Logic – Reexamining the Formalized Notion of Truth https://philpapers.org/archive/OLCPOL.pdf

[wtf]

In this thread I am only prepared to refute the Tarski Undefinability Theorem ...

Yet earlier in this thread you wrote:

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.

Do you retract your earlier claims about Gödel and Turing? And which other undecidable decisions problems to you claim are erroneous? What do you think of Hilbert's tenth problem?