Theoretical Aspects of Computer Software, pp. 594--614, Springer-Verlag, 1991

This paper concerns the relation between parameterized first
order data types and first order logic. Augmenting first order
logic by data type definitions yields in general a strictly
stronger logic than first order logic. We consider some
properties of the new logic for fixed data type definitions.
While our new logic always fulfills the downward
Skolem-Löwenheim property, compactness is fulfilled if and only
if for the given data type definition the new logic has the same
expressive power than first order logic. We show that this last
property is undecidable.

@INPROCEEDINGS{Treinen:tacs91,
title = {First Order Data Types and First Order Logic},
author = {Ralf Treinen},
year = {1991},
month = {"24--27 " # sep},
editor = {"Takayasu Ito and Albert R. Meyer"},
publisher = {"Springer-Verlag"},
booktitle = {Theoretical Aspects of Computer Software},
series = {"Lecture Notes in Computer Science, vol. 526"},
pages = {"594--614"},
address = {"Sendai, Japan"},
note = {"This is en extended version: Interner Bericht A01/91, Universit{\"a}t des Saarlandes, Fachbereich 14: Informatik."},
}