Система L - System L

Система L это естественная дедуктивная логика разработан E.J. Лимон.[1] Полученный из Suppes 'метод,[2] это представляет естественный вычет доказательства как последовательности обоснованных шагов. Оба метода получены из Генцена 1934/1935 система естественного вычета,[3] в котором доказательства были представлены в виде древовидной диаграммы, а не в табличной форме Suppes и Lemmon. Хотя древовидная схема имеет преимущества для философских и образовательных целей, табличная структура намного удобнее для практических приложений.

Похожая табличная структура представлена ​​Клини.[4] Основное отличие состоит в том, что Клини не сокращает левые части утверждений до номеров строк, предпочитая вместо этого либо давать полные списки прецедентных утверждений, либо, в качестве альтернативы, указывать левые части полосами, идущими вниз слева от таблицы, чтобы указать зависимости. . Однако версия Клини имеет то преимущество, что она представлена, хотя и очень схематично, в строгих рамках метаматематической теории, тогда как книги Суппеса[2] и лимон[1] являются приложениями табличного макета для обучения вводной логике.

Описание дедуктивной системы

Синтаксис доказательства регулируется девятью примитивными правилами:

  1. Правило предположения (А)
  2. Modus Ponendo Ponens (MPP)
  3. Правило двойного отрицания (DN)
  4. Правило условного доказательства (CP)
  5. Правило ∧-введения (∧I)
  6. Правило ∧-исключения (∧E)
  7. Правило ∨-введения (∨I)
  8. Правило ∨-исключения (∨E)
  9. Reductio Ad Absurdum (RAA)

В системе L доказательство имеет определение со следующими условиями:

  1. имеет конечную последовательность правильные формулы (или wffs)
  2. каждая его строка обоснована правилом системы L
  3. последняя строка доказательства - это то, что предполагается, и эта последняя строка доказательства использует только те посылки, которые были даны, если таковые имеются.

Если посылка не указана, секвенция называется теоремой. Следовательно, определение теоремы в системе L таково:

  • Теорема - это секвенция, которую можно доказать в системе L, используя пустой набор предположений.

Примеры

Пример доказательства секвенции (Modus Tollendo Tollens в таком случае):

п → q, ¬q ⊢ ¬п [Modus Tollendo Tollens (MTT)]
Номер предположенияНомер строчкиФормула (wff)Используемые линии и обоснование
1(1)(п → q)А
2(2)¬qА
3(3)пA (для RAA)
1, 3(4)q1, 3, МПП
1, 2, 3(5)q ∧ ¬q2, 4, ∧I
1, 2(6)¬п3, 5, RAA
Q.E.D

Пример доказательства секвенции (в данном случае теорема):

⊢п ∨ ¬п
Номер предположенияНомер строчкиФормула (wff)Используемые линии и обоснование
1(1)¬(п ∨ ¬п)A (для RAA)
2(2)пA (для RAA)
2(3)(п ∨ ¬п)2, ∨I
1, 2(4)(п ∨ ¬п) ∧ ¬(п ∨ ¬п)3, 1, ∧I
1(5)¬п2, 4, RAA
1(6)(п ∨ ¬п)5, ∨I
1(7)(п ∨ ¬п) ∧ ¬(п ∨ ¬п)1, 6, ∧I
(8)¬¬(п ∨ ¬п)1, 7, RAA
(9)(п ∨ ¬п)8, DN
Q.E.D

Пример правила (конечного) увеличения помещений.[5] Строки 3-6 демонстрируют увеличение:

п, ¬п ⊢ q
Номер предположенияНомер строчкиФормула (wff)Используемые линии и обоснование
1(1)пA (для RAA)
2(2)¬пA (для RAA)
1, 2(3)п ∧ ¬п1, 2, ∧I
4(4)¬qA (для DN)
1, 2, 4(5)(п ∧ ¬п) ∧ ¬q3, 4, ∧I
1, 2, 4(6)п ∧ ¬п5, ∨E
1, 2(7)¬¬q4, 6, RAA
1, 2(8)q7, DN
Q.E.D

Каждое правило системы L имеет свои собственные требования к типу входных данных или записей, которые оно может принять, и имеет свой собственный способ обработки и расчета допущений, используемых его входными данными.

История табличных систем естественного вывода

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

  • 1940: В учебнике Куайн[6] указали предшествующие зависимости номерами строк в квадратных скобках, предвосхищая нотацию номеров строк Suppes 1957 года.
  • 1950: В учебнике, Куайн (1982, pp. 241–255) продемонстрировал метод использования одной или нескольких звездочек слева от каждой строки доказательства для обозначения зависимостей. Это эквивалент вертикальных полос Клини. (Не совсем ясно, появилась ли звездочка Куайна в оригинальном издании 1950 года или была добавлена ​​в более позднем издании.)
  • 1957: Введение в практическую логику доказательства теорем в учебнике Suppes (1999) С. 25–150). Это указывало на зависимости (т. Е. Предшествующие утверждения) номерами строк слева от каждой строки.
  • 1963: Столл (1979), pp. 183–190, 215–219) использует наборы номеров строк, чтобы указать предшествующие зависимости строк последовательных логических аргументов, основанные на правилах вывода естественного вывода.
  • 1965: Весь учебник Лимон (1965) представляет собой введение в логические доказательства с использованием метода, основанного на методе Suppes.
  • 1967: В учебнике, Клини (2002), pp. 50–58, 128–130) вкратце продемонстрировали два вида доказательств практической логики: одна система использует явные цитаты предшествующих утверждений слева от каждой строки, другая система использует вертикальные черточки слева для обозначения зависимостей.[7]

Смотрите также

Заметки

  1. ^ а б Увидеть Лимон 1965 для вводного изложения естественной дедуктивной системы Леммона.
  2. ^ а б Увидеть Suppes 1999, pp. 25–150, для введения в систему естественной дедукции Суппеса.
  3. ^ Гентцен 1934, Гентцен 1935.
  4. ^ Клини 2002 С. 50–56, 128–130.
  5. ^ Коберн, Барри; Миллер, Дэвид (октябрь 1977 г.). «Два комментария к логике начала Леммона». Журнал формальной логики Нотр-Дам. 18 (4): 607–610. Дои:10.1305 / ndjfl / 1093888128. ISSN  0029-4527.
  6. ^ Куайн (1981). См., В частности, стр. 91–93, где представлена ​​нотация номеров строк Куайна для предшествующих зависимостей.
  7. ^ Особое преимущество табличных систем естественного вывода Клини состоит в том, что он доказывает справедливость правил вывода как для исчисления высказываний, так и для исчисления предикатов. Увидеть Клини 2002 С. 44–45, 118–119.

использованная литература

внешние ссылки