Xaositect,
можно не обсуждать посылку «Если

— истинное высказывание, то

— ложное высказывание», принять ее за истинную, и посмотреть, что из этого следует.
А следует вот что. По Вашему примеру, «2. Схема аксиом

.», предполагая, что
1. Действия выполняются слева направо;
2. Скобки указывают на порядок действий;
как только для

построено отрицание, а

получает значение "ложь", и учитывая, что в Вашей системе разрешено без ограничений записать

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

Что означает "тождественно истинный", не совсем понятно, по-видимому, самому себе.
Если при подстановке я могу представить, откуда следует вот это:

,
и могу эту истинность

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

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

".
Для формализации этого примера я бы взял хорошо знакомые из математики термин и определение "функция", и не изобретал бы "логический" велосипед. По моему мнению,

это простая функция с областью своих значений

, и областью значений аргумента

. Если мы для удобства вычисления (так делают в программировании) символы

заменим на символы

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

функция не определена.
Отсюда:

, — определена на

;

, — определена на

;

, — всюду на

неопределена (функция не задана).
Определение вычитания векторов:

тогда и только тогда, когда

.
Вы хотите показать его некорректность?
Да, конечно. Вы предложили один из возможных путей для определения вычитания векторов. Суть примера не в его значении, оно побочный эффект, а в том, как мог бы работать алгоритм. С векторами и противоречием всё просто. Вычитание векторов ничему не соответствует в физической действительности. С этого момента мы и пойдем назад, от противоречия.
Однако сначала покажу именно для Вашего определения его противоречивость.
Примем за истинные посылки:
1. Можно задать декартову систему координат (СК).
2. В СК по пункту 1 можно задать отрезок.
3. В СК по пункту 2 можно задать два различных отрезка.
4. По определению из геометрии, если точки совпадают координатами, это одна и та же точка.
5. Двумя различными отрезками будут считаться такие, для которых можно указать хотя бы одну точку одного отрезка, координаты которой не совпадают с какой-либо точкой второго.
6. По определению вектора, обозначив концы отрезка разными символами (буквами, треугольничками, координатами, и т.п.), мы задаем порядок для точек отрезка.
7. Продемонстрируем пункт 1-6 графически, (рис. 1):

8. Пункт 5 продемонстрируем следующим примером: (рис 2).
Векторы

и

различные векторы.

9. Операция "сумма" над векторами определена для двух разных (пункт 5) векторов,

и

, если у этих векторов совпадают пары координат: либо начало-начало, либо конец-начало. Для остальных пар операция сумма не определена. (рис. 3):
а) все векторы разные.
б) сложить можно пары (A,B), (A,A'), (A',B) и (D,E). Для остальных пар операция "сумма" не определена.

Далее возьмем для примера [Н. Бухгольц, Основной курс теоретической механики. ч.1. Кинематика, статика, динамика материальной точки., М.: Наука, 1965. стр. 26]:


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

тогда и только тогда, когда

.»
Запишем аналогично для приведенной цитаты:

, если

Если по пунктам 1-9 возражений нет, то из них с необходимостью следует, что векторы

и

сложить нельзя. Отсюда заключаем, что Ваше определение противоречиво (некорректно).
-----------
Движение по алгоритму напоминает игру. Правила простые, им сто лет в обед. Их всего два.
1. Запрет противоречий, как окончательного результата.
2. Рассуждения ведутся по правилам логики (из предположительно истинных высказываний).
Ближняя цель — получить противоречие (с определением, аксиомой, теоремой, или с другим рассуждением на тех же посылках). Да, вот такая странная ближняя цель. Идем к противоречию (или неопределенности в операции), как к первой цели, потому что оно означает, что с этого шага алгоритм разворачивается на рекурсию. Идти постепенно к противоречию хорошо при каких-то частных задачах, но у нас есть свой интеллект, и поэтому в эту игру лучше вступать с уже обнаруженного противоречия.
Но на самом деле, линейный порядок чтения приведенных выше пунктов от 1 к 9, не отображает алгоритма работы, он как иголка швейной машины, рекурсивный. Это просто причесанная, окончательная картина.
Реконструкция.Ограничимся для простоты примера, что определение у термина короткое, по возможности, в одно слово, исключая из счета связку "суть" и служебные слова из грамматики, например, предлоги, союзы и пр. Тогда термин "вектор" имеет определение: "суть стрелка". На десятом шаге-итерации определение должно вырасти линейно до

слов. Это если не будет найдено противоречий. Уверяю, что если работать над конкретным текстом из математики, то без противоречий не обойдется, а десятый шаг в определении может появиться очень нескоро... Образное представление: получается не база знаний предсуществующих знаний, вложенная в заранее продуманную структуру, а запись новых образований: связей терминов, и новых рассуждений. Структура вырастет сама, автоматически, так, как это получается у семени растения. Или у морозной снежинки на стекле. Есть предположение (мое), что начав с любого понятия в существующей математике, работающий алгоритм отрисует одну и ту же, новую, и незнакомую до этого структуру для всей математики. Но это гипотеза, конечно...
Читаем в таком порядке: 0, –1, ...
Процедура (A): Даем произвольное определение вектора.
-3. (Что такое "отрезок"?) множество точек; (Что такое "разные концы"?) точка-начало, точка-конец.
-2. (что такое "стрелка"?) суть отрезок с разными концами.
-1. вектор суть стрелка.
=0======= Противоречие ===========
Определение вектора закончено. Переход на процедуру (B) построения объекта, который получил определение в (A).
Пояснение. В отрицательную сторону мы строим высказывание, уточняющее начальное, назовем его "seed". Например, "

суть число." или "Вектор суть стрелка." Высказывание простое, типа заголовка, просто точка входа в алгоритм. В положительную сторону строятся умозаключения из уточняющих высказываний. Умозаключения могут быть сложнее, чем в два слова.
Процедура (B): Построение Точки-начала.
=0. Можно построить точку-начало.
+1. Из 0. следует, что "точка-начало" отличается от остальных "просто-точек". В определении не задано отношение к другим точкам. Неопределенность. Возврат к задаче определения (A).
Процедура (A): уточнение.
-5. вектор суть множество точек линии, кратчайшей между двумя точками с заданными координатами в декартовой системе с указанными началом-концом.
-4. вектор суть множество точек прямой; точки: "начало", "конец" — их координаты.
Определение закончено. Переход к задаче построения объекта, (B).
...
На этом прервусь, слишком много для одного раза. Шаги алгоритма утрированы, строгость принесена в жертву читаемости.