FOM: HOL is not stronger than FOL

[Vedasystem@aol.com]

In a message dated 3/20/99 6:40:22 PM Eastern Standard Time, with the subject 
"HOL is stronger than FOL" Till Mossakowski writes:

<< Thus, in principle, HOL can be reduced to FOL,
 but at the price of getting more cumbersome
 axiom systems and proofs.
  >>

Adding to FOL Hilbert's epsilon-symbol greatly increases the expressive power
(in a practical sense) of FOL (as was shown for example by Bourbaki - their
tractatus heavily uses the epsilon-symbol).
Lambda-notation can be expressed via the epsilon-symbol. 
A rather small modification of first-order logic by adding new syntactic
constructs for definitions can convert FOL to a useful practical tool - now I
am writing a paper describing such a modification - an abstract of the paper,
contents and an introductory section are below.  

Victor Makarov
EMD
Software Consultant
Brooklyn, New York 
------------------------------------------------------------------------------
----------------------------------------------------
                         Predicate Logic with Definitions

                                 Victor Makarov

                                         EMD
                               vedasystem at aol.com

Abstract

Predicate Logic with Definitions (PLD or D-logic) is a modification of first-
order logic intended mostly for practical formalization of mathematics. The
main syntactic constructs of D-logic are terms, formulas and definitions. A
definition is a definition of variables, a definition of constants, or a
composite definition (D-logic has also abbreviation definitions called
abbreviations). Definitions of constants in D-logic are similar to schemes in
the Z specification language. Definitions can be used inside terms and
formulas. This possibility alleviates introducing new quantifier-like names.
Some theorems of D-logic are proved and basics of the ZFC set theory are
expressed in D-logic. 

Contents

1. Introduction
2. Related work
3. From first-order logic to D - logic
4. A review of D-logic
      4.1 Abbreviations
      4.2 Definitions of constants
      4.3 Definitions of variables
      4.4 Composite definitions
      4.5 Terms
      4.6 Formulas
      4.7 Axioms and inference rules
5. D-languages
6. D-theories
7. Hilbert's  epsilon -symbol
8. Some theorems of D-logic
9. Bounded quantification
10. An important inference rule
11. ZFC set theory as a D-theory
12. Relations and functions



3. From first-order logic to D - logic

The symbols used in the language of first-order logic (we follow basically to
[Davis 93] and [Shoenfield 73]) are usually divided to the following classes:

1. Logical symbols:  ~ (negation), -> (implication), & (conjunction), v
(disjunction), == (equivalence), A(universal quantifier), E(existential
quantifier).
2. Constant symbols.
3. Function symbols.
4. Relation symbols.

For each function and relation symbol, a natural number k, called arity, must
be assigned. The notions of terms and formulas can then be defined [Davis 93].
Fixing the sets of constant, function and relation symbols we receive a
concrete first-order language - for instance, the language of the ZFC set
theory.  
   Let us consider the formulas of the form AxP and ExP, where x is a
variable, P is a formula. Let us slightly change the syntax of such formulas
and write A(x|P) and E(x|P), respectively, where '|' is a punctuation symbol.
Let us call (in this section) the expression x|P as a definition of variables
(actually, a definition of variables in D-logic can contain many variables -
see below).
   An immediate benefit of this approach is the following: it is easier to
introduce new "quantifier-like" names. To show it, let us generalize the
notion of arity in the following way. Let us call a g-arity (or generalized
arity) any finite nonempty sequence of the letters F, T, D (from Formula,
Term, Definition). We assign a g-arity to each symbol as follows: 
1.1 Unary logical symbols (~): FF.
1.2 Binary logical symbols (&, v, ->, == ): FFF.
1.3 Quantifiers (A,E): DF.
2. Constant and variable symbols: T.
3. Function symbols of arity k: the sequence of k+1 letters T.
4. Relation symbols of arity k: TkF (Tk is the sequence of k letters T). For
instance, the g-arity TTF will be assigned to the symbols "=" (equality) and
"in" (is a member of).

   Now it is obvious that for introducing, for example, Hilbert's epsilon-
symbol or the symbol lambda(used in lambda-notation), it is sufficient to
assign to the symbols epsilon and lambda the g-arities DT and DTT respectively
(and, of course, provide defining axioms for the symbols). Note that it is
possible to introduce symbols of g-arities DD, DDD or DFD. Such symbols can be
used for denoting operations on definitions and constructing composite
definitions.  
 For example, if d is a definition of variables of the form (x|P),R is a
formula then the negation of the definition d is the definition (x|~P)and d &
R is the definition (x|P&R). For instance, the following formulas are theorems
of D-logic:

~~A[d] == E[~d]
~~E[d] == A[~d]

Definitions of constants have the form def[c1, ..., ck|P] (i.e.  they have the
same abstract syntax as the definitions of variables)where k > 0, c1, ..., ck
are some constant symbols, P is the defining axiom of the constant symbols.
 It is widely accepted now that every mathematical theory T can be considered
as an extension of the ZFC set theory by adding to ZFC (or an extension of
ZFC) the constants and axioms of the theory T [Dieudonne 82, p.215 ]. So
definitions of constants can be used for defining theories.
   For example a definition of group can have the following form:
               Group  := def[G, * ; <group axioms>]
where the constants G and * represent respectively the carrier set and the law
of composition (a function from G x G to G ). 
  Note that the formula   E[Group] expresses the following statement: the
group theory is consistent.
  Using the & operation on definitions, a definition of commutative group can
be written the following form:
 CommutativeGroup := Group & A[x, y | x in G & y in G -> x * y = y * x].
Using the definition of group Group and a definition of linear order (let us
name it as LinearOrder), a definition of linear ordered group can be written
in the following way:
                LinearOrderedGroup := Group % LinearOrder & R
where % is the operation of hereditary concatenation (see below) and R is an
additional axiom.

------------------------------------------------------------------------------
----------------------------------------------