Формальные системы.Исчисление предикатов

1. Формальные системы

 

Формальные системы — это системы операций над объектами, понимаемыми как последовательности символов (т. е. как слова в фиксированных алфавитах); сами операции также являются операциями над символами. Термин «формальный» подчеркивает, что объекты и операции над ними рассматриваются чисто формально, без каких бы то ни было содержательных интерпретаций символов. Предполагается, что между символами не существует никаких связей и отношений, кроме тех, которые явно описаны средствами самой формальной системы.

Если предложить читателю упорядочить объекты 53, 109, 3, то, скорее всего, он без всяких дополнительных вопросов расположит их в порядке 3, 53, 109. Иначе говоря, этой задаче будет дана обычная арифметическая интерпретация: последовательности цифр рассматриваются как изображения чисел в десятичной системе, упорядочение этих последовательностей есть расположение изображаемых ими чисел по возрастанию, а правила сравнения таких изображений чисел известны настолько хорошо, что обычно о них никто не задумывается. В действительности же такое истолкование задачи, вообще говоря, не вытекает из текста «упорядочить объекты 53, 109, 3»; его можно понимать как задачу лексико-графического упорядочения (что приведет к результату 109, 3, 53), как задачу распределения бегунов с номерами 53, 109, 3 по дорожкам (решение которой зависит от процедуры распределения и заведомо не связано с числовой интерпретацией объектов) и т. д. Возможность неоднозначного извлечения задач из текста означает, что этот текст не содержит формального определения задачи. Для такого определения нужно четко описать класс объектов, для которых задача решается, и явно ввести для них понятие упорядочения, описав его как систему локальных операций над символами, из которых эти объекты состоят.

По существу при таком  понимании «формальное описание» задачи означает ее точное, явное описание — все, что существенно для решения задачи, выписано явно. Поэтому уточнение задачи принято называть ее формализацией.

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

Индуктивное определение  формулы — простой пример описания перечислимого множества, в котором  использованы все существенные составные части понятия «алгоритм», кроме одного — детерминированности. Отбрасывая несущественный здесь порядок перечисления элементов множества, мы выигрываем в компактности описания, которое при этом не становится менее точным. Такое описание, не являюсь алгоритмом, представляет собой формальную систему, Однозначно описывающую множество формул.

Исторически теория формальных систем, так же как Теория алгоритмов, возникла в рамках оснований математики при исследовании строения аксиоматических теорий и методов доказательства в таких теориях. С их изучения и начнется знакомство с формальными системами.

2. Формальные теории (логические исчисления)

 

Формальную систему иногда называют также аксиоматикой, или формальной теорией, или еще проще — множеством формул.

Алфавит, который заранее предполагается конечным, иногда называют словарем. При этом в нем различаются константы, переменные и операторы.

Принципы построения формальных теорий. Всякая точная теория определяется, во-первых, языком, т. е. некоторым множеством высказываний, имеющих смысл с точки зрения этой теории, и, во-вторых, совокупностью теорем —  подмножеством языка, состоящим из высказываний, истинных в данной теории.

Каким образом теория получает свои теоремы?

В математике с античных времен существовал образец систематического построения теории — геометрия Евклида, в которой все исходные предпосылки сформулированы явно, в виде аксиом, а теоремы выводятся из этих аксиом с помощью цепочек логических рассуждений, называемых доказательствами. Однако до середины XIX в. математические теории, как правило, не считали нужным явно выделять действительно все исходные принципы; критерии же строгости доказательств и очевидности утверждений в математике в разные времена были различны и также явно не формулировались. Время от времени это приводило к необходимости пересмотра основ той или иной теории. Известно, например, что основания дифференциального и интегрального исчислений, разработанных в XVIII в. Ньютоном и Лейбницем, в XIX в. подверглись серьезному пересмотру; математический анализ в его современном виде опирается на работы Коши, Больцано, Вейерштрасса по теории пределов. В конце XIX в. такой пересмотр затронул общие принципы организации математических теорий. Это привело к созданию новой отрасли математики — оснований математики, предметом которой стало как раз строение математических утверждений и теорий и которая поставила своей целью ответить на вопросы типа: «как должна быть построена теория, чтобы в ней не возникало противоречий?», «какими свойствами должны обладать методы доказательств, чтобы считаться достаточно строгими?» и т. д. Одной из фундаментальных идей, на которые опираются исследования по основаниям математики, является идея формализации теорий, т, е. последовательного проведения аксиоматического метода построения теорий. При этом не допускается пользоваться какими-либо предположениями об объектах теории, кроме тех, которые выражены явно в виде аксиом; аксиомы рассматриваются как формальные последователь* ности символов( выражения), а методы доказательств — как методы получения одних выражений из других с помощью операций над символами. Такой подход гарантирует четкость исходных утверждений и однозначность выводов, однако может создаться впечатление, что осмысленность и истинность в формализованной теории не играют никакой роли. Внешне это так; однако в действительности и аксиомы, и правила вывода стремятся выбирать таким образом, чтобы построенной с их помощью формальной теории можно было придать содержательный смысл.

Формальная система определена, если:

1. Задан конечный алфавит (конечное множество символов).
2. Определена процедура построения формул (или слов) формальной системы.
3. Выделено некоторое множество формул, называемых аксиомами.

   4.      Задано конечное множество правил вывода. которые позволяют получать из некоторого конечного множества формул другое множество формул. Эти правила могут быть представлены в виде  

U₁ и U₂ и ... U_p→W₁ и W₂ и ... W_n,

Где U_i и W_i — формулы формальной системы, а стрелка → читается как “влечет” или “следует”.

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

Формальное доказательство (или просто доказательство) определяется как конечная последовательность формул M₁, M₂,…, M_r такая, что каждая формула Mi либо является аксиомой, либо при помощи одного из правил вывода выводима из предшествующих ей формул М_j, где j< i.

Формула t называется теоремой, если существует доказательство, в котором она является последней, т. е. М_r≡t. В частности, всякая аксиома является теоремой. Если t есть теорема, то этот факт кратко обозначается так: Hi

Правила вывода называют также правилами словообразования или правилами вывода заключения. В принципе они позволяют определять, является ли данная формула теоремой данной формальной системы. Отметим также, что в соотношении

{теоремы}  {формулы} {цепочки символов  из алфавита}

включение множеств является строгим.

Различают два типа правил вывода: 1) правила, применяемые к формулам, рассматриваемым как единое целое (в этом случае их называют продукциями, правилами продукций или продукционными правилами); 2) правила, которые могут применяться к любой отдельной части формулы, причем сами эти части являются формулами, входящими в формальную систему. В этом случае говорят о правилах переписывания. Так, в обычной математике следующее правило вывода:

х < у и у < z влечет х < z

применяется к формуле как к  целому (в данном случае к предложению математического анализа) — это продукция (с двумя антецедентами, или посылками). Слово ^uвлечет” для краткости при использовании продукции часто заменяется стрелкой →. В отличие от предыдущего правило х — х О имеет смысл при любом виде входящего в него в качестве подвыражения х. Оно является правилом переписывания, и в этом случае для обозначения слова “влечет” используется специальная стрелка

Разумеется, и продукция, и правило переписывания имеют только одно направление вывода — слева направо. Правило переписывания действует в обоих направлениях, если только заданы два правила.

При изучении формальных теорий мы имеем дело с двумя типами высказываний: во-первых, с высказываниями самой теории (теоремами), которые рассматриваются как чисто формальные объекты, определенные ранее, а во-вторых, с высказываниями о теории (о свойствах ее теорем, доказательств и т.д.), которые формулируются на языке, внешнем по отношению к теории, — метаязыке и называются метатеоремами. Различие между теоремами и метатеоремами не всегда будет проводиться явно, но его обязательно надо иметь в виду.

 

3. Основы логики предикатов первого порядка

 

В  логике высказываний атомарным выражением законченной мысли является непосредственно высказывание, рассматриваемое как единое (нераздельное) целое. Ни структура высказывания, ни его содержание не затрагиваются. В то же время и в науке, и на практике используются выражения, существенным образом зависящие как от структуры, так и от содержания используемых в них высказываний.

В связи с этим возникает  необходимость в расширении логики высказываний, в построении такой логической системы, средствами которой можно было бы исследовать структуру высказываний. Такой логической системой является логика предикатов (лат. praedicatum - заявленное, упомянутое, сказанное).

Логика предикатов расчленяет высказывание на объект (подлежащее) и  предикат (сказуемое). Объект - это то, о чем что-то утверждается в высказывании; предикат - это то, что утверждается об объекте.

Предикат - повествовательное предложение, содержащее предметные переменные, определенные на соответствующих множествах. При замене переменных конкретными значениями (элементами) этих множеств предложение обращается в высказывание, т.е. принимает значение "истинно" или "ложно".

С помощью логических связок (и скобок) предикаты могут объединяться в разнообразные логические формулы - предикатные формулы. Исследование предикатных формул и способов установления их истинности является основным предметом логики предикатов. Логика предикатов вместе с входящей в нее логикой высказываний является основой логического языка математики. С ее помощью удается формализовать и точно исследовать основные методы построения математических теорий. Логика предикатов является важным средством построения развитых логических языков и формальных систем (формальных теорий). 
      Логика предикатов, как и логика высказываний, может быть построена в виде алгебры логики предикатов и исчисления предикатов. Здесь, как и в случае логики высказываний, для знакомства с основными понятиями логики предикатов воспользуемся языком алгебры, а не исчислений. Такой выбор обусловлен рядом причин: 
 
• Исследование предикатных формул алгебры логики, выполнение их преобразований значительно проще, чем в исчислении предикатов. 
 
• Ограничения в использовании аппарата алгебры обусловлены тем, что предметные области (множества, на которых определены предметные переменные предикатов) теоретически могут быть и бесконечными. В таких случаях стандартный метод проверки истинности предикатов и формул в целом, требующий подстановки всех возможных значений предметных переменных, не может быть осуществлен в строгом смысле (точнее, процедура вычисления истинности может быть бесконечной и не дать ответа за конечное время). Однако в практических ситуациях при описании реальных систем, процессов, явлений в качестве предметных областей, как правило, используются конечные множества. Поэтому проблема бесконечности в значительной степени теряет свою актуальность.

Исчисление предикатов, которое  не содержит предметных констант, функторов, предикатов и собственных аксиом, называется чистым. Исчисление предикатов, которое содержит предметные константы и/или функторы и/или предикаты и связывающие их собственные аксиомы, называется прикладным. 
           Исчисление предикатов, в котором кванторы могут связывать только предметные переменные, но не могут связывать функторы или предикаты, называется исчислением первого порядка. Исчисления, в которых кванторы могут связывать не только предметные переменные, но и функторы, предикаты или иные множества объектов, называются исчислениями высших порядков.

Например, в высказывании «7 - простое число», «7» - объект, «простое число» - предикат. Это высказывание утверждает, что «7» обладает свойством  «быть простым числом». Если в  рассмотренном примере заменить конкретное число 7 переменной X из множества  натуральных чисел, то получим выражение  «X - простое число». При одних  значениях X (например, 13 или 17) это выражение  истинно, при других (например, 10 или 18) - ложно. Из примера видно, что выражение  «X - простое число» определяет логическую функцию одной переменной X, определенную на множестве натуральных чисел  и принимающую значения из множества {истина, ложь}. Данная функция в виде предиката может быть записана как простое число(X).

Аналогичным образом можно  определить логическую функцию нескольких переменных предикат(X, Y, Z, ...), которая  при одних сочетаниях переменных будет истинна, а при других - ложна. Такую функцию называют n - местным предикатом. Множество всех сочетаний переменных, при которых предикат принимает значение «истина», называется множеством истинности предиката.

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

 

4.Синтаксис логики предикатов первого порядка

 

 

 Синтаксис логики предикатов первого порядка:

- логические константы  – истина (И, TRUE, T,1) и ложь (Л, FALSE, F,0);

- символы констант –  символьные выражения, начинающиеся  со строчной буквы (например, cat, blue);

- символы переменных –  символьные выражения, начинающиеся  с прописной буквы или знака  подчеркивания (например, X, Сat, _blue);

- функциональные и предикатные  символы – символьные выражения,  начинающиеся со строчной буквы,  за которыми следуют список аргументов (термов), заключенных в скобки (например, sin(X), друзья(вася, петя)). Отличие функции от предиката, заключается в том, что функция возвращает результаты любого типа (строку, число, дату и т.д.), а предикат – только логического типа (истину или ложь). В связи с этим предикаты иногда называют логическими функциями;

- логические символы (пропозициональные  связки):

- Ø – отрицание;

- Ù – логическое И (конъюнкция, логическое умножение);

- Ú – логическое ИЛИ (дизъюнкция, логическое сложение);

- ® (Þ) – импликация (если - то);

- « (º) – эквивалентность;

- кванторы переменных:

- $ – квантор существования;

- " – квантор всеобщности;

- вспомогательные символы:  круглые скобки, запятые, +, - и т.п.

 

5. Кванторы

 

5.1. Историческая справка

Философы давно обращали внимание на логические операции, ограничивающие область истинности предиката, однако не выделяли их в отдельный класс  операций. Так, Томас Гоббс считал, что они являются частями имен.

Хотя кванторно-логические конструкции широко используются как в научной, так и в обыденной речи, их формализация произошла только в 1879 г., в книге Фреге «Исчисление понятий». Обозначения Фреге имели вид громоздких графических конструкций и не были приняты. Впоследствии было предложено множество более удачных символов, но общепринятыми стали обозначения   для квантора существования (перевёрнутая первая буква англ. Exists — существует), предложенное Чарльзом Пирсом в 1885 г., и   для квантора общности, образованное Герхардом Генценом в 1935 г. по аналогии с символом квантора существования. Термины «квантор», «квантификация» также предложил Пирс.

Квантор — общее название для логических операций, ограничивающих область истинности какого-либо предиката и создающих высказывание. Чаще всего упоминают:

• Квантор всеобщности (обозначение:  , читается: «для всех…», «для каждого…» или «каждый…», «любой…», «для любого…»).
• Квантор существования (обозначение:  , читается: «существует…» или «найдётся…»).

В математической логике приписывание квантора к формуле называется связыванием или квантификацией.

 

5.2. Примеры использования кванторов.

Обозначим   предикат «x делится на 5». Используя квантор общности, можно формально записать следующие высказывания (конечно, ложные):

1. любое натуральное число кратно 5;
2. каждое натуральное число кратно 5;
3. все натуральные числа кратны 5;

следующим образом:

.

Следующие (уже истинные) высказывания используют квантор существования:

1. существуют натуральные числа, кратные 5;
2. найдётся натуральное число, кратное 5;
3. хотя бы одно натуральное число кратно 5.

Их формальная запись:

.

Кванторы в математической логике:

• Высказывание   означает, что область значений переменной   включена в область истинности предиката  .

(«При всех значениях   утверждение верно»).

• Высказывание   означает, что область истинности предиката   не пуста.

(«Существует   при котором утверждение верно»).

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

5.3. Операции над кванторами

Правило отрицания кванторов — применяется для построения отрицаний высказываний, содержащих кванторы, и имеет вид:

 

6. Семантика логики предикатов первого порядка.

 

Терм - переменная, константа или функция (т.е. объект или его свойство).

Предикат (атомарная формула, атомарное предложение, атом) - отношение, устанавливающее связь между термами (параметрами). Предикат (в математической логике «атом») - простейший случай формулы, т.е. формула, которую нельзя расчленить на подформулы. Например, друзья(отец(андрей), коля) – отец Андрея и Коля являются друзьями. В этом предикате: друзья - предикатный символ, отец(андрей) – функция, коля – константа. Если параметр отец(андрей) был бы не функцией, а предикатом, то предикат друзья был бы предикатом второго порядка.

Количество термов в предикате  называется арностью предиката.

Предикат с арностью, равной 0, обозначает событие, признак или  свойство, относящееся ко всей предметной области, например, end.

Предикат с арностью, равной 1, обозначает свойство сущности, например, дом(кирпичный).

Формула (предложение, правило, правильно построенная  формула) - это либо предикат (атом), либо одна из следующих конструкций: ØА, AÙB, AÚB, A®B, A«B, ("X) A и ($X) А, где A и B - формулы, а X - переменная. Результатом вычисления формулы является либо истина либо ложь.

Примеры формул:

мать(маша, X) Ù мать(маша, Y) ® брат(X, Y) Ú сестра(X, Y) – если Маша мать X и Y, то X является братом или сестрой Y.

человек(X) ® смертен(Х) – если X – человек, то он смертен.

Приоритет операций и кванторов  при исчислении формул показан ниже

В скобках показаны операции (кванторы) с одинаковым приоритетом. Если в формуле используются операции (кванторы) с одинаковым приоритетом, то порядок исчисления слева-направо. Изменение порядка исчисления можно  добиться за счет использования круглых  скобок «( )».

Квантор существования $ указывает, что предложение истинно, по крайней мере, для одного значения переменной. Например, $X друзья(X, петя) – существует, по крайней мере, один субъект X, который является другом Пети.

Квантор всеобщности " указывает, что предложение истинно, для всех значений переменной. Например, "X человек(X) ® смертен(Х) – все люди смертны.

При комбинации кванторов  очень важен порядок их использования, например:

- "X$Y любит(Х, Y) – любой Х любит хотя бы одного Y;

- "Y$X любит(Х, Y) – каждого Y любит хотя бы один Х;

- $X"Y любит(Х, Y) – существует такой Х, который любит всех;

- $Y"X любит(Х, Y) – существует такой Y, которого любят все;

- "X"Y любит(Х, Y) и "Y"Х любит(Х, Y) – все любят всех;

- $X$Y любит(Х, Y) – существует такой X, который любит хотя бы одного из Y;

- $Y$Х любит(Х, Y) – существует такой Y, которого любит хотя бы один X. 

 

7. Исчисление предикатов

 

 

 Исчисление предикатов первого  порядка представляет собой исчисление высказываний, дополненное аксиомами , связанными с кванторами и дополнительными правилами вывода.

1. Алфавит исчисления предикатов состоит из предметных переменных х₁ , х₂, ..., предметных констант а₁, а₂, ..., предикатных букв P₁¹, Р₂¹, ..., Р^j_k... и функциональных букв f₁¹, f₂¹,..., f^j_k, ..., а также знаков логических связок Ú, Ù,¬,→, кванторов , и скобок (,).

Верхние индексы предикатных  и функциональных букв указывают  число аргументов, их нижние индексы  служат для обычной нумерации  букв. Переменные высказывания в исчисление предикатов вводятся либо непосредственно как пропозициональные буквы А₁, А₂, ..., либо как 0-местные предикаты P₁⁰, Р₂⁰, ..., т. е. как предикаты без предметных переменных.

2. Формулы. Понятие формулы определяется в два этапа.

1. Термы:

а) предметные переменные и  константы являются термами;

б) если fⁿ — функциональная буква, a t_1,…, t_n — термы, то fⁿ(t_1,…, t_n) — терм.

 2)Формулы:

а) если Р^п — предикатная буква, a t_1,…, t_n — термы, то Р^п(t_1,…, t_n) — формула; все вхождения предметных переменных в формулу вида Р^п(t_1,…, t_n)называются свободными;

б) если F₁ ,F₂ — формулы, то формулами являются ¬F, (F₁→ F₂),   

  (F₁ Ú F₂) ,(F₁ Ù F₂); все вхождения переменных, свободные в F₁ ,F₂, являются свободными и в указанных четырех видах формул;

в) если F(x) — формула, содержащая свободные вхождения переменной х, .то "xF(x) и $xF(x) — формулы; в этих формулах все вхождения переменной х называются связанными; свободные вхождения остальных переменных в F остаются свободными.

         3. Аксиомы исчисления предикатов делятся на две группы :

1) аксиомы исчисления высказываний (можно взять любую из систем I или II ).

Первая из них непосредственно использует все логические связки:

Система аксиом I:

I 1. A → (B → A);

I 2. (A → B) → ((A → (B → C)) → (A → C));

I 3. (A Ù B) → A;

I 4. (A Ù B) → B;

I 5. A → (B → ( A Ù B));

I 6. A → (A Ú B));

I 7. B → (A Ú B));

I 8. (A → C) → ((B → C) → (( A Ú B) → C));

I 9. (A → B) → ((A → ¬B) → ¬A);

I 10. ¬ ¬A → A

    Другая система использует только две связки ¬ и →; при этом сокращается алфавит исчисления (выбрасываются знаки Ù , Ú) и , соответственно, определение формулы. Операции Ù , Ú рассматриваются не как связки исчисления высказываний, а как сокращения (употреблять которые удобно, но не обязательно) для некоторых его формул: A Ú B заменяет ¬А → В, A Ù B заменяет ¬(A → ¬B). В результате система аксиом становится намного компактнее.

Система аксиом II :

II 1. A → (B → A);

II 2. (A → (B → C)) → ((A → B) → (A → C));

II 3. (¬A → ¬B) → ((¬A → B) → A).

Приведенные системы аксиом равносильны в том смысле, что порождают одно и то же множество формул.

 

2) две предикатные аксиомы:

P1. "xF(x) → F(y);

Р2. F(y) → $xF(x).

В этих аксиомах F(x) — любая формула, содержащая свободные вхождения х, причем ни одно из них не находится в области действия квантора по у; формула F(y) получена из F(x) заменой всех свободных вхождений I на у.

Чтобы пояснить существенность требования к вхождениям х в F, рассмотрим в качестве F(x) формулу $уР(у,х), где это требование нарушено: свободное вхождение х находится в области действия $у. Подстановка этой формулы в аксиому Р1 дает формулу "х$уР(у, х) → $уР(у, у). Если ее проинтерпретировать на множестве N натуральных чисел с предикатом Р «быть больше», то получим высказывание: «если для всякого х найдется у, больший x то найдется у, больший самого себя». Посылка этой импликации истинна на N, а ее заключение ложно, и, следовательно, само высказывание ложно.

 

4. Правила вывода:

Правила вывода позволяют из данной системы аксиом получать другие истинные формулы исчисления высказываний. Назовем формулу исчисления высказываний ложной, если ее отрицание истинно. Будем обозначать истинные формулы буквой R, ложные - F.

К основным правилам вывода относятся два:

1) Правило заключения (Modus Ponens)

Если A  и (A → B) – выводимые формулы, то B также выводима. Это предложение можно записать в виде

A,A→B

B

             2) Правило подстановки

Пусть некоторая формула A  содержит переменное высказывание А. Тогда, заменив высказывание А всюду, где оно встречается, любой формулой B , получим истинную формулу. Это предложение записывается в виде

A (А)

A (B)

Формула называется выводимой  в исчислении высказываний, если ее можно получить, применяя правила  вывода к аксиомам исчисления высказываний. Утверждение, что формула B выводима, записывают так:

 

├ B

Процесс получения формул из аксиом исчисления высказываний называется формальным выводом. Формальный вывод  состоит из указания того, какие  правила, в каком порядке и  к каким формулам применяется  для выведения данной формулы.

В исчислении предикатов первого  порядка (узком исчислении предикатов) два правила вывода (подстановки  и заключения) исчисления высказываний дополняют еще тремя правилами:

1. правило для (если φ₁ → φ₂ выводима и в φ₁ нет х в качестве свободной переменной, а в φ₂ переменная х содержится в виде свободной переменной, то формула φ₁ → (x)φ₂ также выводима);
2. правило для (если φ₁ → φ₂ выводима и х содержится в качестве свободной переменной в φ₁ и не содержится в виде свободной переменной в φ₂, то формула (x)φ₁ → φ₂ также выводима);
3. правило переименования связанных переменных (если φ₁ — выводимая формула и в φ₁ имеется квантор всеобщности или квантор существования, то одна связанная переменная в φ₁ может быть заменена другой связанной переменной одновременно во всех областях действия квантора и в самом кванторе. Полученная формула также выводима).

 

 

 

Заключение

 

Формальная система представляет собой совокупность чисто абстрактных объектов (не связанных с внешним миром), в которой представлены правила оперирования множеством символов в чисто синтаксической трактовке без учета смыслового содержания (или семантики).