Reactive intuitionistic tableaux (Q542126): Difference between revisions
From MaRDI portal
Changed an Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(2 intermediate revisions by 2 users not shown) | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2052587224 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Modal logics of reactive frames / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Craig's theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras / rank | |||
Normal rank |
Latest revision as of 04:08, 4 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Reactive intuitionistic tableaux |
scientific article |
Statements
Reactive intuitionistic tableaux (English)
0 references
8 June 2011
0 references
Every ordinary Kripke model \({\mathfrak m}\) for intuitionistic propositional logic turns into a so-called pre-reactive Kripke model \({\mathfrak n}\) whose worlds are the finite increasing (relative to the immediate accessibility) sequences of worlds in \({\mathfrak m}\), where the accessibility relation \(\alpha\preceq\beta\) means that \(\alpha\) is an initial subsequence of \(\beta\), and for every atom \(A\), \((*)\) \([\alpha\models A\text{ in }{\mathfrak n}\Leftrightarrow|\alpha|\models A\text{ in }{\mathfrak m}]\), where \(|\alpha|\) is the end element in \(\alpha\). In fact, these models are equivalent in the sense that \((*)\) holds for every formula \(A\). A reactive intuitionistic Kripke frame is obtained from a pre-reactive one by forbidding some sequences. Pre-reactive Beth tableaux are defined too. It is proved that the logic defined by the reactive frames is intuitionistic logic. There exists a reactive frame whose logic is not complete for any class of ordinary intuitionistic Kripke frames. This means that reactive semantics is stronger than the ordinary Kripke semantics.
0 references
intuitionistic logic
0 references
Kripke models
0 references
reactive Kripke models
0 references
Beth tableaux
0 references