[isabelle] The Arithmetic Site in Isabelle/CTT (was: Isabelle/HoTT)

[José Manuel Rodriguez Caballero]

This is just a concrete example of a mathematical object which may be
natural to formalize in Isabelle/CTT, but which is not naturally
formalizable in HOL.

Jacques Tits remarked that the group of permutations of n elements was like
the multiplicative group of nonsingular matrices. So, he conjectured that
permutations are like matrices over a hypothetical finite field having
exactly one element: https://ncatlab.org/nlab/show/field+with+one+element

It can be proved in HOL that such a field with exactly one element does not
exist (exercise). Nevertheless, Alain Connes and Caterina Consani defined a
structure, named The Arithmetic Site, which realizes some of the expected
properties of Tits hypothetical field. The problem is that the Arithmetic
Site is a Grothendieck topos in which the law of excluded middle is not
taken as universal. So, to formalize the Arithmetic Site, Isabelle needs to
give up the law of excluded middle like in Isabelle/CTT. Nevertheless, I am
not sure if the type theory in Isabelle/CTT is the same as the internal
logic of The Arithmetic Site: https://ncatlab.org/nlab/show/internal+logic

According to Connes, the Arithmetic Site is the key to go from the famous
result that Andre Weil conjectured when he was in prison to the Riemann
Hypothesis. Notice that Weil conjectures are about the field with q
elements, where q is a prime power, where the Riemann Hypothesis is the
limit when q goes to 1 (abuse of language).

Reference: Geometry of the Arithmetic Site (Connes and Consani)
Link to the paper: http://www.alainconnes.org/docs/geomarithmeticsite.pdf
Video:

Kind Regards,
Jose M.

[Lawrence Paulson]

CTT is a fragment of Martin-Löf's Type Theory with extensional equality. See e.g.

http://www.cse.chalmers.se/research/group/logic/book/book.pdf <http://www.cse.chalmers.se/research/group/logic/book/book.pdf>

I can’t recall whether universes are covered, but maybe you don’t need them.

Larry

Post by José Manuel Rodriguez Caballero
This is just a concrete example of a mathematical object which may be
natural to formalize in Isabelle/CTT, but which is not naturally
formalizable in HOL.
Jacques Tits remarked that the group of permutations of n elements was like
the multiplicative group of nonsingular matrices. So, he conjectured that
permutations are like matrices over a hypothetical finite field having
exactly one element: https://ncatlab.org/nlab/show/field+with+one+element <https://ncatlab.org/nlab/show/field+with+one+element>
It can be proved in HOL that such a field with exactly one element does not
exist (exercise). Nevertheless, Alain Connes and Caterina Consani defined a
structure, named The Arithmetic Site, which realizes some of the expected
properties of Tits hypothetical field. The problem is that the Arithmetic
Site is a Grothendieck topos in which the law of excluded middle is not
taken as universal. So, to formalize the Arithmetic Site, Isabelle needs to
give up the law of excluded middle like in Isabelle/CTT. Nevertheless, I am
not sure if the type theory in Isabelle/CTT is the same as the internal
logic of The Arithmetic Site: https://ncatlab.org/nlab/show/internal+logic <https://ncatlab.org/nlab/show/internal+logic>