FOM: Craig Interpolation

[Till Mossakowski]

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

	(S,F)

   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 
   axioms.

   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.

Greetings,
Till Mossakowski

P.S.
More about CASL can be found under
	
	http://www.brics.dk/Projects/CoFI/index.html