FOM: A better reason, IMO, that SOL is syntactically ``more expressive'' than FOL

[Matt Insall]

Here I will say why I consider SOL to be sytactically more expressive than
FOL.  Some may think that this is a concession on my part, but I think if
you look closely, I never really stated that SOL was either more or less
expressive that FOL.  I had some misconceptions, some of which have been
cleared up by either on-line or off-line discussions with Roger Jones and
Harvey Friedman.  I appreciate the patience they took with me as we came to
some understandings about some previous miscommunications.  I concede most
of the technical details that Roger presented, and if I could read and
digest every bit of it, I might concede all, or perhaps all but one, of the
technical details of our disagreement, which I found eventually to be based
primarily upon some (as I said) misconceptions of my own, and some
miscommunications that are inevitable.  Thus, although I concede to most of
Roger's technical points, and I do see why he considers his measure of
expressiveness to be reasonable, I still have some misgivings about falling
wholeheartedly in line with his concept of ``expressiveness''.  Here, I will
merely outline what I consider to be well-known facts that give me a reason
to consider SOL to be more expressive than FOL.  I begin with the following
statement, which, according to some texts, may seem heretical:

1  There are non-recursive, complete, first order axiomatizations of
arithmetic.

Because of divergent terminology, some explanation is required.  I consider
semantics as primary.  Therefore, a way to describe what I want to do with a
logic system is to say that I want use it to describe classes of structures
that I can describe intuitively.  One may also say this in the following
way, ``Matt wants to `formalize his intuitive understandings of mathematics,
or, more generally, the universe'.''  The trouble, I guess, is that some of
us have different intuitive notions of what it means to ``formalize''
something for which we have an intuitive conception.  Thus, in a technical
sense, one can describe various ``levels'' of formalization.  The level at
which I consider the statement 1 to fall is in the following technical
interpretation:

1'  There is a non-recursive, complete set of first-order formulas which is
satisfied only by all models of arithmetic.


This is because I say that a notion, or concept, or, more technically, a
class K of structures, is axiomatizable if and only if there is a set S of
sentences such that a structure A is a member of K if and only if A is a
model of S.  This differs from many authors' use of the word
``axiomatizable'' to require recursiveness for the set S of axioms.  Thus,
my conception of axiomatizability is equivalent to what Bell and Slomson, in
``Models and Ultraproducts'' call a general first order property.  Moreover,
I have learned that some authors use the term complete to include
decidability, which I do not.  This makes 1' misunderstood by some with whom
I have spoken.  Thus, another restatement of 1 is the following:

1''  The property of being a model of arithmetic is a non-recursive, general
first order property.

I will grant that I am assuming that there is at least one model of
arithmetic, but I do not think most mathematicians would disagree with that
assumption.  (Perhaps I am wrong?)  Now, granting 1 as a restatement of 1'',
I will go further:



2  There is a minimal non-r.e., complete axiomatization for arithmetic.


If you do not like this formulation, try

2'  There is a minimal non-r.e., complete set of first-order formulas which
is satisfied only by all models of arithmetic.

or, using a term I am now inventing (perhaps not originally, for although I
never saw this term, I cannot say it did not previously exist)

2''  The property of being a model of arithmetic is a completely non-r.e.
property.



Contrasting this with the situation for PA, we of course have

3  There is a recursive axiomatization for PA, which is necessarily
incomplete.

or, equivalently and trivially,

3'  There is a recursive set of formulas which is satisfied only by all
models of PA.

or

3''  The property of being a PA-structure is a recursive first order
property.


Now, consider the property ``being a finite model''.  For this property,
there is, as Harvey commented, no sentence in FOL that can express the
property of being finite.  But there is more to the story here, that
separates the property of ``being a finite model'' from the property of
``being a model of arithmetic'', because the former is not even
axiomatizable in my sense:

4  The class of finite structures is not axiomatizable.

or

4'  There is no set of formulas which characterizes the finite structures.

or

4''  The property of being finite is not a general first order property.




Now, if you want to demonstrate the lack of expressiveness of FOL, that is a
way to do it, in my opinion.  That is ``First order logic cannot, even with
a set of sentences, express the property of being finite.''  It eliminates
any objections that say, for instance, some person or other being may
someday find a way to axiomatize finiteness.  Thus, I conclude that SOL is
more expressive, in this very general concept of expressiveness, because in
(semantic) SOL, the property of ``being finite'' is a second-order property,
meaning that in SOL, it is finitely axiomatizable.  (As usual, this entails
that the property of finiteness is expressible with a single sentence.) In
my experience, many mathematicians seem unaware of this, but then, many of
the mathematicians I encounter do not anyway seem to consider logic as a
sufficient foundation for mathematics, or they are quite disinterested in
foundations.  Since in mathematics, one is certainly interested frequently
in results that characterize some class of finite models, it would, in many
cases, I think, be useful for any logic system that is intended to be a
foundation for mathematics to be capable of characterizing the finite
models.  If this were the only case in which a mathematically interesting
property turned out to not be a general first order property, then one might
be tempted to just overlook it, but that is not the case.  In fact, any
property of structures which defines a class which includes only finite
structures, but is satisfied by arbitrarily large finite structures, is not
a general first order property.  This may cause some to believe that almost
everything one wants to do in (discrete) mathematics requires SOL or HOL.
Although I can certainly see uses for HOL, though, I would disagree with
this last assessment that some may have about the inadequacy of FOL in
mathematics.  For in fact, it is the soundness, completeness, and
compactness which I believe work together to make it possible to answer
essentially all humanly answerable mathematics questions using FOL.  This
last is thus far only a belief of mine at this time, for I am not sure I
have the tools, and I may never have the tools, which are required to
demonstrate it to the satisfaction of all or even most of those with whom I
discuss these things.  Suffice it to say that I consider much what I have
seen of the work of Abraham Robinson and Alfred Tarski, and others, to
support this opinion of mine, and I do accept nonstandard models, including
those to which the methods of nonstandard analysis apply, in support of this
belief.  In fact, although I am not at this time convinced that the notion
of recursiveness captures what amount of truth human beings can know, if one
does take the stance that recursiveness and recursive enumerability do
capture what we can know, then I think the case that FOL is (more than)
sufficient is even a trivial consequence.




Dr. Matt Insall
http://www.umr.edu/~insall