We consider fixed point logics, i.e., extensions of first order predicate logic with operators defining fixed points. A number of such operators, generalizing inductive definitions, have been studied in the context of finite model theory, including nondeterministic and alternating operators. We review results established in finite model theory, and also consider the expressive power of the resulting logics on infinite structures. In particular, we establish the relationship between inflationary and nondeterministic fixed point logics and (...) second order logic, and we consider questions related to the determinacy of games associated with alternating fixed points. (shrink)

Michael Kremer defines fixed-point logics of truth based on Saul Kripke’s fixed point semantics for languages expressing their own truth concepts. Kremer axiomatizes the strong Kleene fixed-point logic of truth and the weak Kleene fixed-point logic of truth, but leaves the axiomatizability question open for the supervaluation fixed-point logic of truth and its variants. We show that the principal supervaluation fixed point logic of truth, (...) when thought of as consequence relation, is highly complex: it is not even analytic. We also consider variants, engendered by a stronger notion of ‘fixed point’, and by variant supervaluation schemes. A ‘logic’ is often thought of, not as a consequence relation, but as a set of sentences – the sentences true on each interpretation. We axiomatize the supervaluation fixed-point logics so conceived. (shrink)

We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. (...) We also show how extracted programs can be translated into Haskell. As an application we extract a program converting the signed digit representation of real numbers to infinite Gray code from a proof of inclusion of the corresponding coinductive predicates. (shrink)

Given a simple non-trivial finite-dimensional Lie algebra L, fields $K_i$ and Chevalley groups $L(K_i)$ , we first prove that $\Pi_{\mathcal{U}} L(K_i)$ is isomorphic to $L(\Pi_{\mathcal{U}}K_i)$ . Then we consider the case of Chevalley groups of twisted type ${}^n\!L$ . We obtain a result analogous to the previous one. Given perfect fields $K_i$ having the property that any element is either a square or the opposite of a square and Chevalley groups ${}^n\!L(K_i)$ , then $\pu{}^n\!L(K_i)$ is isomorphic to ${}^n\!L(\pu K_i)$ . (...) We apply our results to prove the decidability of the set of sentences true in almost all finite groups of the form L(K) where K is a finite field and L a fixed untwisted Chevalley type. (shrink)

We consider the reduct to the module language of certain theories of fields with a non surjective endomorphism. We show in some cases the existence of a model companion. We apply our results for axiomatizing the reduct to the theory of modules of non principal ultraproducts of separably closed fields of fixed but non zero imperfection degree.

We develop a variant of Least Fixed Point logic based on First Orderlogic with a relaxed version of guarded quantification. We develop aGame Theoretic Semantics of this logic, and find that under reasonableconditions, guarding quantification does not reduce the expressibilityof Least Fixed Point logic. But we also find that the guarded version ofa least fixed point algorithm may have a greater time complexity thanthe unguarded version, by a linear factor.

We study the expressive power in the finite of the logic Fixed-Point+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count. To this end an isomorphism preserving (`generic') model of computation is introduced whose PTime restriction exactly corresponds to this level of expressive power, while its PSpace restriction corresponds to While+Counting. From this model we obtain a normal form which shows a rather clear separation (...) of the relational vs. the arithmetical side of the algorithms involved. In parallel, we study the relations of Fixed-Point+Counting with the infinitary logics L r ∞ω (∃ ≥ m ) m∈ω and the corresponding pebble games. The main result, however, involves the concept of an arithmetical invariant. By this we mean a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. In particular its values are linearly ordered structures. We establish the existence of a family of arithmetical invariants (J r ) r≥ 1 with the following properties: $\bullet$ The invariants themselves can be evaluated in polynomial time. $\bullet$ A class of finite relational structures is definable in Fixed-Point+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants. $\bullet$ The invariant J r classifies all finite relational structures exactly up to equivalence with respect to the logic L r ∞ω (∃ ≥ m ) m∈ω . We also give a characterization of Fixed-Point+Counting in terms of sequences of formulae in the L r ωω (∃ ≥ m ) m∈ω : It corresponds exactly to the polynomial time computable families (φ n ) n∈ω in these logics. Towards a positive assessment of the expressive power of Fixed-Point+Counting, it is shown that the natural extension of fixed-point logic by Lindström quantifiers, which capture all the PTime computable properties of cardinalities of definable predicates, is strictly weaker than what we get here. This implies in particular that every extension of fixed-point logic by means of monadic Lindstrom quantifiers, which stays within PTime, must be strictly contained in Fixed-Point+Counting. (shrink)

This is indeed a very nice draft that I have read with great pleasure, and that has helped me to better understand the completeness proof for LCC. Modal fixed point logic allows for an illuminating new version (and a further extension) of that proof. But still. My main comment is that I think the perspective on substitutions in the draft paper is flawed. The general drift of the paper is that relativization, (predicate) substitution and product update are (...) general operations on models, and that it is important to check whether given logical languages are closed under these operations. FO logic is closed under relativization, predicate substitution and product constructions (such as those involved in relative interpretation). The minimal modal logic is closed under relativization, which explains the reduction of epistemic logic (withhout common knowledge) + public announcement to epistemic logic simpliciter (as observed in Van Benthem, [2]). The reduction breaks down as soon as one adds common knowledge. The minimal modal logic is also closed under substitution, which explains the reduction of epistemic logic plus (publicly observable) factual change to epistemic logic simpliciter, via the following reduction axioms (I use !p := φ for the operation of publicly changing the truth value of p to φ): [!p := φ]p ↔ φ [!p := φ]q ↔ q (p and q syntactically different ) [!p := φ]¬ψ ↔ ¬[!p := φ]ψ [!p := φ](ψ1 ∧ ψ2) ↔ [!p := φ]ψ1 ∧ [!p := φ]ψ2 [!p := φ][i]ψ ↔ [i][!p := φ]ψ Unlike the case of relativisation, this can be extended to the case of epistemic logic with common knowledge, by means of: [!p := φ]CGψ ↔ CG[!p := φ]ψ We get the following.. (shrink)

We consider separably closed fields of characteristic $p > 0$ and fixed imperfection degree as modules over a skew polynomial ring. We axiomatize the corresponding theory and we show that it is complete and that it admits quantifier elimination in the usual module language augmented with additive functions which are the analog of the $p$-component functions.

The problem of Uniqueness and Explicit Definability of Fixed Points for Interpretability Logic is considered. It turns out that Uniqueness is an immediate corollary of a theorem of Smoryński.

Buchholz’s Ω μ+1-rules provide a major tool for the proof-theoretic analysis of arithmetical inductive definitions. The aim of this paper is to put this approach into the new context of modal fixed point logic. We introduce a deductive system based on an Ω-rule tailored for modal fixed point logic and develop the basic techniques for establishing soundness and completeness of the corresponding system. In the concluding section we prove a cut elimination and collapsing result (...) similar to that of Buchholz (Iterated inductive definitions and subsystems of analysis: recent proof theoretic studies. Lecture notes in mathematics, vol. 897, pp. 189–233, Springer, Berlin, 1981). (shrink)

This paper deals with the modal logics associated with (possibly nonstandard) provability predicates of Peano Arithmetic. One of our goals is to present some modal systems having the fixed point property and not extending the Gödel-Löb system GL. We prove that, for every has the explicit fixed point property. Our main result states that every complete modal logic L having the Craig's interpolation property and such that , where and are suitable modal formulas, has the (...) explicit fixed point property. (shrink)

The problem of Uniqueness and Explicit Definability of Fixed Points for Interpretability Logic is considered. It turns out that Uniqueness is an immediate corollary of a theorem of Smoryski.

We study the relationship between least and inflationary fixed-point logic. In 1986, Gurevich and Shelah proved that in the restriction to finite structures, the two logics have the same expressive power. On infinite structures however, the question whether there is a formula in IFP not equivalent to any LFP-formula was left open.In this paper, we answer the question negatively, i.e. we show that the two logics are equally expressive on arbitrary structures. We give a syntactic translation of (...) IFP-formulae to LFP-formulae such that the two formulae are equivalent on all structures.As a consequence of the proof we establish a close correspondence between the LFP-alternation hierarchy and the IFP-nesting depth hierarchy. We also show that the alternation hierarchy for IFP collapses to the first level, i.e. the complement of any inflationary fixed point is itself an inflationary fixed point. (shrink)

The paper presents a survey of author's results on definable fixed points in modal, temporal, and intuitionistic propositional logics. The well-known Fixed Point Theorem considers the modalized case, but here we investigate the positive case. We give a classification of fixed point theorems, describe some classes of models with definable least fixed points of positive operators, special positive operators, and give some examples of undefinable least fixed points. Some other interesting phenomena are discovered (...) – definability by formulas that do not preserve positivity of parameters and definability by finite sets of formulas. We also consider negative operators, graded modalities, construct undefinable inflationary fixed points, and put some problems. (shrink)

We study a system, μŁΠ, obtained by an expansion of ŁΠ logic with fixed points connectives. The first main result of the paper is that μŁΠ is standard complete, i.e., complete with regard to the unit interval of real numbers endowed with a suitable structure. We also prove that the class of algebras which forms algebraic semantics for this logic is generated, as a variety, by its linearly ordered members and that they are precisely the interval algebras (...) of real closed fields. This correspondence is extended to a categorical equivalence between the whole category of those algebras and another category naturally arising from real closed fields. Finally, we show that this logic enjoys implicative interpolation. (shrink)

We present a quite simple proof of the fixed point theorem for GL. We also use this proof to show that Sambin's algorithm yields a fixed point.

In the context of his theory of numberings, Ershov showed that Kleene's recursion theorem holds for any precomplete numbering. We discuss various generalizations of this result. Among other things, we show that Arslanov's completeness criterion also holds for every precomplete numbering, and we discuss the relation with Visser's ADN theorem, as well as the uniformity or nonuniformity of the various fixed point theorems. Finally, we base numberings on partial combinatory algebras and prove a generalization of Ershov's theorem in (...) this context. (shrink)

In response to the liar’s paradox, Kripke developed the fixed-point semantics for languages expressing their own truth concepts. Kripke’s work suggests a number of related fixed-point theories of truth for such languages. Gupta and Belnap develop their revision theory of truth in contrast to the fixed-point theories. The current paper considers three natural ways to compare the various resulting theories of truth, and establishes the resulting relationships among these theories. The point is to (...) get a sense of the lay of the land amid a variety of options. Our results will also provide technical fodder for the methodological remarks of the companion paper to this one. (shrink)

An algebraic proof is presented for the finite strong standard completeness of the Involutive Uninorm Logic with Fixed Point ($${{\mathbf {IUL}}^{fp}}$$ IUL fp ). It may provide a first step towards settling the standard completeness problem for the Involutive Uninorm Logic ($${\mathbf {IUL}}$$ IUL, posed in G. Metcalfe, F. Montagna. (J Symb Log 72:834–864, 2007)) in an algebraic manner. The result is proved via an embedding theorem which is based on the structural description of the class (...) of odd involutive FL$$_e$$ e -chains which have finitely many positive idempotent elements. (shrink)

This paper introduces a new kind of fixed-point semantics, filling a gap within approaches to Liar-like paradoxes involving fixed-point models à la Kripke (1975). The four-valued models presented below, (i) unlike the three-valued, consistent fixed-point models defined in Kripke (1975), are able to differentiate between paradoxical and pathological-but-unparadoxical sentences, and (ii) unlike the four-valued, paraconsistent fixed-point models first studied in Visser (1984) and Woodruff (1984), preserve consistency and groundedness of truth.

In this paper it is shown that the intuitionistic .xed point theory equation image for α times iterated fixed points of strictly positive operator forms is conservative for negative arithmetic and equation image sentences over the theory equation image for α times iterated arithmetic comprehension without set parameters.This generalizes results previously due to Buchholz [5] and Arai [2].

Jäger, G., Fixed points in Peano arithmetic with ordinals, Annals of Pure and Applied Logic 60 119-132. This paper deals with some proof-theoretic aspects of fixed point theories over Peano arithmetic with ordinals. It studies three such theories which differ in the principles which are available for induction on the natural numbers and ordinals. The main result states that there is a natural theory in this framework which is a conservative extension of Peano arithmeti.

Este trabajo supone un intento serio de introducir y englobar de manera sistemática las investigaciones más recientes acerca de las teorías del punto fijo desde diferentes vertientes que han aparecido en las teorías de la lógica matemática. Es, por lo tanto, un libro sistemático, y de ahí su debilidad, al no haber asumido el origen de determinadas corrientes que aquí se exponen. Por esta razón, ha de indicarse de entrada que lo que el lector no encontrará será una reconstrucción crítica (...) de la basta bibliografía sobre el tema, ni una conclusión amplia de los senderos que ha tomado la investigación. El libro recompila pues, las tendencias más importantes y nos libera de la búsqueda infructuosa por las revistas como Studia Logica, el The Journal of Symbolic Logic, y demás revistas matemáticas especializadas en el tema. Por lo tanto, en resumidas cuentas, estamos ante un excelente modo de introducir pero con un deficiente aparato crítico. (shrink)

Este trabajo supone un intento serio de introducir y englobar de manera sistemática las investigaciones más recientes acerca de las teorías del punto fijo desde diferentes vertientes que han aparecido en las teorías de la lógica matemática. Es, por lo tanto, un libro sistemático, y de ahí su debilidad, al no haber asumido el origen de determinadas corrientes que aquí se exponen. Por esta razón, ha de indicarse de entrada que lo que el lector no encontrará será una reconstrucción crítica (...) de la basta bibliografía sobre el tema, ni una conclusión amplia de los senderos que ha tomado la investigación. El libro recompila pues, las tendencias más importantes y nos libera de la búsqueda infructuosa por las revistas como Studia Logica, el The Journal of Symbolic Logic, y demás revistas matemáticas especializadas en el tema. Por lo tanto, en resumidas cuentas, estamos ante un excelente modo de introducir pero con un deficiente aparato crítico. (shrink)

In this paper we show that the intuitionistic fixed point theory FiXi over set theories T is a conservative extension of T if T can manipulate finite sequences and has the full foundation schema.

Self-referential sentences have troubled our understanding of language for centuries. The most famous self-referential sentence is probably the Liar, a sentence that says of itself that it is false. The Liar Paradox has encouraged many philosophers to establish theories of truth that manage to give a proper account of the truth predicate in a formal language. Kripke’s Fixed Point Theory from 1975 is one famous example of such a formal theory of truth that aims at giving a plausible (...) notion of truth by allowing truth value gaps. However, not only the concept of truth gives rise to paradoxes. A syntactical treatment of epistemic notions like belief and knowledge leads to contradictions that very much resemble the Liar Paradox. Therefore, it seems to be fruitful to apply the established theories of truth to epistemic concepts. In this paper, I will present one such attempt of solving the epistemic paradoxes: I adapt Kripke’s Fixed Point Theory and interpret truth, knowledge and belief within the framework of a partial logic. Thereby I find not only the fixed point of truth but also the fixed points of knowledge and belief. In this fixed point, the predicates of truth, belief and knowledge find their definite interpretation and the paradoxes are avoided. (shrink)

This article defends the Fixed Point Thesis: that it is always a rational mistake to have false beliefs about the requirements of rationality. The Fixed Point Thesis is inspired by logical omniscience requirements in formal epistemology. It argues to the Fixed Point Thesis from the Akratic Principle: that rationality forbids having an attitude while believing that attitude is rationally forbidden. It then draws out surprising consequences of the Fixed Point Thesis, for instance (...) that certain kinds of a priori justification are indefeasible and that misleading all-things-considered evidence about rational requirements is impossible. Finally, the Fixed Point Thesis is applied to defend the Right Reasons position on peer disagreement, according to which an agent who has drawn the correct conclusion from her evidence should retain belief in that conclusion even in the face of disagreeing peers. (shrink)

There is a vibrant community among philosophical logicians seeking to resolve the paradoxes of classes, properties and truth by way of adopting some non-classical logic in which trivialising paradoxical arguments are not valid. There is also a long tradition in theoretical computer science|going back to Dana Scott's fixed point model construction for the untyped lambda-calculus of models allowing for fixed points. In this paper, I will bring these traditions closer together, to show how these model constructions (...) can shed light on what we could hope for in a non-trivial model of a theory for classes, properties or truth featuring fixed points. (shrink)

We prove an analogue of the fixed-point theorem for the case of definably amenable groups.

By an unfounded chain for a function f:X→X we mean a sequence nω of elements of X s.t. fxn+1=xn for every n. Unfounded chains can be regarded as a generalization of fixed points, but on the other hand are linked with concepts concerning non-well-founded situations, as ungrounded sentences and the hypergame. In this paper, among other things, we prove a lemma in general topology, we exhibit an extensional recursive function from the set of sentences of PA into itself without (...) an unfounded chain, and we prove that every term in a Magari algebra has an unfounded chain. (shrink)

We give a characterization of the fixed points and of the lattices of fixed points of fuzzy Galois connections. It is shown that fixed points are naturally interpreted as concepts in the sense of traditional logic.

The relation between least and diagonal fixed points is a well known and completely studied question for a large class of partially ordered models of the lambda calculus and combinatory logic. Here we consider this question in the context of algebraic recursion theory, whose close connection with combinatory logic recently become apparent. We find a comparatively simple and rather weak general condition which suffices to prove the equality of least fixed points with canonical (corresponding to those (...) produced by the Curry combinator in lambda calculus) diagonal fixed points in a class of partially ordered algebras which covers both combinatory spaces of Skordev and operative spaces of Ivanov. Especially, this yields an essential improvement of the axiomatization of recursion theory via combinatory spaces. (shrink)

We study the fixed point property and the Craig interpolation property for sublogics of the interpretability logic \(\textbf{IL}\). We provide a complete description of these sublogics concerning the uniqueness of fixed points, the fixed point property and the Craig interpolation property.