Открытие против изобретения

В то время как телефон - изобретение, которое претерпевает изменения по мере развития науки с течением времени, гравитация - это открытие, которое является очень фундаментальным. Объяснение того, почему гравитация существует во Вселенной, время от времени меняется с объяснением, данным Ньютоном Эйнштейну, существование гравитации - это то, что заставляет нас приземлиться, является фундаментальной истиной. В том же духе люди спорят, изобретена ли математика или открыта. Сторона открытия говорит, что независимо от того, существует вселенная или нет, 2 + 3 всегда равно 5, и вселенная работает по определенным правилам. С точки зрения изобретательности математики утверждают, что математика изобретена человеческим мозгом, потому что ее сложность и математика работают безупречно.

Ignoramus et ignorabimus

Евклид аксиомитизировал геометрию с помощью определенного набора правил, которые хорошо себя зарекомендовали. И поэтому люди хотели формализовать всю математику на аналогичной основе. Давид Гильберт сделал одну такую ​​попытку. Существовала латинская цитата, обозначающая пределы научного знания,

Невежество и пренебрежение

что означает «мы не знаем и не будем знать». Гильберт сразу же придумал еще одну эпическую цитату на немецком языке, опровергая ее:

Wir müssen wissen.

Wir werden wissen.

что означает: «Мы должны знать, мы будем знать». Фактически Гильберт буквально унес эти строки в могилу. Таким образом, попытки формализовать математику проложили путь к развитию метаматематики.

Проблема Гильберта и Энтшайдунга

Гильберт предложил Entscheidungsproblem (также называемую проблемой принятия решения), которая заключается в утверждении, можно ли ответить на него «Да» / «Нет», который универсально действителен во всех контекстах с помощью алгоритма.

Решения Алонзо Черча и Алана Тьюринга

Поиски природы математики дали нам золотой 1936 год, когда проблема принятия решений получила отрицательный ответ, т.е. такого алгоритма не существует. Алонзо Черч придумал лямбда-исчисление и показал, что никакие два выражения в нем не могут быть эквивалентны. И в том же году Алан Тьюринг придумал машину Тьюринга и доказал существование проблемы остановки. Таким образом, проблема решения получила 2 ответа независимо.

Теорема Курта Гёделя о неполноте

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

Ключевой вывод теорем о неполноте состоит в том, что любая система, способная выполнять арифметику, является неполной, т. Е.

В системе могут быть утверждения, которые верны, но не могут быть подтверждены базовыми правилами, которые ее устанавливают

Это очень хорошо видно в сценарии Теории множеств и ее парадоксе. Хотя Курт Гёдель буквально доказал нечто столь фундаментальное для природы математики, процесс, в котором он это делал в свое время, буквально захватывает дух. Он преобразовал каждое логическое утверждение в числа, так что сама логика может быть сведена к логике арифметики (процесс, называемый нумерацией Гёделя). Хотя в его время это может показаться устаревшим, сейчас мы живем в мире, где каждая строка кода, который мы пишем, компилируется до байтов, которые буквально являются числами. Еще до того, как Алан Тьюринг «открыл» после Второй мировой войны «идею» языка программирования, Курт Гёдель как бы использовал для доказательства природы самой математики.

Наследие Курта Гёделя

После Второй мировой войны Гёдель переехал в США. Также он очень близкий друг Альберта Эйнштейна. Подавая заявку на получение гражданства страны в 1947 году, Гёдель сказал Эйнштейну, что в конституции США есть противоречие, которое может допускать диктатуру. Гёдель буквально продолжил формальную проверку законов конституции США и объяснил это судье, которое изучало его форму гражданства.

Дань наследию

Мы живем в эпоху языков программирования и систем статического типа. Хотя, как указал Гёдель, системы, способные к арифметике, неполны сами по себе. Итак, давайте проверим наши любимые языки на логике!

Парадоксальный оператор фиксированной точки с использованием лямбда-выражения

const Y = f => (x => x(x))(x => f(y => x(x)(y)))

А также, если вы используете строго типизированный язык, вы можете представить парадокс Лжеца в своей системе типов и доказать его несогласованность, то есть представить следующее предложение в системе типов

A: A неверно. Вышеупомянутое утверждение нельзя доказать как истинное / ложное. Но некоторые строго типизированные языки по-прежнему позволяют им давать противоречивые результаты. Как и приведенная ниже машинописная версия парадокса лжеца

// credit to Haskell implementation: https://www.cs.unm.edu/~stelleg/liar.html
type Not<X> = (x: X) => false
type Liar = {
    val: Not<Liar>
}
let liarIsFalse: Not<Liar> = (x: Liar) => x.val(x);
const absurd: false = liarIsFalse({
    val: liarIsFalse
});

И с Днем Рождения Курта Гёделя!