Decidable and enumerable predicate logics of provability (Q750418): Difference between revisions
From MaRDI portal
Set profile property. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Q4375098 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4196401 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The degree of the set of sentences of predicate provability logic that are true under every interpretation / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Provability interpretations of modal logic / rank | |||
Normal rank |
Latest revision as of 12:34, 21 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Decidable and enumerable predicate logics of provability |
scientific article |
Statements
Decidable and enumerable predicate logics of provability (English)
0 references
1990
0 references
The predicate modal logic with \(\square\) interpreted as provability in some extension T of arithmetic is not recursively axiomatizable, and the set of true formulas is not arithmetic. The author finds enumerable fragments. A proof of decidability and completeness for formulas in one individual variable x is presented, where \(\forall x\) is interpreted as an S5-modality with additional axiom \(\square \forall A\to \forall \square A\). For provably \(\Pi_ 1\)-complete theories T the predicate version of K is complete for the predicate modal formulas of depth 1, and the predicate version of K4 is complete for the formulas \(\square^ n\perp \to A\) with arbitrary A. \(\Pi_ 1\)-completeness is used to describe inside T the construction of a model.
0 references
provability logic
0 references
predicate modal logic
0 references
enumerable fragments
0 references
decidability
0 references
completeness
0 references
0 references