Matematyka ma wiele symboli. Niektórzy mogą powiedzieć zbyt wiele symboli. Zróbmy więc matematykę ze zdjęciami.
Zróbmy papier, z którego będziemy czerpać. Aby rozpocząć papier jest pusty, powiemy, że jest to odpowiednik lub .prawda
Jeśli napiszemy na papierze inne rzeczy, one również będą prawdziwe.
Na przykład
Wskazuje, że twierdzenia i są prawdziwe.Q
Powiedzmy teraz, że jeśli narysujemy okrąg wokół jakiegoś stwierdzenia, to stwierdzenie jest fałszywe. To logiczne nie.
Na przykład:
Wskazuje, że jest fałszem, a jest prawdą.Q
Możemy nawet umieścić koło wokół wielu instrukcji podrzędnych:
Ponieważ część wewnątrz koła zwykle czyta się jako , umieszczając wokół niego okrąg, oznacza to . Możemy nawet zagnieżdżać kręginie ( P i Q )
Odczytuje to jako .
Jeśli narysujemy okrąg, w którym nic nie ma, oznacza to lub . fałsz
Ponieważ pusta przestrzeń była prawdziwa, negacja prawdy jest fałszywa.
Teraz za pomocą tej prostej metody wizualnej możemy właściwie przedstawić dowolne zdanie w logice zdań.
Dowody
Następnym krokiem po przedstawieniu oświadczeń jest możliwość ich udowodnienia. W przypadku dowodów mamy 4 różne reguły, których można użyć do przekształcenia wykresu. Zawsze zaczynamy od pustego arkusza, który jak wiemy jest pustą prawdą, a następnie używamy tych różnych reguł, aby przekształcić nasz pusty arkusz papieru w twierdzenie.
Naszą pierwszą zasadą wnioskowania jest wstawianie .
Wprowadzenie
Nazwę liczby negacji między pod wykresem a najwyższym poziomem nazywamy „głębią”. Wstawienie pozwala nam wprowadzić dowolne oświadczenie, które chcemy na dziwnej głębokości.
Oto przykład przeprowadzania wstawiania:
Tutaj wybraliśmy , ale równie dobrze moglibyśmy wybrać dowolne oświadczenie, które chcieliśmy.
Skasowanie
Następna reguła wnioskowania to Kasowanie . Erasure mówi nam, że jeśli mamy stwierdzenie, które jest na równej głębokości, możemy je całkowicie usunąć.
Oto przykład zastosowania kasowania:
Tutaj usunęliśmy , ponieważ było zagnieżdżone poziomy. Nawet gdybyśmy tego chcieli, nie moglibyśmy usunąć ponieważ jest on zagnieżdżony na poziomie.2 P 1
Podwójne cięcie
Podwójne cięcie jest równoważne. Co oznacza, że w przeciwieństwie do poprzednich wniosków można go również odwrócić. Double Cut mówi nam, że możemy narysować dwa koła dookoła dowolnego pod-wykresu, a jeśli są dwa koła dookoła pod-wykresu, możemy je usunąć.
Oto przykład z Double Cut używany
Tutaj używamy Double Cut na .
Iteracja
Iteracja jest również równoważna. 1 Odwrotność nazywa się Deiteracją. Jeśli mamy instrukcję i wycięcie na tym samym poziomie, możemy skopiować to wyrażenie wewnątrz wycięcia.
Na przykład:
Deiteration pozwala nam odwracać iteracji . Instrukcja może zostać usunięta przez Deiteration, jeśli istnieje jej kopia na wyższym poziomie.
Ten format przedstawienia i dowodu nie jest moim własnym wynalazkiem. Są one niewielką modyfikacją logiki schematycznej zwanej Alpha Existential Graphs . Jeśli chcesz przeczytać więcej na ten temat, nie ma mnóstwo literatury, ale powiązany artykuł to dobry początek.
Zadanie
Twoim zadaniem będzie udowodnienie następującego twierdzenia:
To po przetłumaczeniu na tradycyjną symbolikę logiczną jest
.
Znany również jako aksjomat Łukasiewicza-Tarskiego .
Może się to wydawać zaangażowane, ale wykresy egzystencjalne są bardzo wydajne, jeśli chodzi o długość dowodu. Wybrałem to twierdzenie, ponieważ uważam, że jest to odpowiednia długość dla zabawnej i wymagającej układanki. Jeśli masz problemy z tym jednym polecam próbuje niektóre bardziej podstawowe twierdzenia pierwszy się zawiesić system. Ich listę można znaleźć na dole postu.
To jest proof-golf, więc twój wynik będzie całkowitą liczbą kroków w twoim proofie od początku do końca. Celem jest zminimalizowanie twojego wyniku.
Format
Format tego wyzwania jest elastyczny można przesłać odpowiedź w dowolnym formacie, który jest wyraźnie czytelny, w tym ręcznie rysowane lub świadczonych formatach. Jednak dla jasności sugeruję następujący prosty format:
Reprezentujemy nacięcie w nawiasach, bez względu na to, co wycinamy, jest ono wstawiane do parens. Puste cięcie byłoby po prostu
()
na przykład.Reprezentujemy atomy tylko ich literami.
Przykładem jest tutaj instrukcja celu w tym formacie:
(((A((B(A))))(((((C)((D((E)))))(((C((D(F))))(((E(D))((E(F))))))))(G))))((H(G))))
Ten format jest fajny, ponieważ jest czytelny zarówno dla ludzi, jak i dla maszyn, więc umieszczenie go w poście byłoby przyjemne.
Jeśli chodzi o twoją rzeczywistą pracę, zalecam ołówek i papier podczas ćwiczeń. Uważam, że tekst nie jest tak intuicyjny jak papier, jeśli chodzi o wykresy egzystencjalne.
Przykładowy dowód
W tym przykładowym dowodzie udowodnimy następujące twierdzenie:
Dowód:
Ćwicz twierdzenia
Oto kilka prostych twierdzeń, których można użyć do ćwiczenia systemu:
Drugi aksjomat Łukasiewicza
Aksjomat Meredith
1: Większość źródeł używa bardziej wyrafinowanej i wydajniejszej wersji Iteracji , ale dla uproszczenia tego wyzwania korzystam z tej wersji. Są funkcjonalnie równoważne.
źródło
Odpowiedzi:
19 kroków
(())
[podwójne cięcie](AB()(((G))))
[wprowadzenie](AB(A)(((G))))
[iteracja](((AB(A)))(((G))))
[podwójne cięcie](((AB(A))(((G))))(((G))))
[iteracja](((AB(A))(((G))))((H(G))))
[wprowadzenie](((AB(A))(((G)(()))))((H(G))))
[podwójne cięcie](((AB(A))(((DE()(C)(F))(G))))((H(G))))
[wprowadzenie](((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G))))
[iteracja](((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G))))
[iteracja](((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G))))
[podwójne cięcie](((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G))))
[iteracja](((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G))))
[podwójne cięcie](((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[podwójne cięcie](((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[podwójne cięcie](((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[podwójne cięcie](((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[podwójne cięcie](((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[podwójne cięcie](((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[podwójne cięcie]Przećwicz twierdzenia
Drugi aksjomat Łukasiewicza: 7 kroków
(())
[podwójne cięcie](A()(B)(C))
[wprowadzenie](A(A(B))(B)(C))
[iteracja](A(AB(C))(A(B))(C))
[iteracja]((AB(C))(A(B))((A(C))))
[podwójne cięcie]((AB(C))(((A(B))((A(C))))))
[podwójne cięcie]((A((B(C))))(((A(B))((A(C))))))
[podwójne cięcie]Aksjomat Meredith: 11 kroków
(())
[podwójne cięcie](()(D(A)(E)))
[wprowadzenie]((D(A)(E))((D(A)(E))))
[iteracja]((D(A)(E))((D(A)(E(A)))))
[iteracja]((D(A)(E))(((E(A))((D(A))))))
[podwójne cięcie](((E)((D(A))))(((E(A))((D(A))))))
[podwójne cięcie](((E)((C)(D(A))))(((E(A))((D(A))))))
[wprowadzenie](((E)((C)(D(A)(C))))(((E(A))((D(A))))))
[iteracja](((E)((C)((A)(C)((D)))))(((E(A))((D(A))))))
[podwójne cięcie](((E)((C)((A)(((C)((D)))))))(((E(A))((D(A))))))
[podwójne cięcie](((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A))))))
[wprowadzenie]Wyszukiwarka dowodów Haskell
(Myślałeś, że zrobię to ręcznie? :-P)
To tylko próbuje wstawić, wprowadzenie podwójnego cięcia i iteracji. Nadal możliwe jest pokonanie tych rozwiązań za pomocą skasowania, podwójnej eliminacji lub deiteracji.
źródło
22 kroki
(((())(())))
(((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))))
Kilka rzeczy, których nauczyłem się podczas układania tej układanki:
Zmniejsz przedstawioną reprezentację. Obejmuje to odwracanie podwójnych cięć i iteracji. Na przykład ten aksjomat redukuje się do
(((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))
po cofnięciu podwójnych cięć i(((AB(A))(()CDE(F)))H(G)))
po odwróceniu iteracji.Szukaj zbłąkanych atomów. Na przykład H jest używane jako zmienna fikcyjna, a zatem można go wstawić w dowolnym momencie.
Przećwicz rozwiązania twierdzeń:
Rozwiązanie drugiego aksjomatu Łukasiewicza: [8 kroków]
(())
(()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))))))
Rozwiązanie dla aksjomatu Meredith: [12 kroków]
(())
(()(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)))))
źródło
\$
jako początek / koniec, który moim zdaniem znacznie ułatwi czytanie. Mam nadzieję, że miło