Вопрос был окончательно решен, когда Лукасевич [1948] опубликовал доказательство того, что аксиома из 13-и литер является кратчайшей.

Первую аксиоматику, использующую эквивалентность в качестве единственного постоянного термина, привел Лесьневский [1929]: EEEprEqpErq, EEpEqrEEpqr + правила подстановки и отделения. После появления ряда аксиоматик, полученных Вайсбергом, Бриманом, Лукасевичем и Собоцинским Лукасевич [1938] доказывает, что формула, содержащая менее 10 литер не может быть единственной аксиомой исчисления, построенного исключительно на функторе эквивалентности.


§ 4. Пропозициональное исчисление с переменными функторами.


Весьма интересным и редко обсуждаемом случаем логической теории является исчисление предложений с переменными функторами. Его появление в определенной степени связано с точкой зрения Лукасевича на определения. Выше упоминалось, что Лукасевич понимал дефиниции как метаязыковые сокращения. Отличную от этой позицию в школе занимал Лесьневский, который трактовал дефиниции как предложения системы. Сравнение этих двух точек зрения побудило Лукасевича к изучению исчисления предложений с переменными функторами, введенными впервые в Прототетике Лесьневского. Первый раз этим вопросом Лукасевич занялся в статье об исчислении предложений эквивалентности [1939]. Лукасевич замечает, что выражение Vp (verum от p) как одноаргументный функтор от пропозициональной переменной может быть введен двояко:

D1 Vp =df Epp

D2 EVpEpp

Отличия D1 и D2 состоят в том, что D1 записано в метаязыке, а D2 является предложением исчисления, но кроме того эти определения "методологически разные" и, как замечает Лукасевич, не находя лучшего выражения, D2 "действует "творчески"". Различия определений D1 и D2 демонстрируются на примере выражения

(I) EEsEppEEsEppEEpqEErqEpr,

которое является выводимой формулой исчисления эквивалентностей. Особенность этой формулы состоит в том, что все ее заключения можно получить исключительно путем подстановки, но не отделением. Тот факт, что формула (I) "неделима" Лукасевич показывает методом, восходящим к Тарскому.[18]

А именно, если из (I) мы хотим получить новую формулу путем отделения, то должны предположить, что существуют две подстановки в (I), одна из которых имеет тип Exy, а вторая - x (все переменные принадлежат метаязыку, т.е. являются переменными, значениями которых суть произвольные выражения языка исчисления эквивалентностей). Эти семиотические условия записываются следующим образом:

(a) Exy :=: EEaEbbEEcEddEEdeEEfeEeg

(b) x :=: EEhEiiEEhEiiEEijEEkjEik

(символ :=: означает здесь эквиморфность).

В (а) литере x соответствует выражение EaEbb, т.е.

(c) x :=: EaEbb,

тогда как из (b) и (c) получаем, что

(d) EaEbb :=: EEhEiiEEhEiiEEijEEkjEik.

Отсюда вытекает, что следующие выражения эквиморфны:

(е) a :=: EhEii

(f) b :=: EhEii

(g) b :=: EEijEEkjEik.

Из (f) и (g) получаем:

(h) h :=: Eij

(i) i :=: Ekj

(j) i :=: Eik.

Последнее выражение абсурдно, поскольку невозможно, чтобы "i" было эквиморфно некоторому выражению, содержащему "i" как свою собственную часть. Отсюда следует, что невозможно получить две подстановки формулы (I), которые были бы подстановками типа Exy и x. Таким образом, к выражению (I) не может быть применено правило отделения. Отсюда непосредственно следует, что из (I) нельзя вывести никакой более короткой формулы, в частности EEpqEErqEpr, которая была бы аксиомой исчисления высказываний.

Однако ситуация измениться, если принять D2. Достаточно в (I) вместо переменной s подставить выражение Vp, чтобы после двукратного применения правила отделения получить аксиому EEpqEErqEpr. Следовательно, дефиниция D2 креативна. Такое решение не удовлетворяет Лукасевича, поскольку D2 вводит в систему выражение, не являющееся первичным, а потому и не характеризуемое аксиомами. Лукасевич [1939] заключает: "Ни в коем случае мы не должны придавать новые свойства первичным терминам системы. Первичные термины должны быть охарактеризованы исключительно аксиомами. Если мы занимаем такую позицию, то следовало бы по возможности избегать творческих определений" (S.249).

К этой проблематике Лукасевич вернулся в работе "О переменных функторах от пропозициональных аргументов"(1951). Рассматривая формулу Прототетики Лесьневского

(1) CfpCfNpfq

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