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

[Harvey Friedman]

Reply to Hodges 11:12AM 7/9/03, and 12:58PM 7/9/03.

Fri, 20 Jun 2003 17:51:09 -0400

>
>I presume he intended a "natural deduction" system, as he did not
>provide for any propositional or predicate variables.

See my posting of 6/20/03 7:51PM.

I was not concerned with that level of detail. Just use any complete 
system of axioms and rules for predicate calculus based on the 
relevant language.

The question of just how to formalize mathematical proofs, and for 
what purpose one is formalizing mathematical proofs, is an entirely 
orthogonal issue.

>
>The claim that everything is either a set, a pair, or a real number, is
>not I think appropriate as an axiom for such a system.


>However, the claim that pairs are not sets and sets are not pairs, seems
>reasonable.  And I have no strong objection to the claim that real
>numbers are not sets.

This matter was already explicitly addressed in my posting of 6/20/03 
7:51PM. There I proposed removing the axiom you are complaining about.

>
>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.
>

In my formulation, integers are defined very naturally as follows. x 
is an integer if and only if x lies in a subgroup of the reals that 
contains 1 and is disjoint from (0,1). Under this definition, 
induction is derivable. This is because of the least upper bound 
axiom. (Provably, there is exactly one such subgroup).

So there is no need for any axiom of induction.

Harvey Friedman