Alex Nelson<p>What is a &quot;structure&quot; 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="tag">#<span>Mizar</span></a> since the answer requires a little bit of Model Theory, which isn&#39;t adequately taught in the US to &quot;generic Mathematicians&quot;.</p><p>The answer is surprisingly deep yet simple: it&#39;s &quot;just&quot; 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="tag">#<span>Isabelle</span></a> as the Metatheory (as done in the Isabelle/Mizar project).</p><p>We can also use a finite set of &quot;attribute&quot;-value pairs, which is called &quot;first-class aggregates&quot; (or &quot;first-class structures&quot;) since they&#39;re defined like any other notion in Mizar, without special metatheoretic considerations. And they&#39;re useful for doing graph theory!</p><p><a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="tag">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/ProofAssistant" class="mention hashtag" rel="tag">#<span>ProofAssistant</span></a> <a href="https://mathstodon.xyz/tags/ModelTheory" class="mention hashtag" rel="tag">#<span>ModelTheory</span></a> <a href="https://mathstodon.xyz/tags/Model_Theory" class="mention hashtag" rel="tag">#<span>Model_Theory</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="tag">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Mathematics" class="mention hashtag" rel="tag">#<span>Mathematics</span></a></p><p><a href="https://thmprover.wordpress.com/2024/10/04/what-is-a-structure-in-mizar/" target="_blank" rel="nofollow noopener noreferrer" translate="no"><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>