DV
Вот аксиоматика классической пропозициональной логики с импликацией и отрицанием
Size: a a a
2021 April 28
ДК
75 строка - это закодированное доказательство?
DV
первые два - это правила формальной грамматики, определяющие построение формул
DV
да, 75 - это скопрессированое доказательство.
DV
-. это отрицание, если чо
DV
Кстати я готовлю статейку на хабр про метамат - хочу объяснить популярно для народа как он работает. Текст уже есть, надо теперь картинки нарисовать.... уже второй год рисую
IK
А какие с ними сложности, какого типа картинки?
DV
ну там стековая машина, как она работает хорошо бы нарисовать. Я подумал что нарисовать на бумаге и отсканировать - это самый быстрый способ это сделать. А так сложность только в том, чтобы собраться и сделать
DV
лано, я домой пошел, отвечать смогу нескоро (завтра??...)
ДК
51 - сомнительное правило. Из истинности одного утверждения не следует, что оно следует из любого другого утверждения.
AT
Как жаль, что Гильберт уже умер и не узнает этого! 😞
ДК
Привет ему от релевантной импликации.
ДК
Как насчёт такой нотации? Тут сначала идёт имя правила, первый ребёнок - следствие, остальные дети - причины.
+ утверждает истинность, - - ложность.ДК
Чуть более сложный пример.
DF
Это ямль?
B
Вы ведь понимаете, что для концептуальной чистоты вы должны верифицировать это в MetaMath?
B
Знакомый из Serokell, который специализируется на Haskell, со мной согласен.
B
Лол