mathematics free of a blackboard (I. Gelfand and M. Gromov)

Wed Mar 10 21:54:34 EST 2021

Ignacio wrote:

> Your enhancement of the Pi calculus, as a first experiment to build a
> programming algebraic language worthy of our intuitive grasp, looks
> very important, I will look into it; but most of the work done in
> proof assistants, seems closer to the knowledge realm, than to the
> Reason sphere...

After watching M. Gromov's lectures "Probability, symmetry, linearity," I
changed my mind concerning proof assistants, including my prototype. Let's
begin with his quote:

We want mathematics free of blackboard, and it is impossible. We want to
> verify mathematics in computers but this depends on the rigid structure of
> computers and sometimes it fails. The great miracle of mathematics is
> there. [...] All traditional descriptions of mathematics, in my view, are
> greatly faulty, and this is the reason why there is no model of mathematics
> realized in computers, why there is no model of understanding languages,
> because we have an absolute wrong perception traditionally build in a
> development of numerical mathematics in logic distorted our perception of
> ourselves, of mathematics and of languages. It is as distorted as the Sun
> orbiting the Earth, [...] it is the wrong language, the wrong description.

M. Gromov, https://youtu.be/aJAQVletzdY?t=3880

My interpretation of this statement is that expressions are like coordinate
systems of a mathematical object. The same mathematical object can be
represented in several ways, using different expressions. A trivial example
is the number 2/3, which can be represented as 2/3, 4/6, 6/9, etc. One of
I. Gelfand's famous quotes is:

all of mathematics is some kind of representation theory

This Gelfand's quotation is mentioned in this book: Huang, J.S. Lectures on
Representation Theory; World Scientific: Singapore, 1999.

Now, let's apply this idea to pi-calculus. Two pi-expressions are
considered to represent the same process if and only if the structural
congruence relates them. Hence, a process is not an expression in
pi-calculus but a class of expressions corresponding to the structural
congruence quotient. Here is a reference to pi-calculus:

Milner, Robin. "Functions as processes." *International Colloquium on
Automata, Languages, and Programming*. Springer, Berlin, Heidelberg, 1990.
https://hal.inria.fr/inria-00075405/document

To define computation from mathematics is questionable from an
epistemological perspective since our direct experience is with computation
(including measurement as a computation in the physical world), not with
mathematics. Mathematics may be the result of abstraction in a computation.
A mathematical object may not be a primitive concept but a concept derived
from computation. The following argument seems to be a counterexample of
this claim:
from the premises:

1. Every language is an algebra
> 2. There are several languages with subgroups unrelated to computation

it can be possible to derive the conclusion

L. Not every algebra is entirely for computation

but rather than a counterexample, it is a positive example. Indeed, an
algebra that is unrelated to computation is an abstraction from an algebra
that is related to computation: this abstraction is obtained by ignoring
the property of being computational.

In this framework, it is rather natural to ask the following questions. I
provided the answers corresponding to the particular point of view that I
am following. Other researchers having a different point of view may
provide different answers.

Why mathematics is useful: The computational universe of computations at a
maximum level of sophistication is reduced by identifying different
expressions as representations of the same mathematical object. Mathematics
is a trick to make shortcuts in irreducible computations. The price to pay
for that is the loss of control over the representative of the mathematical
object, e.g., one representative from one irreducible computation may
transform itself into another representative to make a shortcut. Still, we
are not in the original computation anymore.

Why current proof assistants are a failure for everyday mathematics: In
current proof assistants, a considerable amount of computational effort is
used to change from one representation of a given mathematical object into
another. In real-life, mathematicians consider all the representations
simultaneously, i.e., in coordinate-free differential geometry.

Here is an example of the effort needed to change from one pi-expression to
another pi-expression in the formalization of pi-calculus in Isabelle/HOL:

Bengtson, Jesper, and Joachim Parrow. "Formalising the pi-calculus using
nominal logic." *International Conference on Foundations of Software
Science and Computational Structures*. Springer, Berlin, Heidelberg, 2007.
https://arxiv.org/pdf/0809.3960.pdf

How to develop the first practical proof assistant: Using a mathematical
model where the mathematical objects are treated in a way as independent as
possible to their representation.

The main difference between category theory and set theory is the
foundations of mathematics: Category theory is about the mathematical
objects, independently of the representations, whereas set theory is about
the representations of the mathematical object.

Kind regards,
José M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210310/f5fbbfe0/attachment-0001.html>