Content deleted Content added
→Friedman's grand conjecture: I suspect the actual non-EFA statement related to union-find is its non-constant lower bound, but this needs a source to confirm; remove until sourced |
→Definition: spacing for clarity |
||
Line 14:
The axioms of EFA are
*The axioms of [[Robinson arithmetic]] for 0, 1, +, ×, <
*The axioms for exponentiation: ''x''<sup>0</sup> = 1, ''x''<sup>''y''+1</sup> = ''x''<sup>''y''</sup> × ''x''.
*Induction for formulas all of whose quantifiers are bounded (but which may contain free variables).
| |||