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

[Sandy Hodges]

I wondered what the rules and axioms of the system Harvey Friedman
proposed would look like.  Here is his proposal as quoted by Bill
Taylor:
>>>>>>>>>>>
We have variables of only one sort, but with the following 7 nonlogical
symbols (in addition to the logical symbols not, and, or, implies, iff,
forall, therexists, =).

Sets. (Unary predicate symbol).
Membership. (Binary relation symbol).
Ordered pairing (Binary function symbol).
Real numbers. (Unary predicate symbol).
0,1. (Constant symbols).
<. (Binary relation symbol for ordering of reals).
+. (Ternary relation symbol for addition on reals).

1. Everything is exactly one of: a set, an ordered pair, or a real
number,
2. Only sets can have an element.
3. If two sets have the same elements then they are equal.
4. <x,y> = <z,w> iff (x = z and y = x).
5. 0,1 are distinct real numbers.
6. +(x,y,z) implies x,y,z are reals.
7. x < y implies x,y are reals.
8. Usual axioms that reals are an ordered group with 0,1,+,<.
9. Every nonempty set of reals bounded above has a least upper bound.
10. The set of all reals numbers exists.
11. Pairing, union, power set, separation, replacement, foundation,
choice.

Rationals, integers, natural numbers, are all defined as certain real
numbers. Functions are sets of ordered pairs.
<<<<<<<<<<<<<

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

I found it easier, as well as more in accordance with usage, to adopt
the null set symbol (/), rather than a unary predicate "Set(x)."
Thus, to say some x is a set, one can say x = (/) V (E y) (y e x).

I guessed that "+(x, y, z)" means x + y = z , rather than x = y + z.

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.   For example,
suppose you wanted to do some geometry; something should be a theorem of
some geometry system only if it follows from the axioms of that
system.    Suppose EA is the conjunction of Euclid's axioms.   D is a
theorem of Euclidean geometry if, and only if, (EA => D) is a theorem of
the underlying logic.   But if we have an axiom in the underlying logic
that says that everything is a set, a pair, or a real number, it follows
that a point is a set, a pair, or a real number.   And this is not the
case in Euclidean geometry.

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.

Here is the list of rules.   (/) is the null set, e is the element-of
relation.   \/ is forall, E is therexists.   V is OR.

   deduction: B |- A => B, when B deduced from assumption A.  The
conclusion gets, as used assumptions, all the assumptions used by
premise B except for assumption A.
   \/-intro: A(x) |- (\/ y) A(y) ; the assumptions used to conclude
A(x), must contain no unbound use of variable x.
   modus ponens: A => B, A |- B
   &-intro: A, B |- A & B
   &-commute:  A & B |- B & A
   &-elim:  A & B | B
   V-intro: A |- A V B
   V-commute: A V B |- B V A
   V-elim: A V B, A => H, B => H |- H
   <=>-intro: A=>B, B=>A |- A<=>B
   <=>-commute:  A<=>B |- B<=>A
   <=>-elim: A<=>B |- B=>A
   ~-intro: A => ~(B V ~B) |- ~A
   ~~-elim: ~~A |- A
   \/-elim: (\/ x) A(x) |- A(T)
   E-intro: A(T) |- (E x) A(x) ; not all occurrences of T in A(T) need
be replaced.
   E-dist: (\/ x) (A(x) => B(x) ) |- (E y) A(y) => (E z) B(z)
   \/-group: |- (\/ a) (\/ b) ... (\/ c) A(a, b, ..., c) <=> (\/ c) (\/
b, a) A(a, b, ..., c)
   \/-swap: |- (\/ a) A(a) <=> (\/ b) A(b)
   E-group: |- (E a) (E b) ... (E c) A(a, b, ..., c) <=> (E c) (E b, a)
A(a, b, ..., c)
   E-swap: |- (E a) A(a) <=> (E b) A(b)
   Leibniz: A(T), T = R |- A(R) ; not all occurrences of T in A(T) need
be replaced.
   separation: |- (\/ d) (E s) (\/ m) ( m e s <=> m e d & A(m) )
   replacement: (\/ x)(E y)(\/ z) (z = y <=> A(x, z) ) |-
         (\/ u)(E v)(\/ z) ( z e v <=> (E x) (x e u & A(x, z) ) )

Except as noted, when a variable is replaced all unbound occurrences of
it must be replaced.   A variable put in, as a replacement, must not
become bound, and a term put in, must not have any variables in it that
become bound.  For every rule except Deduction, the conclusion gets, as
used assumptions, all the assumptions used by the premises.

Here are the axioms (the name of each axiom follows it).

(\/ a) (a = a)
          ; Identity is reflexive
(\/ y) ~( y e (/) )
          ; Null set has no elements
(\/ s, t) ( (E x) ( x e s ) & (\/ x) ( x e s <=> x e t ) => s = t )
         ; Extensionality
(\/ x, y) (E s) (\/ z) ( z e s <=> z = x V z = y )
         ; Pairing
(\/ s) (E u) (\/ x) ( x e u <=> (E m) ( x e m &  m e s ) )
         ; Union
(\/ s) (E p) (\/ x) ( x e p <=>
    ( (\/ n) ( n e x => n e s ) & (E n) ( n e x ) ) V x = (/) )
         ; Powerset
(\/ a, b, c, d) ( <a, b> = <c, d> <=> a = c & b = d )
         ; Contents determine pairs
(\/ s) ( s = (/) V (E m) (m e s) => ~(E a, b) ( s = <a, b> ) )
         ; Sets are not pairs
0 < 1
         ; Zero is less than one
(\/ a, b, c) ( a < b & b < c => a < c )
         ; Less than is transitive
(\/ a, b) ( a < b => ~(a = b) & ~(b < a) )
         ; Trichotomy
(\/ a, b) ( a < b => (E c) ( a < c & c < b ) )
         ; Reals are continuous
(E s) (\/ x) ( x e s <=> +(x, 0, x) )
         ; There is a set of reals
(\/ a, b) ( a < b => +(a, 0, a) & +(b, 0, b) )
        ; Only reals compare
(\/ a, b) (+(a, 0, a) & +(b, 0, b) =>
                 a < b V a = b V b < a )
        ; Tripotency
(\/ y) ( (E x, u) ( +(y, x, u) V +(x, y, u) V +(x, u, y) ) =>
             +(y, 0, y) )
         ; Only reals in sums
(\/ b, c) ( +(b, 0, b) & +(c, 0, c) =>
       (E a)(\/ x) ( x = a <=> +(b, c, x) ) )
         ; Sums exist uniquely
(\/ a, b, c) ( +(a, b, c) => +(b, a, c) )
         ; Addition is commutative
(\/ a, b, c, t) ( (E d) ( +(a, b, d) & +(d, c, t) ) <=>
        (E d) ( +(a, d, t) & +(b, c, d) ) )
         ; Addition is associative
(\/ a, b, c, d, e) (+(a, b, c) & +(a, d, e) & b < d => c < e )
         ; Addition is increasing
(\/ a) (+(a, 0, a) => (E b) +(a, b, 0) )
         ; negatives exist
(\/ s) ( (E m) ( m e s ) & (E b) (\/ m) ( m e s => m < b ) =>
           (E k) ( (\/ m) ( m e s => m < k V m = k ) &
                   (\/ b) ( (\/ m) ( m e s => m < b ) =>
                       k = b V b < k ) ) )
         ; Bounded sets have least bounds

These following axioms, could perhaps be regarded as postulates rather
than axioms:

(\/ r) ( +(r, 0, r) =>
          ~(r = (/) ) & (\/ x) ~(x e r) & ~(E a, b) ( r = <a, b> ) )
         ; Reals are neither sets nor pairs
(E x) ( (/) e x & (\/ y) (y e x => Union({y,{y}}) e x )
         ; Infinity (not needed, I think, since the reals are an
infinite set)

   ; Axiom of choice ( content omitted due to laziness )
(\/ x) ( ~(x = (/) ) => (E y) ( y e x & (\/ z)( z e x => ~(z e y) ) )
     ; Regularity

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