🚀 go-pugleaf

In article <1992Oct8.071027.9935@greco-prog.fr> billaud@greco-prog.fr 
(Michel BILLAUD) writes:

   >Explication simpliste: les propositions mathematiques sont codees par
   >des termes, exemple : qqsoit  X ilexiste Y telque  p(X,Y) ou non p(Y,X).
   >si les quantificateurs portent sur des symboles 'de base' on est au premier
   >ordre, si ils portent sur l'existence d'une fonction telle que gnagna, 
   >on est a un ordre superieur. 

   An explanation such as this can cause considerable confusion, I believe,
even for somebody who knows French (which I don't). For how are we to
make sense, given this explanation, of statements such as those of axiomatic
set theory, which are said to be first order, but are nevertheless read
"for every function.." etc?

  So I suggest another explanation: the essential characteristic of
statements of first order logic is that they contain quantifiers only over
the "objects" in some "domain". This domain may contain anything,
including functions. We get higher order logic if we introduce quantifiers
over subsets of the domain, functions over the domain, etc.

  From this it may appear that the distinction is of little importance,
since instead of using higher order logic, one may use first order
logic simply by expanding the domain to contain the functions, etc,
that one is interested in. And indeed this is what is done in set
theory.

  In logic, the importance of the distinction emerges when we consider
the concepts of "truth in a model" and logical consequence in first
order logic and in second order logic. They are defined in quite
similar term, using more formal versions of my explanation of the
quantifiers above. However, logical consequence in first order logic
has a set of complete formal inference rules. This is not true of
second or higher order logic. Also, it is possible to uniquely
characterize infinite structures by second order axioms. This can
not be done using first order axioms.

  Note: what about e.g. logic with infinite disjunctions? Is this
first or higher order? There seems to be no standard usage. So when
"first order logic" is spoken of, it is usually assumed that ordinary
predicate logic is intended, as in my remarks above.