Many-valued logics—implications and semantic consequences

In this paper an application of the well-known matrix method to an extension of the classical logic to many-valued logic is discussed: we consider an n-valued propositional logic as a propositional logic language with a logical matrix over n truth-values. The algebra of the logical matrix has operations expanding the operations of the classical propositional logic. Therefore we look over the Łukasiewicz, Post, Heyting and Rosser style expansions of the operations negation, conjunction, disjunction and with a special emphasis on implication. In the frame of consequence operation, some notions of semantic consequence are examined. Then we continue with the decision problem and the logical calculi. We show that the cause of difficulties with the notions of semantic consequence is the weakness of the reviewed expansions of negation and implication. Finally, we introduce an approach to finding implications that preserve both the modus ponens and the deduction theorem with respect to our definitions of consequence.

Equational Logic Programming

Sections 2.3.4 and 2.3.5 of the chapter ‘Introduction: Logic and Logic Programming Languages’ are crucial prerequisites to this chapter. I summarize their relevance below, but do not repeat their content. Logic programming languages in general are those that compute by deriving semantic consequences of given formulae in order to answer questions. In equational logic programming languages, the formulae are all equations expressing postulated properties of certain functions, and the questions ask for equivalent normal forms for given terms. Section 2.3.4 of the ‘Introduction . . .’ chapter gives definitions of the models of equational logic, the semantic consequence relation . . . T |=≐(t1 ≐ t2) . . . (t1 ≐ t2 is a semantic consequence of the set T of equations, see Definition 2.3.14), and the question answering relation . . . (norm t1,…,ti : t) ?- ≐ (t ≐ s) . . . (t ≐ s asserts the equality of t to the normal form s, which contains no instances of t1, . . . , ti, see Definition 2.3.16).

Three-Valued Predicates for Software Specification and Validation

Partial functions, hence also partial predicates, cannot be avoided in algorithms. However, in spite of the fact that partial functions have been formally introduced into the theory of software very early, partial predicates are still not quite commonly recognized. In many programming- and software-specification languages partial Boolean expressions are treated in a rather simplistic way: the evaluation of a Boolean sub-expression to an error leads to the evaluation of the hosting Boolean expression to an error and, in the consequence, to the abortion of the whole program. This technique is known as an eager evaluation of expressions. A more practical approach to the evaluation of expressions – gaining more interest today among both theoreticians and programming-language designers – is lazy evaluation. Lazily evaluated Boolean expressions correspond to (non-strict) three-valued predicates where the third value represents both an error and an undefinedness. On the semantic ground this leads to a three-valued propositional calculus, three-valued quantifiers and an appropriate logic. This paper is a survey-essay devoted to the discussion and the comparison of a few three-valued propositional and predicate calculi and to the discussion of the author’s claim that a two-valued logic, rather than a three-valued logic, is suitable for the treatment of programs with three-valued Boolean expressions. The paper is written in a formal but not in a formalized style. All discussion is carried on a semantic ground. We talk about predicates (functions) and a semantic consequence relation rather than about expressions and inference rules. However, the paper is followed by more formalized works which carry our discussion further on a formalized ground, and where corresponding formal logics are constructed and discussed.