System Hilbertowski (założenia)

[itsonlylogic]

Podpowiedziałby mi ktoś w miarę możliwości prostym językiem bo próbuje "rozgryźć" system hilbertowski.

Mam przykład

\(\displaystyle{ Przykład. ⊢(𝐴 \rightarrow 𝐵) \rightarrow [(𝐵 \rightarrow 𝐶) \rightarrow (𝐴 \rightarrow 𝐶)]}\)
\(\displaystyle{ 1. {A \rightarrow B,B \rightarrow C,A}⊢A}\) Założenie
\(\displaystyle{ 2. {A \rightarrow B,B \rightarrow C,A}⊢A \rightarrow B}\) Założenie
\(\displaystyle{ 3. {𝐴 \rightarrow 𝐵,𝐵 \rightarrow 𝐶,𝐴}⊢𝐵 \rightarrow 𝐶}\) Założenie
\(\displaystyle{ 4. {𝐴 \rightarrow 𝐵,𝐵 \rightarrow 𝐶,𝐴}⊢𝐵 }\)MP:1,2
\(\displaystyle{ 5. {𝐴 \rightarrow 𝐵,𝐵 \rightarrow 𝐶,𝐴}⊢𝐶 }\)MP:4,3
\(\displaystyle{ 6. {𝐴 \rightarrow 𝐵,𝐵 \rightarrow 𝐶}⊢𝐴 \rightarrow 𝐶}\) reguła dedukcji: 5
\(\displaystyle{ 7. {𝐴 \rightarrow 𝐵}⊢[(𝐵 \rightarrow 𝐶) \rightarrow (𝐴 \rightarrow 𝐶)]}\) reguła dedukcji: 6
\(\displaystyle{ 8. ⊢(𝐴 \rightarrow 𝐵) \rightarrow [(𝐵 \rightarrow 𝐶) \rightarrow (𝐴 \rightarrow 𝐶)]}\) reguła dedukcji:7

I związane z tym kilkapytań.
Wyczytałem, że np.
\(\displaystyle{ U ⊢ A}\)
tutaj znaczek \(\displaystyle{ ⊢}\) oznacza, że po lewej są formuły ze zbioru \(\displaystyle{ U}\), które są założeniami w dowodzie formuły \(\displaystyle{ A}\). Nawet to zadanie mam rozwiązane, ale skąd wiedzieć, że akurat mają być trzy założenia i tak mają wyglądać? Czemu nie ma założenia np:
\(\displaystyle{ \{A→B,B→C,A\}⊢A→C}\)
I czemu akurat dowód formuł \(\displaystyle{ A, A \rightarrow B, B \rightarrow C}\)

albo
\(\displaystyle{ Przykład ⊢ \neg 𝐴 \rightarrow (𝐴 \rightarrow 𝐵)}\)
\(\displaystyle{ 1. { \neg 𝐴}⊢ \neg 𝐴 \rightarrow ( \neg 𝐵 \rightarrow \neg 𝐴)}\) Aksjomat 1
\(\displaystyle{ 2. { \neg 𝐴}⊢ \neg 𝐴}\) Założenie

Skąd wiedzieć, że najpierw mam wziąć aksjomat, a potem założenie i czemu takie założenie?

Tutaj to samo:
\(\displaystyle{ Przykład ⊢(𝐴→𝐵)→( \neg 𝐵 \rightarrow \neg 𝐴)}\)
\(\displaystyle{ 1. {𝐴→𝐵, \neg 𝐵, \neg \neg 𝐴}⊢ \neg \neg 𝐴}\)Założenie

Czemu akurat takie założenia a nie inne?, albo aksjomat+założenie?:D

[Jan Kraszewski]

Nawet to zadanie mam rozwiązane, ale skąd wiedzieć, że akurat mają być trzy założenia i tak mają wyglądać?

W tym rozwiązaniu jest duży (z Twojego punktu widzenia) skrót myślowy. Otóż w twierdzeniu

\(\displaystyle{ ⊢(𝐴 \rightarrow 𝐵) \rightarrow [(𝐵 \rightarrow 𝐶) \rightarrow (𝐴 \rightarrow 𝐶)]}\)

nie ma żadnych założeń. Natomiast trzykrotne kolejne zastosowanie twierdzenia o dedukcji prowadzi do problemu równoważnego:

\(\displaystyle{ \{𝐴 \rightarrow 𝐵, 𝐵 \rightarrow 𝐶,𝐴\}\vdash 𝐶\ \ \ \ \ \ \ \ \heartsuit}\)

I to tak naprawdę dowód tego twierdzenia masz na początku przykładu.

Zapis może być trochę mylący (bo twierdzenie o dedukcji pojawia się na końcu i nie bardzo wiadomo, skąd się bierze początek). Ja bym zapisał ten dowód tak:

Najpierw dowodzę \(\displaystyle{ \heartsuit}\):
\(\displaystyle{ 1.\ A}\) Założenie
\(\displaystyle{ 2.\ A \rightarrow B}\) Założenie
\(\displaystyle{ 3.\ 𝐵 \rightarrow 𝐶}\) Założenie
\(\displaystyle{ 4.\ 𝐵 }\) MP:1,2
\(\displaystyle{ 5.\ 𝐶 }\) MP:4,3
co kończy dowód. Następnie stosuję trzykrotnie tw. o dedukcji, by pokazać, że

1. \(\displaystyle{ \heartsuit}\) jest równoważne z \(\displaystyle{ \{𝐴 \rightarrow 𝐵,𝐵 \rightarrow 𝐶\}⊢𝐴 \rightarrow 𝐶}\),
2. \(\displaystyle{ \{𝐴 \rightarrow 𝐵,𝐵 \rightarrow 𝐶\}⊢𝐴 \rightarrow 𝐶}\) jest równoważne z \(\displaystyle{ \{𝐴 \rightarrow 𝐵\}⊢[(𝐵 \rightarrow 𝐶) \rightarrow (𝐴 \rightarrow 𝐶)]}\),
3. \(\displaystyle{ \{𝐴 \rightarrow 𝐵\}⊢[(𝐵 \rightarrow 𝐶) \rightarrow (𝐴 \rightarrow 𝐶)]}\) jest równoważne z \(\displaystyle{ ⊢(𝐴 \rightarrow 𝐵) \rightarrow [(𝐵 \rightarrow 𝐶) \rightarrow (𝐴 \rightarrow 𝐶)]}\).

W Twoim dowodzie jest zapisane w zasadzie to samo, ale w sposób, który nie pozwala Ci tego zrozumieć.

JK

[itsonlylogic]

Dzięki, faktycznie teraz jest to zdecydowanie lepiej widoczne, ale jak tak uczą to co poradzić, trzeba się dostosować

Czyli rozumiem, ze generalnie żadnego sposobu na to nie ma, jest to bardziej kwestia praktyki i zauważania pewnych "podobnych" sytuacji?
No tutaj to widzę, ze był wyciągnięty poprzednik implikacji a potem pousuwane przez MP regułą odrywania. W każdym bądź razie wydaje mi się, że załapałem.
Teraz mam takie pytanka i jeśli można to poprosiłbym o odpowiedź
1) Aksjomaty 1,2,3 mogę bez problemu dorzucać do dowodu?
2) Mam taki zapis
Twierdzenia dla innych operatorów logicznych
Stosujemy następujące prawa:
\(\displaystyle{ A \wedge B \Leftrightarrow \neg \left( A \Rightarrow \neg B\right) }\)
\(\displaystyle{ A∨B \Leftrightarrow \left( \neg A \Rightarrow B\right) }\)
\(\displaystyle{ \left( A \Leftrightarrow B\right) \Leftrightarrow \left( A \Rightarrow B\right) \wedge \left( B \Rightarrow A\right) }\)

Przykład
\(\displaystyle{ ⊢A\Rightarrow(B\Rightarrow(A \wedge B))}\)
\(\displaystyle{ 1.{A,B}⊢(A\Rightarrow \neg B)\Rightarrow(A\Rightarrow \neg B)}\) twierdzenie 1
itd..
O ile dalej co się dzieje mniej więcej rozumiem to nie nie wiem skąd się wzieło to twierdzenie skoro wyżej jest podane że
\(\displaystyle{ A \wedge B}\)
jest równoważne z
\(\displaystyle{ \neg \left( A \Rightarrow \neg B\right) }\) Czyli to jest po prostu jeszcze bardziej rozpisane w tym twierdzeniu 1?

3) Najważniejsze - czy to dobrze rozpocząłem to zadanie?
\(\displaystyle{ A \rightarrow (B \rightarrow A \vee B)}\)

skoro wyżej w twierdzeniach dla innych operatorów logicznych miałem podane, że:
\(\displaystyle{ A∨B \Leftrightarrow \left( \neg A \Rightarrow B\right) }\)

to podstawiłem
\(\displaystyle{ A \rightarrow (B \rightarrow \left( \neg A \Rightarrow B\right))}\)

No i wtedy już dałem
\(\displaystyle{ 1. {A,B, \neg A} ⊢ B}\) założenie
a dalej już regułą dedukcji
i rach ciach rozwiązane..

I pytanie, czy mogę wykorzystać jako założenie tylko
\(\displaystyle{ {A,B, \neg A} ⊢ B}\) założenie
czy musze też
\(\displaystyle{ {A,B, \neg A} ⊢ \neg A}\) założenie
\(\displaystyle{ {A,B, \neg A} ⊢ A}\) założenie
ale wtedy niebardzo bym wiedział jak pójść dalej

4. Inny przykład - wskazówka
\(\displaystyle{ A \wedge B→B \wedge A.}\) nalezy zrobić korzystając z reguły kontrapozycji
I myślałem tak jak wyżej podstawić pod
\(\displaystyle{ A \wedge B \Leftrightarrow \neg \left( A \Rightarrow \neg B\right) }\)
i wtedy dopiero zacząc rozwiązywać, ale wtedy wychodziło by coś takiego
\(\displaystyle{ \left( A \Rightarrow \neg B\right) \rightarrow \left( B \Rightarrow \neg A\right)}\)
Nie widzę po prostu co dalej mogę z tym zrobić
myślałem tak:
\(\displaystyle{ 1. \left\{ \left( A \Rightarrow \neg B\right), B \right\} ⊢ \left( A \Rightarrow \neg B\right)}\) założenie
\(\displaystyle{ 2. \left\{ \left( A \Rightarrow \neg B\right), B \right\} ⊢B}\) założenie
i dalej nie mogę rozgryźć.

PS. starałem się używać LaTeX'a.

[Jan Kraszewski]

Czyli rozumiem, ze generalnie żadnego sposobu na to nie ma, jest to bardziej kwestia praktyki i zauważania pewnych "podobnych" sytuacji?

Tak.

1) Aksjomaty 1,2,3 mogę bez problemu dorzucać do dowodu?

Tak, aksjomaty w takiej wersji, jak masz podane oraz dowolny wynik podstawienia pod aksjomaty (jak np. tu: \(\displaystyle{ \vdash \neg 𝐴 \rightarrow ( \neg 𝐵 \rightarrow \neg 𝐴)}\)).

Na resztę odpowiem Ci później.

JK

[itsonlylogic]

Na resztę odpowiem Ci później.

Dziękuje, czekam z zaciekawieniem

[Jan Kraszewski]

2) Mam taki zapis
Twierdzenia dla innych operatorów logicznych
Stosujemy następujące prawa:
\(\displaystyle{ A \wedge B \Leftrightarrow \neg \left( A \Rightarrow \neg B\right) }\)
\(\displaystyle{ A\lor B \Leftrightarrow \left( \neg A \Rightarrow B\right) }\)
\(\displaystyle{ \left( A \Leftrightarrow B\right) \Leftrightarrow \left( A \Rightarrow B\right) \wedge \left( B \Rightarrow A\right) }\)

Nie wiem, jak to było u Ciebie robione, ale dla mnie to są definicje, a nie twierdzenia. W typowym systemie hilbertowskim mamy język, w którym są dwa spójniki: negacja i implikacja. Jeżeli pojawiają się inne spójniki, to jako skróty zgodnie z powyższymi definicjami.

Przykład
\(\displaystyle{ ⊢A\Rightarrow(B\Rightarrow(A \wedge B))}\)
\(\displaystyle{ 1.{A,B}⊢(A\Rightarrow \neg B)\Rightarrow(A\Rightarrow \neg B)}\) twierdzenie 1
itd..
O ile dalej co się dzieje mniej więcej rozumiem to nie nie wiem skąd się wzieło to twierdzenie skoro wyżej jest podane że
\(\displaystyle{ A \wedge B}\)
jest równoważne z
\(\displaystyle{ \neg \left( A \Rightarrow \neg B\right) }\) Czyli to jest po prostu jeszcze bardziej rozpisane w tym twierdzeniu 1?

Dla mnie ten pierwszy krok to po pierwsze przygotowanie do dwukrotnego zastosowania tw. o dedukcji (jak porównałeś w poprzednim przypadku swój dowód z moim, to powinieneś wiedzieć, o co chodzi) oraz zastąpienie koniunkcji zgodnie z definicją tego spójnika, która u Ciebie nazywa się tw. 1.

3) Najważniejsze - czy to dobrze rozpocząłem to zadanie?
\(\displaystyle{ A \rightarrow (B \rightarrow A \vee B)}\)

Jesteś pewny, że ono tak wygląda? Bo to jest dość trywialne. Nie chodziło przypadkiem o \(\displaystyle{ A \rightarrow (B \rightarrow A\ \red{\land}\ B)}\)?

skoro wyżej w twierdzeniach dla innych operatorów logicznych miałem podane, że:
\(\displaystyle{ A∨B \Leftrightarrow \left( \neg A \Rightarrow B\right) }\)

to podstawiłem
\(\displaystyle{ A \rightarrow (B \rightarrow \left( \neg A \Rightarrow B\right))}\)

No i wtedy już dałem
\(\displaystyle{ 1. {A,B, \neg A} ⊢ B}\) założenie
a dalej już regułą dedukcji
i rach ciach rozwiązane..

OK. Tylko na końcu musisz jeszcze powołać się na "twierdzenie 1".

I pytanie, czy mogę wykorzystać jako założenie tylko
\(\displaystyle{ {A,B, \neg A} ⊢ B}\) założenie
czy musze też
\(\displaystyle{ {A,B, \neg A} ⊢ \neg A}\) założenie
\(\displaystyle{ {A,B, \neg A} ⊢ A}\) założenie
ale wtedy nie bardzo bym wiedział jak pójść dalej

Nie musisz, nie masz obowiązku wykorzystywania założeń.

4. Inny przykład - wskazówka
\(\displaystyle{ A \wedge B→B \wedge A.}\) nalezy zrobić korzystając z reguły kontrapozycji

Rozumiem, że masz tę regułę udowodnioną? Bo to jest syntaktycznie nietrywialne twierdzenie.

I myślałem tak jak wyżej podstawić pod
\(\displaystyle{ A \wedge B \Leftrightarrow \neg \left( A \Rightarrow \neg B\right) }\)
i wtedy dopiero zacząc rozwiązywać, ale wtedy wychodziło by coś takiego
\(\displaystyle{ \left( A \Rightarrow \neg B\right) \rightarrow \left( B \Rightarrow \neg A\right)}\)

A jak wychodzi? Po podstawieniu dostajesz

\(\displaystyle{ \neg \left( A \Rightarrow \neg B\right) \Rightarrow \neg \left( B \Rightarrow \neg A\right)}\)

a to syntaktycznie co innego. Pewnie chcesz zastosować "regułę kontrapozycji", ale wolałbym wiedzieć, co przez to rozumiesz, bo pewnym zagrożeniem w dowodach syntaktycznych jest stosowanie semantycznych metod.

ow \neg A\right)[/latex]
Nie widzę po prostu co dalej mogę z tym zrobić
myślałem tak:
\(\displaystyle{ 1. \left\{ \left( A \Rightarrow \neg B\right), B \right\} ⊢ \left( A \Rightarrow \neg B\right)}\) założenie
\(\displaystyle{ 2. \left\{ \left( A \Rightarrow \neg B\right), B \right\} ⊢B}\) założenie
i dalej nie mogę rozgryźć.

Tutaj będziesz potrzebował innych aksjomatów. Ale tutaj musiałbym wiedzieć, jaką masz wersję aksjomatu 3.

JK

[itsonlylogic]

oraz zastąpienie koniunkcji zgodnie z definicją tego spójnika, która u Ciebie nazywa się tw. 1.

No tak, ale definicja tego spójnika wygląda tak:
\(\displaystyle{ A\lor B \Leftrightarrow \left( \neg A \Rightarrow B\right) }\)
a twierdzenie 1
\(\displaystyle{ 1.{A,B}⊢(A\Rightarrow \neg B)\Rightarrow(A\Rightarrow \neg B)}\) twierdzenie 1
Nie widzę w jaki sposób ten spójnik został zastąpiony
Bo skoro mam przykład
\(\displaystyle{ ⊢A\Rightarrow(B\Rightarrow(A \wedge B))}\)
to ja bym to zamienił zgodnie z definicją spójnika na:
\(\displaystyle{ ⊢A\Rightarrow(B\Rightarrow \neg(A \rightarrow \neg B)}\)
stąd nie wiem skąd się wziął zapis w twierdzeniu 1.
Mam to zapisane jako "Twierdzenie 1" o poprawności systemu.

Jesteś pewny, że ono tak wygląda? Bo to jest dość trywialne. Nie chodziło przypadkiem o \(\displaystyle{ A \rightarrow (B \rightarrow A\ \red{\land}\ B)}\)?

Tak, jest ze spójnikiem "lub" v.

OK. Tylko na końcu musisz jeszcze powołać się na "twierdzenie 1".

Czyli na to prawo?
\(\displaystyle{ A∨B \Leftrightarrow \left( \neg A \Rightarrow B\right) }\)

Rozumiem, że masz tę regułę udowodnioną? Bo to jest syntaktycznie nietrywialne twierdzenie.

Tzn mam tylko prawo tego spójnika "i" ^
\(\displaystyle{ A \wedge B \Leftrightarrow \neg \left( A \Rightarrow \neg B\right) }\)

I myślałem tak jak wyżej podstawić pod
\(\displaystyle{ A \wedge B \Leftrightarrow \neg \left( A \Rightarrow \neg B\right) }\)
i wtedy dopiero zacząc rozwiązywać, ale wtedy wychodziło by coś takiego
\(\displaystyle{ \left( A \Rightarrow \neg B\right) \rightarrow \left( B \Rightarrow \neg A\right)}\)

A jak wychodzi? Po podstawieniu dostajesz
\(\displaystyle{ \neg \left( A \Rightarrow \neg B\right) \Rightarrow \neg \left( B \Rightarrow \neg A\right)}\)

No właśnie tak chciałem napisać, zgubiłem negację.

Pewnie chcesz zastosować "regułę kontrapozycji", ale wolałbym wiedzieć, co przez to rozumiesz, bo pewnym zagrożeniem w dowodach syntaktycznych jest stosowanie semantycznych metod.

U mnie reguła kontrapozycji jest zapisana tak:
\(\displaystyle{ \frac{U ⊢ \neg B \rightarrow \neg A}{U ⊢ A \rightarrow B} }\)

A aksjomat 3
\(\displaystyle{ ⊢ ( \neg B \rightarrow \neg A) \rightarrow (A \rightarrow B)}\)

Jeszcze jedno dodatkowe pytanko:
Czy jeżeli aksjomat 1 wygląda tak
\(\displaystyle{ ⊢ (A \rightarrow (B \rightarrow A))}\)
to mogę go sobie zastępować np. ?
\(\displaystyle{ ⊢ ( \neg \neg A \rightarrow ( \neg \neg B \rightarrow \neg \neg A))}\)
Bo wychodziloby na to samo, ale nie wiem czy tak można.

Dodano po 5 godzinach 5 minutach 33 sekundach:
@edit
Dzięki za podpowiedź z aksjomatem 3 - co do tego ostatniego to tak mogłem zrobić?
\(\displaystyle{ A \wedge B \rightarrow B \wedge A}\)
\(\displaystyle{ 1.\ \neg (A \rightarrow \neg B) \rightarrow \neg (B \rightarrow \neg A)}\)
\(\displaystyle{ 2.\ \vdash (B \rightarrow \neg A) \rightarrow (A \rightarrow \neg B)}\) reguła kontrapozycji
\(\displaystyle{ 3.\ \{ (B \rightarrow \neg A), A \} \vdash (B \rightarrow \neg A)}\) założenie
\(\displaystyle{ 4.\ \{ (B \rightarrow \neg A), A \} \vdash A }\) założenie
\(\displaystyle{ 5.\ \{ (B \rightarrow \neg A), A \} \vdash ( \neg B \rightarrow \neg A) \rightarrow (A \rightarrow B)}\) aksjomat 3
\(\displaystyle{ 6.\ \{ (B \rightarrow \neg A), A \} \vdash ( \neg B \rightarrow \neg A) \rightarrow B}\) MP 5,4
\(\displaystyle{ 7.\ \{ (B \rightarrow \neg A), A \} \vdash \neg B}\) MP 3,6
itd... regułą dedukcji a potem znowu regułą kontrapozycji w drugą stronę?

Czy źle zrobiłem regułę odrywania?

Dodano po 21 godzinach 38 minutach 29 sekundach:
Informacja dla osób, które by miały podobny przykład.
Wracając do tego twierdzenia 1 skąd się wzieło już wiem
bo miałem udowodnione, że z:
\(\displaystyle{ ⊢𝐴 \rightarrow 𝐴}\)
z A wynika A
i w pierwszym twierdzeniu za A zostało podstawione
\(\displaystyle{ (𝐴 \rightarrow \neg B)}\)

więc z
\(\displaystyle{ ⊢𝐴 \rightarrow 𝐴}\)
wyszło
\(\displaystyle{ (𝐴 \rightarrow \neg B) \rightarrow (𝐴 \rightarrow \neg B)}\)


a co do przykładu
\(\displaystyle{ A \wedge B \rightarrow B \wedge A}\)
to jeszcze nie wiem czy dobrze to zacząłem ale jakoś wynik wyszedł