Eliminating Undecidability and Incompleteness in Formal Systems

[PeteOlcott]

No it is more like I say "I am go to eat some lunch" and people quibble endlessly
over what "to" really means, and have to go home when the restaurant closes
without even looking at the menu.

Axioms aren't true or false. They're simply statements accepted without proof in order to get some axiomatic system off the ground. They can be anything you want. You can do geometry with the parallel postulate, in which case you get Euclidean geometry; or with the negation of the parallel postulate, in which case you get non-Euclidean geometry. You can do group theory with the assumption that your group operation is commutative, in which case you get the theory of Abelian groups; or with the assumption that it's not, in which case you get the theory of non-Abelian groups. Being Abelian isn't true or false in general; it's true or false of some particular group.

It is a mandatory prerequisite that I have as the ultimate foundation of my complete and consistent
formalization of the notion of truth to have the Haskell Curry specification of axiom as my basis:
http://liarparadox.org/Haskell_Curry_45.pdf

All other notions of axioms are beside my point.
What is the technical term for specified definitions?

[wtf]

No it is more like I say "I am go to eat some lunch" and people quibble endlessly
over what "to" really means, and have to go home when the restaurant closes
without even looking at the menu.

Axioms aren't true or false. They're simply statements accepted without proof in order to get some axiomatic system off the ground. They can be anything you want. You can do geometry with the parallel postulate, in which case you get Euclidean geometry; or with the negation of the parallel postulate, in which case you get non-Euclidean geometry. You can do group theory with the assumption that your group operation is commutative, in which case you get the theory of Abelian groups; or with the assumption that it's not, in which case you get the theory of non-Abelian groups. Being Abelian isn't true or false in general; it's true or false of some particular group.

It is a mandatory prerequisite that I have as the ultimate foundation of my complete and consistent
formalization of the notion of truth to have the Haskell Curry specification of axiom as my basis:
http://liarparadox.org/Haskell_Curry_45.pdf

All other notions of axioms are beside my point.
What is the technical term for specified definitions?

As usual, you can't directly engage with a challenge.

I strongly doubt that Haskell Curry was confused on what an axiom is. Rather, you're confused about what Haskell Curry said.

So if I give you the following axiom:

* For each x, if x isn't 0, then there exists y such that xy = 1

Is it true? Or false? It's neither, till we pick an interpretation. If our universe of discourse is the real numbers, it's true. If our universe is the integers, it's false. Can you engage directly with this example?

[PeteOlcott]

It is a mandatory prerequisite that I have as the ultimate foundation of my complete and consistent
formalization of the notion of truth to have the Haskell Curry specification of axiom as my basis:
http://liarparadox.org/Haskell_Curry_45.pdf

All other notions of axioms are beside my point.
What is the technical term for specified definitions?

I strongly doubt that Haskell Curry was confused on what an axiom is. Rather, you're confused about what Haskell Curry said.

So if I give you the following axiom:

* For each x, if x isn't 0, then there exists y such that xy = 1

Is it true? Or false? It's neither, till we pick an interpretation. If our universe of discourse is the real numbers, it's true. If our universe is the integers, it's false. Can you engage directly with this example?

OK, first click on the link and verify that I am right about Curry.
I went through a lot of trouble to get that page, highlight it and make it available.

Apparently many books stores advertise a 2010 edition of his book (even though he
died in 1981) and Wikipedia quotes from this edition AND IT DOES NOT ACTUALLY EXIST.
https://en.wikipedia.org/wiki/Theory_(m ... _generally

Without specifying an explicit type you are implicitly referring to everything
in the universe of all things thus picking reals makes it true.

[wtf]

OK, first click on the link and verify that I am right about Curry.

LOL. I did and you're wrong. He makes the exact same point I did; that a sentence has no truth value until you choose an interpretation. He uses the example of "He is a jackass," which is neither true nor false until you define "jackass" and say who "he" refers to.

Your example makes the exact same point I did. I was surprised to click on your link and see it so obviously refute your claim about what Curry said.

There is absolutely nothing on that page that supports your false claim that axioms are regarded as unconditionally true. Evidently you misunderstood something you read 22 years ago and have been obsessively fixated on your error all this time.

It's the most elementary fact of logic that a sentence is neither true nor false until an interpretation is supplied. And the link you gave absolutely verifies this point. There is Haskell Curry explaining to you exactly what I'm explaining to you. Readers can click on your link and verify this.

[PeteOlcott]

OK, first click on the link and verify that I am right about Curry.

There is absolutely nothing on that page that supports your false claim that axioms are regarded as unconditionally true. Evidently you misunderstood something you read 22 years ago and have been obsessively fixated on your error all this time.

Above Link 1977 edition
Let T be such a theory. 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.

Here is the far less clumsy 2010 edition
The elementary statements which belong to T are called the
elementary theorems of T and said to be true. In this way, a
theory is a way of designating a subset of E which consists
entirely of true statements.

NO MODEL THEORY NEEDED

[wtf]

OK, first click on the link and verify that I am right about Curry.

There is absolutely nothing on that page that supports your false claim that axioms are regarded as unconditionally true. Evidently you misunderstood something you read 22 years ago and have been obsessively fixated on your error all this time.

Above Link 1977 edition
Let T be such a theory. 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.

Here is the far less clumsy 2010 edition
The elementary statements which belong to T are called the
elementary theorems of T and said to be true. In this way, a
theory is a way of designating a subset of E which consists
entirely of true statements.

NO MODEL THEORY NEEDED

They're SAID to be true, in a colloquial sense. It's true that in chess the knight can jump over other pieces. It's not a law of nature, it's a rule SAID to be true in a formal game.

I'm done here. You won't directly engage with the question I asked you. And when I looked at your link, it said EXACTLY what I was saying and exactly the opposite of what you claim.

[Logik]

You keep saying that knowing that is nothing was standard this communication
(using standard English) would be impossible. Why do you keep contradicting yourself?

Strawman.

English doesn't have inflexible rules like the ones you are trying to impose. And you have dodged the point over and over. How does one inject new meaning into a closed system with fixed/deterministic truth?

The constraints are for the purpose of communicating with math people,
they are not arbitrary.

Higher order predicate logic with types would be Chomsky level-2.
The semantics of its operators can be defined in a tiny subset of "c".

Now that is irony of epic proportions.

Observe what is happening here:

1. You are unable to communicate with Math people because you are missing:
* Operators like Recursion (:=) and WellFormulatedFormula()
* Predicates like Provable()

You are missing adequate tools to express yourself.

2. In order to communicate better with Math people ..... you are ..... INVENTING ..... NEW OPERATORS and NEW PREDICATES.

You are EVOLVING the language because the the one you have been given is... what? INSUFFICIENT to express... what you MEAN?

So you are trying to improve communication, by allowing yourself to express yourself better. And you have done that by? INVENTING....NEW....LANGUAGE.

Communication is transfer of meaning from one person to another via any medium (English, pictures, art, music, mathematics, video etc. etc. etc)
What you are trying to devise is an inflexible protocol.

Even mathematicians are moving into the 21st century with tools like Coq and going towards automated theorem proving: https://en.wikipedia.org/wiki/Coq

Methinks you are suffering from a bad case of the sunk cost fallacy.

[PeteOlcott]

You keep saying that knowing that is nothing was standard this communication
(using standard English) would be impossible. Why do you keep contradicting yourself?

Strawman.

English doesn't have inflexible rules like the ones you are trying to impose. And you have dodged the point over and over. How does one inject new meaning into a closed system with fixed/deterministic truth?

The constraints are for the purpose of communicating with math people,
they are not arbitrary.

Higher order predicate logic with types would be Chomsky level-2.
The semantics of its operators can be defined in a tiny subset of "c".

Now that is irony of epic proportions.

Observe what is happening here:

1. You are unable to communicate with Math people because you are missing:
* Operators like Recursion (:=) and WellFormulatedFormula()
* Predicates like Provable()

You are missing adequate tools to express yourself.

2. In order to communicate better with Math people ..... you are ..... INVENTING ..... NEW OPERATORS and NEW PREDICATES.

You are EVOLVING the language because the the one you have been given is... what? INSUFFICIENT to express... what you MEAN?

So you are trying to improve communication, by allowing yourself to express yourself better. And you have done that by? INVENTING....NEW....LANGUAGE.

Communication is transfer of meaning from one person to another via any medium (English, pictures, art, music, mathematics, video etc. etc. etc)
What you are trying to devise is an inflexible protocol.

Even mathematicians are moving into the 21st century with tools like Coq and going towards automated theorem proving: https://en.wikipedia.org/wiki/Coq

Methinks you are suffering from a bad case of the sunk cost fallacy.

Tarski "proved" that there cannot possibly be any correct formalization of the notion of truth entirely on the basis of an insufficiently expressive formal system that was incapable of recognizing and rejecting semantically incorrect expressions of language.

∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))
∀F ∈ Formal_Systems ∀x ∈ WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
∀F ∈ Formal_Systems ∀x ∈ WFF(F) (Boolean(F, x) ↔ (True(F, x) ∨ False(F, x)))

[Logik]

Tarski "proved" that there cannot possibly be any correct formalization of the notion of truth entirely on the basis of an insufficiently expressive formal system that was incapable of recognizing and rejecting semantically incorrect expressions of language.

∀F ∈ Formal_Systems ∀x ∈ WFF(F) (Boolean(F, x) ↔ (True(F, x) ∨ False(F, x)))

Semantically incorrect?

You are venturing into the real of semantic prescriptivism.

As in things that I am allowed or not allowed to think/say.

[PeteOlcott]

Tarski "proved" that there cannot possibly be any correct formalization of the notion of truth entirely on the basis of an insufficiently expressive formal system that was incapable of recognizing and rejecting semantically incorrect expressions of language.

∀F ∈ Formal_Systems ∀x ∈ WFF(F) (Boolean(F, x) ↔ (True(F, x) ∨ False(F, x)))

Semantically incorrect?

You are venturing into the real of semantic prescriptivism.

As in things that I am allowed or not allowed to think/say.

You are not allowed to correctly say: (True ⇔ False)

[Logik]

You are not allowed to correctly say: (True ⇔ False)

The universe allows it. Who are you to forbid it?

Here is me DOING that which you claim I am not "allowed" to say.

https://repl.it/repls/RoughPointlessLoop

Code: Select all

True = FalseClass
False = FalseClass

def ⇔(a,b)
  return a == b
end

⇔(True, False).class
=> TrueClass

[PeteOlcott]

You are not allowed to correctly say: (True ⇔ False)

The universe allows it. Who are you to forbid it?

Here is me DOING that which you claim I am not "allowed" to say.

I never said you weren't allowed to say that. One little word changes everything.

correctly

You are not allowed to [correctly] say: (True ⇔ False)

[Logik]

You are not allowed to [correctly] say: (True ⇔ False)

My Ruby interpreter still disagrees with you.

What is your criterion for "correctness"?

[PeteOlcott]

You are not allowed to [correctly] say: (True ⇔ False)

My Ruby interpreter still disagrees with you.

What is your criterion for "correctness"?

You seem to be just playing head games. I really don't have time for that.

[Logik]

You seem to be just playing head games. I really don't have time for that.

A physical system (called a computer) has DECIDED (via an algorithm that you can examine) that True ⇔ False

I have satisfied the decidability criterion despite your objections.

What "games" do you think I am playing? If you believe my algorithm fails to satisfy some "correctness" criterion - then you need to provide a formal mechanism to assert violations of said criterion. Prevent me from expressing that which I have expressed.

Write me a unit test or something.
A compiler, or a syntax checker.

Then I'll show you how deep the rabbit hole goes. Buffer overflows, input validation, escape character injection, code injection, timing attacks.

If you want decidability (which is a nice short-hand for "closed-system determinism") you need to control ALL variables. Demonstrate to me that you have any actual control, and not just a prescriptivist delusion.