ВПЕРЁД

НАЗАД



Формальная система

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

Состав формальной системы:

  1. Предметный язык формальной системы. Язык считается полностью определённым, когда определены все его символы и формулы.
  2. Аксиомы формальной системы. Любая аксиома является формулой языка формальной системы. Аксиомы формальной системы также являются и её теоремами.
  3. Правила вывода формальной системы, на основе которых из аксиом получаются теоремы. Любое правило вывода утверждает, что, при некоторых условиях, одна формула, называемая заключением правила, может быть выведена из некоторых других формул, называемых посылками правила. Если все посылки некоторого правила являются теоремами, то и заключение этого правила является теоремой.

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

Мы могли бы в качестве предметного языка формальной системы использовать утверждающие предложения, записанные на языке той предметной области, для которой выполянется исследование. Например, можно было бы исследовать предложения, записанные на русском языке:

  • Все братья носят одну и ту же фамилию. Павел и Иван - братья. Иван носит фамилию Максимов. Следовательно, Павел носит фамилию Максимов
  • Все кролики одной породы имеют одинаковую длину ушей. Белка и Стрелка - кролики одной породы. Стрелка имеет короткие уши. Следовательно, Белка имеет короткие уши

Однако, при попытке исследовать формулы, записанные на нативном языке (то есть на языке, естественном для) целевой предметной области, неизбежно приходится искать ответы на следующие вопросы:

  • Как в математической логике единообразно выполнять исследования формул из различных предметных областей? Если проводить исследования самих нативных языков, то скорей всего под каждый из языков придётся выстраивать свою собственную систему исследований, применимую только для конкретного языка, и не применимую для остальных языков. Нужно каким-то способом абстрагироваться от семантики исследуемых языков. Без выполнения унификации (абстрагирования от) предметных языков, исследование формул любых предметных областей так или иначе будет предполагать выполнение анализа сути понятий, входящих в ту или иную предметную область. Предположим, что нас всё же не пугает перспектива формировать свой собственный особенный (специфичный) механимз исследований под каждый нативный язык предметной области. Тем не менее, подобная наша готовность не поможет легко найти ответ на следующий вопрос.
  • А что, если понятия исследуемой предметной области сами по себе слишком абстрактны и трудны для понимания кроющейся в них сути? Например, понятия в различных разделах высшей математики могут быть слишком абстрактными для возможности их лёгкого трактования обычным человеком. Как доказывать теоремы на основе понятий и аксиом, являющихся труднопонимаемыми для человека?

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

Общая форма записи рассужденийРассуждение №1Рассуждение №2
Все являются Все братья являются персонами, носящими одну и ту же фамилиюВсе кролики одной породы являются животными, имеющими одинаковую длину ушей
и являются Павел и Иван являются братьямиБелка и Стрелка являются кроликами одной породы
является Иван является персоной, носящей фамилию МаксимовСтрелка является животным, имеющим короткую длину ушей
Следовательно, является Следовательно, Павел является персоной, носящей фамилию МаксимовСледовательно, Белка является животным, имеющим короткую длину ушей

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

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

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

, где - конкретная формула унифицированного предметного языка.

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

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



ВПЕРЁД

НАЗАД