Пример 1. Введение в формальные системы

Введение в формальные системы

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

Внутренняя логическая связность некоторой математической теории и её адекватность для описания того или иного круга физических явлений – это две совершенно разные вещи. Данный факт был осознан математиками, когда им пришлось объяснять существование евклидовой геометрии и различных неевклидовых геометрий (например, геометрии Лобачевского-Бойаи).

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

Формальная система описывается с помощью символического (формального) языка, для которого точно определяется синтаксис (посредством «правил образования») и логика (посредством «правил вывода» или «правил преобразования»). Обсуждение свойств формальной системы производится в некоторой другой теории (средствами другого языка), которую назовём метатеорией (а этот другой язык – метаязыком). Саму же формальную систему называют предметной (или объектной) теорией (и соответственно употребляют термины «предметный язык» или «язык-объект»).

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

Пусть алфавит формальной системы есть А={0, 1, 2, 3, 4, 5, 6, 7, 8, 9, +, –}.

Мы хотим определить два множества, а именно множество целых чисел без знака и множество целых чисел. Чтобы сформулировать правила образования этих множеств, мы введём метаязыковую переменную С, которая принимает любое значение из множества {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}, метаязыковую переменную, принимающую значение из множества целых чисел без знака, и метаязыковую переменную Е, принимающую значение из множества целых чисел.

Скобки «á» и «ñ» будут использоваться для разграничения вхождения переменных; вертикальная черта «½» обозначает союз «или»; символ «::=» означает разрешение заменить то, что стоит слева от него, каким-либо из выражений, стоящих справа от него и разделённых вертикальными чертами. Для обозначения конкатенации (соединения двух цепочек) используется «классический» типографский прием – простое соположение (без специального знака).

Правила порождения интересующих нас множеств:

Правило 1: áWñ::=áCñ½áWñ áCñ;

Правило 2: áEñ::=áWñ½+áWñ½-áWñ.

Дата добавления: 2015-06-27