LOGIC FOR THE THEORY OF CONCEPTS

In this paper, we follow Gödel’s remarks on an envisioned theory of concepts to determine which properties should a logical basis of such a theory have. The discussion is organized around the question of suitability of the classical predicate calculus for this role. Some reasons to think that classical logic is not an appropriate basis for the theory of concepts, will be presented. We consider, based on these reasons, which alternative logical system could fare better as a logical foundation of, in Gödel’s opinion, the most important theory in logic yet to be developed. This paper should, in particular, motivate the study of partial predicates in a certain system of three-valued logic, as a promising starting point for the foundation of the theory of concepts.

Sequent calculi of first-order logics of partial predicates with extended renominations and composition of predicate complement

We study new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations and a composition of predicate complement. For these logics, various logical consequence relations are specified and corresponding calculi of sequent type are constructed. We define basic sequent forms for the specified calculi and closeness conditions. The soundness, completeness, and counter-model existence theorems are proved for the introduced calculi.

Algebraic properties of if-then-else and commutative three-valued tests

This paper establishes a finite axiomatization of possibly non-halting computer programs and tests, with the if-then-else operation. The model is a two-sorted algebra, with one sort being the programs and the other being the tests. The main operation on programs is composition, and 1 and 0 represent the programs skip and loop (i.e. never halts) respectively. Programs are modeled as partial functions on some state space [Formula: see text], with tests modeled as partial predicates on [Formula: see text]. The operations on the tests are the usual logical connectives ∧, ∨, [Formula: see text], [Formula: see text] and [Formula: see text]. In addition, there is the hybrid operation of if-then-else, and the test-valued operation [Formula: see text] on programs which is true when a program halts, and undefined otherwise. The halting operation [Formula: see text] implies that operations of domain [Formula: see text] and domain join ∨ may also be expressed. When tests are assumed to be possibly non-halting, the evaluation strategy of the logical connectives affects the result. Here we model parallel evaluation, as opposed to the common sequential (or short-circuit) evaluation strategy. For example, we view [Formula: see text] as false if either [Formula: see text] or [Formula: see text] is false, even if the other does not halt.

An Inference System of an Extension of Floyd-Hoare Logic for Partial Predicates

Summary In the paper we give a formalization in the Mizar system [2, 1] of the rules of an inference system for an extended Floyd-Hoare logic with partial pre- and post-conditions which was proposed in [7, 9]. The rules are formalized on the semantic level. The details of the approach used to implement this formalization are described in [5]. We formalize the notion of a semantic Floyd-Hoare triple (for an extended Floyd-Hoare logic with partial pre- and post-conditions) [5] which is a triple of a pre-condition represented by a partial predicate, a program, represented by a partial function which maps data to data, and a post-condition, represented by a partial predicate, which informally means that if the pre-condition on a program’s input data is defined and true, and the program’s output after a run on this data is defined (a program terminates successfully), and the post-condition is defined on the program’s output, then the post-condition is true. We formalize and prove the soundness of the rules of the inference system [9, 7] for such semantic Floyd-Hoare triples. For reasoning about sequential composition of programs and while loops we use the rules proposed in [3]. The formalized rules can be used for reasoning about sequential programs, and in particular, for sequential programs on nominative data [4]. Application of these rules often requires reasoning about partial predicates representing preand post-conditions which can be done using the formalized results on the Kleene algebra of partial predicates given in [8].

Kleene Algebra of Partial Predicates

Summary We show that the set of all partial predicates over a set D together with the disjunction, conjunction, and negation operations, defined in accordance with the truth tables of S.C. Kleene’s strong logic of indeterminacy [17], forms a Kleene algebra. A Kleene algebra is a De Morgan algebra [3] (also called quasi-Boolean algebra) which satisfies the condition x ∧¬:x ⩽ y ∨¬ :y (sometimes called the normality axiom). We use the formalization of De Morgan algebras from [8]. The term “Kleene algebra” was introduced by A. Monteiro and D. Brignole in [3]. A similar notion of a “normal i-lattice” had been previously studied by J.A. Kalman [16]. More details about the origin of this notion and its relation to other notions can be found in [24, 4, 1, 2]. It should be noted that there is a different widely known class of algebras, also called Kleene algebras [22, 6], which generalize the algebra of regular expressions, however, the term “Kleene algebra” used in this paper does not refer to them. Algebras of partial predicates naturally arise in computability theory in the study on partial recursive predicates. They were studied in connection with non-classical logics [17, 5, 18, 32, 29, 30]. A partial predicate also corresponds to the notion of a partial set [26] on a given domain, which represents a (partial) property which for any given element of this domain may hold, not hold, or neither hold nor not hold. The field of all partial sets on a given domain is an algebra with generalized operations of union, intersection, complement, and three constants (0, 1, n which is the fixed point of complement) which can be generalized to an equational class of algebras called DMF-algebras (De Morgan algebras with a single fixed point of involution) [25]. In [27] partial sets and DMF-algebras were considered as a basis for unification of set-theoretic and linguistic approaches to probability. Partial predicates over classes of mathematical models of data were used for formalizing semantics of computer programs in the composition-nominative approach to program formalization [31, 28, 33, 15], for formalizing extensions of the Floyd-Hoare logic [7, 9] which allow reasoning about properties of programs in the case of partial pre- and postconditions [23, 20, 19, 21], for formalizing dynamical models with partial behaviors in the context of the mathematical systems theory [11, 13, 14, 12, 10].

Satisfiability in composition-nominative logics

Composition-nominative logics are algebra-based logics of partial predicates constructed in a semantic-syntactic style on the methodological basis, which is common with programming. They can be considered as generalizations of traditional logics on classes of partial predicates that do not have fixed arity. In this paper we present and investigate algorithms for solving the satisfiability problem in various classes of composition-nominative logics. We consider the satisfiability problem for logics of the propositional, renominative, and quantifier levels and prove the reduction of the problem to the satisfiability problem for classical logics. The method developed in the paper enables us to leverage existent state-of-the-art satisfiability checking procedures for solving the satisfiability problem in composition-nominative logics, which could be crucial for handling industrial instances coming from domains such as program analysis and verification. The reduction proposed in the paper requires extension of logic language and logic models with an infinite number of unessential variables and with a predicate of equality to a constant.