[FOM] Rules and axioms for Harvey Friedman's system.

[Sandy Hodges]

I left out an axiom:

(\/ r) ( 0 e r &
         (\/ n, m, p) ( n e r & +(n, 1, m) & (p < m V p = m) => p e r)
=>
         (\/ n) (0 < n => n e r ) )
         ; Induction

Friedman did not include induction; Taylor suggested it.   I don't see
how to avoid having it as an axiom.   The form given here is based on
the fact that the system does not have Integer as a fundamental
concept.   It seemed more elegant to use only undefined symbols in the
axioms; a statement of induction in the usual integer-based form, would
be very long, if only the undefined symbols were used.

------- -- ---- - --- -- --------- -----
Sandy Hodges / Alameda,  California,   USA
Remove THESE WORDS from SandyTHESEhodges at AlamedaWORDSnet.net
Note: This is a new address as of 20 June 2003