ABSTRACT

A proof to Godel’s completeness theorem Henkin style proceeds by constructing a model directly from the syntax of the given theory. The structure is obtained by putting terms that are provably equal into equivalence classes, then defining a free structure on the equivalence classes. The computing enterprise requires more general techniques of model construction and extension, since it has to accommodate dynamically changing world descriptions and theories. The techniques the author has applied

since 1980s for model building as applied to computing allows us to build and extend models with generic diagrams defined from a minimal set of function symbols with which a model can be defined inductively. Generic diagrams allow us to define canonical models with specific functions. Sentential logic is the standard formal language applied when defining basic models. The language L is a set of sentence symbol closed by finite application of negation and conjunction to sentence symbols. Once quantifier logical symbols are added to the language, the language of first order logic can be defined. A Model A for a language is a structure with a set A, for each constant symbol in the language there corresponds a constant in A. The signature or similarity type for a set of formulas or terms is the set of nonlogical symbols appearing. A languages signature encompasses the arity-coarity of the function and relation symbols.