for-muł z poprzednika lub następnika rozważanego sekwentu i dla każdej takiej formuły tworząc sekwent-przesłankę, gdzie element poprzednika (ϕi) umiesz-czamy w następniku a element następnika (ψj) w poprzedniku sekwentu-przesłanki; pozostałe formuły sekwentu wyjściowego tworzą zbiory Γ−ii ∆−j sekwentu-wniosku. Krańcowy przypadek, to Γ−k i ∆−n, czyli oba zbiory są puste, reguła ma k+n przesłanek, po jednej dla każdej formuły z wyjściowego sekwentu, a sekwent wniosek zawiera tylko sumy parametrów z przesłanek. Dla odmiany, jeżeli uwzględnimy sytuację, gdy zarazem Γ−0 i ∆−0, to nasz schemat dotyczy również przypadku reguły z zerową ilością przesłanek, czyli wyjściowego sekwentu.
Dla lepszego zrozumienia sposobu generowania reguł proponujemy czy-telnikowi samodzielne wypisanie piętnastu schematów reguł, które można wyprowadzić z sekwentu ϕ1, ϕ2 ⇒ ψ1, ψ2
4.5 Własności reguł
Pomimo wprowadzenia kilku wariantów RS, które istotnie różnią się co do swych własności, można zaobserwować pewne cechy wspólne, zwłaszcza je-żeli chodzi o budowę reguł. Poprzedni podrozdział pokazywał jakie formy mogą potencjalnie przyjmować reguły w systemach RS. Łatwo zauważyć, że reguły w standardowych RS typu Gentzenowskiego (tj. dokładniej w pod-typie typu pierwszego wyróżnionego przez nas w paragrafie 2.2.2) podlegają w tym względzie istotnym ograniczeniom w porównaniu do innych typów RS, które omówimy w rozdziale 10. Poniżej podamy listę kilkunastu waż-nych cech, które posiada większość reguł w standardowych Gentzenowskich systemach RS.
Przypomnijmy, że typ 1 RS (w stylu Gentzena) charakteryzuje się tym, że ilość sekwentów bazowych jest ograniczona do minimum natomiast rachunek opiera się na regułach. Ponadto, sekwenty aksjomatyczne mają charakter strukturalny, a zawartość logiczna (charakterystyka stałych) zawarta jest w regułach. Dodatkowo, w ramach typu pierwszego, standardowe RS w stylu Gentzena spełnia warunek progresywności:
Każda reguła logiczna jest regułą wprowadzania stałej do dowodu. Innymi słowy są to reguły podpadające pod schemat (c) i (d) z paragrafu 2.2.1. Warunek progresywności możemy uznać za wyróżnik standardowych systemów RS w obrębie typu pierwszego. Inne RS należące do tego typu, które nie spełniają warunku progresywności, np. sekwentowe DN, nazwiemy
niestandardowymi. Omówimy je również w rozdziale 10, obok systemów re-prezentujących typ drugi (w stylu Hertza) i trzeci (mieszany; por. paragraf 2.2.2). Pozostałe własności reguł podzielimy na trzy grupy: ogólne, logiczne i strukturalne.
Do najważniejszych własności ogólnych zaliczyć możemy:
1. Rozdzielność: każdy element reguły jest albo parametrem albo formułą poboczną, albo zasadniczą.
2. Własność podformuł: każda formuła występująca w przesłankach wy-stępuje też we wniosku jako podformuła (niekoniecznie właściwa). 3. Odwracalność: przesłanki są dedukowalne z wniosku.
Własność rozdzielności ma w zasadzie charakter definicyjny. Jak dotąd dużo uwagi poświęciliśmy własności odwracalności reguł. Jak wiemy, nie jest ona uniwersalna, gdyż nie spełniają jej np. (W ), (→⇒) w LK. Własność pod-formuł jest jeszcze ważniejsza i łatwo zauważyć, że spełniają ją wszystkie reguły oprócz (Cut). Obu własnościom i ich konsekwencjom, w szczególności analityczności i zbieżności, poświęcimy wiele uwagi w rozdziale 6.
Własności logiczne to cechy reguł logicznych; najważniejsze z nich to: 1. Kumulatywność: formuła zasadnicza jest zawsze złożona.
2. Separowalność: schemat reguły logicznej dla danej stałej nie zawiera innych stałych.
3. Symetria słaba: każda stała ma reguły wprowadzania do następnika lub poprzednika sekwentu (i żadnych innych).
4. Symetria mocna: każda stała ma obie reguły wprowadzania (i żadnych innych).
5. Eksplicytność słaba: stała występuje tylko w sekwencie-wniosku. 6. Eksplicytność mocna: stała występuje tylko raz w sekwencie-wniosku. 7. Wyłączność: formuły poboczne występują tylko w sekwentach-przesłankach.
Warto zauważyć, że separowalność oznacza, iż reguła daje czysto struk-turalne wyjaśnienie znaczenia stałej, bez odwoływania się do znaczenia in-nych stałych logiczin-nych. Ta, i inne wyżej podane, własności reguł logiczin-nych
4.5. WŁASNOŚCI REGUŁ 83 przyczyniły się do ufundowania antyrealistycznej teorii znaczenia stałych lo-gicznych, tzw. inferencjalizmu, w której znaczenie stałej określa się poprzez warunki jej użycia2. Zauważmy też, że wszystkie reguły logiczne należące do LK, oraz do każdego z wariantów RS opisanych w tym rozdziale, spełniają wszystkie podane wyżej warunki. Nie jest to regułą w przypadku standardo-wych RS dla wielu logik nieklasycznych (a nawet dla KRK, jak zobaczymy w rozdziale 9).
Własności strukturalne dotyczą parametrów (ale we wszystkich regułach a nie jedynie strukturalnych):
1. Kongruencja: każdy parametr we wniosku ma dokładnie jednego bez-pośredniego przodka w (każdej) przesłance.
2. Niezależność kontekstowa: poprawność danej reguły nie jest zakłócona przez zmiany dokonane na parametrach, w szczególności:
(a) dodanie dalszych parametrów do sekwentów-przesłanek i sekwentu-wniosku;
(b) skasowanie tych samych parametrów w przesłankach i wniosku; (c) zamianę danego parametru na inny w przesłankach i wniosku. Kongruencja z dodatkiem w nawiasie jest kongruencją mocną, która za-chodzi dla reguł k-jednolitych, ale niekoniecznie dla reguł k-niezależnych. Łatwo sprawdzić, że wszystkie reguły każdego wariantu spełniają całkowicie niezależność kontekstową, ale już w RS z int-sekwentami jest ona ograniczona tylko do poprzedników. Jak przekonamy się w rozdziale 9 w regułach kwan-tyfikatorowych (konkretnie (⇒ ∀) i (∃ ⇒)) z tej własności tylko kasowanie parametrów jest możliwe3.
Wymienione wyżej własności reguł mają wagę nie tylko dla pewnej fi-lozofii znaczenia stałych logicznych. Jak pokażemy w następnym rozdziale, występowanie tych własności reguł, pozwala na przeprowadzenie pewnego typu dowodów eliminacji cięcia, które polegają na globalnych przekształce-niach fragmentów dowodu, możliwych dzięki własnościom reguł.
2
Literatura poświęcona tym zagadnieniom jest ogromna, z ważniejszych prac wymienić można m.in.: Dummett [35], Prawitz [113], Hacking [60], Sundholm [132]. Przystępne podsumowanie tych propozycji w polskiej literaturze znaleźć można np. w Maciaszek [97].