Kanoniczne i dualne rachunki erotetyczne dla logiki I-rzędu
Loading...
Date
2018
Authors
Advisor
Editor
Journal Title
Journal ISSN
Volume Title
Publisher
Title alternative
Canonical and Dual Erotetic Calculi for First-Order Logic
Abstract
W swojej książce First-Order Logic and Automated Theorem Proving Fitting wprowadził pojęcie własności niesprzeczności (CP), blisko spokrewnione z pojęciem zbioru Hintikki. Własność niesprzeczności jest rodziną formuł spełniającą pewne kryteria. Główne twierdzenie dotyczące CP głosi, że każdy zbiór należący do CP posiada model Herbranda. Z punktu widzenia teorii dowodu, własności niesprzeczności mogą zostać z powodzeniem użyte w celu jednorodnego dowodu pełności dla rozmaitych systemów dowodzenia twierdzeń, w tym tabel analitycznych, systemów aksjomatycznych, rachunku sekwentów czy rezolucji, nie mogą być jednak w prosty sposób wykorzystane w dowodach pełności systemów dualnych, np. dualnej rezolucji. W rozprawie wprowadzone zostają pojęcia dualnego zbioru Hintikki oraz własności falsyfikowalności (RF) oraz udowodnione zostaje twierdzenie o istnieniu kontrmodelu, zgodnie z którym każdy zbiór należący do RF posiada kontrmodel Herbranda. Wprowadzona zostaje technika oparta na pojęciu RF, którą zastosowano w celu uzyskania jednorodnego dowodu pełności dla trzech dualnych rachunków erotetycznych dla logiki I-rzędu zdefiniowanych w rozprawie.
In his book First-Order Logic and Automated Theorem Proving Fitting introduced the notion of a first-order consistency property, which is closely related to the notion of a Hintikka set. Consistency property is a family of sets of first-order sentences meeting certain conditions. The central observation called model existence theorem states that every member of a consistency property has a Herbrand model. From a proof-theoretical point of view, the notion of a consistency property enables an uniform completeness proof for various proof systems such as tableaux method, sequent calculus, and resolution, but is not so natural when applied to dual systems, such as dual resolution. In the dissertation notions of dual Hintikka set and first-order refutability property are introduced together with counter model existence theorem, which states that every member of a first-order refutability property can be falsified in some Herbrand model. These concepts are used to prove completeness of three new dual erotetic calculi (based on Inferential Erotetic Logic and resolution) for first-order logic.
In his book First-Order Logic and Automated Theorem Proving Fitting introduced the notion of a first-order consistency property, which is closely related to the notion of a Hintikka set. Consistency property is a family of sets of first-order sentences meeting certain conditions. The central observation called model existence theorem states that every member of a consistency property has a Herbrand model. From a proof-theoretical point of view, the notion of a consistency property enables an uniform completeness proof for various proof systems such as tableaux method, sequent calculus, and resolution, but is not so natural when applied to dual systems, such as dual resolution. In the dissertation notions of dual Hintikka set and first-order refutability property are introduced together with counter model existence theorem, which states that every member of a first-order refutability property can be falsified in some Herbrand model. These concepts are used to prove completeness of three new dual erotetic calculi (based on Inferential Erotetic Logic and resolution) for first-order logic.
Description
Wydział Nauk Społecznych
Sponsor
Keywords
teoria dowodu, inferencyjna logika pytań, logika I-rzędu, proof theory, inferential erotetic logic, first-order logic