I feel like this is an instance of a larger question:

When might it be nice to work with an axiomatic description of a theory rather than an explicit construction?

This comes up all the time, e.g. in topology, cohomology, algebra (e.g. abstract groups rather than permutation groups), and more recently with homotopy type theory.

Some possible answers to this question:

• Working with axioms provides the right level of abstraction: proofs often become much easier since you're left with only the essential facts, rather than the forest of theorems being obscured by the trees of the particular construction.

In NSA, you're trying to justify the algebraic manipulations done by Newton or Euler on paper: but these are naturally stated in the abstract language of calculus, and involving ultrafilters just complicates matters. Of course you can just re-derive all the required inference rules, but the point is that the logical rules themselves are a useful conceptual framework.

• Having an axiomatic framework opens the door to unexpected realizations of a concept. This is of course easy to see for a concept with many different realizations like groups, where things as disparate as field automorphisms, toplogical braids and integers all have a group structure, but can be more surprising for things like, e.g. cohomology or real closed fields, where there are only few immediately apparent models. It's probably useful to note that the concept of group itself has turned out to be much more general than envisioned originally. Once you have an axiom system, it becomes very easy to try to find "non-standard" models by various techniques (including ultrafilters, of course), or even dropping axioms, as in the famous "extra-ordinary" cohomology theories. One might even suggest that NSA itself is the result of finding non-standard models of an axiomatic theory of real numbers. It's not surprising therefore that people working with NSA might be more amenable to the advantages of the axiomatic approach.

I feel like this is an instance of a larger question:

When might it be nice to work with an axiomatic description of a theory rather than an explicit construction?

This comes up all the time, e.g. in topology, cohomology, algebra (e.g. abstract groups rather than permutation groups), and more recently with homotopy type theory.

Some possible answers to this question:

• Working with axioms provides the right level of abstraction: proofs often become much easier since you're left with only the essential facts, rather than the forest of theorems being obscured by the trees of the particular construction.

  In NSA, you're trying to justify the algebraic manipulations done by Newton or Euler on paper: but these are naturally stated in the abstract language of calculus, and involving ultrafilters just complicates matters. Of course you can just re-derive all the required inference rules, but the point is that the logical rules themselves are a useful conceptual framework.

• Having an axiomatic framework opens the door to unexpected realizations of a concept. This is of course easy to see for a concept with many different realizations like groups, where things as disparate as field automorphisms, toplogical braids and integers all have a group structure, but can be more surprising for things like, e.g. cohomology or real closed fields, where there are only few immediately apparent models. It's probably useful to note that the concept of group itself has turned out to be much more general than envisioned originally. Once you have an axiom system, it becomes very easy to try to find "non-standard" models by various techniques (including ultrafilters, of course), or even dropping axioms, as in the famous "extra-ordinary" cohomology theories. One might even suggest that NSA itself is the result of finding non-standard models of an axiomatic theory of real numbers. It's not surprising therefore that people working with NSA might be more amenable to the advantages of the axiomatic approach.

I feel like this is an instance of a larger question:

When might it be nice to work with an axiomatic description of a theory rather than an explicit construction?

This comes up all the time, e.g. in topology, cohomology, algebra (e.g. abstract groups rather than permutation groups), and more recently with homotopy type theory.

Some possible answers to this question:

• Working with axioms provides the right level of abstraction: proofs often become much easier since you're left with only the essential facts, rather than the forest of theorems being obscured by the trees of the particular construction.

In NSA, you're trying to justify the algebraic manipulations done by Newton or Euler on paper: but these are naturally stated in the abstract language of calculus, and involving ultrafilters just complicates matters. Of course you can just re-derive all the required inference rules, but the point is that the logical rules themselves are a useful conceptual framework.

• Having an axiomatic framework opens the door to unexpected realizations of a concept. This is of course easy to see for a concept with many different realizations like groups, where things as disparate as field automorphisms, toplogical braids and integers all have a group structure, but can be more surprising for things like, e.g. cohomology or real closed fields, where there are only few immediately apparent models. It's probably useful to note that the concept of group itself has turned out to be much more general than envisioned originally. Once you have an axiom system, it becomes very easy to try to find "non-standard" models by various techniques (including ultrafilters, of course), or even dropping axioms, as in the famous "extra-ordinary" cohomology theories. One might even suggest that NST itself is the result of finding non-standard models of an axiomatic theory of real numbers. It's not surprising therefore that people working with NST might be more amenable to the advantages of the axiomatic approach.

I feel like this is an instance of a larger question:

When might it be nice to work with an axiomatic description of a theory rather than an explicit construction?

This comes up all the time, e.g. in topology, cohomology, algebra (e.g. abstract groups rather than permutation groups), and more recently with homotopy type theory.

Some possible answers to this question:

• Working with axioms provides the right level of abstraction: proofs often become much easier since you're left with only the essential facts, rather than the forest of theorems being obscured by the trees of the particular construction.

In NSA, you're trying to justify the algebraic manipulations done by Newton or Euler on paper: but these are naturally stated in the abstract language of calculus, and involving ultrafilters just complicates matters. Of course you can just re-derive all the required inference rules, but the point is that the logical rules themselves are a useful conceptual framework.

• Having an axiomatic framework opens the door to unexpected realizations of a concept. This is of course easy to see for a concept with many different realizations like groups, where things as disparate as field automorphisms, toplogical braids and integers all have a group structure, but can be more surprising for things like, e.g. cohomology or real closed fields, where there are only few immediately apparent models. It's probably useful to note that the concept of group itself has turned out to be much more general than envisioned originally. Once you have an axiom system, it becomes very easy to try to find "non-standard" models by various techniques (including ultrafilters, of course), or even dropping axioms, as in the famous "extra-ordinary" cohomology theories. One might even suggest that NSA itself is the result of finding non-standard models of an axiomatic theory of real numbers. It's not surprising therefore that people working with NSA might be more amenable to the advantages of the axiomatic approach.