SUO: Re: KIF & Re: Naming Problems
John F. Sowa wrote:
>
> 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
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
John,
OK, but a theory is a set of 'sentences',
and a sentence is a syntactic construct
that is bound to a particular 'alphabet'
of primitive tokens as actually scribed.
So the concept of a 'theorem' is already an abstract type,
whose extension as a sort of scattergram cluster within the
framework of a concrete and a particular 'discursive universe',
in effable effect, as realized within a particular formal language,
is already the sort of object that requires some rather fancy morphism
mechanics just say what the heck we might mean by the apparently or the
ostensibly natural equivalence of 'same theorem in a different language'.
I mean, I believe you and everything, but I do not see it as a simple fact.
Cheers,
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤