Передмова

Ця книга є вступом в металогіку, орієнтоване особливо на студентів інформатики та філософії. «Металогіка» так називається тому, що саме дисципліна вивчає саму логіку. Логіка власне стосується канонів дійсного висновку, і його символічна або формальна версія представляє ці канони, використовуючи формальні мови, такі як пропозиції та присудок, він же, логіка першого порядку. Мета-логіка досліджує властивості цих мов та канони правильного висновку, які їх використовують. Він вивчає такі теми, як надати точне значення виразам цих формальних мов, як обґрунтувати канони дійсного висновку, які властивості різних доказових систем, включаючи їх обчислювальні властивості. Ці питання є важливими та цікавими самі по собі, оскільки досліджувані мови та системи доказування застосовуються у багатьох різних областях - у математиці, філософії, інформатиці та лінгвістиці, особливо - але вони також служать прикладами того, як вивчати формальні системи загалом. Логічні мови, які ми вивчаємо тут, не єдині, які цікавляться людьми. Наприклад, лінгвісти та філософи цікавляться мовами, які є набагато складнішими, ніж мови пропозиції та логіки першого порядку, а інформатики цікавляться іншими мовами взагалі, такими як мови програмування. І методи, які ми тут обговорюємо - як дати семантику формальних мов, як довести результати про формальні мови, як досліджувати властивості формальних мов - застосовні і в цих випадках.

Як і будь-яка дисципліна, металогіка має як набір результатів або фактів, так і магазин методів і прийомів, і цей текст охоплює обидва. Деяким студентам не потрібно знати деякі результати, які ми обговорюємо поза цим курсом, але їм знадобляться і використовувати методи, які ми використовуємо для їх встановлення. Теорема Левенгейма-Сколема, скажімо, не часто з'являється в інформатиці, але методи, які ми використовуємо, щоб довести це, роблять. З іншого боку, багато результатів, які ми обговорюємо, мають актуальність для певних дебатів, скажімо, у філософії науки та метафізики. Студентам філософії, можливо, не потрібно мати можливість довести ці результати поза цим курсом, але вони повинні зрозуміти, які результати - і ви дійсно розумієте ці результати лише в тому випадку, якщо ви продумали визначення та докази, необхідні для їх встановлення. Частково це причини, чому результати та методи, висвітлені в цьому тексті, рекомендуються вивчення—у деяких випадках навіть потрібно - для студентів інформатики та філософії.

Матеріал ділиться на три частини. Частина 1 стосується самої теорії множин. Логіка та металогіка історично пов'язані дуже тісно з тим, що називається «основами математики». Математичні основи стосуються того, як в кінцевому підсумку слід розуміти математичні об'єкти, такі як цілі числа, раціональні та дійсні числа, функції, пробіли тощо. Теорія множин дає одну відповідь (є й інші), і тому теорія множин і логіка вже давно вивчаються пліч-о-пліч. Множини, відносини та функції також є повсюдними в будь-якому формальному розслідуванні, не тільки в математиці, але і в інформатиці та в деяких з більш технічних куточків філософії. Звичайно, для цілей формулювання та доведення результатів про семантику та теорію доказів логіки та основи обчислюваності важливо мати мову, якою це робити. Наприклад, ми поговоримо про множини виразів, зв'язки наслідків та доказовості, інтерпретації символів предикатів (які виявляються відносинами), обчислювані функції та різні відносини між ними та конструкціями. Буде добре мати стенографічні символи для них, і продумати загальні властивості множин, відносин і функцій для того, щоб зробити це. Якщо ви не звикли мислити математично і формулювати математичні докази, то подумайте про першу частину з теорії множин як про навчальний полігон: будуть дані всі основні визначення, і ми наведемо все більш складні докази, використовуючи їх. Зауважте, що розуміння цих доказів - і можливість самостійно їх знайти і сформулювати - мабуть, важливіше, ніж розуміння результатів, особливо в першій частині, і особливо якщо ви новачок у математичному мисленні, важливо продумати приклади та проблеми.

Однак у першій частині ми встановимо один важливий результат. Цей результат - теорема Кантора - спирається на один з найяскравіших прикладів концептуального аналізу, який можна знайти в будь-якій точці наук, а саме на аналіз нескінченності Кантора. Нескінченність спантеличувала математиків і філософів протягом століть. Ніхто не знав, як правильно про це думати. Багато людей навіть вважали помилкою думати про це взагалі, що поняття нескінченного предмета або нескінченної колекції саме по собі незв'язне. Кантор перетворив нескінченність в предмет, з яким ми можемо злагоджено працювати, і розробив цілу теорію нескінченних колекцій - і нескінченних чисел, за допомогою яких ми можемо вимірювати розміри нескінченних колекцій - і показав, що існують різні рівні нескінченності. Ця теорія «трансскінченних» чисел красива і заплутана, і ми не заглибимося дуже далеко в неї; але ми зможемо показати, що існують різні рівні нескінченності, зокрема, що існують «лічильні» та «незліченні» рівні нескінченності. Цей результат має важливі програми, але це також дійсно той результат, який повинен знати будь-який поважаючий себе математик, інформатик або філософ.

У другій частині переходимо до логіки першого порядку. Визначимо мову логіки першого порядку та її семантику, тобто, що таке структури першого порядку і коли речення логіки першого порядку вірно в структурі. Це дозволить нам зробити дві важливі речі: (1) Ми можемо визначити з математичною точністю, коли речення є логічним наслідком іншого. (2) Ми також можемо розглянути, як відносини, що складають структуру першого порядку, описуються - характеризуються реченнями, які є істинними в них. Це, зокрема, призводить нас до обговорення аксіоматичного методу, в якому речення мов першого порядку використовуються для характеристики певних видів структур. Теорія доказів займе нас далі, і ми розглянемо оригінальний варіант послідовного числення та природного дедукції, визначеного в 1930-х роках Герхардом Гентценом. (Ваш інструктор може вибрати, щоб охопити лише один, тоді будь-яке посилання на «похідні» та «доказовість» означатиме будь-яку систему, яку вони обрали.) Смислове поняття слідства та синтаксичне поняття доказовості дають нам два абсолютно різні способи зробити точним уявлення про те, що речення може випливати з деяких інших. Теореми про обґрунтованість та повноту пов'язують ці дві характеристики. Зокрема, ми доведемо теорему про повноту Геделя, яка стверджує, що всякий раз, коли речення є смисловим наслідком деяких інших, там воно також є доказовим з них. Еквівалентним формулюванням є: якщо сукупність речень є послідовною - в тому сенсі, що нічого суперечливого з них не можна довести - тоді існує структура, яка робить всі вони правдивими.

Друга формулювання теореми повноти, мабуть, більш дивовижна. Приблизно в той час, коли Гедель довів цей результат (у 1929 році), німецький математик Девід Гільберт хвацько дотримувався думки, що послідовність (тобто свобода від суперечності) - це все, що вимагає математичне існування. Іншими словами, всякий раз, коли математик може узгоджено описати структуру або клас структур, то вони повинні мати право вірити в існування таких структур. У той час багато хто вважав цю ідею безглуздою: просто тому, що ви можете описати структуру, не суперечивши собі, це точно не випливає, що така структура насправді існує. Але це саме те, що говорить теорема про повноту Геделя. На додаток до цього парадоксального - і, безумовно, філософськи інтригуючого аспекту, теорема про повноту також має два важливих застосування, які дозволяють нам довести подальші результати про існування структур, які роблять дані речення істинними. Це компактність і теореми Левенгейма-Сколема.

У третій частині ми пов'язуємо логіку з обчислюваністю. Знову ж таки, існує історичний зв'язок: Девід Гільберт поставив як фундаментальну проблему логіки, щоб знайти механічний метод, який би вирішував із даного речення логіки, чи має він доказ. Такий метод існує, звичайно, для логіки пропозиції: треба просто перевірити всі таблиці істинності, а оскільки їх лише нескінченно багато, то метод в кінцевому підсумку дає правильну відповідь. Такий простий метод неможливий для логіки першого порядку, так як кількість можливих структур нескінченно (а самі структури можуть бути нескінченними). Логіки роками працювали над пошуком більш геніальних методів. Алонзо Черч і Алан Тьюринг врешті-решт встановили, що такого методу немає. Для того щоб це зробити, необхідно було спочатку дати точне визначення того, що таке механічний метод взагалі. Якби була запропонована процедура прийняття рішення, імовірно, вона була б визнана ефективним методом. Щоб довести, що ефективного методу не існує, потрібно спочатку визначити «ефективний метод» і дати докази неможливості на основі цього визначення. Ось що зробив Тьюринг: він запропонував ідею машини Тьюринга ¹ як математичної моделі того, що може, в принципі, зробити механічна процедура. Це ще один приклад концептуального аналізу неформальної концепції з використанням математичної техніки; і це, мабуть, такий же порядок важливості для інформатики, як аналіз нескінченності Кантора для математики. Наше останнє велике починання буде доказом двох теорем про неможливість: ми покажемо, що так звана «проблема зупинки» не може бути вирішена машинами Тьюринга, і, нарешті, що «проблема рішення» Гільберта (для логіки) також не може.

Цей текст є математичним, в тому сенсі, що ми обговорюємо математичні визначення і доводимо свої результати математично. Але це не математичне в тому сенсі, що вам потрібні великі математичні базові знання. Ніщо в цьому тексті не вимагає знань алгебри, тригонометрії або числення. Ми доклали особливих зусиль, щоб також не вимагати ніякого знайомства з тим, як працює математика: насправді, частина справи полягає в тому, щоб розвинути види міркувань та доказових навичок, необхідних для розуміння та доведення наших результатів. Організація тексту слідує за математичною конвенцією, з однієї причини: ці конвенції були розроблені, оскільки чіткість і точність особливо важливі, і тому, наприклад, критично важливо знати, коли щось стверджується як висновок аргументу, пропонується як причина чогось іншого, або призначений для введення нового словникового запасу. Тому ми дотримуємося математичних угод і позначаємо уривки як «визначення», якщо вони використовуються для введення нової термінології або символів; і як «теореми», «пропозиції», «леми» або «наслідки», коли ми записуємо результат або знахідку. Окрім цих умовностей, ми будемо використовувати методи логічного доказування, які вже можуть бути знайомі з першого логічного курсу, а також широко використовуємо метод індукції для доведення результатів. Дві глави додатка присвячені цим методам доказів.