<div dir="ltr">Hi Rob,<div><br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div>I take it that for you only equality and choice are primitive.</div></div></div></blockquote><div><br></div><div>That is correct.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div>ETA_AX and SELECT_AX only use outermost universal quantifier, so you could just have stripped that off, giving equivalent readable axioms with free variables.</div></div></div></blockquote>
<div><br></div><div>Another OpenTheory convention is that theorems don't have any free variables, so I was trying to find a solution that satisfied this constraint (though doing so meant throwing out readability).</div>
<div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div>
<div>But I don't really understand the problem you are trying to guard against. In addition to the axiom of infinity, the package axiom-infinity inputs the logical connectives and the quantifiers and has assumptions that say these things and injective and surjective have their standard meaning. You use the quantifiers and logical connectives in the assumptions about injective and surjective, so why does it cause a problem to use them in the axiom of infinity?</div>
</div></div></div></blockquote><div><br></div><div>The assumptions collectively enforce that the standard definition of basic logical constants are used. Consider the following two assumptions of the axiom-infinity theory package:</div>
<div><br></div><div><div>  |- (!) = \p. p = \x. T</div><div>  |- !f. surjective f <=> !y. ?x. y = f x<br></div></div><div><br></div><div>The first assumption enforces that universal quantification has the standard definition, so it can't cause problems to use universal quantification in the definition of surjectivity.</div>
<div><br></div><div>The real problem I was trying to solve is recognizing the 3 standard axioms so that I don't falsely report them as "unsatisfied assumptions" of a theory. This is much easier if the standard axioms are expressed solely in terms of primitive constants and type operators, so that the tool doesn't have to check any definitions. The little axiom-* theories translate from the primitive versions of the axioms to readable versions, assuming that the standard definitions are being used. And note that the opentheory tool reports all their assumptions as being satisfied, even though the primitive versions of the axioms are not satisfied by any required theories but are recognized as standard axioms.</div>
<div><br></div><div>I was thinking of changing the OpenTheory pretty printer so that the primitive versions of the axioms would simply print as "AXIOM OF INFINITY" instead of the monster term, which would perhaps avoid some future confusion. I'm also open to better ways of booting up the OpenTheory standard theory library, if you have any ideas.</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div></div></div></div></div>