FOM: Craig Interpolation

Till Mossakowski till at Informatik.Uni-Bremen.DE
Mon Jul 20 09:45:32 EDT 1998

During the design of the algebraic specification language CASL,
the following questions arose:

1. Consider partial first-order logic as introduced by Burmeister
   and Beeson (the logic is strict, i.e. undefinedness is propageted
   from subterms to the terms containing them, while atomic formulae 
   containing an undefined term are interpreted as false, keeping
   the logic two-valued).
   I was told by Ray Gumb that Craig Interpolation does hold for
   (many-sorted) partial first-order logic (he calls it strict negative 
   free logic). But he could only tell me of one of his papers
   where Craig interpolation is proved for a similar logic.
   Is there any published proof of Craig Interpolation for partial 
   first-order logic?
2. Enrich many-sorted partial first-order logic by axioms of the form


   where S is a set of sort symbols and F is a set of function symbols.
   (S,F) holds in a model M iff each element of a carrier M_s (s\in S)
   is the value of a term under some variable assignment, where the
   term is built from function symbols in F and variables with sorts
   outside S.
   These axioms are a generalized form of second-order Peano induction 

   Does Craig interpolation hold for this logic as well?
   Any pointers to literature?

Actually, a positive answer of these questions would simplify
theorem proving for structured specifications in CASL.

Till Mossakowski

More about CASL can be found under

More information about the FOM mailing list