A Formalisation of the Propositional Calculus Corresponding to Wang's Calculus of Partial Predicates

1963 ◽  
Vol 9 (12-15) ◽  
pp. 177-198 ◽  
Author(s):  
Alan Rose
1991 ◽  
Vol 14 (4) ◽  
pp. 387-410
Author(s):  
Andrzej Blikle

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.


2011 ◽  
Vol 21 (4) ◽  
pp. 671-677 ◽  
Author(s):  
GÉRARD HUET

This special issue of Mathematical Structures in Computer Science is devoted to the theme of ‘Interactive theorem proving and the formalisation of mathematics’.The formalisation of mathematics started at the turn of the 20th century when mathematical logic emerged from the work of Frege and his contemporaries with the invention of the formal notation for mathematical statements called predicate calculus. This notation allowed the formulation of abstract general statements over possibly infinite domains in a uniform way, and thus went well beyond propositional calculus, which goes back to Aristotle and only allowed tautologies over unquantified statements.


1962 ◽  
Vol 46 (356) ◽  
pp. 119 ◽  
Author(s):  
John Evenden

Author(s):  
Ronald Harrop

In this paper we will be concerned primarily with weak, strong and simple models of a propositional calculus, simple models being structures of a certain type in which all provable formulae of the calculus are valid. It is shown that the finite model property defined in terms of simple models holds for all calculi. This leads to a new proof of the fact that there is no general effective method for testing, given a finite structure and a calculus, whether or not the structure is a simple model of the calculus.


Sign in / Sign up

Export Citation Format

Share Document