The FOL Distinction

The architecture of First Order Logic (FOL) involves a fundamental distinction or polarity. I initially wanted to call this the extrinsic-intrinsic distinction. But the term extrinsic has the unfortunate connotation of superficial or shallow, and this is not what the meaning of the FOL distinction. One could also call this the external-internal distinction, the outer-inner distinction, the exomorphic-endomorphic distintion, but these also suffer from the same unfortunate connotation. A much pithier terminology is the shell-kernel distinction. This also has a bit of the superficial connotation, but it is a well-known in Computer Science.

The exomorphic aspect of FOL, which is needed for a principled formulation of the "lattice of theories" concept, has been handled by the current version of the IFF Ontology (meta) Ontology (IFF-OO). Exomorphic refers to the architecture outside the notion of an FOL language or lexicon, whereas endomorphic refers to the architecture within an FOL language.

• The shell or exomorphic aspect of FOL, which is implicit in the development of Information Flow (see the book Information Flow: The Logic of Distributed Systems by Barwise and Seligman and the paper The Information Flow Foundation for Conceptual Knowledge Organization by Kent), aims at the architecture illustrated by the diagrams in Figure 1 consisting of four fundamental and sorted categories of language, theory, model and logic, and their adjoint connections.
  

• The kernel or endomorphic aspect of FOL, which is formalized in various treatments of categorical logic (see the paper Categorical Logic by Andy Pitts and the paper Hyperdoctrines, natural deduction, and the Beck condition by Robert Seely), is concerned with the hyperdoctrine approach to FOL; this is a standard stratified indexed category architecture of FOL based on substitution along tuples in the Lawvere construction.

Formulation of a categorical extension for the kernel aspect of the IFF-FOL needs three additions.

• The conjunction and disjunction operators should be defined on constant arity collections of expressions. This needs to use the relative power construction discussed in the core considerations.

• Substitution needs a thorough axiomatization. This includes an extension that obviates clash of variables. We are more than halfway finished with this formulation.

• An entailment order needs to be inductively defined in the expression fibers. This can be expressed in sequent form. Example axioms are: (1) for any two expression subsets related by the inclusion E₁ ⊆ E₂ we have the entailment ^E₂ ≤ ^E₁; or more generally, (2) the entailment holds ^E₂ ≤ ^E₁, if for every φ₁ in E₁ there is an φ₂ in E₂ such that φ₂ ≤ φ₁; (3) for any two expressions related by entailemnt φ₁ ≤ φ₂, their negations are related by reverse entailment ¬φ₂ ≤ ¬φ₁;