September 2nd, 2021

P≠NP. Якобы решение.

Проблема перебора: равны ли классы задач P и NP? 1 миллион долларов за решение.
P=?NP - одна из семи проблем тысячелетия.
https://ru.wikipedia.org/wiki/Задачи_тысячелетия

===
Верно ли, что P=NP?
Ответ: P≠NP.
Доказательство: простая идея, по сути диагональный аргумент Кантора.
---
Примечание.
Могу ошибаться, не моя область. В таких вещах требуется аккуратность, поэтому это всего лишь идея. Кроме того, я мог уже забыть какие-то существенные детали и нюансы определений или просто их когда-то неверно понял, да еще и забыл. )
---
Идея доказательства.
Требуется построить задачу состоящую из подзадач, каждая из которых требует полного перебора, а число этих подзадач растет экспоненциально.

Берем математическую структуру, порождающую случайность (МСПС).
Генерируем со скоростью быстро растущей функцией последовательность вышеуказанных МСПС(k), зависящих от параметра k.
Этим шагом мы гарантируем отсутствие решений за полиномиальное время по причине того, что требуется каждый раз проверять всё множество пространства возможных решений, которое растет очень быстро.
Случайность гарантирует отсутствие "трюков" по нахождению решений иных, кроме полного перебора.
Следовательно, P≠NP.
===
Пример быстро растущей функции
https://ru.wikipedia.org/wiki/Функция_Аккермана
---
Пример математической структуры, порождающей случайность.
«Класс» уравнений порождается путём придания параметру k базового уравнения различных целочисленных значений.
диофантово уравнение k*x^2=2*k^2*y
где x,y неизвестные
k={1,2,3...} целочисленный параметр
оказывается число решений этого уравнения величина случайная.

Подробнее смотрите тут
Случайность в арифметике. ГРЕГОРИ ДЖ.ЧЕЙТИН
http://www.ega-math.narod.ru/Nquant/Random.htm
===

Комментарий. Популярная информация о задаче.
===
Проблема перебора (равны ли классы P и NP).

https://ru.wikipedia.org/wiki/Класс_NP
https://ru.wikipedia.org/wiki/Равенство_классов_P_и_NP
https://ru.wikipedia.org/wiki/Класс_PH
---

Проблема перебора. Александр Шень
https://postnauka.ru/faq/43795
Определение переборной задачи
Для начала надо объяснить, что такое переборная задача. Неформально можно сказать так: переборная задача — эта задача, в которой нужно найти объект, удовлетворяющий каким-то условиям. Причем эти условия легко проверить, но возможных кандидатов много. Пример такой задачи: есть ребус в виде кружков, соединенных линиями, и нужно расставить в кружках буквы А, Б и В (одну букву в каждом), причем требуется, чтобы кружки, соединенные линией, содержали разные буквы. Ясно, что когда буквы уже расставлены, то надо просто проверить условие для всех линий, это несложно. Зато вариантов расстановок очень много, и если перебирать их все, то это будет очень долго. Для этой задачи никакого существенно более быстрого способа пока не открыли. Существует такой способ или нет — в этом как раз и состоит проблема перебора.
---
https://rjlipton.wpcomstaging.com/2010/08/15/the-p%E2%89%A0np-proof-is-one-week-old/
The P≠NP “Proof” Is One Week Old
P ≠ NP «Доказательство» прошло неделю назад
15 АВГУСТА 2010 Г.
---

Список доказательств того, что P=NP, P!=NP, что проблема неразрешима, всего 116 штук. )
The P-versus-NP page
https://www.win.tue.nl/~gwoegi/P-versus-NP.htm
---

Карри-Говард для FOL

https://akuklev.livejournal.com/1296572.html

Карри-Говард для FOL
Как все тут знают, по соответствию Карри-Говарда интуиционистской логике высказываний (логике нулевого порядка) соотведствует просто-типизированное лямбда-исчисление с произведениями STLC.

Утверждениям в логике соответствуют типы в STLC, доказательствам утверждений — термы соответствующих типов. У STLC с произведениями есть прекрасная категорная семантика — декартово-замкнутые категории.

С логикой первого порядка всё чуть сложнее. Там кроме утверждений появляются предикаты и отношения — утверждения, зависимые от одной или нескольких переменных, которые тоже имеют свои типы, в зависимости от подлежащей теории. Например, если мы в рамках логики первого порядка описываем линейные пространства, у нас будут типы K скаляров и V векторов.

То есть тут у нас есть такие сущности:
– Типы элементов (например, скаляров и векторов), они образуют категорию с конечными (декартовыми) произведениями. Среди них выделенный тип “1” — нейтральный элемент произведений. Назовём эту категорию T, и в ней особо выделим проекции X ↠ Y (морфизмы, которые выделяют из произведения A × B ×···× D подпроизведение, скажем, B × C, и, опционально, меняют порядок аргументов).
– Типы предикатов P(x : T), где T какой-то тип элементов. Отношения суть предикаты на произведении нескольких элементарных типов отношений, например Id(p : T × T), а обыкновенные высказывания суть предикаты на 1. Если мы хотим чтобы у нас была логика первого порядка с равенством, то как раз постулируется что для каждого типа элементов автоматически есть предикат Id(x : T, y : T).
– Мы хотим, чтобы совокупность предикатов над одним и тем же типом была реализацией логики высказываний (т.е. категория предикатов над T была декартово замкнутой)
– Мы хотим, чтобы каждая проекция в категории элементов X ↠ Y порождала контравариантный функтор между категориями предикатов над Y и предиктов над X (это значит мы можем менять местами переменные у предикатов и добавлять переменные, которые никак не используются), сохраняющий структуру декартовой замкнутости.
— Далее мы хотим, чтобы у нас были кванторы — функторы сопряженные с вложениями слева и справа, соответственно предикаты P(x : X, y : Y) в предикаты (∀x,P)(y : Y) и (∃y,P)(y : Y). То есть мы уменьшаем количество переменных (можем уменьшить и до нуля, тогда получатся предикаты над единицей, то есть высказывания), замыкая убираемые переменные квантором всеобщности или существования.

Вот собственно и вся категорная семантика FOL, называются такие штуковины гипердоктринами (или, соответственно гипердоктринами с равенством, если требуются id-типы). Привожу определение по Pierre Clairambault, “From Categories with Families to Locally Cartesian Closed Categories”:

(картинка)

А вообще это классика, R. A. G. Seely, Hyperdoctrines, natural deduction, and the Beck condition, Zeitschrift für math. Logik und Grundlagen der Math., Band 29, 505-542 (1983).