July 31st, 2019

ДР Цертуса 2011

Карри-Говард для 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”:

Screen Shot 2019-07-30 at 15.03.07

А вообще это классика, 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).

марксоглупости с их ТТС (трудовая теория стоимости)

очередные марксоглупости с их ТТС (трудовая теория стоимости)

Сталинское искажения основного экономического закона социализма
https://yury-st.livejournal.com/320778.html

*** а такой, примерно, формулой: на основе совершенствования и развития производства, обобществленного в масштабе целого общества, и соответственного умножения фонда потребления - все более полное и неукоснительное осуществление экономического равенства всех членов общества, достижимого при системе оплаты труда по его количеству. Этот закон действителен и в социалистическом обществе и на пути к социалистическому обществу. В уже построенном социалистическом обществе этот закон действует без отклонений.

это как раз глубоко неверно и неправильно

ибо сказано

15 Бойтесь лжепророков! В овечьей шкуре приходят они к вам, нутром же они - волки хищные.
16 По делам* их узнаете, кто они. Разве собирают гроздья виноградные с терновника или с репейника смоквы?
17 Всякое хорошее дерево приносит добрые плоды, а плохое - худые.
18 Хорошее дерево не может приносить худых плодов, а плохое дерево - добрых плодов.
19 Всякое дерево, не приносящее добрых плодов, срубают и бросают в огонь.
20 Итак, по плодам их узнаете, кто они.

хоть я и атеист ))

Collapse )