Комплексная логика А. Зиновьева

[Dorje]

- на "самом деле" комплексная логика доказывает реальное существование более чем трех адекватных, взаимозаменяемых решений одной и той-же задачи..
Например - из пункта А в пункт Б через пункт С, или через пункт Д, или через пункт Е, или через....
Доказывает существование многомерности реальности.. Предоставляет возможность КОМПЛЕКСНОГО "подхода" при реализации идей..

[Sonic86]

Не понял, можно подробнее.
Вы специалист?

[AD]

Dorje в сообщении #180021 писал(а):

Доказывает существование многомерности реальности.

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

[Чудо-в-перьях]

Sonic86 писал(а):

О "Комплексной логике" Зиновьева А.А. Текст в скобках можно не читать.

Видимо, это книгу можно считать включающей все наиболее значительное и пока опубликованное у Зиновьева. (У Клини этого точно нет)

"Очерк многозначной логики" - довольно интересный и разнообразный раздел, но особого ничего не нашел . Для математиков - не знаю, вряд ли там что есть. Есть там некоторые мысли, которые полезно запомнить. Например, мысль о том, что истинностные значения логики есть некоторое построение, которое не является в ней обязательным - это изобретенное средство исследования. Есть мысль о "привилегированности" двузначной логики.

Раздел "Логическое следование" показался мне более глубоким с идейной точки зрения. Я смогу изложить только то, что понял. Автор рассматривает проблему логического следствия. Ее можно сформулировать так: нет в логике некоторой конструкции, которая более-менее удовлетворительно отражала понятие следования, в частности следствия в математике, которое привычно обозначают $\Rightarrow$. В терминологии Зиновьева: нет экспликации понятия "логического следования". В матлогике конструкцией, претендующей на такую роль является импликация $\to$, причем единственной.
(Лично я, когда мне показали таблицу истинности для импликации, очень удивился, что она - формальное описание понятия "следовательно". Я попробовал составить свою таблицу и у меня получилась конъюнкция! В общем с помощью таблиц истинности ничего другого и не подберешь. Потом быстро привык - противоречий-то не возникает.
Если есть математики, которые считают импликацю адекватной логическому следованию, то хотелось бы услышать аргументацию.)

Скажем, в ряде релевантных систем импликация (символ $\longrightarrow$ )как раз-таки и определяется через логическое следование, в системе R.
Вот эта теоремка (теорема следования):
A $\models$ B $\Leftrightarrow$ $\mathcal{j}\ A $\longrightarrow$ B $\mathcal{j}\ o = 1, где под $o$ понимается "выделенный", главный мир, под$\mathcal{j}\ A $\longrightarrow$ B $\mathcal{j}\ o = 1 -- значение импликативной формулы в указанном выделенном мире, а под $\models$ --семантический аналог логического следования ("Общезначимо"). 1 --это "истинно".
А классическая теорема дедукции? чем Вам не связь между логическим следованием ($\vdash$и импликацией, даже материальной импликацией (обычно ее записывают как $\supset$)?

Цитата:

Автор рассматривает существующие попытки решить эту проблему: импликация Рассела и Уайтхеда, сильная импликация Аккермана, логические системы Льюиса, Орлова, интуиционистская логика - и высказывает свою критику. Очень грубо говоря, ход экспликации идет так:
строится импликация как логическая конструкция, выясняется непротиворечивость хотя бы исчисления высказываний. Но при интерпретации формул импликации как высказываний естественного языка получается бессмыслица. Например, если $A,B$ - ложны, то $A \to B$ - истинно. Но если взять A="2+2=5", B="снег черный", то получаем, что высказывание "если 2+2=5, то снег черный" - истинно. Но по смыслу - выглядит как чепуха. Формулы, при интерпретации которых возможно получение таких бессмысленных высказываний, называются парадоксальными. Требуется построить исчисление, где есть знак $\vdash$ логического следования - здесь он читается именно так - где нет парадоскальных формул. При построении класса доказуемых формул должен быть сужением класса доказуемых соответствующих формул, где знак логического следования заменен на знак импликации. Автор попытки построить такое исчисление - в них не произошло исключение этого класса. Впрочем, само понятие "парадоксальная формула" оказывается строго не определенным. Автор перечисляет необходимые требования к логическому следованию, рассматривае разные варианты. Рассмотренны: значения истинности высказываний, принцип дедукции, связь посылки и следствия по смыслу - наличие общих для посылки и следствия терминов, логическое следование как конструкци метатеории (из "А" следует "В"), количество знаков логического следования в доказуемых формулах, аксиоматизация теории, парадоксальность интуиционистского следования. Причем, некоторые из них он, видимо, оставляет без последующего развития (если я правильно понял). В каких-то случаях он получает несколько вариантов, удовлетворяющих условиям - получаются разные исчисления. Наиболее строгое получается так: выбрасываются вообще все формулы, которые содержат хоть какой-то намек на парадоксальность, перечисляются набор допустимых схем и объявляется искомым исчислением. В целом есть некоторый ряд исчислений, ослабляющийся по непарадоксальности. Парадоксальные формулы оказываются недоказуемыми. В самом строгом исчислении оказываются доказуемыми формулы, которые автор считает бесперспективными для дедукции: $X \vdash X \vee \sim X, \sim X \wedge X \vdash X$, ... - автор считает их "законной платой за дедуктивный метод".
В разделе также есть конструкции для логики предикатов и для логики с кванторами, рассматривается теория терминов.
(Хочу от себя заметить, что мне кажется, что сложное терминологическое строение в матлогике отразить вообще нельзя)

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

Я не совсем поняла, в чем ход мысли А.А. Зиновьева отличается от рассуждений "релевантных" логиков--по-моему, они очень близки. Система напоминает формализацию первопорядкового релевантного следования.
Подробнее можно почитать здесь:
http://psi-logic.narod.ru/psi/rele.htm

[epros]

Чудо-в-перьях писал(а):

Sonic86 писал(а):

Раздел "Логическое следование" показался мне более глубоким с идейной точки зрения. Я смогу изложить только то, что понял. Автор рассматривает проблему логического следствия. Ее можно сформулировать так: нет в логике некоторой конструкции, которая более-менее удовлетворительно отражала понятие следования, в частности следствия в математике, которое привычно обозначают $\Rightarrow$. В терминологии Зиновьева: нет экспликации понятия "логического следования". В матлогике конструкцией, претендующей на такую роль является импликация $\to$, причем единственной.

Скажем, в ряде релевантных систем импликация (символ $\longrightarrow$ )как раз-таки и определяется через логическое следование, в системе R.
А классическая теорема дедукции? чем Вам не связь между логическим следованием ($\vdash$и импликацией, даже материальной импликацией (обычно ее записывают как $\supset$)?

Очевидно, что все эти "философские" проблемы в математической логике невыразимы.
Связь между импликацией и "логическим следованием" (правильнее говорить: "формальным выводом") определяется правилом modus ponens. Если в нашей логической системе есть такое правило, то с использованием импликации можно сделать формальный вывод. И наборот: доказать импликацию, не зная предпосылки, можно только с помощью формального вывода.

Чудо-в-перьях писал(а):

http://psi-logic.narod.ru/psi/rele.htm

Ага, старый знакомый...

[Чудо-в-перьях]

epros писал(а):

Связь между импликацией и "логическим следованием" (правильнее говорить: "формальным выводом") определяется правилом modus ponens. Если в нашей логической системе есть такое правило, то с использованием импликации можно сделать формальный вывод. И наборот: доказать импликацию, не зная предпосылки, можно только с помощью формального вывода.

А если я введу такое правило вывода, скажем, в натуральном исчислении:
A $\supset$ B $\Rightarrow$ \neg$ A $\vee$ B под $\Rightarrow$ я подразумеваю знак перехода между посылками и заключением, то я смогу осуществлять формальный вывод без m.p. (добавив правило исключения дизъюнкции). А импликация тем временем будет присутствовать. Я даже смогу вводить ее по теор. дедукции

epros писал(а):

Чудо-в-перьях писал(а):

http://psi-logic.narod.ru/psi/rele.htm

Ага, старый знакомый...

там еще большее чудо?))

[epros]

Чудо-в-перьях писал(а):

А если я введу такое правило вывода, скажем, в натуральном исчислении:

Что значит "в натуральном исчислении"?

Чудо-в-перьях писал(а):

A $\supset$ B $\Rightarrow$ \neg$ A $\vee$ B под $\Rightarrow$ я подразумеваю знак перехода между посылками и заключением

Если я правльно понял, то $\supset$ здесь означает импликацию, а $\Rightarrow$ - формальный вывод?
Тогда я не понял смысла такого правила вывода. Вот у Вас есть доказанное $A$ и доказанное $A \supset B$, как Вы отсюда сделаете вывод $B$? У Вас будет только $\neg A \vee B$.

Чудо-в-перьях писал(а):

то я смогу осуществлять формальный вывод без m.p. (добавив правило исключения дизъюнкции).

А "правило исключения дизъюнкции" это что? Правильно ли я понял, что если у нас есть доказанные $A$ и $\neg A \vee B$, то по этому правилу мы можем сделать вывод $B$? Ну так это фактически и есть то же самое правило modus ponens. Только здесь Вы вместо того, чтобы изложить его одним правилом, изложили его двумя: Сначала принимаете правило "преобразования импликации в дизъюнкцию", а потом - правило "исключения дизъюнкции".

Чудо-в-перьях писал(а):

А импликация тем временем будет присутствовать. Я даже смогу вводить ее по теор. дедукции

Где будет присутствовать?

[TypucT]

Sonic86 писал(а):

5. Теория кванторов является полной и разрешимой. Наличие результатов Геделя о существовании оистинных, но недоказуемых высказываний с квантором всеобщности есть результат плохой логической обработки математической логики. В частности, необходимо принимать во внимание Исследователя - объекта, занимающегося выводом.

Для справки: в 1929 Пресбургер доказал полноту формальной арифметики без умножения (логические аксиомы + аксиомы для равенства и сложения), в 1930 году Геделем доказана полнота исчисления предикатов первого порядка (только логические аксиомы), а в 1931 - неполнота формальной арифметики (логические аксиомы + аксиомы для равенства, сложения и умножения).

[Чудо-в-перьях]

epros писал(а):

Чудо-в-перьях писал(а):

А если я введу такое правило вывода, скажем, в натуральном исчислении:

Что значит "в натуральном исчислении"?

Чудо-в-перьях писал(а):

A $\supset$ B $\Rightarrow$ \neg$ A $\vee$ B под $\Rightarrow$ я подразумеваю знак перехода между посылками и заключением

Если я правльно понял, то $\supset$ здесь означает импликацию, а $\Rightarrow$ - формальный вывод?
Тогда я не понял смысла такого правила вывода. Вот у Вас есть доказанное $A$ и доказанное $A \supset B$, как Вы отсюда сделаете вывод $B$? У Вас будет только $\neg A \vee B$.

Чудо-в-перьях писал(а):

то я смогу осуществлять формальный вывод без m.p. (добавив правило исключения дизъюнкции).

А "правило исключения дизъюнкции" это что? Правильно ли я понял, что если у нас есть доказанные $A$ и $\neg A \vee B$, то по этому правилу мы можем сделать вывод $B$? Ну так это фактически и есть то же самое правило modus ponens. Только здесь Вы вместо того, чтобы изложить его одним правилом, изложили его двумя: Сначала принимаете правило "преобразования импликации в дизъюнкцию", а потом - правило "исключения дизъюнкции".

Чудо-в-перьях писал(а):

А импликация тем временем будет присутствовать. Я даже смогу вводить ее по теор. дедукции

Где будет присутствовать?

В нат. исчислении -- в одной из систем натурального, или т.н. "естественного" вывода.
Да, Вы правы насчет импликации--действительно получается m.p. в завуалированном виде(именно такое правило исключения дизъюнкции я имела в виду). Однако мои коллеги даже как-то разрабатывали такую вещь. чтобы доказвать импликации именно через дизъюнкции--прикладными целями объяснялось такое "неэкономное" применение.
Ммммм, ну как где присутствовать? В моем примере-- в натуральном выводе. Там же импликация вводится по доказанному консеквенту. Антецедент--последнее неисключенное допущение.
Просто мне непривычна мысль , что импликацию связывает с формальным выводом лишь m.p.

Добавлено спустя 9 минут 16 секунд:

Вот исчисление секвенций-- там как раз аналог теоремы дедукции используется для введения импликации. Разве в секвенциальных исчислениях у нас происходит нечто отличное от формального вывода?
(Я хочу сказать, что импликацию и формальный вывод роднит еще и Теорема следования(дедукции)). При ее доказательстве тот факт , что нек-рая формула получена по m.p., явялется одним из индуктивных случаев, так что теоремы следования не могут сводиться к правилам удаления импликации (m.p).

Добавлено спустя 2 минуты 30 секунд:

По крайней мере. в натуральных исчислениях формальный вывод присутствует 100%.

[epros]

Чудо-в-перьях писал(а):

В нат. исчислении -- в одной из систем натурального, или т.н. "естественного" вывода.

Ну, я не берусь судить о том, какие из систем вывода являются "естественными".

Чудо-в-перьях писал(а):

Ммммм, ну как где присутствовать? В моем примере-- в натуральном выводе. Там же импликация вводится по доказанному консеквенту. Антецедент--последнее неисключенное допущение.
Просто мне непривычна мысль , что импликацию связывает с формальным выводом лишь m.p.

Системы исчисления высказываний могут быть самыми разнообразными и даже весьма экзотическими. В них не обязательно должно использоваться правило mp, и тогда значок импликации может иметь совсем другой (может быть весьма неожиданный) "смысл". Но если уж такое правило вывода у нас есть, то в данном исчислении значок импликации означает именно "выводимость".

Чудо-в-перьях писал(а):

Вот исчисление секвенций-- там как раз аналог теоремы дедукции используется для введения импликации. Разве в секвенциальных исчислениях у нас происходит нечто отличное от формального вывода?

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

[luitzen]

epros писал(а):

Очевидно, что все эти "философские" проблемы в математической логике невыразимы.

Смотря что понимать под «математической логикой».

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

У нас же из-за разных исторических причин мнение о том, что всякая логика является математической по методу, менее общепринято. Соответственно, математической логикой объявляется всего-навсего логика, математическая по методу. Но при этом как-то забывается об исследовании систем, поверх которых содержательная матеиматика вряд ли может быть построена, но иследование которых является делом вполне строгим и интересным.

Так что, если понимать математическую логику по-западному, то, в самом деле, места для «всех этих философских вопросов» в ней нет. Она, насколько это возможно, заточена под обслуживание нужд работающих математиков. Если же понимать её по-русски и честно, то очень даже есть.

epros писал(а):

Связь между импликацией и "логическим следованием" (правильнее говорить: "формальным выводом") определяется правилом modus ponens.

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

epros писал(а):

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

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

TypucT писал(а):

Для справки: в 1929 Пресбургер доказал полноту формальной арифметики без умножения (логические аксиомы + аксиомы для равенства и сложения), в 1930 году Геделем доказана полнота исчисления предикатов первого порядка (только логические аксиомы), а в 1931 - неполнота формальной арифметики (логические аксиомы + аксиомы для равенства, сложения и умножения).

Для справки: рукопись Über formal unentscheidbare Sätze… поступила в редакцию в декабре 1930 года.

[epros]

luitzen писал(а):

Но при этом как-то забывается об исследовании систем, поверх которых содержательная матеиматика вряд ли может быть построена, но иследование которых является делом вполне строгим и интересным.

Намекнули бы хотя бы о чём речь.

luitzen писал(а):

Так что, если понимать математическую логику по-западному, то, в самом деле, места для «всех этих философских вопросов» в ней нет.

Собственно, в том комментарии я высказался относительно интерпретаций "смысла" импликации. С моей точки зрения "смысл" понятиям мы придаём тогда, когда находим им какое-то применение. Поэтому стандартный смысл у импликации появляется именно в связи с использованием её для выводов (доказательств) в рамках теорий. Но можно, конечно, этот значок и как-то иначе интерпретировать. Не думаю, что это имеет какое-то отношение к "западной" или "русской" традиции.

luitzen писал(а):

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

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

luitzen писал(а):

И далась людям эта импликация… Можно выкинуть её и MP

Вот именно.

[Sonic86]

Чудо-в-перьях! Спасибо за внимание!
Я здесь уже понял, что есть разные логические системы (друг друга не опровергающие), в которых пара понятий "импликация - логическое следование" определяется по-разному. Видимо, таковой является и упоминаемая Вами система $R$. И действительно, то же самое имеет место в матлогике, которую учат в универе: $A \vdash B \Lefgtrightarrow \vdash (A \to B)$. У Зиновьева они различны.
В принципе определения можно придумывать достаточно отфонарно и получать много разнообразных логик с различными определениями пары понятий "импликация - логическое следование". Зиновьев делает так: он берет некий стихийный (неформальный) навык обращения со словом естественного языка "следует", "логически следует" и пытается его формализовать, эксплицировать - построить определение, которое было бы наиболее близко к интуитивному пониманию этого слова. Поэтому он обращается к парадоксальным формулам и
высказываниям типа "Если 2+2=5, то снег черный". Операция формализации неформальна, поэтому опровергать ее с позиций логики нельзя в принципе. Ее можно только проверить практикой - годится ли для чего-то или нет? Но для этого нужен какой-то специфический опыт, а у меня его нет.
У Зиновьева было $x \to y \equiv \sim x \vee y$ ($\sim$ - т.н. внешнее отрицание, для которого верен закон исключенного третьего). А для $\vdash$ было такое:
Система $Z^1$
1) $x \vdash \sim \sim x$
2) $\sim \sim x \vdash x$
3) $xy \vdash x$
4) $xy \vdash yx$
5) $xyz \vdash x(yz)$
6) $x^1 ... x^n \vdash a$, где $a$ - перестановка $x^1...x^n$
7) $\sim (xy) \vdash (x \sim y) : (\sim xy) : (\sim x \sim y)$ ($:$ - либо)
8) $\sim (x:y) \vdash xy : \sim x \sim y$
9) $\sim (x^1 : ... : x^n) \vdash a^1 : ... : a^k$, $a^1 : ... : a^k \vdash \sim (x^1 : ... : x^n)$, где $a^1 : ... : a^k$ - множество формул, разделенных :, в которое включается $x^1...x^n$ и всевозможные формулы, которые отличаются от нее наличием $\sim$ перед всеми $x^1,...,x^n$ или перед $x^i, i=1...n-2$.
10) $x^1 : ... : x^n \vadsh a$, где а отличается от поссылки расстановкой скобок
11) $b \vdash a^1 ... a^n$, где $a^j$ имеет вид либо $\sim x x$, либо $a^{i1}x^1...a^{im}x^m$, где $a^{i1},...,a^{im}$ означают наличие или отсутствие $\sim$, и все $a^{i1}x^1...a^{im}x^m$ попарно
различаются лишь числом и расположением $\sim$, $b$ отличается от $a^1:...:a^n$ лишь расстановкой скобок.
12) $xz:yz \vdash (x : y)z$, $x^1y:...<!-- s:x --><img src=\\
13) $(x:y)z \vdash xz:y$, $(x^1:...<!-- s:x --><img src=\\.
Правила вывода в $Z^1$:
1) подстановка в переменную
2) если $a \vdash b$ и $b \vdash a$ и $d$ получается из $c$ путем замены вхождения $a$ формулой $b$, то
$c \vdash d$
3) если $a \vdash b$ и $b \vdash c$, то $a \vdash c$
4) если $a \vdash b$ и $a \vdash c$, то $a \vdash bc$
И формула доказуема $\Leftrightarrow$ она аксиома или выводима по правилам и только в этом случае.
Тогда в $Z^1$ недоказуемы формулы:
$\sim x x \vdash y$, $x \vdash \sim (\sim y y)$, $x \vdash (y \to x)$, $x \vdash (\sim x \to y)$, $x \vdash y : \sim y$.
Отсюда следует, что $a \vdash b$ доказуема в $Z^1$ $\Leftrightarrow$ формула $a \to b$ - тавтология двузначной логики и в $b$ фходят те и только те пропозициональные переменные, которые входят в $a$.
epros вот тоже правильно пишет: "Очевидно, что все эти "философские" проблемы в математической логике невыразимы". Но они выразимы в опыте. Тут вот в соседней теме ругают конструктивистов, но доказать, что "конструктивизм хуже классической математики" тоже нельзя
Хотя... можно такую "философскую" проблему поставить: "если а то b" $\equiv a \to b$ или нет И потом сказать, что она в логике тоже не формализуема.

Турист! Спасибо за справку! Меня лично интригует такое высказывание автора, но я его толком не понимаю, поэтому повторюсь: нужно мнение специалиста - полезно ли, тривиально ли или нет.

З.Ы. А при чем тут "верующий-неверующий"?

[luitzen]

epros писал(а):

Намекнули бы хотя бы о чём речь.

Есть такое устойчивое словосочетание «неклассические логики». Критерием неклассичности обыкновенно объявляется отказ (как изначальная задумка или как следствие каких-то других задумок) от тех или иных законов логики. Не претендуя на классификацию, обычно упоминают несколько разновидностей: интуиционистские, паранепротиворечивые, релевантные…

Можно ещё говорить о «нетрадиционных логиках» — тех, в которых синтаксис слегка или не слегка отличен от привычного нам. Здесь следует упомянуть модальные системы, всяческую прототетику и т. п. Нетрадиционные логики могут быть неклассическими, а могут, наверное, и не быть.

Изучать все эти неклассические/нетрадиционные логические системы можно по отдельности, а можно и скопом.

По отдельности — это если у них есть шанс обрести важные приложения. К примеру, какая-нибудь система с деонтическими модальностями в будущем глядишь, и ляжет в основу автоматического правосудия .

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

epros писал(а):

С моей точки зрения "смысл" понятиям мы придаём тогда, когда находим им какое-то применение. Поэтому стандартный смысл у импликации появляется именно в связи с использованием её для выводов (доказательств) в рамках теорий. Но можно, конечно, этот значок и как-то иначе интерпретировать. Не думаю, что это имеет какое-то отношение к "западной" или "русской" традиции.

Мною были перечислены логические системы, которые относятся к математической логике в «честном отечественном» её понимании, но не относятся в «западном».

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

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

[epros]

Sonic86 писал(а):

Хотя... можно такую "философскую" проблему поставить: "если а то b" $\equiv a \to b$ или нет И потом сказать, что она в логике тоже не формализуема.

Это прекрасно формализуется на уровне мета-теории:
$(T \vdash a) \rightarrow (T \vdash b) \equiv (T \vdash a \rightarrow b)$,
где $T \vdash$ означает: "доказуемо в предметной теории $T$".

Только это неверно.

luitzen писал(а):

В этих системах тоже есть понятие логического вывода, но применениями они имеют не математику, а какие-то другие сферы деятельности.

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

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

luitzen писал(а):

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

Я не вкладывал в слово "стандартный" какой-то особый смысл. Только то, что речь идёт об "особом месте среди прочих". Можно, конечно, под импликацией $a \rightarrow b$ понимать какую-нибудь совсем уж нетривиальную вещь, например, что высказывание $b$ является подстрокой высказывания $a$, но согласитесь, что это будет уже сильно "нестандартное" понимание импликации.