What is a "structure" in Mizar?

This was always one of the most confusing things to me when I first got started with #Mizar since the answer requires a little bit of Model Theory, which isn't adequately taught in the US to "generic Mathematicians".

The answer is surprisingly deep yet simple: it's "just" a finite partial map in the Metatheory. This can be made precise using something like #Isabelle as the Metatheory (as done in the Isabelle/Mizar project).

We can also use a finite set of "attribute"-value pairs, which is called "first-class aggregates" (or "first-class structures") since they're defined like any other notion in Mizar, without special metatheoretic considerations. And they're useful for doing graph theory!

#Mizar #ProofAssistant #ModelTheory #Model_Theory #Logic #Mathematics

https://thmprover.wordpress.com/2024/10/04/what-is-a-structure-in-mizar/