Приведенное доказательство показывает насколько логически сильным оказывается правило подстановки с апострофом, что позволяет по-новому посмотреть на определения в логических системах. [19] Вместе с тем оказывается, что роль переменных функторов от пропозициональных аргументов шире, нежели вопросы теории определений. В частности, иначе открывается перспектива аксиоматизации исчисления высказываний. В пропозициональном исчислении с переменными функторами доказуема формула

(11) Cf0CfC00fp,

которая может быть прочитана следующим образом: если что-либо истинно о тождественно ложном предложении, и то же истинно для тождественно истинного предложения, то это же верно и для любого предложения. Поэтому Лукасевич (11) трактует как принцип двузначности, поскольку это предложение говорит, что существуют предложения истинные или ложные и только такие предложения. Вместе с тем Лукасевич высказывает мнение, что из (11) следуют аксиомы импликативно-негативного исчисления высказываний; именно эту роль и выполняет формула CfC00Cf0fp. Ученик Лукасевича, Мередит, показал, что все законы обычного исчисления высказываний, а также законы исчисления высказываний с кванторами и переменными функторами содержатся в 6-и буквенной формуле Cff0fp [1951]; эта формула по свидетельству Собоцинского была известна Лукасевичу. В этой связи Лукасевич писал следующее: "Вывод из этой формулы всего исчисления высказываний при помощи правила подстановки, правила отделения и правил для кванторов следует признать шедевром дедуктивного искусства".[20]


§ 5. Натуральный вывод Ст. Яськовского.


В 1926 г. Лукасевич поставил проблему, истоки которой можно заметить в рассмотренной выше работе "О науке". А именно, в математических доказательствах не используются логические формулы, но в них обращаются к предпосылкам и правилам рассуждений. Можно ли эти методы доказательства отобразить в системе структурных правил и исследовать их отношение к утверждениям аксиоматического исчисления высказываний? В 1927 г. Яськовский ответил на этот вопрос; результаты изложены в работе "О правилах допущений в формальной логике[1934].

Вначале Яськовский приводит примеры, с помощью которых выясняет интуитивный смысл метода допущений. Если мы хотим убедиться в истинности формулы CpCCpqq, то можно это сделать следующим образом:


1. Допустим p.

2. Допустим Cpq.

3. Из 1 и 2 следует q.

4. С учетом того, что q есть следствие допущения Cpq получим импликацию Cpqq.

5. С учетом допущения p получаем выражение CpCpqq.

Приведенный неформальный вывод кодируется следующим образом:

1.Sp

1.1.SCpq

1.1.q

1.CCpqq

CpCCpqq

Символ S является сокращением для оборота "допускается". Каждое допущение предваряет цифровой префикс. Префикс, составленный из одной цифры и точки означает главное допущение в данном выводе, а префикс, составленный из большего числа цифр и точек, означает дальнейшие допущения. Если последующее допущение обозначено префиксом, начальный сегмент которого идентичен с префиксом некоторого уже записанного в данном выводе допущения, то это значит, что мы имеем дело с допущением, охватываемом предыдущим допущением, например, SCpq находится, если можно так выразиться, в области допущения Sp. Если строка вывода предваряется цифровым префиксом, после которого знак S не записывается, то тогда выражение, стоящее непосредственно после префикса, является следствием допущения, имеющего тот же префикс, например, q является следствием SCpq.

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

Описание системы начинается приведенным выше примером и Яськовский предполагает, что к моменту написания первого допущения никакие прочие формулы не существуют. Если какая-либо формула T имеет номер n, то все формулы, имеющие в начальном сегменте номер n, принадлежат (вместе с T) к области T; в приведенном примере к области формулы q принадлежат выражения Sp, SCpq и само q. Под абсолютной областью Яськовский понимает множество всех записанных формул системы, а сама абсолютная область увеличивается одновременно с развитием всей системы. К моменту написания первой формулы абсолютная область представляет собой пустое множество. Эти свойства пополнения формальной системы свидетельствуют о влиянии Лесьневского. В 1926 г. на семинаре Лукасевича понятие области Яськовский эксплицировал следующим образом:


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