Wejsciówka 5.06 Flashcards
Operacja podstawienia A(u/α)
- wyłącznie za zmienne wolne
- konsekwentnie
- żadna zmienna wolna nie może zostać związana w wyniku operacji podstawienia
Reguła odrywania
RO
A->B
A
——
B
Reguła podstawiania
RP
A
—
A(u/α)
Reguła opuszczania kwantyfikatora ogólnego w następniku
O/\N
A->/u\B
————
A -> B
Reguła dołączania kwantyfikatora ogólnego w następniku
A->B
———
A-> /u\ B *Pod warunkiem że u nie jest zmienną wolną w A
Reguła opuszczania kwantyfikatora szczegółowego w poprzedniku
OVP
\u/A -> B
—————
A->B
Reguła opuszczania kwantyfikatora szczegółowego w poprzedniku
OVP
\u/ A-> B
————-
A->B
Reguła dołączania kwantyfikatora szczegółowego w poprzedniku
DVP
A->B
——-
\u/A->B *pod warunkiem że u nie jest zmienną wolną w B
Reguła generalizacji
RG
A
—-
/u\A
Dowód zaliczeniowy wprost
Ciąg formuł, zaczynający się od założeń,
w którym jako kolejne formuty mogą wystąpić:
-wcześniej udowodnione twierdzenia
-formuly otrzymane z poprzedzajacych je w tym dowodzie
przy pomocy regut dowodzenia
ostatnia formuła to wniosek
Dowód założeniowy nie wprost
Ciąg formuł zaczynający się od założeń oraz negacji wniosku
Mogą wystąpić wcześniej udowodnione twierdzenia
Formuły otrzymane przez reguły dowodzenia
Ostatnia formuła jest sprzeczna z którąś z poprzednich
Reguły dowodzenia (pierwotne)
- reguła odrywania
- reguła dołączania i opuszczania koniunkcji
- reguła dołączania i opuszczania alternatywy
- reguła dołączania i opuszczania równoważności
- reguła transpozycji
Reguła dołączania kwantyfikatora ogólnego
D /\
A
—
/u\ A * pod warunkiem że zmienna u nie jest wolna w założeniach dowodu ani indeksem
Reguła dołączania kwantyfikatora szczegółowego
DV
A(u/α)
———-
\u/A * pod warunkiem że zmienna u nie jest indeksem
Reguła opuszczania kwantyfikatora szczegółowego
OV
\u/A(u)
————
A(u/a)* pod warunkiem że nazwa a nie występuje dotąd w żadnym wierszu dowodu
