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

Sandy Hodges sandyhodges at alamedanet.net
Wed Jul 9 15:58:41 EDT 2003

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

More information about the FOM mailing list