RE: SUO: RE: Re: KIF & Naming Problems
Jay,
I agree that some clarification of what is being standardized
should be included somewhere in the SUO standard.
>Folk sometimes use the term "FOL" without much specification. As you point
>out, John, there are many systems or versions of 'first-order' logic, which
>provably equivalent in some respects, and not equivalent in other respects.
>These systems may differ in proof theories and in intended semantics,
>perhaps in SUO-relevant respects. Such systems also agree in having those
>significant characteristics like compactness which make them 'first-order'.
>Perhaps part of the SUO task will be to delineate what 'first-order' means.
The term "classical first-order logic" could be interpreted
in many different ways. But there is one interpretation in
which it has a single, very well-defined meaning. That is the
definition that focuses on its expressive power and the set of
all possible theorems that can be proved in it.
Those four systems that I mentioned in my previous note are
very different in their notations, proof procedures, and choice
of axioms. But they are all exactly equivalent in what they
can express and in the collection of possible theorems that
can be proved by means of their very different proof procedures.
There are also other notations, such as SUO Controlled English,
which would look very different from any of those four, but
which could also express exactly the same propositions.
A definition of FOL that would focus on the expressive power
would allow a great deal of flexibility in notation and
proof procedures while guaranteeing that anything expressed
in any one of the notations could be translated to and from
any of the others without loss or distortion.
John