Re: SUO: RE: Re: KIF & Naming Problems
John, Chris et al,
It may clearer (more semantic) to define the lattice of theories as the
concept lattice of the truth classification of a first-order language L,
whose instances are L-structures, whose types are L-sentences, and whose
classification relation is satisfaction. A formal concept in this lattice
has an intent which is a closed theory (set of sentences) and an extent
which is the collection of all models for that theory. The theory (intent)
of the join (sup) of two concepts is the closure of the intersection of the
theories (conceptual intents), and the theory (intent) of the meet (inf) of
two concepts is the theory of the common models.
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "John F. Sowa" <sowa@bestweb.net>
To: "Chris Menzel" <cmenzel@philebus.tamu.edu>; <sowa@bestweb.net>;
<standard-upper-ontology@ieee.org>
Sent: Tuesday, October 24, 2000 8:45 AM
Subject: Re: SUO: RE: Re: KIF & Naming Problems
>
> Chris,
>
> When we are talking about theories as deductive closures
> of a set of axioms, we are using proof-theoretical terms.
> Technically, I would define the top as the deductive closure
> of the empty set of axioms. For a complete logic, such as
> FOL, the deductive closure of the empty set happens to coincide
> with the set of all tautologies. (This definition presumes
> a proof theory, such as natural deduction, which does not need
> any explicit starting axioms, unlike the axioms of P.M.)
>
> >Actually, let me qualify the assertion that top and bottom are as in
> >your account. You identify top with the set of tautologies of L, but
> >(I think we've gone down a similar bunny trail before) the standard
> >meaning of "tautology" is a statement that is true under all truth value
> >assignments to its atomic constituents. This will not cover the
> >quantificational axioms of first-order logic (or the identity axioms).
> >Hence, I think it is better to use the broader term "logical truth"
> >instead of "tautology" to characterize top.
>
> I would consider the quantificational axioms, the rules of
> inference, the axioms for "=" in FOL+equality, and the model
> theory to belong to the metatheory about the language. You
> could express those axioms in FOL, when used as a metalanguage,
> but that would be a highly specialized theory about KIF, or
> predicate calculus, or CGs, or whatever other language is used
> to state the theories. I would not consider that theory to be
> in the topmost node of the lattice. It is, of course, necessary
> to define the lattice, but it is not a necessary part of the
> lattice itself.
>
> John