Cóż, myślę, że najwyższy czas, abyśmy mieli kolejne pytanie dotyczące gry w golfa .
Tym razem udowodnimy dobrze znaną logiczną prawdę
W tym celu użyjemy trzeciego schematu aksjomatycznego Łukasiewicza , niezwykle eleganckiego zestawu trzech aksjomatów, które są kompletne w stosunku do logiki zdań .
Oto jak to działa:
Aksjomaty
System Łukasiewicza ma trzy aksjomaty. Oni są:
Aksjomaty są uniwersalnymi prawdami niezależnie od tego, co wybraliśmy dla , i . W dowolnym momencie dowodu możemy wprowadzić jeden z tych aksjomatów. Wprowadzając aksjomat, zamieniasz każdy przypadek , i na „wyrażenie złożone”. Złożone wyrażenie to dowolne wyrażenie złożone z atomów (reprezentowane przez litery - ), a operatory oznaczają ( ), a nie ( ).
Na przykład, gdybym chciał wprowadzić pierwszy aksjomat (LS1), mógłbym wprowadzić
lub
W pierwszym przypadku było a było , podczas gdy w drugim przypadku oba były bardziej zaangażowanymi wyrażeniami. to i Było .
Wybór zamienników będzie zależał od tego, czego potrzebujesz w dowodzie w tej chwili.
Modus Ponens
Teraz, gdy możemy wprowadzić oświadczenia, musimy je powiązać, aby tworzyć nowe oświadczenia. Sposób ten jest realizowany w schemacie aksjomatycznym Łukasiewicza (LS) w przypadku Modusa Ponensa. Modus Ponens pozwala nam przyjąć dwa oświadczenia formularza
i utwórz nową instrukcję
Podobnie jak w przypadku naszych Axioms i mogą zastąpić dowolne zdanie.
Te dwa stwierdzenia mogą znajdować się w dowolnym miejscu dowodu, nie muszą znajdować się obok siebie ani na specjalne zamówienie.
Zadanie
Twoim zadaniem będzie udowodnienie prawa środków antykoncepcyjnych . To jest stwierdzenie
Teraz możesz zauważyć, że jest to dość znane, jest to tworzenie odwrotności naszego trzeciego aksjomatu
Nie jest to jednak trywialny wyczyn.
Punktacja
Punktacja dla tego wyzwania jest dość prosta, za każdym razem, gdy tworzysz aksjomat, liczy się jako punkt, a każde użycie modus ponens liczy się jako punkt. Jest to zasadniczo liczba linii w dowodzie. Celem powinno być zminimalizowanie twojego wyniku (uczynienie go jak najniższym).
Przykład dowodu
Ok, teraz użyjmy tego do skonstruowania małego dowodu. Udowodnimy .
Czasami najlepiej jest pracować wstecz, ponieważ wiemy, gdzie chcemy być, możemy ustalić, jak możemy się tam dostać. W tym przypadku, ponieważ chcemy skończyć na i nie jest to jeden z naszych aksjomatów, wiemy, że ostatnim krokiem muszą być modus ponens. Tak będzie wyglądał koniec naszego dowodu
φ
φ → (A → A)
A → A M.P.
Gdzie jest wyrażeniem, którego jeszcze nie znamy. Teraz skupimy się na . Można to wprowadzić albo modus ponens, albo LS3. LS3 wymaga od nas udowodnienia co wydaje się tak samo trudne jak , więc przejdziemy do modus ponens. Więc teraz wygląda nasz dowód
φ
ψ
ψ → (φ → (A → A))
φ → (A → A) M.P.
A → A M.P.
Teraz wygląda bardzo podobnie do naszego drugiego aksjomatu LS2, więc wypełnimy go jako LS2
A → χ
A → (χ → A)
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A) M.P.
A → A M.P.
Teraz nasze drugie zdanie można dość wyraźnie zbudować z LS1, więc wypełnimy je jako takie
A → χ
A → (χ → A) L.S.1
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A) M.P.
A → A M.P.
Teraz musimy tylko znaleźć , abyśmy mogli udowodnić, że . Można to bardzo łatwo zrobić za pomocą LS1, więc spróbujemy tego
A → (ω → A) L.S.1
A → ((ω → A) → A) L.S.1
(A → ((ω → A) → A)) → ((A → (ω → A)) → (A → A)) L.S.2
(A → (ω → A)) → (A → A) M.P.
A → A M.P.
Teraz, gdy wszystkie nasze kroki są uzasadnione, możemy wypełnić , jak każde oświadczenie, którego chcemy, a dowód będzie ważny. Mogliśmy wybrać jednak wybiorę tak, że jest oczywiste, że nie trzeba być .
A → (B → A) L.S.1
A → ((B → A) → A) L.S.1
(A → ((B → A) → A)) → ((A → (B → A)) → (A → A)) L.S.2
(A → (B → A)) → (A → A) M.P.
A → A M.P.
I to jest dowód.
Zasoby
Program weryfikacji
Oto program Prolog, za pomocą którego możesz sprawdzić, czy twój dowód jest rzeczywiście ważny. Każdy krok powinien być umieszczony na osobnej linii. ->powinny być używane do implikacji i -powinny być używane do nie, atomy mogą być reprezentowane przez dowolny ciąg znaków alfabetycznych.
Metamath
Metamath korzysta z systemu Łukasiewicza jako dowodu w rachunku zdań, więc możesz się tam trochę pogrzebać . Mają także dowód na twierdzenie, o które prosi wyzwanie, które można znaleźć tutaj . Oto wyjaśnienie , jak czytać dowody.
Incredible Proof Machine
@ Antony uświadomił mi narzędzie o nazwie The Incredible Proof machine, które pozwala konstruować proofy w wielu systemach przy użyciu ładnego graficznego systemu proofów. Jeśli przewiniesz w dół, przekonasz się, że obsługują one system Łukasiewicza. Więc jeśli jesteś bardziej zorientowany wizualnie, możesz popracować nad tym dowodem. Twój wynik będzie liczbą użytych bloków minus 1.
((P → Q) → R) → ((R → P) → (S → P))
