A comment I tried to send

comment.txt

Sniffnoy <a href="http://www.scottaaronson.com/blog/?p=2741#comment-1099870">#59</a>:

(I lost the first version of this reply)

<blockquote>Would it be possible to shrink it further by using collection instead of replacement, since collection is simpler to state?</blockquote>

Maybe?  The Metamath version of the <a href="http://us.metamath.org/mpegif/cp.html">collection principle</a> is shorter than its <a href="http://us.metamath.org/mpegif/ax-rep.html">axiom of replacement</a>; but you'll notice we don't have Separation in our list, because it can be derived from Replacement, but unless I'm missing something you can't do that with Collection and we'd need to re-add Separation.

So far I've been focusing on compiler improvements.  I'd hoped to get down to 1000 states with no substantive changes to zf.nql itself (as I told Scott in an email earlier), but I greatly underestimated the state budget for jumps, and I'm already hitting diminishing returns on optimizations.  Current scores are 432 states for Goldbach, 1008 for RH, and 1929 for Con(ZF).  Only one of these reaches <a href="http://www.scottaaronson.com/blog/?p=2725#comment-1084762">Scott's objectives</a>.

<blockquote>Or is the metamath version of replacement already actually collection?</blockquote>

It's not.

<blockquote>I find the way metamath writes its axioms to be too hard to read; I honestly can’t tell.</blockquote>

Are you talking about the RPN garbage in zf.nql or the infix version in the actual database and the website?  If the former, I completely agree, if the latter I'm curious what changes you'd make.

<blockquote>I was also wondering whether going for NBG might be shorter than ZFC, since it’s finitely axiomatizable, but it looks like the way that metamath handles axiom schemas means those aren’t actually too horrible and so doing this might actually make things worse?</blockquote>

Yeah, I don't think that'd help — one scheme is simpler than N (10?) Gödel operators.  This is a systems perspective: we already need schemes to support propositional and predicate axioms in a Hilbert-style formalism, so we might as well keep using them for set theory.

<blockquote>Also, would you mind explaining just why you re-added foundation?</blockquote>

Metamath's basic axiom of infinity (<a href="http://us.metamath.org/mpegif/ax-inf.html">ax-inf</a>) asserts the existence of a non-empty set y such that for each element z, y contains another element that con tains z.  In other words, y has no rank-maximal element.  If you have Foundation, that forces y to be infinite, which means it has subsets of every finite cardinality, which gives you omega by replacement.  If you don't have Foundation … y could just be a Quine atom and you've achieved nothing.

There's another version (<a href="http://us.metamath.org/mpegif/ax-inf2.html">ax-inf2</a>) which directly asserts the existence of (a superset of) omega and stands without Foundation; we can try that later.

<blockquote>Seeing as there’s no link to the list discussion. </blockquote>

I linked the Metamath thread <a href="http://www.scottaaronson.com/blog/?p=2725#comment-1085923">on the previous Shtetl-Optimized thread</a>.

Norm called out my lack of Foundation <a href="https://groups.google.com/d/msg/metamath/OumBq83Ksqs/FogyOlLIBwAJ">here</a>.