Импликация Введение сформулировано как теорема?

Два разных символа на странице, на которую вы ссылаетесь, действительно разные. Первый - это символ турникета Ⱶ, который можно прочитать как «доказательство», в то время как стрелка → является материальным значением. Они очень разные. Материальная импликация — это символ на объектном языке, определяемый приведенной вами таблицей истинности, т. е. T/F/T/T. Турникет — это символ на метаязыке, который можно прочесть так: P доказывает Q или Q — теорема о P.

Правило условного введения можно понимать как означающее, что если Q — теорема о P, то P → Q — теорема. В более общем виде это можно было бы записать так: если Γ — множество предложений, то из Γ,P Ⱶ Q можно вывести Γ Ⱶ P → Q. Если Γ вместе с P доказывает Q, то Γ доказывает, что P материально влечет В. Это называется теоремой дедукции.

В естественной дедукции мы можем использовать правило условного доказательства с тем же эффектом. Вы можете принять любое P, которое вам нравится, перейти к доказательству Q на его основе, а затем опровергнуть предположение, чтобы ввести материальную импликацию P → Q.

Что касается логических констант, имеющих соответствующие правила введения и исключения, то это не случайно. В системе Fitch логические константы определяются этими правилами. Идея гармоничных правил введения и исключения была предложена Герхардом Генценом и подхвачена многими другими. Идея состоит в том, что соответствующие правила I и E должны быть «обратными» друг другу, чтобы гарантировать, что они не будут иметь неконтролируемых последствий. В знаменитой статье еще в 1960 году Артур Прайор («Билет вывода о малолитражке», анализ 21: 38-9) показал, что определение логических констант без ограничений может позволить вам доказать что угодно.

Эта обратная связь между правилами I и E называется логической гармонией. Майкл Даммет утверждал, что у классической логики нет гармоничного способа определения правил отрицания, в то время как у интуиционистской логики есть, хотя это оспаривается. Если вы хотите получить дополнительную информацию о логической гармонии, эти статьи могут быть вам полезны:

Стейнбергер, Ф. (2011) «Какой может и не может быть гармония». Австралазийский философский журнал 89: 617-639. Рамфит, Ян (2016) «Против гармонии». Готовится к публикации в издании Роберта Хейла, Криспина Райта и Александра Миллера, The Blackwell Companion to the Philosophy of Language, 2-е издание. Оксфорд: Блэквелл.

Я полагаю, что обе статьи можно найти на philpapers.org.

То, что можно рассматривать как введение импликации, →I , иногда называют условным доказательством или CP .

Основная стратегия состоит в том, чтобы принять антецедент и вывести следствие. Как только консеквент получен, допущение может быть снято. Вот пример:

{1} 1. (P ∨ Q) → R Prem.
{2} 2. П Предполож.
{2} 3. P ∨ Q 2 ∨ I (правая)
{1,2} 4. Р 1,3 МП
{1} 5. П → Р 2,4 КП

Антецедент предполагается в строке 2, а консеквент выводится в строке 4. Это соответствует условиям для → Введение или CP в строке 5.

В этой конкретной системе доказательств номера зависимостей перечислены слева. Везде, где появляется число {2} , это означает, что соответствующий номер строки зависит от предположения, сделанного в строке 2. Обратите внимание, что после введения импликации номер зависимости для предположения отменяется. Вы можете видеть, что вывод основан только на {1} , что является предпосылкой.

Другой символ:

Статья в Википедии гласит:

Правило modus ponens можно записать в последовательной записи:

Р → Q, Р ⊢ Q

где ⊢ — металогический символ, означающий, что Q — синтаксическое следствие P → Q и P в некоторой логической системе;

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

Как я упоминал в своем комментарии, отношение, выраженное ((A & (A → B)) → B), является принципом, управляющим как введением, так и исключением, поэтому одна и та же таблица истинности действительна для обоих.