FOM: HOL is not stronger than FOL Vedasystem at
Mon Mar 22 13:30:03 EST 1999

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
Software Consultant
Brooklyn, New York 
                         Predicate Logic with Definitions

                                 Victor Makarov

                               vedasystem at


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. 


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


More information about the FOM mailing list