Polski Zjazd Filozoficzny

wrzesień, 2019

wt10wrz17:3018:00System tablicowy dla SCImgr Magdalena Welle (Uniwersytet Warszawski)17:30 - 18:00 CTW-219 (Centrum Transferu Wiedzy) organizator: Sekcja Logiki

abstrakt

Zdaniowa logika SCI (Sentential calculus with identity) została wprowadzona do literatury logicznej przez polskiego logika Romana Suszkę w pracy (Suszko 1968). System ten należy do szerszej klasy logik, tzw. logik niefregowskich, na gruncie których odrzuca się aksjomat Fregego głoszący, że denotacją zdania jest jego wartość logiczna. Konstruując system logiki niefregowskiej, Suszko postępował zgodnie z programem Fregego, odrzucając jedynie aksjomat Fregego. Konsekwencją odrzucenia tego aksjomatu było wprowadzenie uniwersum sytuacji będących semantycznymi korelatami zdań. Aby możliwe było stwierdzanie rozmaitych faktów dotyczących zależności pomiędzy sytuacjami w uniwersum modelu SCI, do języka klasycznego rachunku zdań zostaje dodany dwuelementowy spójnik ≡, nazwany spójnikiem identyczności: zdanie α≡β wyraża fakt, że sytuacje będące denotacjami zdań i są identyczne.

Rachunek SCI jest najsłabszą logiką niefregowską, która powstaje przez rozszerzenie klasycznego rachunku zdań o aksjomaty charakteryzujące spójnik identyczności. Suszko zdefiniował rachunek SCI jako system aksjomatyczny w stylu Hilberta. Rachunek sekwentów dla SCI został zaproponowany w pracy (Michaels 1974), a później zmodyfikowany w pracach (Wasilewska 1976, 1984). System tablicowy w stylu dual tableaux skonstruowany został w pracy (Golińska-Pilarek 2007). Jednak wszystkie te systemy są z pewnej perspektywy nieoptymalne. Otóż logika SCI jest rozstrzygalna, stąd naturalne jest poszukiwanie systemu dedukcyjnego dla SCI będącego procedurą decyzyjną, którą można by łatwo poddać automatyzacji. System sekwentów z Michaelsa (1974), jak i system tablicowy Golińskiej- Pilarek (2007), nie są procedurami decyzyjnymi. Jedyną znaną procedurą decyzyjną dla SCI jest system Gentzena skonstruowany przez Wasilewską, jednak jest to system bardzo skomplikowany, nieintuicyjny i trudny w implementacji.

W ostatnich dekadach za wzorcowy typ systemów łatwych w automatyzacji uznaje się systemy tablicowe w stylu Smullyana. Celem referatu jest przedstawienie najnowszych wyników dotyczących systemu tablicowego dla SCI będącego jednocześnie procedurą decyzyjną dla SCI.

Literatura

  1. Michaels, “A uniform proof procedure for SCI tautologies”, Studia Logica 33(3), 1974, 299-310.
  2. J. Golińska-Pilarek, “Rasiowa-Sikorski Proof System for the non-Fregean Sentential Logic SCI”, Journal of Applied Non-Classical Logics, 17(4) 2007, 509-517.
  3. R. Suszko, “Non-Fregean logic and theories”, Analele Universitatii Bucaresti. Acta Logica 11, 1968, 105-125.
  4. A. Wasilewska, “A sequence formalization for SCI”, Studia Logica 35(3), 1976, 213-217.
  5. A. Wasilewska, “DFC-algorithms for Suszko logic and one-to-one Gentzen type formalization”, Studia Logica 43 (4), 1984, 395-404.

dzień i godzina

(Wtorek) 17:30 - 18:00

sala

CTW-219 (Centrum Transferu Wiedzy)

organizator

Sekcja LogikiPrzewodnicząca Sekcji: dr hab. Joanna Golińska-Pilarek (UW)
Sekretarz Sekcji: dr Michał Zawidzki (UW)

obradom przewodniczy

dr hab. Kordula Świętorzecka, prof. UKSW

Uniwersytet Kardynała Stefana Wyszyńskiego w Warszawie

Dodaj komentarz

Twój adres email nie zostanie opublikowany. Pola, których wypełnienie jest wymagane, są oznaczone symbolem *

Font Resize
Contrast
X