First-order interpolation derived from propositional interpolation (Q2193292)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | First-order interpolation derived from propositional interpolation |
scientific article |
Statements
First-order interpolation derived from propositional interpolation (English)
0 references
25 August 2020
0 references
While interpolation properties in a propositional logic $L$ usually hinge upon the underlying algebras of $L$, the study of interpolation in first-order logics does not have a similar algebraic flavor. In the paper under review the authors give a method to reduce first-order to propositional interpolation. Suitable skolemizations and Herbrand expansions are constructed which, combined with a \textit{propositional} interpolant, yield a \textit{first-order} interpolant. The proof-theoretic constructions of this paper are applicable to lattice-based finite-valued logics and to the weak quantifier and subprenex fragments of infinitely-valued first-order Gödel logic. Interpolation turns out to be decidable for these logics.
0 references
proof theory
0 references
interpolation
0 references
lattice-based many-valued logics
0 references
Gödel logics
0 references
0 references
0 references