A mathematical perspective on the phenomenon of "miracles"

[Skepdick]

There is a difference between evaluating an expression and trying to prove another statement from it.

Both are typically done by rewriting it.

So how does doing the same thing (rewriting) result in a "difference"?
Evaluating an expression is the same thing as providing the continuous transformation of the expression to normal form.
Proving f:A -> B is providing the continuous transformation of an expression of type A to an expression of type B.

In your example, x=x generally evaluates to true, unless x is an undefined value of sorts. In that case, it may evaluate to false or undefined, but that depends on the language/implementation at hand. For example, null == null is true in C but undefined === undefined is false in JavaScript.

You've never heard of dependent types? *tsk*tsk*tsk*

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

It is not about evaluating the expression. It's about obtaining another equivalent one.

That's what evaluation IS. It's a demonstration that two expressions are of equivalent value. EQUI. VALENT.

That's what the axiom of identity IS!

LHS ≡ RHS

You really need to re-examine what a Mathematics looks like from the lens of Univalent foundations; and from the intuition of a Computer Scientist.

[godelian]

There is a difference between evaluating an expression and trying to prove another statement from it.

Both are typically done by rewriting it.

So how does doing the same thing (rewriting) result in a "difference"?
Evaluating an expression is the same thing as providing the continuous transformation of the expression to normal form.
Proving f:A -> B is providing the continuous transformation of an expression of type A to an expression of type B.

In your example, x=x generally evaluates to true, unless x is an undefined value of sorts. In that case, it may evaluate to false or undefined, but that depends on the language/implementation at hand. For example, null == null is true in C but undefined === undefined is false in JavaScript.

You've never heard of dependent types? *tsk*tsk*tsk*

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

It is not about evaluating the expression. It's about obtaining another equivalent one.

That's what evaluation IS. It's a demonstration that two expressions are of equivalent value. EQUI. VALENT.

That's what the axiom of identity IS!

LHS ≡ RHS

You really need to re-examine what a Mathematics looks like from the lens of Univalent foundations; and from the intuition of a Computer Scientist.

There is a difference between evaluation/execution and proof steps.

During evaluation/execution, there is the expectation and requirement that all free variables will be bound to a value. There is no such expectation in a proof step.

- Evaluation: a=2, b=5 => a+b=7
- Proof step: (a+b)² => a²+2ab+b²

The goal of evaluation/execution is to bind all free variables to values and to compute the final value.
The goal of a proof is to perform all rewrite steps that are necessary for the final output to become the statement that was to be proven.

Now, for a specialized execution engine that is an automated prover, evaluating is indeed proving. This is, however, not generally the case for standard execution engines. By the way, automated provers generally do not work and are generally not able to prove arbitrary true statements.

[Skepdick]

There is a difference between evaluation/execution and proof steps.

Maybe from the lens of your philosophy. Not from the lens of mine.

During evaluation/execution, there is the expectation and requirement that all free variables will be bound to a value. There is no such expectation in a proof step.

Distinction without a difference. A step in the evaluation of an expression; or a step in the reduction of an expression; or a step in the construction of an object. A step is a step is a step. In the end - you get a sequence of steps. With a beginning. And an end.

The difference is merely that between partial and total evaluations.
Partial and total functions.

- Proof step: (a+b)² => a²+2ab+b²

Sounds like input and output to some evaluation function to me.
Input: (a+b)²
Output: a²+2ab+b²

The goal of evaluation/execution is to bind all free variables to values and to compute the final value.

The final value for ALL mathematical identities is "true". Axiomatically. By first law of logic: the law of identity.

The goal of a proof is to perform all rewrite steps that are necessary for the final output to become the statement that was to be proven.

This is an incoherent statement. What does "(a+b)² => a²+2ab+b²" prove exactly. You've simply evaluated "(a+b)²". The value of your evaluation is "a²+2ab+b²"

Now, for a specialized execution engine that is an automated prover, evaluating is indeed proving. This is, however, not generally the case for standard execution engines. By the way, automated provers generally do not work and are generally not able to prove arbitrary true statements.

It is generally the case. Once you view Mathematics from the lens of Univalent foundations.

That's literally what Univalence is about. Uni. Valent. One value. That ONE value is "true".

Identity is equivalent to equivalence.

[godelian]

The difference is merely that between partial and total evaluations.
Partial and total functions.

Examples of automated provers:

- Coq
- Isabelle
- Lean

These engines are not good automated provers but they are good proof assistants (for verifying proofs).

Examples of (standard) execution engines:

- nodejs
- Perl

There are hundreds of scripting engines. They are all able to evaluate expressions but out-of-the-box they are not theorem provers or proof assistants.

Concerning partial evaluation (and currying) this is supported in many evaluation engines, but certainly not always out of the box.

But then again, support for partial evaluation and currying is not enough to turn a scripting engine into a theorem prover or a proof assistant. It requires lots of extra logic. For example, the Vulcan library tries to implement a theorem prover in Javascript:

https://rmarcus.info/blog/2015/09/02/vulcan.html

Of course, like all theorem provers, it generally does not work, but it is undoubtedly still a great research project.

Concerning univalent foundations, it is looks like an interesting approach to create a type-theoretical foundation for mathematics, but it has currently not (yet) managed to replace set theory (or even arithmetic theory) as the dominant theory in mathematics. If you look at the state of the art in mathematics, I think it is premature to see univalence as more than an interesting research project.

[Skepdick]

The difference is merely that between partial and total evaluations.
Partial and total functions.

Examples of automated provers:

- Coq
- Isabelle
- Lean

These engines are not good automated provers but they are good proof assistants (for verifying proofs).

Examples of (standard) execution engines:

- nodejs
- Perl

ROFL. You've just listed a bunch of computer programs. Insisting that some are different to others. In some unspecified way.

Logic 101. Law of identity! A program is a program is a program. Proofs ARE programs!

https://en.wikipedia.org/wiki/Curry%E2% ... espondence

There are hundreds of scripting engines.

There are infinitely many programs! Some of them are scripting engines. Some of them are proof assistants. Some of them are string reversers.
Some of them are infinite loops that do nothing.

They are all able to evaluate expressions but out-of-the-box they are not theorem provers or proof assistants.

But ALL of them are proofs! Because proofs ARE programs.

But then again, support for partial evaluation and currying is not enough to turn a scripting engine into a theorem prover or a proof assistant. It requires lots of extra logic.

Non-sequitur. ALL programs are programs. This includes the programs you call "proof assistants".

Concerning univalent foundations, it is looks like an interesting approach to create a type-theoretical foundation for mathematics, but it has currently not (yet) managed to replace set theory (or even arithmetic theory) as the dominant theory in mathematics. If you look at the state of the art in mathematics, I think it is premature to see univalence as more than an interesting research project.

I don't give a shit about the status quo. I already live in the future. Computation is a priori Mathematics.

Through the lens of Univalence all Mathematics becomes nothing but some purpose-built programming language for manipulating symbols according to rules. Rule-following is for robots, not humans.

Rule-design is for humans.

[godelian]

But ALL of them are proofs! Because proofs ARE programs.

In the following blog post, this mathematician argues that the Curry-Howard correspondence is misunderstood as "proofs = programs".

https://xenaproject.wordpress.com/2019/ ... -programs/

What is true is that if you stick to constructive maths or intuitionistic logic or one of the flavours of maths where you’re not allowed to use the axiom of choice or the law of the excluded middle — in other words a version of maths which is unrecognisable to over 95% of pure mathematicians working in mathematics departments — then you might be in good shape.

What do you think about his view on the matter?

[Skepdick]

But ALL of them are proofs! Because proofs ARE programs.

In the following blog post, this mathematician argues that the Curry-Howard correspondence is misunderstood as "proofs = programs".

No. You are misunderstanding. What does the program called "=" DO?

What happens when you execute the program "=" with two parameters: "1+1" and "2" ?

What is true is that if you stick to constructive maths or intuitionistic logic or one of the flavours of maths where you’re not allowed to use the axiom of choice or the law of the excluded middle

I know! I explained this to you a while back. You missed it!

According to LEM either X is true or the negation of X is true. This is a disjunction!
The process of determining which disjunct is true is the Either monad!

Either X or not-X.

∀x: (x = x) ≡ Either(True,False). I trust you are familiar with the Either() monad.

in other words a version of maths which is unrecognisable to over 95% of pure mathematicians working in mathematics departments — then you might be in good shape. What do you think about his view on the matter?

What I think about it has already been covered.

The tradition of mathematics has gone under many names (geometry, astronomy, ballistics) in the past. In contemporary society it's now called "computer science"; whereas "Mathematician" can now be better understood as "astrologer".

[godelian]

According to LEM either X is true or the negation of X is true. This is a disjunction!
The process of determining which disjunct is true is the Either monad!
Either X or not-X.

What about his example?

Here’s an example of a proof which is not a program. The original proof that the class numbers of imaginary quadratic fields tended to infinity was the following rather extraordinary argument. First Landau showed that the theorem was true assuming that a certain generalisation of the Riemann Hypothesis was true, and then Heilbronn managed to show that the theorem was true assuming that this generalisation was false!

[Skepdick]

According to LEM either X is true or the negation of X is true. This is a disjunction!
The process of determining which disjunct is true is the Either monad!
Either X or not-X.

What about his example?

Here’s an example of a proof which is not a program. The original proof that the class numbers of imaginary quadratic fields tended to infinity was the following rather extraordinary argument. First Landau showed that the theorem was true assuming that a certain generalisation of the Riemann Hypothesis was true, and then Heilbronn managed to show that the theorem was true assuming that this generalisation was false!

You start with premises and end with conclusions?

Sounds like a program.

[Skepdick]

According to LEM either X is true or the negation of X is true. This is a disjunction!
The process of determining which disjunct is true is the Either monad!
Either X or not-X.

What about his example?

Here’s an example of a proof which is not a program. The original proof that the class numbers of imaginary quadratic fields tended to infinity was the following rather extraordinary argument. First Landau showed that the theorem was true assuming that a certain generalisation of the Riemann Hypothesis was true, and then Heilbronn managed to show that the theorem was true assuming that this generalisation was false!

You have some argument, some linguistic expression (passed to the computer in your head) which is evaluated as either true or false?

Sounds like a program.

[godelian]

You start with premises and end with conclusions?
Sounds like a program.

He also says the following:

The (simple) theorem (mentioned above) is just the axiom of choice in disguise, and the axiom of choice is about as non-constructive as you can get. Programs are algorithms. The axiom of choice says that we can do something when there is no algorithm.

He seems to say that what Curry-Howard defines as "proof" is just a subset of all proofs.
Well, that is how I interpret what he said.
(Not sure that this is what he means, actually)

[Skepdick]

You start with premises and end with conclusions?
Sounds like a program.

He also says the following:

The (simple) theorem (mentioned above) is just the axiom of choice in disguise, and the axiom of choice is about as non-constructive as you can get. Programs are algorithms. The axiom of choice says that we can do something when there is no algorithm.

The DOING of that SOMETHING IS some function. Even if you don't understand its implementation.

You know that it makes a choice between two options. HOW it makes a choice? Don't know!
But it does make a choice!

Such as the choice to map "x=x" to true OR false.

If you can't prove it - you axiomatize it.

He seems to say that what Curry-Howard defines as "proof" is just a subset of all proofs.
Well, that is how I interpret what he said.
(Not sure that this is what he means, actually)

He's mistaken, but this drags us down into the battleground of philosophy.

Just like philosophers can't agree or define what philosophy IS; so mathematicians can't agree or define what mathematics IS.
There needs not be any unifying property between any two conceptions of mathematics even.

There's mathematics with the axiom of choice. 95% of mathematicians and 100% of computer scientists practice it.
There is mathematics without the axiom of choice. 0% of Mathematicians and 100% of computer scientists practice it.

Both of those mathematics are mathematical.

Constructive mathematics doesn't prevent you from using choice, but it only constrains you to using those instances of it you have already proven.

The Lean proof assistant is not built using Univalent foudnations. So it's not cutting edge in terms of theoretical understanding.
It's trying to formalize classical (set theoretical) Mathematics. Not ALL mathematics.

[Skepdick]

The (simple) theorem (mentioned above) is just the axiom of choice in disguise, and the axiom of choice is about as non-constructive as you can get. Programs are algorithms. The axiom of choice says that we can do something when there is no algorithm.

Here's why he's wrong in a nutshell. "choice" is the name of the non-deterministic operator.

https://en.wikipedia.org/wiki/Nondeterm ... rogramming

And it's ultimately any function where the cardinality of the inputs is lower than the cardinality of the output. A choice function is a 1 to 2 relationship.

You canmap "x=x" to True, False or leave it undefined. Which one do you map it to? You can't compute this algorithmically - there is not enough information!

All of those options (functions!) exist. Which one you use in your Mathematics... that's just another choice.

That's synthesis.

[godelian]

The (simple) theorem (mentioned above) is just the axiom of choice in disguise, and the axiom of choice is about as non-constructive as you can get. Programs are algorithms. The axiom of choice says that we can do something when there is no algorithm.

Here's why he's wrong in a nutshell. "choice" is the name of the non-deterministic operator.

https://en.wikipedia.org/wiki/Nondeterm ... rogramming

And it's ultimately any function where the cardinality of the inputs is lower than the cardinality of the output. A choice function is a 1 to 2 relationship.

You canmap "x=x" to True, False or leave it undefined. Which one do you map it to? You can't compute this algorithmically - there is not enough information!

All of those options (functions!) exist. Which one you use in your Mathematics... that's just another choice.

That's synthesis.

I don't believe that the axiom of choice would necessarily be nondeterministic. It just says that the Cartesian product of nonempty infinite sets is nonempty.

https://en.m.wikipedia.org/wiki/Axiom_of_choice

It's automatically true for finite sets. AC extends it to infinite sets.

[Skepdick]

I don't believe that the axiom of choice would necessarily be nondeterministic. It just says that the Cartesian product of nonempty infinite sets is nonempty.

https://en.m.wikipedia.org/wiki/Axiom_of_choice

It's automatically true for finite sets. AC extends it to infinite sets.

And what about the Cartesian product of neither infinite nor finite, neither empty nor non-empty sets?
AC implies Excluded middle so it's constructively self-defeating: https://en.wikipedia.org/wiki/Diaconesc ... orem#Proof

Rice's theorem... Again. Semantic properties are undecidable. Unless they are encoded in your notation.

You have a set X.

The claim that the set is Empty requires a proof. It requires the proof Empty(X) ≡ ⊤ to terminate.
The claim that the set is non-empty requires a proof. It requires the proof NonEmpty(X) ≡ ⊤ to terminate.
Without excluded middle there's no a priori proof that Empty and NonEmpty are complementary. I mean - they could be, but you have to prove it!

The claim that the set is finite requires a proof. It requires the proof Finite(X) ≡ ⊤ to terminate.
The claim that the set is finite requires a proof. It requires the proof Infinite(X) ≡ ⊤ to terminate.
Without excluded middle there's no a priori proof that Finite and Infinite are complementary. I mean - they could be, but you have to prove it!

Mathematics becomes a weird place soon as Mathematicians stop pretending they are omniscient. Not all propositions are decidable.

Here's a paper that might upset your sensibilities: https://www.ams.org/journals/bull/2017- ... 1556-4.pdf