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

(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