[FOM] quantum foundations of mathematics

José Manuel Rodriguez Caballero josephcmac at gmail.com
Tue Sep 11 05:53:25 EDT 2018

> Sam wrote:
> Finally, it seems your notion of ?genuine vs CCS? includes some kind of
> implicit strict finitism (and temporal/physical dimension): for a given
> theorem to be implemented in a
> proof assistant, there have to be ?good? definitions that result in a
> proof that can be run on a physical machine (in the here and now).

The fundamental presuppositions in Foundations of Mathematics is the
following: each time we check a proof Y of Theorem X, we always conclude
that the proof Y is either fine or it contains a mistake.

This principle is similar to the fundamental presupposition of classical
physics: each time we repeat an experiment with identical initial
conditions, we will obtain the same results. In quantum physics this is not
longer true. Because reality is ultimately quantum, there is certain
probability that checking the proof Y of theorem X, either by hand or using
a proof assistant, we will conclude that the proof is fine sometimes and
that it contains a mistake other times. Indeed, both in the human brain and
in a computer, mistakes may happens because of quantum fluctuations.

So, ordinary proof assistants are just an approximate way to formally
verify mathematics, which is much more precise than checking by hand, but
to formally verify mathematics (formalized in ZFC) with absolute accuracy
it is physically impossible. This is because in ZFC any meaningful
statement is either true or false, whereas in the quantum world everything
is based in superpositions.

A reconciliation between the foundations of mathematics and the physical
reality could be to reformulate mathematics in a quantum way, where each
proposition will be a linear combination of true and false rather than
being either true or false. So, the corresponding proof assistant should be
implemented in a quantum computer. This is just a theoretical solution, for
practical purposes, ordinary computers and ordinary proof assistants are

Kind Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180911/8b7016f2/attachment.html>

More information about the FOM mailing list