Synthetic Completeness Proofs for Seligman-style Tableau Systems

Klaus Frovin Jørgensen, Patrick Rowan Blackburn, Thomas Bolander, Torben Braüner

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Hybrid logic is a form of modal logic which allows reference to worlds. We can think of it as ‘modal logic with labelling built into the object language’ and various forms of labelled deduction have played a central role in its proof theory. Jerry Seligman’s work [11,12] in which ‘rules involving labels’ are rejected in favour of ‘rules for all’ is an interesting exception to this. Seligman’s approach was originally for natural deduction; the authors of the present paper recently extended it to tableau inference [1,2]. Our earlier work was syntactic: we showed completeness by translating between Seligman-style and labelled tableaus, but our results only covered the minimal hy- brid logic; in the present paper we provide completeness results for a wider range of hybrid logics and languages. We do so by adapting the synthetic approach to tableau completeness (due to Smullyan, and widely applied in modal logic by Fitting) so that we can directly build maximal consistent sets of tableau blocks.
Original languageEnglish
Title of host publicationProceedings of Advances in Modal Logic 2016
EditorsLev Beklemishev, Stéphane Demri, András Máté
Volume11
PublisherCollege Publications
Publication date2016
Pages302-321
ISBN (Print)978-1-84890-201-5
Publication statusPublished - 2016
EventAdvances in Modal Logic 2016 - Eotvos University, Budapest, Hungary
Duration: 30 Aug 20162 Sep 2016
http://phil.elte.hu/aiml2016/ (Link to Conference)

Conference

ConferenceAdvances in Modal Logic 2016
LocationEotvos University
CountryHungary
CityBudapest
Period30/08/201602/09/2016
Internet address

Keywords

    Cite this

    Jørgensen, K. F., Blackburn, P. R., Bolander, T., & Braüner, T. (2016). Synthetic Completeness Proofs for Seligman-style Tableau Systems. In L. Beklemishev, S. Demri, & A. Máté (Eds.), Proceedings of Advances in Modal Logic 2016 (Vol. 11, pp. 302-321). College Publications.
    Jørgensen, Klaus Frovin ; Blackburn, Patrick Rowan ; Bolander, Thomas ; Braüner, Torben. / Synthetic Completeness Proofs for Seligman-style Tableau Systems. Proceedings of Advances in Modal Logic 2016. editor / Lev Beklemishev ; Stéphane Demri ; András Máté. Vol. 11 College Publications, 2016. pp. 302-321
    @inproceedings{be2316063b7f47a397ee4507732a871a,
    title = "Synthetic Completeness Proofs for Seligman-style Tableau Systems",
    abstract = "Hybrid logic is a form of modal logic which allows reference to worlds. We can think of it as ‘modal logic with labelling built into the object language’ and various forms of labelled deduction have played a central role in its proof theory. Jerry Seligman’s work [11,12] in which ‘rules involving labels’ are rejected in favour of ‘rules for all’ is an interesting exception to this. Seligman’s approach was originally for natural deduction; the authors of the present paper recently extended it to tableau inference [1,2]. Our earlier work was syntactic: we showed completeness by translating between Seligman-style and labelled tableaus, but our results only covered the minimal hy- brid logic; in the present paper we provide completeness results for a wider range of hybrid logics and languages. We do so by adapting the synthetic approach to tableau completeness (due to Smullyan, and widely applied in modal logic by Fitting) so that we can directly build maximal consistent sets of tableau blocks.",
    keywords = "Hybrid logic, difference operator, universal modality, tense logic, pure axioms, Bridge rule, synthetic completeness method, Seligman-style, tableaus",
    author = "J{\o}rgensen, {Klaus Frovin} and Blackburn, {Patrick Rowan} and Thomas Bolander and Torben Bra{\"u}ner",
    year = "2016",
    language = "English",
    isbn = "978-1-84890-201-5",
    volume = "11",
    pages = "302--321",
    editor = "Lev Beklemishev and St{\'e}phane Demri and Andr{\'a}s M{\'a}t{\'e}",
    booktitle = "Proceedings of Advances in Modal Logic 2016",
    publisher = "College Publications",

    }

    Jørgensen, KF, Blackburn, PR, Bolander, T & Braüner, T 2016, Synthetic Completeness Proofs for Seligman-style Tableau Systems. in L Beklemishev, S Demri & A Máté (eds), Proceedings of Advances in Modal Logic 2016. vol. 11, College Publications, pp. 302-321, Advances in Modal Logic 2016, Budapest, Hungary, 30/08/2016.

    Synthetic Completeness Proofs for Seligman-style Tableau Systems. / Jørgensen, Klaus Frovin; Blackburn, Patrick Rowan; Bolander, Thomas; Braüner, Torben.

    Proceedings of Advances in Modal Logic 2016. ed. / Lev Beklemishev; Stéphane Demri; András Máté. Vol. 11 College Publications, 2016. p. 302-321.

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    TY - GEN

    T1 - Synthetic Completeness Proofs for Seligman-style Tableau Systems

    AU - Jørgensen, Klaus Frovin

    AU - Blackburn, Patrick Rowan

    AU - Bolander, Thomas

    AU - Braüner, Torben

    PY - 2016

    Y1 - 2016

    N2 - Hybrid logic is a form of modal logic which allows reference to worlds. We can think of it as ‘modal logic with labelling built into the object language’ and various forms of labelled deduction have played a central role in its proof theory. Jerry Seligman’s work [11,12] in which ‘rules involving labels’ are rejected in favour of ‘rules for all’ is an interesting exception to this. Seligman’s approach was originally for natural deduction; the authors of the present paper recently extended it to tableau inference [1,2]. Our earlier work was syntactic: we showed completeness by translating between Seligman-style and labelled tableaus, but our results only covered the minimal hy- brid logic; in the present paper we provide completeness results for a wider range of hybrid logics and languages. We do so by adapting the synthetic approach to tableau completeness (due to Smullyan, and widely applied in modal logic by Fitting) so that we can directly build maximal consistent sets of tableau blocks.

    AB - Hybrid logic is a form of modal logic which allows reference to worlds. We can think of it as ‘modal logic with labelling built into the object language’ and various forms of labelled deduction have played a central role in its proof theory. Jerry Seligman’s work [11,12] in which ‘rules involving labels’ are rejected in favour of ‘rules for all’ is an interesting exception to this. Seligman’s approach was originally for natural deduction; the authors of the present paper recently extended it to tableau inference [1,2]. Our earlier work was syntactic: we showed completeness by translating between Seligman-style and labelled tableaus, but our results only covered the minimal hy- brid logic; in the present paper we provide completeness results for a wider range of hybrid logics and languages. We do so by adapting the synthetic approach to tableau completeness (due to Smullyan, and widely applied in modal logic by Fitting) so that we can directly build maximal consistent sets of tableau blocks.

    KW - Hybrid logic

    KW - difference operator

    KW - universal modality

    KW - tense logic

    KW - pure axioms

    KW - Bridge rule

    KW - synthetic completeness method

    KW - Seligman-style

    KW - tableaus

    M3 - Article in proceedings

    SN - 978-1-84890-201-5

    VL - 11

    SP - 302

    EP - 321

    BT - Proceedings of Advances in Modal Logic 2016

    A2 - Beklemishev, Lev

    A2 - Demri, Stéphane

    A2 - Máté, András

    PB - College Publications

    ER -

    Jørgensen KF, Blackburn PR, Bolander T, Braüner T. Synthetic Completeness Proofs for Seligman-style Tableau Systems. In Beklemishev L, Demri S, Máté A, editors, Proceedings of Advances in Modal Logic 2016. Vol. 11. College Publications. 2016. p. 302-321