First-order logics with partial predicates for checking variable definedness

Abstract

We study semantic properties of new classes of program-oriented logics of partial quasiary predicates without monotonicity restriction. A feature of these logics is the use of special 0-ary parametric compositions – partial predicates which checks whether a subject name (variable) has a value in a given data. Such predicates-indicators are needed for quantifier elimination: from formulas of the form x we come to formulas of the form To perform such elimination in logics of non-monotonic predicates, the condition of definedness of a name z is needed, meaning a component with the name zis contained in the input data. We propose two types of pure first-order logics with partial predicates-indicators: L_^Q and L_^Q. Logics L_^Q use extended renominations, while L_^Q use traditional renominations. In this paper we describe composition algebras and languages of these logics, and introduce and investigate logical consequence relations for formulas and sets of formulas of the language: irrefutability (IR), truth (T), falsity (F) and strong (TF) logical consequences. Conditions that guarantee the logical consequence relation are considered, and their main properties are specified. Special attention is paid to the properties related to predicates-indicators and quantifier elimination. Logical consequence relations’ properties are the semantic basis for sequent calculi’s construction. Basic properties of a given logical consequence relation induce respective sequent forms for the corresponding calculus; properties that guarantee the logical consequence relation induce closedness conditions for sequents in this calculus. Construction of such sequent calculi is planned in the future works.

Prombles in programming 2024; 4: 23-33