- Tytuł:
- A Syntactic Proof of the Decidability of First-Order Monadic Logic
- Autorzy:
-
Orlandelli, Eugenio
Tesi, Matteo - Powiązania:
- https://bibliotekanauki.pl/articles/43188312.pdf
- Data publikacji:
- 2024
- Wydawca:
- Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
- Tematy:
-
proof theory
classical logic
decidability
Herbrand theorem - Opis:
- Decidability of monadic first-order classical logic was established by Löwenheim in 1915. The proof made use of a semantic argument and a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3-style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity-optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the modal logic T.
- Źródło:
-
Bulletin of the Section of Logic; 2024, 53, 2; 223-244
0138-0680
2449-836X - Pojawia się w:
- Bulletin of the Section of Logic
- Dostawca treści:
- Biblioteka Nauki
Artykuł