Rational Pavelka Logic
Origin. Pavelka (1979), Hájek (1998). Graded provability. Truth constants for rationals. Complete degree calculus. Foundation for graded deduction.
Models. Łukasiewicz logic with rational constants. r̄ denotes truth degree r ∈ [0,1] ∩ ℚ. Graded theorems. Fuzzy deduction theorem.
Formalism.
Language: Standard connectives plus constants. r̄ for each r ∈ [0,1] ∩ ℚ. Interpretation: v(r̄) = r.
Graded consequence: Γ ⊨_r φ: degree of φ at least r given Γ. |φ|_Γ = inf{v(φ) : v ⊨ Γ} (if Γ consistent)
Graded provability: ||φ||_Γ = sup{r : Γ ⊢ r̄ → φ} Syntactic degree.
Pavelka completeness: |φ|_Γ = ||φ||_Γ Semantic = syntactic degree.
Axioms (over Ł): r̄ ↔ s̄ if r = s (r̄ → s̄) ↔ min(1, 1-r+s) (r̄ & s̄) ↔ max(0, r+s-1)
Deduction theorem: Γ, φ ⊢ ψ iff Γ ⊢ φⁿ → ψ for some n. Local, inherited from Ł; the constants do not repair it.
Bookkeeping axioms: Axioms compute truth degrees. Infinitely many axioms.
Modus ponens: From φ and φ → ψ, infer ψ. Degree calculus: from r and r → s, get s.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| ⊢ | U+22A2 | Right tack | Derivability in RPL |
| ⊨ | U+22A8 | Satisfaction | Truth in all models of a theory |
| → | U+2192 | Rightwards arrow | Łukasiewicz implication, min(1, 1−x+y) |
| ↔ | U+2194 | Left right arrow | Provable equivalence, used in the bookkeeping axioms |
| & | U+0026 | Ampersand | Strong conjunction, max(0, x+y−1) |
| ℚ | U+211A | Double-struck Q / Rationals | The constants range over [0,1] ∩ ℚ |
| Γ | U+0393 | Gamma | A theory: a set of premise formulas |
| φ | U+03C6 | Phi | A formula |
| r̄ | — | Truth constant | Names the rational degree r; v(r̄) = r |
| ⊢_r | — | Graded provability | φ derivable to degree at least r |
| ⊨_r | — | Graded consequence | φ true to degree at least r in every model |
| |φ|_Γ | — | Truth degree | inf{v(φ) : v ⊨ Γ} |
| ||φ||_Γ | — | Provability degree | sup{r : Γ ⊢ r̄ → φ} |
| RPL | — | Rational Pavelka logic | Ł∞ plus rational constants and bookkeeping |
Metatheory. Pavelka (1979) proved a completeness theorem for a graded consequence relation, but at the cost of an infinitary apparatus; Hájek (1995, 1998) showed that the same result is available from a finitary schematic extension of infinite-valued Łukasiewicz logic — add a constant r̄ for each rational r in [0,1] together with the bookkeeping axioms fixing the values of r̄ → s̄ and r̄ & s̄, and Pavelka-style completeness follows. That theorem states an identity rather than an implication: for every theory Γ and formula φ, the provability degree ||φ||_Γ equals the truth degree |φ|_Γ, so the syntactic supremum and the semantic infimum coincide exactly. RPL is a conservative extension of Ł∞ — a constant-free formula is provable in one iff in the other. The result depends on a specific property of the base logic: the Łukasiewicz residuum min(1, 1−x+y) is continuous, and Pavelka-style completeness fails in this form for Gödel and product logic, whose residua jump at the diagonal. The bookkeeping axioms are infinitely many but form a decidable set, so RPL remains recursively axiomatized. Hájek extended the graded completeness theorem to the first-order case.
Applies to. Approximate reasoning. Graded beliefs. Expert systems. Fuzzy databases.
Limitations. Pavelka-style completeness is a statement about degrees, not about theoremhood: the formulas provable to degree 1 are those of Ł∞ together with what the constants add, so the graded apparatus adds expressiveness rather than deductive strength. The constants must stay rational — admitting a constant for every real would make the axiom set undecidable and destroy recursive axiomatizability, so no irrational degree can be named. The construction does not generalize across the fuzzy family: it turns on the continuity of the Łukasiewicz implication and fails for Gödel and product logic. Provability and truth degrees are defined relative to a theory, and an inconsistent theory collapses them, so the machinery gives no graded account of inconsistency. In the first-order case graded completeness holds but is not effective: the set of first-order Łukasiewicz validities over the standard algebra is Π₂-complete, so there is no recursive enumeration of what the theorem asserts to be provable.
© 2026 Lingenic LLC