Rachunki sekwentowe dla trzech teorii niefregowskich
Loading...
Date
2024
Authors
Editor
Journal Title
Journal ISSN
Volume Title
Publisher
Title alternative
Sequent Calculi for Three non-Fregean Theories
Abstract
Celem pracy jest przedstawienie trzech rachunków sekwentów dla trzech rozszerzeń aksjomatycznych Rachunku Zdaniowego z Identycznością (SCI). Formalizacje teorii WB, WT i WH w rachunkach sekwentowych opierają się na włączeniu dodatkowych reguł dla identyczności. Powstałe rachunki sekwentów to, kolejno, G3WB (gdzie sekwenty są dodatkowo etykietowane), G3WT i G3WH; w dwóch pierwszych dodana reguła jest formalizacją definicji logiki z wykorzystaniem operacji konsekwencji, natomiast w przypadku ostatniego wymienionego systemu, dodana reguła powstała z aksjomatu logiki WH. W powstałych systemach dowodowych problemem jest eliminacja reguł strukturalnych. W przypadku systemów powstałych przez dodanie reguł prawostronnych, tj. w G3WB i G3WT reguła cięcia może być wyeliminowana, ale wiąże się to z dodaniem do zbioru reguł reguły osłabiania; w przypadku G3WH mamy do czynienia z tą samą sytuacją, jako że rachunek ten jest rozszerzeniem G3WT. Analiza rachunków sekwentów uzupełniona jest o dostosowanie semantyki algebraicznej i wykazanie względem niej pełności i trafności trzech wspomnianych rachunków. Każdy rachunek oparty jest na innej semantyce algebraicznej, kolejno, algebrach Boole’a, topologicznych algebrach Boole’a i algebrach Henlego. W pracy wskazane są różnice w opisie semantycznym powstałych systemów sekwentowych, będące konsekwencją wykorzystania trzech wspomnianych algebr.
The aim of the work is to present three sequent calculi for three axiomatic extensions of non-Fregean logic called Sentential Calculus with Identity (SCI). Theories WB, WT and WH are formalised as sequent calculi through the addition of different identity-dedicated rules, thus obtaining, respectively, G3WB (in this case the sequents are additionally labelled to control the application of rules), G3WT and G3WH. In the case of G3WB and G3WT the added rules refer to the definitions of theories through consequence operation, whereas for WH, the added rule is a formalization of an axiom. In the resulted proof systems the main problems are concerned with the admissibility of structural rules. Due to the addition of right-sided rules in G3WB and G3WT the cut rule can be eliminated provided the weakening rule is included in the set of rules; the same goes for G3WH since it is built upon G3WT. The mentioned analysis was accompanied by adapting algebraic semantics to sequents along with providing proofs for completeness and soundness with regard to these semantics, that is, respectively, Boole algebra, topological Boolean algebra and Henle algebra. The work indicates the differences within the semantic description of the resulted sequent calculi, which are stemming from the utilisation of the three mentioned algebraic systems.
Description
Wydział Nauk Politycznych i Dziennikarstwa
Wydział Psychologii i Kognitywistyki
Sponsor
National Science Centre, grant no 2017/26/E/HS1/00127
Keywords
rachunek sekwentów, logika niefregowska, SCI, identyczność, eliminacja cięcia, sequent calculus, non-Fregean logic, identity, cut elimination