Predicate Logic with Sequence Variables and Sequence Function Symbols

We describe an extension of first-order logic with sequence variables and sequence functions. We define syntax, semantics and inference system for the extension so that Completeness, Compactness, L¨owenheim-Skolem, and Model Existence theorems remain valid. The obtained logic can be encoded as a special order-sorted first-order theory. We also define an inductive theory with sequence variables and formulate induction rules. The calculus forms a basis for the top-down systematic theory exploration paradigm.

• Type: Conference
• Year: 2004
• Where: MKM
• Authors: Temur Kutsia, Bruno Buchberger
• Keywords: MKM 2004, Model Existence Theorems, Sequence Functions, Sequence Variables