Rachunki sekwentowe w logice klasycznej

Wprowadzenie v
1 Klasyczny Rachunek Zdań 1
1.1 Język 1
1.2 Aksjomatyczne ujęcie KRZ 3
1.2.1 Dowiedlność 5
1.2.2 Reguły wtórne 7
1.2.3 Sprzeczność 8
1.3 Semantyka KRZ 9
1.4 Adekwatność H-KRZ 11
1.4.1 Dowody twierdzenia o pełności – uwagi ogólne: 12
1.4.2 Zbiory maksymalnie niesprzeczne 13
1.4.3 Inne metody dowodzenia pełności 16
1.4.4 Pełność H-KRZ 19
1.5 Wybrane własności KRZ 22
1.6 Dedukcja Naturalna 23
2 Sekwenty, reguły, rachunki 27
2.1 Ogólne pojęcie rachunku sekwentowego. 27
2.1.1 Rodzaje sekwentów 28
2.1.2 Alternatywy RS 29
2.1.3 Uogólnienia RS 30
2.2 Reguły sekwentowe 32
2.2.1 Rodzaje reguł 33
2.2.2 Warianty i typy RS 36
2.3 Interpretacje sekwentów 38
2.4 RS a relacje konsekwencji 40
3 LK Gentzena dla KRZ 46
3.1 Rachunek sekwentów LK Gentzena 46
3.1.1 Reguły 47
3.1.2 Dowody 50
3.2 Adekwatność LK 57
3.3 Semantyczna interpretacja 59
4 Warianty standardowego RS dla KRZ 61
4.1 Warianty reguł 61
4.1.1 Aksjomaty uogólnione 63
4.1.2 Warianty reguł dwuprzesłankowych 64
4.1.3 Reguły Ketonena 65
4.2 Odwracalność reguł 66
4.3 Eliminacja reguł strukturalnych 71
4.4 Równoważność reguł 77
4.5 Własności reguł 81
4.6 Klasyczny RS na int-sekwentach 84
5 Dowody twierdzenia o eliminacji cięcia 88
5.1 Uwagi wprowadzające 89
5.1.1 Eliminacja czy dopuszczalność 90
5.1.2 Ogólna strategia dowodu 91
5.2 Dowód Gentzena 94
5.2.1 Kroki wstępne 95
5.2.2 Dowód 98
5.3 Dowody oparte na lokalnych przekształceniach 108
5.3.1 Dowód Dragalina 109
5.3.2 Dowód Smullyana 112
5.3.3 Dowód metodą Schüttego 115
5.4 Dowody oparte na globalnych transformacjach dowodu 118
5.4.1 Dowód Curry’ego 118
5.4.2 Dowód metodą Taita-Bussa 122
5.5 Porównanie 126
6 Konsekwencje eliminacji cięcia 129
6.1 Analityczność 130
6.1.1 Własność podformuł 130
6.1.2 Własność podformuł a analityczność 132
6.2 Rozstrzygalność KRZ 134
6.2.1 Zbieżność 138
6.2.2 Algorytmy 140
6.3 Twierdzenie o interpolacji 142
7 Metody semantyczne w RS 146
7.1 Pełność ARS z (Cut) metodą Henkina 147
7.1.1 Alternatywne dowody 151
7.2 Dowód analityczny pełności 152
7.2.1 Metoda bezpośrednia 153
7.2.2 Dowód pośredni 155
7.3 Pełność RS z analitycznym (Cut) 157
7.4 ARS a postacie normalne 159
8 Klasyczny Rachunek Kwantyfi atorów 161
8.1 Zagadnienia syntaktyczne 161
8.1.1 Języki pierwszego rzędu 162
8.1.2 Zmienne indywiduowe 166
8.1.3 Podstawianie i zastępowanie 168
8.2 Teorie pierwszego rzędu 171
8.2.1 Aksjomatyzacja KRK 171
8.2.2 Aksjomatyzacje teorii elementarnych 174
8.3 Semantyka 177
8.3.1 Struktura Interpretacyjna – ogólne pojęcie: 178
8.3.2 Ważne pojęcia semantyczne: 179
8.4 Adekwatność H-KRK 186
8.4.1 Przystosowanie 186
8.4.2 Pełność 187
8.4.3 Pełność KRKI 191
8.5 Wybrane własności KRK 192
8.6 Dedukcja naturalna 194
9 RS dla KRK i teorii elementarnych 196
9.1 Zagadnienia językowe 197
9.2 LK dla logiki pierwszego rzędu 200
9.3 PV-dowody 203
9.3.1 Podejście Kleene’go 204
9.3.2 Alternatywne podejście 206
9.4 Eliminacja cięcia w LK 208
9.5 ARS dla KRK 211
9.6 Metody semantyczne w ARS 217
9.6.1 Dowód adekwatności ARS 217
9.6.2 Istnienie modelu 218
9.6.3 Saturacja 221
9.7 Wzmocnienie twierdzenia o eliminacji (Cut) 224
9.8 Teorie elementarne 227
9.8.1 Systemy RS z dodanymi aksjomatami 228
9.8.2 RS z dodatkowymi regułami 230
9.8.3 RS-KRKI 235
10 Niestandardowe typy RS 237
10.1 Regułowe systemy RS 238
10.1.1 Sekwentowy DN Gentzena i jego warianty 238
10.1.2 Systemy DN logików rosyjskich 240
10.1.3 DN Andrewsa 241
10.1.4 Systemy DN Suppesa i Lemmona 242
10.1.5 Systemy Hermesa i Ebbinhgausa, Fluma, Thomasa . . 243 10.1.6 System Leblanca 245
10.1.7 Strukturalny system Do˘sena 246
10.2 Typ strukturalny RS Hertza 248
10.2.1 System Suszki 249
10.3 Typ mieszany 256
10.3.1 Kleene i sekwentowe DN 257
10.3.2 System Hasenjaegera 258
10.3.3 System Riegera 259
10.4 RS a inne systemy dedukcyjne 261
11 Dodatek 264
11.1 Zbiory, relacje, funkcje 264
11.2 Indukcja matematyczna 269
11.2.1 Stosowanie dowodów indukcyjnych w logice 272
Bibliografia 276
Skorowidz 286
Summary 297