11.4.4: Історія логіки речень

Sentential Logic була створена в 225 році до н.е. давньогрецьким логіком Хрисіппом. Це знання логіки було втрачено в темних віках, але було знову відкрито французьким філософом Абеларом в 12 столітті. Система таблиць істини для Sentential Logic була винайдена в 1902 році американським логіком Чарльзом Пірсом, щоб відобразити, як істинність одних речень вплине на правду інших. Таблиці правди були знову відкриті самостійно Людвігом Вітгенштейном та Емілем Постом.

Ми не досліджували систему доказів у цій книзі, але система доказів для Sentential Logic була розроблена в 1879 році німецьким логіком Готтлобом Фреге, щоб ми могли створювати докази, аналогічні доказів у плоській геометрії, в якій правила висновку e та аксіоми використовуються для висновку речення з раніше встановленого речення, не знаючи нічого про те, які речення є істинними. Доказ - це список пропозицій, послідовність кроків. Типовим правилом висновку є modus ponens:

З будь-яких двох кроків доказу, що мають форми P, а також P→Q, ви можете додати новий крок форми Q.

Речення P і Q можуть бути складними; вони не повинні бути простими літерами речення. При застосуванні того чи іншого правила умовиводу немає необхідності знати або згадувати істинно-значення задіяних пропозицій. Доказову систему для логіки речень часто називають сентенціальним обчисленням. Якщо Sentential Logic йде замість імені Пропозиційна логіка, то її система доказів називається Пропозиційне обчислення.

Будь-який аргумент, який може бути показаний дійсним методом таблиць істинності, також є тим, чий висновок можна довести з його передумов, використовуючи аксіом та правила висновку в системі доказування. Це властивість Sentential Logic називається повнотою. Повнота речення була вперше доведена американським логіком Емілем Постом в 1921 році.

Sentential Logic також має зворотну властивість, що будь-який аргумент, який є доказовим, також є дійсним. Отже, обгрунтованість і доказовість приходять до одного і того ж в тому сенсі, що сукупність аргументів, які є дійсними, також є сукупністю аргументів, висновок яких можна довести з його передумов.

Коли існує механічний метод, який в принципі міг би відповісти на всі питання певного роду, ніколи не даючи неправильної відповіді і завжди даючи певну відповідь в кінцевий час і ніколи не покладаючись на ймовірність або творчість, метод, як кажуть, вирішує питання. Метод таблиці істинності може бути використаний для вирішення питання про те, які пропозиції Sentential Logic є логічними істинами, тобто тавтологіями. Ми також робимо точку, кажучи логічну правду в Sentential Logic можна вирішити. Питання про те, чи є довільна послідовність символів добре сформованим пропозицією Sentential Logic, також є вирішальним. Чи можете ви уявити, як розробити комп'ютерну програму, яка, коли дається введення будь-якого рядка символів, завжди правильно скаже вам, чи це добре сформоване речення в Sentential Logic?

Комп'ютери є логічними машинами в двох сенсах: їх електронний дизайн відповідає основним принципам символічної логіки, а їх програми також засновані на принципах символічної логіки. Перша мова програмування еволюціонувала з формальної мови для символічної логіки.

Тризначна логіка була винайдена британським логіком Х'ю Макколлом в 1906 році. Ян Лукасевич був ще одним раннім прихильником тризначної логіки. Він прочитав «прощальну лекцію» в Варшавському університеті в 1918 році, в якій різко оголосив: «Я оголосив духовну війну з усім примусом, який обмежує вільну творчу діяльність людини». Логічною формою цього примусу, на думку Лукасевича, була Аристотелівська логіка, яка обмежувала судження істинними чи хибними. Його власною зброєю в цій війні була тризначна логіка.