Alex Nelson<p>What is a "structure" in Mizar?</p><p>This was always one of the most confusing things to me when I first got started with <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Mizar</span></a> since the answer requires a little bit of Model Theory, which isn't adequately taught in the US to "generic Mathematicians".</p><p>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 <a href="https://mathstodon.xyz/tags/Isabelle" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Isabelle</span></a> as the Metatheory (as done in the Isabelle/Mizar project).</p><p>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!</p><p><a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistant" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProofAssistant</span></a> <a href="https://mathstodon.xyz/tags/ModelTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ModelTheory</span></a> <a href="https://mathstodon.xyz/tags/Model_Theory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Model_Theory</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Mathematics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Mathematics</span></a></p><p><a href="https://thmprover.wordpress.com/2024/10/04/what-is-a-structure-in-mizar/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">thmprover.wordpress.com/2024/1</span><span class="invisible">0/04/what-is-a-structure-in-mizar/</span></a></p>