Remarks on remarks on many-sorted equational logic

The plurivalent logics considered in Graham Priest's recent paper of that name can be thought of as logics determined by matrices (in the `logical matrix' sense) whose underlying algebras are power algebras (a.k.a. complex algebras, or `globals'), where the power algebra of a given algebra has as elements \textit{subsets} of the universe of the given algebra, and the power matrix of a given matrix has has the power algebra of the latter's algebra as its underlying algebra, with its designated elements being selected in a natural way on the basis of those of the given matrix. The present discussion stresses the continuity of Priest's work on the question of which matrices determine consequence relations (for propositional logics) which remain unaffected on passage to the consequence relation determined by the power matrix of the given matrix with the corresponding (long-settled) question in equational logic as to which identities holding in an algebra continue to hold in its power algebra. Both questions are sensitive to a decision as to whether or not to include the empty set as an element of the power algebra, and our main focus will be on the contrast, when it is included, between the power matrix semantics (derived from the two-element Boolean matrix) and the four-valued Dunn--Belnap semantics for first-degree entailment a la Anderson and Belnap) in terms of sets of classical values (subsets of {T, F}, that is), in which the empty set figures in a somewhat different way, as Priest had remarked his 1984 study, `Hyper-contradictions', in which what we are calling the power matrix construction first appeared.

Download Full-text

A. Tarski. Equational logic and equational theories of algebras. Contributions to mathematical logic, Proceedings of the Logic Colloquium, Hannover 1966, edited by H. Arnold Schmidt, K. Schütte, and H.-J. Thiele, Studies in logic and the foundations of mathematics, North-Holland Publishing Company, Amsterdam1968, pp. 275–288.

Journal of Symbolic Logic ◽

10.2307/2271553 ◽

1971 ◽

Vol 36 (1) ◽

pp. 161-162

Author(s):

Ralph Seifert

Keyword(s):

Mathematical Logic ◽

Publishing Company ◽

Foundations Of Mathematics ◽

Equational Logic ◽

North Holland Publishing Company ◽

Equational Theories ◽

North Holland Publishing

Download Full-text

Second-Order Equational Logic (Extended Abstract)

Computer Science Logic - Lecture Notes in Computer Science ◽

10.1007/978-3-642-15205-4_26 ◽

2010 ◽

pp. 320-335 ◽

Cited By ~ 9

Author(s):

Marcelo Fiore ◽

Chung-Kil Hur

Keyword(s):

Second Order ◽

Equational Logic

Download Full-text

Equational Logic Programming

Handbook of Logic in Artificial Intelligence and Logic Programming: Volume 5: Logic Programming ◽

10.1093/oso/9780198537922.003.0005 ◽

1998 ◽

Author(s):

Michael J. O’Donnell

Keyword(s):

Normal Form ◽

Logic Programming ◽

Programming Languages ◽

Question Answering ◽

Normal Forms ◽

Equational Logic ◽

Consequence Relation ◽

Logic Programming Languages ◽

Semantic Consequence

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).

Download Full-text

Introduction: Logic and Logic Programming Languages

Handbook of Logic in Artificial Intelligence and Logic Programming: Volume 5: Logic Programming ◽

10.1093/oso/9780198537922.003.0004 ◽

1998 ◽

Author(s):

Michael J. O’Donnell

Keyword(s):

Logic Programming ◽

Programming Languages ◽

Historical Development ◽

Theoretical Computer Science ◽

Equational Logic ◽

Computer Scientists ◽

General Schema ◽

Similarities And Differences ◽

Logic Programming Languages ◽

Order Predicate Calculus

Logic, according to Webster’s dictionary [Webster, 1987], is ‘a science that deals with the principles and criteria of validity of inference and demonstration: the science of the formal principles of reasoning.' Such 'principles and criteria’ are always described in terms of a language in which inference, demonstration, and reasoning may be expressed. One of the most useful accomplishments of logic for mathematics is the design of a particular formal language, the First Order Predicate Calculus (FOPC). FOPC is so successful at expressing the assertions arising in mathematical discourse that mathematicians and computer scientists often identify logic with classical logic expressed in FOPC. In order to explore a range of possible uses of logic in the design of programming languages, we discard the conventional identification of logic with FOPC, and formalize a general schema for a variety of logical systems, based on the dictionary meaning of the word. Then, we show how logic programming languages may be designed systematically for any sufficiently effective logic, and explain how to view Prolog, Datalog, λProlog, Equational Logic Programming, and similar programming languages, as instances of the general schema of logic programming. Other generalizations of logic programming have been proposed independently by Meseguer [Meseguer, 1989], Miller, Nadathur, Pfenning and Scedrov [Miller et al., 1991], Goguen and Burstall [Goguen and Burstall, 1992]. The purpose of this chapter is to introduce a set of basic concepts for understanding logic programming, not in terms of its historical development, but in a systematic way based on retrospective insights. In order to achieve a systematic treatment, we need to review a number of elementary definitions from logic and theoretical computer science and adapt them to the needs of logic programming. The result is a slightly modified logical notation, which should be recognizable to those who know the traditional notation. Conventional logical notation is also extended to new and analogous concepts, designed to make the similarities and differences between logical relations and computational relations as transparent as possible. Computational notation is revised radically to make it look similar to logical notation.

Download Full-text