Выводятся ли таблицы истинности логических связок из аксиом логики высказываний?

(Я собираюсь собрать много хороших моментов из комментариев.)

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

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

К сожалению, логика высказываний слишком бедна для описания любого интересного математического утверждения. Наилучшая попытка использования таблиц истинности для кванторов состоит в том, чтобы интерпретировать кванторы как логические связки, охватывающие всю область дискурса. Например,$\forall x P(x)$когда областью дискурса являются натуральные числа, это означает$P(0)\land P(1)\land P(2)\dots$и так далее для всех натуральных чисел. Поскольку множество всех натуральных чисел бесконечно, мы не можем вычислить истинное значение$\forall x P(x)$. Таблицы истинности нецелесообразны для логики с кванторами, например для любой логики первого порядка.

Цитата из учебника «Введение в математическую логику» Эллиотта Мендельсона (2015 г., 6-е изд., глава 2.3 «Теории первого порядка»), в которой подробно рассматриваются трудности вычислительного подхода к истине.

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

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

Поскольку многие системы вывода были изобретены во время формализации математики, возникает естественный вопрос, какая из них лучше. Для того, чтобы решить это, нам нужно знать их свойства и сравнить их. Это делается в теоретической математической логике. Для изучения систем вывода были введены формальные определения правильно построенной логической формулы и доказательства. Логические связки — это всего лишь синтаксические конструкции, символы. Затем было введено понятие семантики (интерпретации) логических связок и кванторов. Таблицы истинности являются частью семантики. Семантика помогает доказать утверждения о доказуемости. Семантика — это теоретическое определение логических связок. Это ответ на вопрос, зачем нужны таблицы истинности.

Обратите внимание, что все изучение систем вывода происходит внутри системы вывода, принадлежащей метауровне. Эта система вывода обычно остается неявной, а рассуждения в ней записываются на естественном языке. Изучаемые системы вывода относятся к объектному уровню. Эти 2 уровня являются характерным свойством теоретической математической логики.

Взгляд на логические связки, который вы хотите принять, зависит от вашей цели. Если вы заботитесь о практическом доказательстве, значение логических связок определяется системами вывода. Семантика полезна для теоретических исследований, но не применима на практике.

Прежде всего, давайте определим аксиому.

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

На самом деле вы не ссылались на какую-либо правильно сформированную формулу (внимательно проверьте определение!), но это, вероятно, можно исправить, и это не меняет вопроса здесь.

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

Итак, я полагаю, вы, возможно, намеревались спросить, существует ли какой-то металогический способ вывести таблицы истинности, скажем, из набора аксиом (когда-то преобразованных в правильно сформированные формулы), на которые вы ссылались. Это повлечет за собой уникальность таблиц истинности как интерпретации аксиом. Однако существует следующая интерпретация связок, приписываемых Дмитрию Бочварю, где «Т» указывает на истинностное значение «истина», «N» — третье истинностное значение, а «F» — ложность.

$\lnot$Т = Ф

$\lnot$Н = Т

$\lnot$Ф = Т

(Т -> Т) = Т

(Т -> Н) = F

(Т -> Ф) = Ф

(Н -> Т) = Т

(Н -> Н) = Т

(Н -> Ф) = Т

(Ф -> Т) = Т

(Ф -> Н) = Т

(Ф -> Ф) = Т

Другими словами, если вы проведете расчеты с приведенным выше, вы увидите, что все аксиомы ранее упомянутого набора аксиом Лукасевича верны, а также правило отстранения. И никаких других новых тавтологий не следует.

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

Простой ответ на вопрос в шапке - да.

Когда вы читаете первоисточники, вы приходите к выводу, что не было никакого различия между "$=$" и "$\leftrightarrow$в ранних работах Фреге и Рассела. В то время как Фреге явно боролся с новым логическим исчислением, основанным на концепции функции, Рассел и Уайтхед работали над аксиоматическими системами.

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

Ваши последующие вопросы сложнее. Ответ зависит от вашей философии математики.

Нововведение Фреге заключалось в том, что он привнес понятие функции в логику. Таблицы истинности отражают «расширенное» представление функции, имеющей домен. Вот почему к связкам, связанным с классическими таблицами истинности, относятся с помощью определителя «материал». «Правда» и «Ложь» Фреге предназначены для рассмотрения как существующие объекты.

Но, поскольку инновация включает концепцию функции, можно аксиоматизировать логическую связность с «интенсиональным» представлением. Позвольте мне подчеркнуть логическую связность , потому что я не говорю о булевых полиномах.

Обозначим материальный бикондиционал через$LEQ$, и рассмотрим аксиому, заданную

Таблицы истинности для$OR$и$NAND$являются

Если теперь выполнить покомпонентное применение$XOR$,

получается таблица истинности для$LEQ$,

Конечно, чтобы реализовать это, нужно назвать все шестнадцать таблиц истинности.

Теперь можно понять систему как аппликативную структуру. Это требует, чтобы набор скобок интерпретировался с использованием либо$NOR$или$NAND$. То есть строка имён,

оценивает в соответствии с

В том же духе можно сформулировать магму, обрабатывая$NOR$и$NAND$как левое произведение и правое произведение, если установить соглашение для выражений вида$(A)$. Я считаю, что его следует интерпретировать как унарное отрицание.

Причина того, что все это зависит от чьей-либо философии математики, заключается в вопросе о том, что может служить основанием для изучения этой системы в рамках основ. Предположим, вы называете все шестнадцать таблиц истинности. Далее, предположим, что вы изучаете отрицания и спряжения де Моргана как инволюции в этой системе. Это разделит систему по определенному шаблону, и этот шаблон соответствует конечной аффинной геометрии в шестнадцати точках. Связанная с ним проективная плоскость имеет двадцать одну точку. В теории дизайна хорошо известно, что 21-точечная проективная плоскость уникальна с точностью до изоморфизма. Но современные основы возникают почти исключительно из арифметизации математики. Итак, эта геометрическая перспектива расходится с полученным представлением.

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

«Счет, психологически возникший из требований практической жизни, ввел ученых в заблуждение».

Другими словами, в основах математики есть некоторые вопросы, на которые вы можете ответить только сами.

@ Дуг Спунвуд

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

Аксиомы классического исчисления высказываний выполняются в любой булевой алгебре. Таким образом, может быть 4, 8, 16,... "истинных" значений.