Математическое доказательство.

Математическое доказательство – этот прорыв в системе взглядов человечества, который может рассматриваться наравне с повторяющимися экспериментами, как в химической лаборатории. Разница в том, что вместо физических объектов предметом эксперимента выступает человек. Эксперимент состоит из последовательности утверждений, в форме «из этого и этого следует то и то». И если субъект соглашается, эксперимент продолжается. В случае успешности эксперимент ведет к одобрению всей последовательности. Если субъект не соглашается с некоторым утверждением, эксперимент терпит неудачу. Эксперимент может быть успешным с некорректным доказательством, или он может потерпеть неудачу с корректным доказательством из-за способности человека совершать ошибки.

Математическая нотация не играет роли в доказательстве за исключением облегчения рассуждений и вычислений с помощью ранее оговоренных процедур. Действительно, математическая логика только формализует ранее принятые правила для «соглашения с тем что очевидно», и для следования таким правилам могут быть использованы компьютеры, там где они сделаны достаточно точно. Как человеческая деятельность, построение доказательства обнаруживает много сходств с проектированием программы. Сложное доказательство, как и сложная программа, может быть понято только как иерархия под-доказательств. Но тогда как программы выполняются машинами, доказательства выполняются (читаются) людьми, и должны быть учтены не только способность человека совершать ошибки, но и внимание и мотивация. Не очень хорошо произвести отличное доказательство из 1000 утверждений, если предмет теряет интерес и перестает слушать после 100 утверждений. Не очень хорошо произвести доказательство в 10 шагов, если шаги слишком большие, чтобы для того, чтобы быть усвоены предметом. И как уровень формализма должен быть разным для разных применений одной программы, предмет будет терпеть больше шагов доказательства для одного и того же доказательства в зависимости от важности момента. Не существует правильного уровня для каждого случая и нет наибольшего уровня доказательства.

В одних обстоятельствах лучшей стратегией доказательства корректности программы может быть утверждение: «как вы можете видеть, программа очевидно корректна в соответствии со спецификацией». Это приемлемое доказательство, и для простых программ может быть основание не тратить больше усилий. Однако, общие усилия необходимые для понимания и согласия с корректностью программы обычно уменьшают доказательство до некоторой разумной длины. Фактически, доказательство корректности служит лучшей документацией для программы. Набросок главных функций проекта служит как минимальное доказательство, например: «Композиция этих функций, очевидно, удовлетворяет спецификации».

Все сказанное выше было сказано для того, чтобы явное доказательство корректности программ не представлялось излишеством логиков, но необходимостью для благоразумных программистов. Доказательство в одно утверждение «это очевидно» - не доказательство. Любая документация является разновидностью доказательства. Поэтому не стоит вопрос нужны ли доказательства, вопрос, какую форму они могут принимать.