Математика имеет много символов. Некоторые могут сказать слишком много символов. Итак, давайте сделаем немного математики с картинками.
Давайте иметь бумагу, на которой мы будем рисовать. Для начала бумага пуста, мы скажем, что эквивалентно или true .
Если мы напишем на бумаге другие вещи, они тоже будут правдой.
Например
Указывает, что претензии и Q верны.
Теперь давайте скажем, что если мы рисуем круг вокруг некоторого утверждения, то это утверждение является ложным. Это логично, что нет.
Например:
Указывает, что ложно, а Q верно.
Мы даже можем поместить круг вокруг нескольких вложенных утверждений:
Так как пустое пространство было истиной, то отрицание истины ложно.
Теперь, используя этот простой визуальный метод, мы можем фактически представить любое утверждение в логике высказываний.
Доказательств
Следующим шагом после того, как вы сможете представлять заявления, будет возможность доказать их. Для доказательства у нас есть 4 различных правила, которые можно использовать для преобразования графа. Мы всегда начинаем с пустого листа, который, как мы знаем, является бессодержательной истиной, а затем используем эти разные правила, чтобы превратить наш пустой лист бумаги в теорему.
Наше первое правило вывода - вставка .
вставка
Мы будем называть количество отрицаний между подграфом и верхним уровнем «глубиной». Вставка позволяет нам вводить любое утверждение на любой глубине.
Вот пример того, как мы выполняем вставку:
подчистка
Следующее правило вывода - Erasure . Erasure говорит нам, что если у нас есть заявление, которое находится на равной глубине, мы можем полностью удалить его.
Вот пример применения стирания:
Двойной разрез
Double Cut - это эквивалентность. Это означает, что, в отличие от предыдущих выводов, его также можно изменить. Double Cut говорит нам, что мы можем нарисовать два круга вокруг любого подграфа, и если есть два круга вокруг подграфа, мы можем удалить их оба.
Вот пример Double Cut используется
итерация
Итерация также является эквивалентностью. 1 Обратное называется Deiteration. Если у нас есть оператор и разрез на одном уровне, мы можем скопировать этот оператор в разрез.
Например:
Deiteration позволяет нам полностью изменить Итерацию . Выписка может быть удалена с помощью Deiteration, если на следующем уровне существует ее копия.
Этот формат представления и доказательства не является моим собственным изобретением. Они представляют собой незначительную модификацию схематической логики и называются альфа-экзистенциальными графами . Если вы хотите прочитать больше об этом, литературы не много, но ссылка на статью - хорошее начало.
задача
Ваша задача будет доказать следующую теорему:
Это при переводе на традиционную логическую символику
,
Также известен как аксиома Лукасевича-Тарского .
Это может показаться сложным, но экзистенциальные графы очень эффективны, когда дело доходит до длины доказательства. Я выбрал эту теорему, потому что я думаю, что это подходящая длина для веселой и сложной головоломки. Если у вас возникли проблемы с этим, я бы порекомендовал сначала попробовать несколько более простых теорем, чтобы получить представление о системе. Список их можно найти внизу поста.
Это пробная игра, поэтому ваш счет будет общим количеством шагов в вашей проверке от начала до конца. Цель состоит в том, чтобы минимизировать ваш счет.
Формат
Формат этого задания гибкий, вы можете отправлять ответы в любом удобном для чтения формате, включая рукописные или визуализированные форматы. Однако для ясности я предлагаю следующий простой формат:
Мы представляем разрез с круглыми скобками, все, что мы режем, помещается в скобки. Пустой разрез будет просто
()
для примера.Мы представляем атомы только их буквами.
В качестве примера приведем формулировку цели в этом формате:
(((A((B(A))))(((((C)((D((E)))))(((C((D(F))))(((E(D))((E(F))))))))(G))))((H(G))))
Этот формат хорош, потому что он удобен для чтения человеком и машиной, поэтому было бы неплохо включить его в ваш пост.
Что касается вашей реальной работы, я рекомендую карандаш и бумагу при разработке. Я считаю, что этот текст не так интуитивен, как бумага, когда дело доходит до экзистенциальных графиков.
Пример доказательства
В этом примере доказательства мы докажем следующую теорему:
Доказательство:
Теоремы о практике
Вот несколько простых теорем, которые вы можете использовать для практики системы:
Лукасевич Вторая аксиома
Аксиома Мередит
1: Большинство источников используют более сложную и мощную версию Итерации , но для упрощения этой задачи я использую эту версию. Они функционально эквивалентны.
источник
Ответы:
19 шагов
(())
[двойной разрез](AB()(((G))))
[Вставка](AB(A)(((G))))
[Итерационный](((AB(A)))(((G))))
[двойной разрез](((AB(A))(((G))))(((G))))
[Итерационный](((AB(A))(((G))))((H(G))))
[Вставка](((AB(A))(((G)(()))))((H(G))))
[двойной разрез](((AB(A))(((DE()(C)(F))(G))))((H(G))))
[Вставка](((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G))))
[Итерационный](((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G))))
[Итерационный](((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G))))
[двойной разрез](((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G))))
[Итерационный](((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G))))
[двойной разрез](((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[двойной разрез](((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[двойной разрез](((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[двойной разрез](((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[двойной разрез](((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[двойной разрез](((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[двойной разрез]Практические теоремы
Вторая аксиома Лукасевича: 7 шагов
(())
[двойной разрез](A()(B)(C))
[Вставка](A(A(B))(B)(C))
[Итерационный](A(AB(C))(A(B))(C))
[Итерационный]((AB(C))(A(B))((A(C))))
[двойной разрез]((AB(C))(((A(B))((A(C))))))
[двойной разрез]((A((B(C))))(((A(B))((A(C))))))
[двойной разрез]Аксиома Мередит: 11 шагов
(())
[двойной разрез](()(D(A)(E)))
[Вставка]((D(A)(E))((D(A)(E))))
[Итерационный]((D(A)(E))((D(A)(E(A)))))
[Итерационный]((D(A)(E))(((E(A))((D(A))))))
[двойной разрез](((E)((D(A))))(((E(A))((D(A))))))
[двойной разрез](((E)((C)(D(A))))(((E(A))((D(A))))))
[Вставка](((E)((C)(D(A)(C))))(((E(A))((D(A))))))
[Итерационный](((E)((C)((A)(C)((D)))))(((E(A))((D(A))))))
[двойной разрез](((E)((C)((A)(((C)((D)))))))(((E(A))((D(A))))))
[двойной разрез](((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A))))))
[Вставка]Haskell поисковик
(Что, ты думал, что я собираюсь сделать это вручную? :-P)
Это только попытка вставки, двойного введения и итерации. Таким образом, все еще возможно, что эти решения могут быть побеждены, используя стирание, устранение двойного сокращения или deiteration.
источник
22 шага
(((())(())))
(((AB())(CDE(F)()))H(G))
(((AB(A))(CDE(F)(CD(F)))(G))H(G))
(((A((B(A))))(((((C))DE(F)(C((D(F)))))(G))))((H(G))))
(((A((B(A))))(((((C)DE)DE(F)(C((D(F)))))(G))))((H(G))))
(((A((B(A))))(((((C)((D((E)))))((((((D))E(F)))(C((D(F)))))))(G))))((H(G))))
(((A((B(A))))(((((C)((D((E)))))((((((D)E)E(F)))(C((D(F)))))))(G))))((H(G))))
(((A((B(A))))(((((C)((D((E)))))((((((D)E)((E(F)))))(C((D(F)))))(G))))))((H(G))))
Несколько вещей, которые я узнал из этой головоломки:
Уменьшите предоставленное представление. Это включает в себя реверс двойных разрезов и итераций. Например, эта аксиома сводится к
(((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))
после реверсирования двойных резов и(((AB(A))(()CDE(F)))H(G)))
после реверсирования итераций.Ищите беспризорные атомы. Например, H используется в качестве фиктивной переменной и, следовательно, может быть вставлен в любую точку.
Практика Теорема Решения:
Решение для второй аксиомы Лукасевича: [8 шагов]
(())
(()AB(C))
((AB(C))AB(C))
((A((B(C))))A((B))(C))
((A((B(C))))A(A(B))(C))
((A((B(C))))(((A(B))((A(C))))))
Решение для аксиомы Мередит: [12 шагов]
(())
(()(A)D(E))
(((A)D(E))(A)D(E(A)))
(((((A)D))(E))(A)D(E(A)))
(((((A(B))D)(C))(E))(A)D(E(A)))
(((((A(B))(C)D)(C))(E))(A)D(E(A)))
(((((A(B))(((C)((D)))))(C))(E))(((((A)D))(E(A)))))
источник
\$
в качестве начала / конца, который, я думаю, сделает ваше решение намного проще для чтения. Я надеюсь, что вы хорошо