[дедуктивная система]: Дедуктивная система (сокращенно ДС) - это какая-нибудь строгая система правил, предназначенных для преобразования формул, фраз, текстов и тому подобного.

Что в данном случае является критерием строгости? На практике это определяется "постфактум": стараются сделать систему правил по-строже, и соблюдать достигнутый уровень строгости. Вот например школьная геометрия - это дедуктивная система. Сами можете судить, насколько она строга. В ВУЗе ее излагают по-строже, чем в школе, а в какой-нибудь высокоученой диссертации, посвященной вопросам геометрии, изложение может быть еще более формальным и детальным.

В качестве "пробного камня" для создания эталона строгости можно взять какой-нибудь не очень сложный компьютер (уровня персоналки). Если соблюдение правил способен проверить даже такой компьютер, то правила достаточно строги и для человека (не считая имбецилов). Здесь и далее я буду говорить о строгости правил именно в этом смысле.

В некоторых случаях можно натолкнуться на ограничения, связанные с объемом памяти или быстродействием такого компьютера. Поэтому, строго говоря, надо рассматривать не реальный компьютер, а "машину Тьюринга". Машина Тьюринга - это абстрактная примитивная модель компьютера, которая кое в чем превосходит реальность. Во-первых, машина Тьюринга не ломается, и может работать сколь угодно долго. Во-вторых, объем памяти у машины Тьюринга неограничен, а у любой реальной ЭВМ есть предел, выше которого невозможно наращивать объем памяти и диска. Мы можем рассмотреть в качестве эталона фантастический гибрид серийного компьютера и машины Тьюринга. Тогда свойства дедуктивных систем до определенного предела будут поддаваться практической проверке, а после этого предела могут рассматриваться чисто теоретически.

[(+)строгие правила]: Строгими правилами называется правило или набор из нескольких правил, соблюдение которых может проконтролировать за конечное время даже конечный автомат, похожий по свойствам на какой-нибудь серийный персональный компьютер, скажем, на базе платформы Intel, ценой не более 1000, 2000-го года выпуска.

Перво-наперво, следует определиться, с какими текстами может работать данная ДС. Например, геометрия Евклида имеет дело с текстами, где ведутся рассуждения о фигурах типа точки, прямой, плоскости. Правила геометрии позволяют преобразовывать одни утверждения о геометрических фигурах в другие. Другими словами, нужно определить понятие "формулы" (или "формы") для данной ДС.

[формула]: Формулой в данной дедуктивной системе называют объекты, которые данная дедуктивная система может преобразовывать.

Классический подход состоит в том, чтобы описать алфавит и правила построения формул.

[алфавит]: Алфавит дедуктивной системы - это список элементарных символов, которых достаточно для того, чтобы составить из них любую формулу.

[правила построения формул]: Правила построения формул - это строгие правила, по которым из символов алфавита можно строить формулы и только формулы.

С алфавитом все более-менее ясно - список букв, цифр, значков и прочих обозначений, встречающихся при работе с данной ДС, составить нетрудно. Что касается правил построения формул, то они очень часто формулируются в виде списка допустимых действий (если хотите, в виде программы), с помощью которых можно строить формулы ДС. И обратно: всякий текст, построенный с помощью этих действий, автоматически считается формулой данной ДС. Например:

1. true - формула.
2. false - формула.
3. Одна отдельная переменная, для которой область значений - либо true, либо false - формула.
4. Если X - формула, то из нее можно построить формулу (X).
5. Если X - формула, то из нее можно построить формулу (~X).
6. Если X и Y - формулы, то из них можно построить формулу (X & Y).
7. Если X и Y - формулы, то из них можно построить формулу (X Y).
8. Если X и Y - формулы, то из них можно построить формулу (X Y).
9. Если X и Y - формулы, то из них можно построить формулу (X Y).
10. Если X и Y - формулы, то из них можно построить формулу (X Y).

[формальный язык]: Алфавит, правила построения формул и сами формулы составляют формальный язык данной ДС.

Формальный язык дедуктивной системы - это не то же самое, что обычный язык типа русского, английского и даже не то же самое, что какой-нибудь компьютерный язык типа Алгола. Формулы тех языков несут некоторый смысл - то, что называют "семантикой". Для формального языка это необязательно, здесь имеются только символы, формулы и правила построения формул из символов - то, что называют "синтаксисом". В дедуктивных системах от семантики того или иного языка, как правило, абстрагируются.

Заметим, что мы сейчас говорим о свойствах некоторого языка, используя другой язык - обычный русский с кое-какими специфическими добавками вроде значков и "&". Как говорят, в данном случае русский язык играет роль "метаязыка".

[метаязык]: Метаязык - язык, на котором обсуждаются свойства другого языка.

Язык и метаязык могут поменяться местами, если, например, мы захотим исследовать свойства русского языка, применяя некоторую дедуктивную систему.