The death of Classical logic and the birth of Constructive Mathematics

[Logik]

The law of identity is the cornerstone of Arostotelian/Classical logic.
A = A is True.
In the 2nd half of the 20th century the American mathematician Haskell Curry and logician William Alvin Howard discovered an analogy between logical proofs and working computer programs. This is known as the Curry-Howard correspondence.
Mathematical proofs are working computer programs. https://en.wikipedia.org/wiki/Curry%E2% ... espondence
Therefore, if we can write a working computer program which asserts that A = A is false without producing an error then we have living proof contradicting the founding axiom of Classic/Aristotelian logic.
I hereby reject the law of identity, and give you the law of humanity: A = A is False.

Yet another expert opinion:

According to the Curry-Howard correspondance, a computer programme is analogous to a proof in intuitionistic logic, not classical logic.What programs implement is fundamentally constructive. The correspondance is only an analogy and in fact we already know that it should break down at some point.

So, whatever you infer from the correspondance you may like but no one should feel compelled to accept it as true.
Oh, what a disappointment!
EB

You keep claiming expert opinions, but you do not provide citations or references nor do you bring your experts to defend their positions.

What do you call that fallacy again? APPEAL TO AUTHORITY.

I am an expert. I am defending my position. I called my peers. They said your experts are wrong.

Classical logic is one giant false dichotomy. Propositions are either true or false. 1 or 0.

Computer science rejects that notion. Propositions are either true, false or UNDECIDABLE.

There are some claims that are true.
There are some claims that are false.
There are some claim whose truth or false-value CANNOT BE DECIDED.

The law of identity is one such example.

From identity follows that: for all x in Z+: x = x

The set of positive integers is infinite but countable
https://en.wikipedia.org/wiki/Integer

Z is a subset of the set of all rational numbers Q, in turn a subset of the real numbers R. Like the natural numbers, Z is countably infinite.

Suppose that the axiom of identity is true then it follows: ∞ = ∞ => true.
But from computational complexity theory we KNOW that the identity "∞ = ∞" is NOT DECIDABLE.

It is called the halting problem. https://en.wikipedia.org/wiki/Halting_problem

Contradiction!

for ALL x: x = x => Undecidable
for SOME x: x = x => True

The correspondance is only an analogy and in fact we already know that it should break down at some point.

It SHOULD break down? This is a violation of the is-ought gap.

It SHOULD break down, BUT IT DOESN'T!

[Speakpigeon]

The official tool used by Mathmatician in 2019 for automated theorem-proving ASSUMES the law of identity as axiomatic.
The axiom of Classical logic cannot be DECIDED true.

Even idiot knows this.
An axiom is a logical formula accepted as true on the face of it, without formal proof or empirical evidence that it is true.

Which only leaves us with one important question: is decidability important?

It's an empirical fact that we decide axioms are true.
This is the whole point of being an axiom. No one and nothing can decide for us to accept a formula as axiomatic. We make our decision ourselves.
And "decidability" in logic has a specific technical meaning:

Decidability
In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer.

However, the decision to accept axioms is not in itself a logical problem. So, the notion of decidability in logic is irrelevant to your choice of axioms.
Essentially, you have to decide for yourself whether you accept such and such axioms. There's no logical procedure to decide this. And this is pretty obvious as well. Try to define any formal logic at all without first assuming any axiom, rule of inference, or method of proof!

The Curry-Howard correspondence is a mathematical correspondence between particular logical systems and particular λ-calculi.

Yes. Precisely! It is a Mathematical correspondence between particular logical systems called Turing machines.
All Turing machines obey the laws of physics.

Sure, the brain too.
And as my expert says, "the correspondance is only an analogy and in fact we already know that it should break down at some point". It is expected to breaks down because we can't prove that the brain is a Turing machine.
I works for you because you don't use your brain.

Logic/Mathematics is a subset of computation.

Precisely not.
EB

[Logik]

It's an empirical fact that we decide axioms are true.

It is a fact THAT we decide our axioms.
What is NOT an empirical fact is HOW we decide our axioms.

HOW do we make choices?

If you can CHOOSE that an axiom is true.
I can CHOOSE that the axiom is false.

The process by which you DECIDE is called an algorithm.
https://en.wikipedia.org/wiki/Decision_problem

In computability theory and computational complexity theory, a decision problem is a problem that can be posed as a yes-no question of the input values.

And so please tell us. What was the algorithm by which you decided that x = x is true?
And equally important question: HOW and WHY did you dismiss the alternative hypothesis: x = x is false?

This is the whole point of being an axiom. No one and nothing can decide for us to accept a formula as axiomatic. We make our decision ourselves.

Very good! This settles it then.

If you can accept the axiom x = x
I can accept the axiom: x != x

Which one of us is "wrong" and which is "right"?

And "decidability" in logic has a specific technical meaning:

YES IT DOES!!

In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer.

We call those algorithms. Computer science is the study of algorithms.

I am the computer scientist

Decidability

Logic/Mathematics is a subset of computation.

Precisely not.
EB

Dimwit. You just ADMITTED that WE, HUMANS make CHOICES.

You ADMITTED that WE, HUMANS decide which axioms to lay down and which axioms to reject.

So IF Mathematics is the DECISION to lay down the axiom: for all x: x = x

Then..... you are ADMITTING that you are behaving like an Oracle Machine. That which decides!

https://en.wikipedia.org/wiki/Oracle_machine

In complexity theory and computability theory, an oracle machine is an abstract machine used to study decision problems. It can be visualized as a Turing machine with a black box, called an oracle, which is able to solve certain decision problems in a single operation. The problem can be of any complexity class. Even undecidable problems, such as the halting problem, can be used

YOU can solve decision problems in a single operation.
YOU can decide if x = x is True, or if x = x is False.
YOU are a computer.

You, the computer have INVENTED Mathematics!

Welcome to my world.

[Speakpigeon]

It's an empirical fact that we decide axioms are true.

It is a fact THAT we decide our axioms.
What is NOT an empirical fact is HOW we decide our axioms.

HOW do we make choices?

If you can CHOOSE that an axiom is true.
I can CHOOSE that the axiom is false.

The process by which you DECIDE is called an algorithm.
https://en.wikipedia.org/wiki/Decision_problem

In computability theory and computational complexity theory, a decision problem is a problem that can be posed as a yes-no question of the input values.

And so please tell us. What was the algorithm by which you decided that x = x is true?
And equally important question: HOW and WHY did you dismiss the alternative hypothesis: x = x is false?

This is the whole point of being an axiom. No one and nothing can decide for us to accept a formula as axiomatic. We make our decision ourselves.

Very good! This settles it then.

If you can accept the axiom x = x
I can accept the axiom: x != x

Which one of us is "wrong" and which is "right"?

And "decidability" in logic has a specific technical meaning:

YES IT DOES!!

In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer.

We call those algorithms. Computer science is the study of algorithms.

I am the computer scientist

Decidability

Logic/Mathematics is a subset of computation.

Precisely not.
EB

Dimwit. You just ADMITTED that WE, HUMANS make CHOICES.

You ADMITTED that WE, HUMANS decide which axioms to lay down and which axioms to reject.

So IF Mathematics is the DECISION to lay down the axiom: for all x: x = x

Then..... you are ADMITTING that you are behaving like an Oracle Machine. That which decides!

https://en.wikipedia.org/wiki/Oracle_machine

In complexity theory and computability theory, an oracle machine is an abstract machine used to study decision problems. It can be visualized as a Turing machine with a black box, called an oracle, which is able to solve certain decision problems in a single operation. The problem can be of any complexity class. Even undecidable problems, such as the halting problem, can be used

YOU can solve decision problems in a single operation.
YOU can decide if x = x is True, or if x = x is False.
YOU are a computer.

You, the computer have INVENTED Mathematics!

Welcome to my world.

You're not making much sense.
EB

[Logik]

It's an empirical fact that we decide axioms are true.

It is a fact THAT we decide our axioms.
What is NOT an empirical fact is HOW we decide our axioms.

HOW do we make choices?

If you can CHOOSE that an axiom is true.
I can CHOOSE that the axiom is false.

The process by which you DECIDE is called an algorithm.
https://en.wikipedia.org/wiki/Decision_problem

In computability theory and computational complexity theory, a decision problem is a problem that can be posed as a yes-no question of the input values.

And so please tell us. What was the algorithm by which you decided that x = x is true?
And equally important question: HOW and WHY did you dismiss the alternative hypothesis: x = x is false?

This is the whole point of being an axiom. No one and nothing can decide for us to accept a formula as axiomatic. We make our decision ourselves.

Very good! This settles it then.

If you can accept the axiom x = x
I can accept the axiom: x != x

Which one of us is "wrong" and which is "right"?

And "decidability" in logic has a specific technical meaning:

YES IT DOES!!

In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer.

We call those algorithms. Computer science is the study of algorithms.

I am the computer scientist

Decidability

Precisely not.
EB

Dimwit. You just ADMITTED that WE, HUMANS make CHOICES.

You ADMITTED that WE, HUMANS decide which axioms to lay down and which axioms to reject.

So IF Mathematics is the DECISION to lay down the axiom: for all x: x = x

Then..... you are ADMITTING that you are behaving like an Oracle Machine. That which decides!

https://en.wikipedia.org/wiki/Oracle_machine

In complexity theory and computability theory, an oracle machine is an abstract machine used to study decision problems. It can be visualized as a Turing machine with a black box, called an oracle, which is able to solve certain decision problems in a single operation. The problem can be of any complexity class. Even undecidable problems, such as the halting problem, can be used

YOU can solve decision problems in a single operation.
YOU can decide if x = x is True, or if x = x is False.
YOU are a computer.

You, the computer have INVENTED Mathematics!

Welcome to my world.

You're not making much sense.
EB

Then read it slowly and ask for clarification.

You said you have CHOSEN to the axiom to be true. So I asked how you made the choice.

Because a yes/no, true/false CHOICE is called a decision problem.
https://en.wikipedia.org/wiki/Decision_problem

What algorithm did you use to decide the correct answer?
What was the question (input) to the algorithm?

[Speakpigeon]

Another expert on the Curry-Howard...

The essence of the Curry-Howard correspondance is "propositions as types" so that the Curry-Howard correspondence cannot possibly be relevant to languages like Python that do not have build-in types.

In other words, you "proof" is a fraud.

I haven't been able to find anyone anywhere who could give credence to your "proof".
EB

[Logik]

Another expert on the Curry-Howard...

The essence of the Curry-Howard correspondance is "propositions as types" so that the Curry-Howard correspondence cannot possibly be relevant to languages like Python that do not have build-in types.

In other words, you "proof" is a fraud.

I haven't been able to find anyone anywhere who could give credence to your "proof".
EB

You are working your ass off to reject Curry-Howard when you fail to realize that you can bootstrap ANY type system you want on ANY Turing-machine.
Turing-completeness does neither mandate nor require types. The language C is Turing-complete it does NOT have types.
But you can construct every single language that has types from C.

You want Haskell? Construct it.
You want Coq? Construct it.
You want types? CONSTRUCT THEM.

From first principles!

What is a type ? Is an integer not a TYPE of thing, Is a digit not a TYPE of thing?

Please prove to me (in a mathematic of your choice) that
digit(1) = integer(1)

I am the real deal. You are just ignorant. But - maintain your religion if it makes you happy.

[Speakpigeon]

You're not making much sense.
EB

Then read it slowly and ask for clarification.
You said you have CHOSEN to the axiom to be true. So I asked how you made the choice.
Because a yes/no, true/false CHOICE is called a decision problem.
https://en.wikipedia.org/wiki/Decision_problem
What algorithm did you use to decide the correct answer?
What was the question (input) to the algorithm?

You're not fit for any kind of rational debate. You're hysterical. You produce wild claim after wild claim and any effort I made to discuss them have proved futile.
EB

[Logik]

You're not making much sense.
EB

Then read it slowly and ask for clarification.
You said you have CHOSEN to the axiom to be true. So I asked how you made the choice.
Because a yes/no, true/false CHOICE is called a decision problem.
https://en.wikipedia.org/wiki/Decision_problem
What algorithm did you use to decide the correct answer?
What was the question (input) to the algorithm?

You're not fit for any kind of rational debate. You're hysterical. You produce wild claim after wild claim and any effort I made to discuss them have proved futile.
EB

You don't know what "rationality" means. You are abusing the word to imply that I won't discuss the topic on YOUR terms.

Correct you are!

Furthermore you are making no attempts to discuss anything. You are just flinging poop, appealing to fake authorities to reject my claims and continuously trying to undermine my character.

That's not rational - that's just defending a religion.

Use your own brain. Or don't.

[Speakpigeon]

It's an empirical fact that we decide axioms are true.

It is a fact THAT we decide our axioms. The process by which you DECIDE is called an algorithm.
And so please tell us. What was the algorithm by which you decided that x = x is true?

This is an example of the wild claims you make. The choices that we make as human beings are brain processes, not algorithms. Your claim is just moronic.

And equally important question: HOW and WHY did you dismiss the alternative hypothesis: x = x is false?

Our brain just does it. I already told you and yet you keep asking the same stupid question. Nobody knows how the brain works exactly. Not you, not anybody.
And if you understood what the Law of Identity means you would accept it. But you don't understand what it means. You seem to think axiom can be decided by logical proof but the can't. Which why they are axioms.
EB

[Atla]

Poor Logikal Timeseeker spending almost every minute of every day for half a year on this forum, and achieving less than nothing.

How high is the utility value of that?

[Speakpigeon]

Another expert on the Curry-Howard...

The essence of the Curry-Howard correspondance is "propositions as types" so that the Curry-Howard correspondence cannot possibly be relevant to languages like Python that do not have build-in types.

In other words, you "proof" is a fraud.

I haven't been able to find anyone anywhere who could give credence to your "proof".
EB

You are working your ass off to reject Curry-Howard when you fail to realize that you can bootstrap ANY type system you want on ANY Turing-machine.
Turing-completeness does neither mandate nor require types. The language C is Turing-complete it does NOT have types.
But you can construct every single language that has types from C.

You want Haskell? Construct it.
You want Coq? Construct it.
You want types? CONSTRUCT THEM.

From first principles!

What is a type ? Is an integer not a TYPE of thing, Is a digit not a TYPE of thing?

Please prove to me (in a mathematic of your choice) that
digit(1) = integer(1)

I am the real deal. You are just ignorant. But - maintain your religion if it makes you happy.

The essence of the Curry-Howard correspondance is "propositions as types" so that the Curry-Howard correspondence cannot possibly be relevant to languages like Python that do not have build-in types.
EB

[Speakpigeon]

YOU can solve decision problems in a single operation.
YOU can decide if x = x is True, or if x = x is False.
YOU are a computer.
You, the computer have INVENTED Mathematics!
Welcome to my world.

Where's the problem already?
EB

[Logik]

YOU can solve decision problems in a single operation.
YOU can decide if x = x is True, or if x = x is False.
YOU are a computer.
You, the computer have INVENTED Mathematics!
Welcome to my world.

Where's the problem already?
EB

It's an axiom. False authority.

You have invented a God.

And you discriminate against everybody who is not part of your religion.

[Speakpigeon]

Poor Logikal Timeseeker spending almost every minute of every day for half a year on this forum, and achieving less than nothing.

How high is the utility value of that?

Yes, that's what I thought. Anybody with anything like a substantial discovery would definitely not spend most of his life on any forum!
EB