[drdeca]

I don't understand. If I say Define L to be a thing of type J. Where j is a J, define T j L to be j Define T L j to be the same as j. Where j is a J define W j to be a J. And where a and b are both J, define T a W b to be the same as T W a b Define a K to be a J and either be L or W L or where k can be determined to be a K, W k. I think these definitions are sufficient to show that if a and b are both a K then T a b can be shown to be the same as T b a. ( though this does not neccisarily make addition over the natural numbers because I did not include the requirement that if a and b are both a K and are not the same then W a must not be the same as W b)

And while I'm not totally sure about the definition of K ( specifically the whether something can be shown part), I think this would be based just on definitions, without really any axioms?

Although I suppose it is possible that I included an axiom and just wrote "Define" before it.

(tangent: I suppose one could say "define a system with the following axioms" and then make a proof about that system, and claim that it was a proof by definition?)

Maybe I don't really understand what a priori really means (this seems fairly likely) but I don't think definitions are considered a priori?

[abruzzi]

Definitions can absolutely be a priori. Think of the definition of a triangle, some thing like "a closed geometrical shape with three sides." There is nothing about observation of the world that will tell you that this is or isn't true. It is true by definition. Then all closed three sided shapes are triangles, by definition. Then you can start building all sorts of proofs from that, and a few other definitions. You get to the Pythagorean theorem, trigonometry, and off you go, without ever needing anything other than the ideas and definitions.