Перейти к содержимому
Topos Uranos
Русский

Индукция по натуральным числам и по формулам

Краткое содержание

Формул логики высказываний бесконечно много, и всякое утверждение обо всех них требует метода, который не сводится к их проверке по одной. Этот урок строит такой метод в два этажа. Первый этаж есть индукция по натуральным числам, в простой форме и в сильной, которая выводится из простой; второй есть индукция по сложности формул, или структурная индукция, которая обосновывается сильной индукцией по длине. С её помощью доказывается лемма о весе для языка кружков и дисков (всякая формула весит +1+1, а всякий собственный непустой префикс по словам весит не более 00), и из неё выводится, что никакая формула не является собственным префиксом другой, а отсюда однозначность разбора: каждая составная формула единственным образом раскладывается на свой начальный диск и две свои компоненты. Наконец, однозначность разбора обосновывает рекурсивные определения на формулах (длина, число переменных и дисков-связок, подформулы, глубина) и подстановку вместо одной подформулы другой.

Цели обучения

  1. Доказывать простой и сильной индукцией свойства натуральных чисел, проверяя базу индукции и находя ошибку в неверной индукции.
  2. Доказывать индукцией по сложности, что все формулы обладают некоторым свойством, рассматривая переменные и единственное правило образования как единственные случаи.
  3. Доказывать лемму о весе и выводить из неё, что никакая формула не является собственным префиксом другой и что всякая составная формула допускает однозначный разбор.
  4. Определять функции на формулах по рекурсии (длина, глубина, подформулы, подстановка) и доказывать индукцией соотношения между ними.

Утверждения обо всех формулах

В уроке о языке логики высказываний формулы были построены из двух символов, ∘\sigO и ∙\sigI, которые мы называем кружком и диском, и единственного правила образования. Формул бесконечно много, и многие важные утверждения относятся ко всем ним: что всякая формула оканчивается диском, что никакая формула не читается двумя способами, что во всякой формуле переменных на одну больше, чем дисков-связок. Такие утверждения не являются формулами изучаемого языка; это высказывания о нём, сформулированные в метаязыке (русском языке, дополненном математическими обозначениями); поэтому их доказательство есть не вывод внутри формальной системы, а обычное математическое рассуждение, предметом которого является формальная система. Оттого такие доказательства называют метатеоретическими, или внешними.

Однако никакое количество проверенных примеров не доказывает утверждения о бесконечном множестве объектов. Отсюда следует, что нужен принцип, который позволяет из конечного числа проверок заключить, что свойство выполняется в бесконечном числе случаев. Этот принцип есть индукция. Сначала он излагается для натуральных чисел, где он привычнее, а затем для формул, где он опирается на предыдущий. Тот же инструмент докажет в разделе метатеории корректность и полноту дедуктивной системы.