Алфавит КИВ
[предыдущая глава]  [оглавление]  [следующая глава]

Есть много разных вариантов КИВ. Все они ведут к практически одинаковым результатам просто потому, что их изначально строят так, чтобы получить одни и те же результаты, используя чуть-чуть другой порядок изложения. Мы немного поговорим о различных вариантах, и в конечном счете остановимся на одном из них, с которым продолжим работу.

Алфавит КИВ включает в себя следующие символы: (, ), , переменные (в том числе с индексами). В зависимости от варианта КИВ в алфавите могут также присутствовать символы: , , &, , true, false. Из-за того, что переменных бесконечно много (с учетом индексов), символов алфавите КИВ также бесконечно много.

Обратите внимание на то, что true считается одним символом алфавита КИВ, как и переменная a1234. Это важно для замен: при замене a на b нельзя превратить a1234 в b1234 поскольку a1234 представляет собой единый символ алфавита - элементарный и неделимый фрагмент текста. В другом языке (английском) другой алфавит и текст "true" представляет собой 4 отдельных символа, а не один. Вас это не должно смущать, это нормально даже для обычных языков. Так в русском языке есть буква "Ы", которая считается единой буквой, но может быть изображена с помощью двух букв латинского алфавита: "Ь" и "I".

Прежде всего, рассмотрим правила построения формул. В любом варианте КИВ есть правила:

  1. Одна отдельная переменная - формула.
  2. Если X - формула, то из нее можно построить формулу (X).
  3. Если X и Y - формулы, то из них можно построить формулу (X Y).

Обратите внимание на то, что в первом правиле область значений для переменной не задается. Это потому, что в КИВ не предусмотрено подстановки значений на место переменных, оно лишь позволяет переходить от одних формул с переменными к другим формулам с переменными.

Нам понадобится два вида переменных. Одни будут применяться в алфавите и формулах КИВ (см. правило 1), обозначая нечто неопределенное. Для таких переменных будем применять только малые латинские буквы a, b,..., z, возможно, с индексами. Другие переменные - такие, как X и Y в правилах 2 и 3 будут обозначать различные формулы КИВ. Выше X - это не отдельная переменная КИВ, а целая формула, которая может состоять из множества переменных КИВ, скобок и знаков операций (но может состоять и всего из одной переменной КИВ). Для обозначения формул мы будем применять только большие латинские буквы A, B,..., Z, возможно, с индексами. Таким образом, переменные a,... z - это переменные языка КИВ, а переменные A,... Z - это переменные метаязыка, на котором можно говорить о КИВ. Для обозначения числовых переменных (для индексов) будем применять малые буквы греческого алфавита α, β,..., ω.

Далее, здесь вы видите знакомый по булевой алгебре символ материальной импликации "". Никакой таблицы истинности для него не строится. Вместо этого он упоминается в аксиомах и правилах вывода. Булева алгебра и КИВ - это как бы два отдельных языка. Один и тот же символ может означать одно в языке булевой алгебры и совсем другое - в языке КИВ. То, что между этими двумя логическими системами есть много общего, еще только предстоит доказать. Попробуйте воспринимать КИВ как новый язык, который использует те же самые символы, но эти символы могут означать разные вещи (подобно английскому и латыни). Правила перевода с одного языка на другой нам еще только предстоит выяснить, булевско-кивский и кивско-булевский словари еще только предстоит составить.

Символы true и false могут присутствовать в КИВ, а могут и не присутствовать - зависит от варианта. У А.Черча символ false есть полноправная формула, подобная переменной. Символ true есть всего лишь сокращение для формулы false false. И символ ~ также служит всего лишь для сокращения: если X - формула, то формула (X false) сокращенно записывается как ~X. Если следовать Черчу, то надо добавить к правилам построения формул такое:

Соответственно, у Черча появляются аксиомы, которые позволяют доказывать теоремы, содержащие символ false. А символы true и ~ Черч использует исключительно как средство более компактной записи формул, содержащих false (примерно как я использую запись "X" вместо того, чтобы писать "а здесь, дорогой читатель, извольте мысленно вписать формулу, которая прячется под переменной X").

В изложении С.Клини в КИВ совсем нет символов true и false, зато символ ~ служит полноправной составляющей формул, а не просто сокращением.

Соответственно, у Клини появляются аксиомы, которые позволяют доказывать теоремы, содержащие символ ~.

Что касается символов , , , &, то для них ситуация такова. Каждый из символов можно рассматривать исключительно как сокращение для какой-то формулы с участием значков , ~, true, false, но можно рассматривать и как полноправный символ алфавита. Если считать эти символы всего лишь сокращением, то изложение упрощается. Однако тогда мы не будем иметь права доказывать для них полезные теоремы и не сможем провести параллели между применением этих символов в КИВ и в булевой алгебре.

Если же мы добавим эти символы в алфавит:

- тогда придется добавить для них и аксиомы, чтобы можно было выводить теоремы с участием этих символов.

Мы поступим следующим образом. В качестве правил построения формул возьмем 1, 2, 3, 4" (вариант Клини), 5, 6, 7, 8. Однако мы до поры до времени будем доказывать только теоремы с участием формул, построенных по правилам 1, 2 и 3, чтобы посмотреть, на что способна эта часть КИВ.

Символы ~, &, , , , называют "логическими операциями" или "пропозициональными связками". Приоритет у них один и тот же, независимо от того, где они применяются: в булевой алгебре, в КИВ или где-то еще. Некоторые скобки можно убирать, если это не помешает потом восстановить порядок операций.