ОТРИЦАНИЯ.
Правильно сформированная формула перед которой стоит тильда также правильно сформирована.
Примеры: ~S0=0 ~Eb:(b+b)=S0 ~<0=0эS0=0> ~b=S0
Кванторный статус переменной (говорящий нам, свободна или квантифицирована эта переменная) не меняется при отрицании.
СОСТАВНЫЕ.
Если x и у — правильно сформированные формулы и при этом ни одна переменная, свободная в одной из них, не квантифицирована в другой, тогда все следующие формулы правильно сформированы: <x Λ y>, <x V y>,<x э y>
Примеры: <0=0э~0=0>
Кванторный статус переменной здесь не меняется.
КВАНТИФИКАЦИЯ.
Если u — переменная и x — правильно сформированная формула, в которой и свободна, то следующие строчки — также правильно сформированные формулы:Eu:x и Au:x
Примеры: Ab: Ac:~Eb:(b+b)=c ~Еc:Sc=d
ОТКРЫТЫЕ ФОРМУЛЫ содержат по крайней мере одну свободную переменную.
Примеры: ~c=c b=b
ЗАМКНУТАЯ ФОРМУЛА (суждение) не содержит свободных переменных.
Примеры: S0=0 ~Ad:d=0 Ec:
Это дает нам полную таблицу Правил Образования для правильно сформированных формул ТТЧ.
Еще несколько упражнений на перевод
Вот еще несколько упражнений для вас, чтобы проверить, насколько вы поняли нотацию ТТЧ. Попробуйте перевести первые четыре из приведенных ниже высказываний Ч в высказывания ТТЧ, а последнее — в открытую правильно сформированную формулу.
Все натуральные числа равны 4.
Ни одно натуральное число не равно собственному квадрату.
Различные натуральные числа имеют различные последующие элементы.
Если 1 равняется 0, то любое число нечетно.
b — это степень 2.
Последнее может показаться вам трудным. Однако это еще цветочки по сравнению со следующим:
b — это степень 10.
Как это ни странно, чтобы записать это выражение в нашей нотации, требуется большая ловкость. Приступайте к нему только в том случае, если вы готовы просидеть над ним несколько часов — и если при этом вы уже хорошо знакомы с теорией чисел.
Нетипографская система
Мы изложили нотацию ТТЧ; остается только превратить ТТЧ в ту амбициозную систему, которую мы только что описали. Если нам это удастся, это будет значить, что интерпретация, которую мы дали символам, была правильна. До тех пор, однако, наши интерпретации не более оправданы, чем интерпретация «лошадь — яблоко — счастливая» для символов системы pr.
Можно было бы предложить следующий способ для построения ТТЧ: (1) Не использовать никаких правил вывода — они не нужны, так как (2) мы будем считать за аксиомы все истинные суждения теории чисел (записанные нотацией ТТЧ). Какой простой рецепт! К несчастью, он начисто лишен смысла, как нам и подсказывает наша первая реакция. Часть (2), разумеется, не является типографским описанием строчек, в то время как целью ТТЧ является именно типографское описание истинных высказываний.
Пять аксиом и первое правило ТТЧ
Таким образом, нам придется отказаться от простого рецепта, предложенного выше, и пойти по более сложному пути: у нас будут аксиомы и правила вывода. Прежде всего, как было обещано, все правила исчисления высказываний будут использованы в ТТЧ. Итак, первой теоремой ТТЧ будет следующая:
Она может быть выведена так же, как <P V ~ P >. Прежде чем приводить правила, давайте запишем пять аксиом. ТТЧ:
АКСИОМА 1: Aa:~Sa=0
АКСИОМА 2: Aa:(a+0)=a
АКСИОМА 3: Aa:Ab:(a+Sb)=S(a+b)
АКСИОМА 4: Aa:(a*0)=0
АКСИОМА 5: Aa:Ab:(a*Sb)=((a*b)+a)
(В строгой версии вместо b используйте a'.) Все они очень просты. Аксиома 1 сообщает что-то о числе 0; аксиомы 2 и 3 говорят о свойствах сложения; аксиомы 4 и 5 говорят о свойствах умножения и о его отношении к сложению.
Пять постулатов Пеано
Интерпретация первой аксиомы — «Нуль не следует ни за каким натуральным числом» — это одно из пяти знаменитых свойств натуральных чисел, впервые выраженных математиком и логиком Джузеппе Пеано в 1889 году. Излагая свои постулаты, Пеано следовал за Эвклидом в том смысле, что он не пытался формализовать принципы логических рассуждений. Вместо этого он хотел дать небольшой набор свойств натуральных чисел, из которого можно было бы вывести все остальные путем логических рассуждений. Таким образом, попытка Пеано может быть названа «полуформальной.» Работа Пеано оказала на математиков большое влияние, поэтому я приведу здесь его постулаты. Поскольку Пеано пытался определить именно «натуральное число», мы не будем использовать знакомый и вызывающий ассоциации термин «натуральное число» — вместо него мы будем пользоваться неопределенным термином гений — словом свежим и свободным от математических ассоциаций. Итак, пять постулатов Пеано устанавливают пять ограничений для гениев. Другие неопределенные термины, которыми мы будем пользоваться — джинн и мета. Читатель может догадаться сам, какие знакомые понятия скрываются за этими двумя терминами. Далее следуют пять постулатов Пеано:
(1) Джинн — это Гений.
(2) Каждый Гений имеет мету (которая тоже является Гением).
(3) Джинн не является метой никакого Гения.
(4) Различные Гении имеют различные меты.
(5) Если джинн имеет X и каждый Гений передает X своей мете, тогда все Гении получают X.
В свете ламп «Маленького гармонического лабиринта» мы должны наименовать множество всех Гениев «БОГом». Это напоминает нам о знаменитом высказывании немецкого математика и логика Леопольда Кроникера, архиврага Георга Кантора: «Бог сотворил натуральные числа; все остальное — работа человека.»
Вы можете узнать в пятом постулате Пеано принцип математической индукции — другой термин для «наследственного» доказательства. Пеано надеялся, что его ограничения понятий «джинна», «Гения» и «меты» были так сильны, что эти понятия были бы идентичны для всех людей и формировали бы у них в сознании совершенно изоморфные структуры. Например, для любого человека существовало бы бесконечное число различных Гениев. И, предположительно, каждый согласился бы с тем, что ни один Гений не совпадает со своей метой или мета-метой… и т. д.
В своих пяти постулатах Пеано хотел выразить сущность натуральных чисел. Математики обычно считают, что ему это удалось; однако это не уменьшает важности вопроса «каким образом можно отличить истинное высказывание о натуральных числах от ложного?» Ответа на этот вопрос математики ищут в формальных системах, подобных ТТЧ. Вы найдете в ТТЧ влияние Пеано, поскольку все его постулаты так или иначе вошли в эту систему.
Новые правила ТТЧ: спецификация и обобщение
Мы подошли к новым правилам ТТЧ. Многие из них позволят нам забраться внутрь этой системы и поменять внутреннюю структуру ее атомов. В этом смысле эти правила имеют дело с «микроскопическими» особенностями строчек в большей степени, чем правила исчисления высказываний, обращающиеся с атомами как с неделимыми. Например, было бы хорошо, если бы мы могли выделить строчку ~S0=0 из первой аксиомы. Для этого нам понадобилось бы правило, позволяющее опустить общий квантор и при необходимости одновременно поменять внутреннюю структуру остающейся строчки. Вот это правило:
ПРАВИЛО СПЕЦИФИКАЦИИ. Предположим, что u — переменная, встречающаяся внутри строчки x. Если строчка Au:x — теорема, то x — тоже теорема, как и все строчки, получающиеся из x путем замены и на любой (один и тот же) терм.
(Ограничение: Терм, заменяющий и, не должен содержать никакой переменной, квалифицированной в x.)
