Статья 403

Утверждение является истинным. Действительно, импликация если и закончит работу, то является истинной, поскольку по правилам логики из ложной посылки следует все, что угодно. Но посылка закончит работу всегда ложна, так как конъюнкция ложна, если ложен хотя бы один из ее членов. В рассматриваемом примере утверждения закончит работу исключают друг друга, т.е. не могут быть вместе истинными. Следовательно, их конъюнкция является ложной и влечет любое утверждение, в том числе заключение, которое, конечно, противоречиво, а потому ложно. Однако вся импликация будет истинна, откуда утверждение также истинно, что по определению означает частичную правильность программы хотя в интуитивном смысле программу относительно данных пред- и постусловий трудно считать правильной. Вместе с тем утверждение ложно, поэтому понятие тотальной правильности в большей степени соответствует интуиции.