Swipe to navigate through the chapters of this book
We consider some advanced topics in logic including fuzzy logic, temporal logic, intuitionist logic, undefined values, logic and AI and theorem provers. Fuzzy logic is an extension of classical logic that acts as a mathematical model for vagueness. Temporal logic is concerned with the expression of properties that have time dependencies. Brouwer and others developed intuitionist logic as the logical foundation for intuitionism, which was a controversial theory of the foundations of mathematics based on a rejection of the law of the excluded middle and an insistence on constructive existence. We discuss several approaches that have been applied to dealing with undefined values that arise with partial functions including the logic of partial functions; Dijkstra’s approach with his cand and cor operators; and Parnas’s approach which preserves a classical two-valued logic.
Please log in to get access to this content
To get access to this content you need the following product:
It is best to avoid undefinedness by taking care of the definitions of terms and expressions.
The above expression would evaluate to true under Jones three-valued logic of partial functions.
The above expression evaluates to true for Parnas logic (a two-valued logic).
It seems strange to assign the value false to the primitive predicate calculus expression y = 1/ 0.
The approach avoids the undefined logical value (⊥) and preserves the two-valued logic.
First-order logic allows quantification over objects but not functions or relations. Higher order logics allow quantification of functions and relations.
For example, the statement ∃ x such that x = \( \sqrt 4 \) states that there is an x such that x is the square root of 4, and the constructive existence yields that the answer is that x = 2 or ( x – (−2)) i.e. constructive existence provides more the truth of the statement of existence, and an actual object satisfying the existence criteria is explicitly produced.
John McCarthy received the Turing Award in 1971 for his contributions to Artificial Intelligence. He also developed the programming language LISP.
Perhaps a good analogy might be that a mathematical proof is like a program written in a high-level language such as C, whereas a formal proof in logic is like a program written in assembly language.
Russell is said to have remarked that he was delighted to see that the Principia Mathematica could be done by machine, and that if he and Whitehead had known this in advance that they would not have wasted 10 years doing this work by hand in the early twentieth century.
Temporal Logic. Stanford Encyclopedia of Philosophy. http://plato.stanford.edu/entries/logic-temporal/
Intuitionist Logic. An Introduction. A. Heyting. North-Holland Publishing. 1966.
Intuitionist Type Theory. Per Martin Löf. Notes by Giovanni Savin of lectures given in Padua, June, 1980. Bibliopolis. Napoli. 1984.
Predicate Calculus for Software Engineering. David L.Parnas. IEEE.
Systematic Software Development using VDM. Cliff Jones. Prentice Hall International. 1986.
Programs with Common Sense. John McCarthy. Proceedings of the Teddington Conference on the Mechanization of Thought Processes. 1959.
A. Newell and H. Simon. The Logic Theory Machine. IRE Transactions on Information Theory, 2, 61–79. 1956.
Principia Mathematica. B.Russell and A.N. Whitehead. Cambridge University Press. Cambridge. 1910.
A Computational Logic. The Boyer Moore Theorem Prover. Robert Boyer and J.S. Moore. Academic Press. 1979.
- Advanced Topics in Logic
- Springer International Publishing
- Sequence number
- Chapter number
- Chapter 16