Notes – On the Law of the Excluded Middle
The Law of the Excluded Middle is a simple idea. A logical statement should be either true or false:
a ÚØa
The development of multi-value logic systems brought new awareness to the possibilities of a logical value that is not true and not false. Some statements do not fit easily into the law of the excluded middle and seem more appropriate to explanation using multi-value logical systems. The notes on this page describes a simple example of a statement that could be interpreted as neither true nor false and applies the statement to basic concepts of program construction.
The weakest precondition represents all the program states that guarantee that termination of a program statement with an expected result.
The weakest precondition of program statement r with respect to result R is denoted on these pages as
WP.r.R
Consider the statement:
Given that the precondition is in set P, the outcome of activating program statement r is in the expected result R.
For the sake of simplicity, suppose that the Universal set of discourse divides neatly into two sets: the weakest precondition of R and the weakest precondition of ~R.
The set P is a precondition that has one of three configurations relative to the weakest precondition of program statement r.
a. P Í WP.r.R.
b. P Í WP.r.~R
c. Ø(P Í WP.r.R) ÙØ(P Í WP.r.~R)
In configuration (a) the statement shown above is true. In configuration (b) the statement is false. Configuration (c) renders an undecidable result unless more information is known about the current point in P prior to activating the program statement.
One of the basic programming notions is the concept of the Hoare Triple used on these pages to describe a programming solution. In the example above, the Hoare Triple
P {r} R
could be interpreted as neither true nor false, because the set P contains points that are solutions and points that are not solutions.
One approach to the problem is to use multi-valued logic in which true and false are not the only logical values. First, decide whether each point results in condition R or not. Each point should be decidable whether or not that R can be reached. Suppose that 80% of the points lead to the result R. Then we could conclude that the statement is 80% true and 20% false.
Suppose that the precondition P, the guarded command {(a or (b and c)) ®r}, and the expected result R forms a valid solution:
(a) P {(a or (b and c)) ®r} R
Now suppose that the programmer uses another, slightly different guarded command
(b) (a or b) and c) ®r}
Activation of the second guarded command behaves exactly like the first guarded command 75% of the time, and it behaves differently on 2 out of the 8 possible outcomes of the guard. A multi-value solution might say that the Hoare Triple with the alternate guard is 75% true.
Most program bugs come from situations as shown in the simple example above. Often, a bug is a side effect of an attempted solution that is correct most but not all of the time. The simple programming example shown above is inspired by the real-life experiences of a programmer who did not understand the syntax rules for logical operators in the COBOL programming language, so his solution behaved like example (a) above when his intention was to emulate the behavior of example (b). The program gave correct results 75% of the time, so the programmer was unshaken in his belief that his bug was somewhere else in his program.
Obviously, program bugs do not represent a desirable goal; so undecidable solutons with two or more possible outcomes are also not desirable. It seems that the law of the Excluded Middle is very useful in finding programming solutions. If a Hoare Triple represents only a partial solution, it is better to discard the partial solution altogether and label it as a false solution.
References:
Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall
Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag
Hoare, C. A. R., 1969, An Axiomatic Basis for Computer Programming, Communications of the ACM, Volume 12, Number 10, 576-580, 583
http://en.wikipedia.org/wiki/Logic#Bivalence_and_the_law_of_the_excluded_middle
Tait, W. W., Beyond the axioms: The question of objectivity in mathematics, http://home.uchicago.edu/~wwtx/objectivity.pdf