• Polski
  • English

Metateoria systemów tablicowych

Kierownik projektu:  dr hab. Tomasz Dariusz Jarmużek

Logika jako dyscyplina naukowa zajmuje się badaniem metod pozwalających stwierdzać poprawność rozumowań. Wśród wielu metod istnieją także metody tablicowe.

Metody te są bardzo efektywne, jednak zwykle prezentowane  są jedynie w dydaktyczny i intuicyjny  sposób. Naszym  celem jest opis i unifikacja metod tablicowych w sposób formalny. Rezultatem tego ma być formalna metateoria systemów tablicowych, sformułowana w kategoriach teoriomnogościowych, zawierająca ogólne pojęcia istotne dla budowy dowodów tablicowych, a więc pojęcia reguły tablicowej oraz gałęzi i tablic różnych rodzajów (maksymalnych, otwartych, zamkniętych itd.), które są stałe, a zmieniają się w nich jedynie parametry zależne od logiki/klasy logik, dla której dany system tablicowy jest budowany.

Przyjęta hipoteza badawcza mówi, że taka metateoria jest możliwa, a w konsekwencji zarówno systemy tablicowe, jak i dowody tablicowe mogą być określane precyzyjnie, a zależności między nimi można badać już na poziomie wyjściowych pojęć tablicowych.

Prowadzone w ramach projektu badania mają charakter badań podstawowych, ponieważ logika jest dyscypliną teoretyczną i każde prowadzone na jej gruncie ba- danie ma charakter badań podstawowych.

Można wyróżnić dwa aspekty znaczenia i wpływu podejmowanego projektu. Je- den z aspektów jest bezpośredni, a drugi pośredni.  Bezpośrednie znaczenie wiąże się z nowym i ogólnym podejściem, które stanowi generalizację wcześniejszych prac w tym zakresie, w tym prac autora projektu, oraz będzie pierwszym pełnym ujęciem metateorii systemów tablicowych.

Z kolei aspekt pośredni wiąże się z możliwością badania oraz stosowania wypracowanych narzędzi do nowych systemów tablicowych. Pośrednie  znaczenie wynika z możliwości stosowania ogólnych i formalnych pojęć tablicowych oraz ich konsekwencji (takich jak metatwierdzenie tablicowe) do różnych metalogicznych proble- mów, takich jak efektywność czy siła dedukcyjna  poszczególnych systemów tablicowych. Pośrednio narzędzia takie pozwalają precyzyjne badać również zagadnienia pokrewne  rozstrzygalności  (oszacowanie długości dowodów, zamykanie tablic czy w końcu tablicowa rozstrzygalność).

Podsumowując, nie powstała  jeszcze ogólna i formalna metateoria systemów tablicowych, więc projekt ma pionierski charakter. Projekt badawczy wypełni tę lukę, gdyż jego trwałym efektem będzie cykl artykułów w anglojęzycznych czasopismach naukowych.

W realizacji projektu zamierzamy stosować przyjęte w naukach formalnych meto- dy matematyczne, definiując pojęcia na gruncie teorii mnogości oraz dowodząc klasycznie związków pomiędzy pojęciami. Będziemy również stosować metodę studium przypadku, definiując pojęcia tablicowe  dla dwuwartościowych logik zdaniowych, logik z interpretacją wielowartościową oraz logik z kwantyfikatorami.  Na podstawie tych przypadków dokonamy generalizacji wyjściowych pojęć, zachowując w ich zakresie zastosowania, które zostały przebadane we wcześniejszych pracach.

https://projekty.ncn.gov.pl/index.php?s=7153