An effective fixed-point theorem in intuitionistic diagonalizable algebras |
| |
Authors: | Giovanni Sambin |
| |
Affiliation: | (1) Institute of Mathematics, Siena University, Italy |
| |
Abstract: | Summary Within the technical frame supplied by the algebraic variety of diagonalizable algebras, defined by R. Magari in [2], we prove the following:LetT be any first-order theory with a predicate Pr satisfying the canonical derivability conditions, including Löb's property. Then any formula inT built up from the propositional variables q, p1, ..., pn, using logical connectives and the predicate Pr, has the same fixed-points relative to q (that is, formulas (p1 ..., pn) for which for all p1, ..., pn T((p1, ..., pn), p1, ..., pn) (p1, ..., pn)) of a formula * of the same kind, obtained from in an effective way.Moreover, such * is provably equivalent to the formula obtained from substituting with * itself all the occurrences of q which are under Pr. In the particular case where q is always under Pr in , * is the unique (up to provable equivalence) fixedpoint of .Since this result is proved only assumingPr to be canonical, it can be deduced that Löb's property is, in a sense, equivalent to Gödel's diagonalization lemma.All the results are proved more generally in the intuitionistic case.The algebraization of the theories which express Theor, IXAllatum est die 19 Decembris 1975 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|