Publications   of   Saeed Salehi

• Mathematical Logic
  
  
  • Intuitionistic and Constructive Arithmetics
  
  
  
  • Incompleteness in Classical Weak Arithmetics
  
  
  
• Theoretical Computer Science
  
  
  • Tree Automata and Tree Languages
  
  
  
  • Finite Universal Algebra
  
  
  

---

        Intuitionistic and Constructive Arithmetics

---

[ARS03] Mohammad Ardeshir & Wim Ruitenburg & Saeed Salehi, "Intuitionistic Axiomatizations for Bounded Extension Kripke Models", Annals of Pure and Applied Logic, Vol. 124, No. 1-3, (2003) pages 267-285 .

As an assistant researcher at IPM, I worked under the guidance of M. Ardeshir. The problem we started to work together was the completeness of Heyting Arithmetic HA with respect to its end-extension Kripke models (the models in which the upper node is and end-extension of the lower one), proposed by K.F. Wehmeier in [W96].
It is a folklore fact that constant-domain Kripke models (of intuitionistic logic) are axiomatized by the schema
"x ( A(x) Ú B ) Þ "x A(x) Ú B   where x is not free in B. It turned out that when the language of a predicate theory contains the symbol £, then the class of Krikp models that are end-extension with respect to £ can be axiomatized by the schema
"x £ y ( A(x,y) Ú B(y) ) Þ "x £ y A(x,y) Ú B(y)   where x is not free in B(y). Later on W. Ruitenburg joined us (in a visit to IPM) and proved that the above schema is provable in HA. So we solved the problem: HA is sound and (strongly) complete with respect to its end-extension Kripke models.
In [ARS03] we moreover axiomatized cofinal-extension Kripke models, and showed that the cofinal-extension Kripke models of HA are models of classical logic as well (satisfy the principle of excluded middle). The above axiomatizations were provided in a uniform (and much more general) form.

[W96] Wehmeier, K.F., "Classical and Intuitionistic Models of Arithmetic", Notre Dame Journal of Formal Logic, Vol. 37, No. 3 (1996) pages 452-461.

[S02] Saeed Salehi, "Decidable Formulas of Intuitionistic Primitive Recursive Arithmetic", Reports on Mathematical Logic, No. 36 (2002) pages 55-61 .

One way of measuring the strength of theories is characterizing their provably total (or provably recursive) functions. For intuitionistic theories, provably total functions reveal a lot about their decidable formulas; j is called decidable in T if the universal closure of jÚØj is T-provable. It is well-known that jÚØj is equivalent to $y£1 [(y=0 Þ j) & (y =1 Þ Øj)] in intuitionistic arithmetical theories. So, j is decidable in T if and only if its characteristic function [c_j(x)=1 when j(x) holds, and c_j(x)=0 when Øj(x) holds] is provably total in T. In [S02] I used the already known characterizations of provably total functions of Heyting Arithmetic HA, Intuitionistic Primitive Recursive Arithmetic iPRA, and Intuitionistic S₁-induction Arithmetic iS₁, to characterize their decidable formulas. In all the three cases, their decidable formulas are exactly their (provably) D₁-formulas. This gave a syntactic proof of a (model-theoretically proved) theorem of Z. Markovic & D. De Jongh in [M93] for HA.
The paper [S02] was accepted as my Mater Thesis with the highest grade (very good) at the School of Exact Sciences in Warsaw.

[M93] Markovic, Z., "On the Structure of Kripke Models of Heyting Arithmetic", Mathematical Logic Quarterly, Vol. 39, No. 4 (1993) pages 531-538.

[S03] Saeed Salehi, "Provably Total Functions of Basic Arithmetic", Mathematical Logic Quarterly, Vol. 49, No. 3 (2003) pages 316-322.

Realizability is a powerful semantics for intuitionistic theories, in particular for characterizing their provably total functions. As an interesting open problem we can mention the fact that the Double Negation Shift [DNS   "xØØf(x) ® ØØ"xf(x)] is not provable in HA; while we do not have a concrete Kripke model of HA which does not satisfy DNS. The only reason we have for the unprovability of DNS in HA is that it is not Kleene realizable, though HA is. As a matter of fact, the only (non-trivial) Kripke models that we can construct for HA are the ones described by C. Smorynski (1973); all of them are on finite frames, and so satisfy DNS. Though realizability provides a sound semantics for constructive arithmetics, it is not complete. For example the formalized form of Church's Thesis (which is classically false) is Kleene realizable.
In [S03] I introduced a new (numerical) realizability by primitive recursive functions, abbreviated by PR-realizability, and showed the soundness of Ruitenburg's Basic Arithmetic with respect to it. Basic Propositional Logic was invented by A. Visser (1981) and extended to predicates by W. Ruitenburg (1998); M. Ardeshir's PhD thesis (1995) investigated different aspects of this (predicate) logic. Basic Arithmetic BA is the counterpart of Heyting Arithmetic (on intuitionistic logic) and of Peano Arithmetic (on classical logic) based on basic logic. PR-realizability is very similar to Kleene's (recursive) realizability, only that recursive functions are restricted to primitive recursives.
This PR-realizability was further studied by D.A. Viter [V02] and by B.H. Park [P03] in their PhD dissertations under the supervision of V.A. Plisko.

[V02] Viter, D.A., "Primitive Recursive Realizability and Constructive Theory of Models" (in Russian), PhD Dissertation, Moscow State University, 2002.
[P03] Park, B.H., "Subrecursive Realizability and Predicate Logic" (in Russian), PhD Dissertation, Moscow State University, 2003.

[S05] Saeed Salehi, "Polynomially Bounded Recursive Realizability", Notre Dame Journal of Formal Logic, Vol. 46, No. 4 (2005) pages 407-417.

Two essential facts about the primitive recursive functions that were used in [S03] are

1. that those functions can be defined by an arithmetical formula; i.e., there exists a formula PR in the language of arithmetic such that when PR(n) holds then {n}, the recursive function with Gödel code n, is primitive recursive, and for any primitive recursive f there exists a natural m such that f={m} and PR(m) holds;
2. all the S-m-n functions can be chosen to be primitive recursive.

As a matter of fact, all the polynomially bounded (primitive) recursive functions satisfy these two properties as well. So, in [S05] I introduced another realizability, this time by polynomially bounded recursive functions, in notation P-realizability. Basic Arithmetic BA is not sound with respect to P-realizability, but a faithful subtheory of it is. This subtheory has the same provably total functions as BA, and since its own provably total functions are polynomially bounded primitive recursives, then every function provably total in BA is polynomially bounded primitive recursive too. This sharpens the earlier result of [S03] where (by the soundness of BA to PR-realizability) those functions were shown to be primitive recursives.

---

        Incompleteness in Classical Weak Arithmetics

---

[Sa02] Saeed Salehi, "Herbrand Consistency in Arithmetics with Bounded Induction", PhD Dissertation, Institute of Mathematics, Polish Academy of Sciences, 2002.
[Sa01] Saeed Salehi, "Unprovability of Herbrand Consistency in Weak Arithmetics" in Striegnitz K. (ed.), Proceedings of the sixth ESSLLI Student Session, European Summer School for Logic, Language, and Information (2001) pages 265-274.

Gödel's second incompleteness theorem (GST) was stated originally for sufficiently strong arithmetical theories: the ones which can carry about enough arithmetic are not able to prove their own consistency. Gödel's proof applied for all theories that contain (in a sense) primitive recursive arithmetic, PRA. However, the question as to whether even weaker theories can (or cannot) prove their own consistency, is interesting and even intriguing. If the theory is too weak to recognize any useful property of consistency (or provability) then its consistency statement is just another complicated sentence in the theory's eyes; and thus its unprovability in the theory is devoid of any philosophical meaning. Just because the theory is too weak to recognize anything official about the consistency statement, and the fact the theory cannot derive the consistency statement goes to say that the theory is too weak, not that the statement is too strong. But there are some theories weaker than PRA which are still able to prove some nice properties of the provability (and the consistency) predicate. One prominent example is IΔ₀+ Ω₁ which can prove all the derivability conditions of Hilbert-Bernays-Löb (J.B. Paris & A.J. Wilkie 1987). Indeed, GST can be proved for all recursively enumerable extensions of (the very weak) Robinson's Arithmetic Q. In particular, both IΔ₀ and IΔ₀+ Ω₁ cannot prove their own consistency.
Another way of generalizing GST is to weaken the consistency predicate in addition to weakening the underlying theory. For example, one can consider the provability (or unprovability) of cut-free consistency in weak arithmetics. Historically, an interest in this line of research came out of the problem of Π₁–separating the hierarchy of bounded arithmetics, e.g., Π₁–separating IΔ₀+exp over IΔ₀ ([PW81]). Unprovability of cut-free consistency (Herbrand consistency) of theories weaker than IΔ₀+exp in themselves was stated as an open problem by P. Pudlák ([P85]). We note that the cost of cut-elimination in proof theory is super-exponential, so in weak arithmetics cut-free provability is not equivalent to the usual (Hilbert style) provability. The first demonstration of the unprovability of cut-free consistency in weak arithmetics was made by Z. Adamowicz who proved in an unpublished manuscript in 1999 (later appeared as a technical report) that the Tableau-consistency of IΔ₀+Ω₁ is not provable in itself. Later on with P. Zbierski ([AZ01]) she proved GST for Herbrand consistency of IΔ₀+Ω₂, and a bit later she gave a model theoretic proof of it (2002). Extending these results for IΔ₀ was proposed to me as a topic for my PhD thesis by her at IMPAN.
By modifying the definition of Herbrand consistency, Z. Adamowicz's model-theoretic proof is generalized to IΔ₀+Ω₁ in Chapter 5 of [Sa02] (the result is not published anywhere else). Also, it is shown in Chapter 3 (published in [Sa01]) that the Herbrand Consistency of IΔ₀ is not IΔ₀–provable, where the theory IΔ₀ is axiomatized by a conventional axiomatization of IΔ₀ augmented with two IΔ₀–provable sentences. Also in Chapter 5 the second of the three questions posed in [AZ01] is answered negatively, by elaborating a concrete counter-example.

[AZ01] Adamowicz, Z. & Zbierski, P., "On Herbrand Consistency in Weak Arithmetic", Archive for Mathematical Logic, Vol. 40, No. 6 (2001) pages 399-413.
[PW81] Paris, J.B. & Wilkie, A.J., "Δ₀–sets and Induction", Open Days in Model Theory and Set Theory, Proceedings of a conference held in 1981 at Jadwisin, Poland (Leeds University Press 1983) pages 237-248.
[P85] Pudlák, P., "Cuts, Consistency Statements and Interpretation" Journal of Symbolic Logic, Vol. 50, No. 2 (1985) pages 423-442.

---

        Tree Automata and Tree Languages

---

[S05a] Saeed Salehi, "Varieties of Tree Languages Definable by Syntactic Monoids", Acta Cybernetica, Vol. 17, No. 1 (2005) pages 21-41.

In this paper the long-standing open problem of the defining power of syntactic monoids/semigroups in tree languages has been solved. It was already known that (syntactic) monoids or semigroups are not as strong tools for characterizing families of tree languages, as are syntactic algebras. Some varieties of tree languages (definable by algebras) that are not definable by monoids had been found; and it was settled that any family of tree languages definable by monoids is a variety (definable by algebras). But a variety theorem for (varieties of ) monoids and (families of) tree languages was missing; this was mentioned by several authors such as M. Steinby [S98], Z. Ésik [E99], and Th. Wilke [W96].
It is also noted in [S05a] that definite tree languages are not definable by syntactic monoids (neither by semigroups), which refutes a result of M. Nivat & A. Podelski for the first time after its publication in 1989 ([NP89]).
Here is a concrete counter-example for Theorem 1 of [NP89] in the original notation of the paper.

[S98] Steinby, M., "General Varieties of Tree Languages", Theoretical Computer Science, Vol. 205, No. 1-2 (1998) pages 1-43.
[E99] Ésik, Z., "A Variety Theorem for Trees and Theories", Publications Mathematicae Debrecen, Vol. 54, suppl. (1999) pages 711-762.
[W96] Wilke, T., "An Algebraic Characterization of Frontier Testable Tree Languages", Theoretical Computer Science, Vol. 154, No. 1 (1996) pages 85-106.
[NP89] Nivat, M. & Podelski, A., "Definite Tree Languages (cont'd)", Bulletin of the European Association for Theoretical Computer Science, Vol. 38 (1989) pages 186-190.

[PS05] Tatjana Petkovic & Saeed Salehi, "Positive Varieties of Tree Languages", Theoretical Computer Science, Vol. 347, No. 1 (2005) pages 1-35.

In this long "fundamental study" paper, we have introduced the notions of ordered algebras, syntactic ordered algebras, and recognizability by ordered algebras (in which the set of final states gives its place to a downward closed subset of the algebra). A positive variety of tree languages, loosely speaking, is a family of tree languages that is closed under all the closure properties of varieties (including intersection and union) except complementation. This was inspired by J.-E. Pin's positive variety theorem for ordered semigroups and positive varieties of word languages [P95].
Also, the variety theorem for monoids in [S05a] is generalized to a variety theorem between certain positive families of tree languages (not necessarily closed under complements) and varieties of ordered monoids.
Two instances of the above variety theorems (and that of [S05a]) are extensively elaborated.

[P95] Pin, J.-E., "A Variety Theorem without Complementation", Izvestiya VUZ Matematika Vol. 39 (1995), pages 80-90. English version, Russian Mathematics (Izv. VUZ Mat.) Vol. 39 (1995), pages 74-83.

[SS06] Saeed Salehi & Magnus Steinby, "Tree Algebras and Varieties of Tree Languages", submitted for publication.
Technical Report: TUCS 761 (April 2006).

Th. Wilke introduced tree algebras in [W96] for characterizing binary tree languages, and gave a concrete axiomatization for frontier testable (reverse definite) ones. A variety theorem for tree algebras was called for by some other authors (e.g. M. Steinby and Z. Ésik) and Wilke himself anticipated a variety theorem for label-generated tree algebras. In [SS06] we started a thorough study of tree algebras, aiming at a variety theorem. As tree algebras are many-sorted, along the way, we made a complete survey of the theory of many-sorted algebras (some old and some new – in [SS04]).
It turned out that there cannot exist any variety theorem for tree algebras (not even for label-generated ones). We introduced more restricted tree algebras (called "reduced" tree algebras) and proved a variety theorem for certain classes of reduced tree algebras and certain families of binary tree languages. Due to the richness of the signature of tree languages, they have a more powerful expressive power (for characterizing varieties of tree languages) than ordinary algebras, though their defining power is not much stronger than that of algebras.

---

        Finite Universal Algebra

---

[Sa03] Saeed Salehi, "A Completeness Property of Wilke's Tree Algebras", Proceedings of MFCS 2003, Lecture Notes in Computer Science 2747, Springer-Verlag (2003) pages 662-670.

While trying to understand the choice of Wilke's functions as the signature of (many-sorted) tree languages, I came up with the idea that those functions generate exactly the congruence-preserving functions. An m-ary function f : A^m® A over an algebra A is called congruence-preserving, if for any congruence relation θ on A and any elements a₁,...,a_m, b₁,...,b_m of A, if a_jθb_j holds for all jÎ{1,...,m}, then f (a₁,...,a_m) θ f (b₁,...,b_m) holds too. Trivial examples of congruence-preserving functions are term functions on A (with parameters from A). In fact, a relation is called "congruence" just in case is preserved by all term functions. An algebra is called hemiprimal if its every congruence-preserving function is a term function. This is a useful and well-studied notion in Universal Algebra (see e.g. the book [KP01]).
In [Sa03] I have shown that term algebras, which are free algebras over the class of all algebras, generated by at least seven elements are hemiprimal. This is not true for term algebras generated by one element (a counter-example is constructed in [Sa03] for one-generated term algebra where the signature contains a unary function symbol only), and we do not yet know if n-generated term algebras, where 2£ n £6, are hemiprimal or not.

[KP01] Kaarli, K. & Pixley, A.F., Polynomial Completeness in Algebraic Systems, Chapman & Hall / CRC, Boca Raton, FL, 2001.

[Sa05] Saeed Salehi, "Congruence Preserving Functions of Wilke's Tree Algebras", Algebra Universalis, Vol. 53, No. 4 (2005) pages 451-470 .

It is proved in [Sa05] that free tree algebras over alphabets which contain at least seven letters are hemi-primal. Note that free tree algebras are not (many-sorted) term algebras; so the results of [Sa05] are not the many-sorted version of the results of [Sa03]. Translating this result into the language of tree automata, it means that all the functions that preserve congruences of binary tree languages are generated by Wilke's functions, for sufficiently large alphabets (with at least seven letters). This is not true for two-letter alphabets (a counter-example is constructed in [Sa05]) and is unknown for alphabets with 3,4,5 or 6 letters.

[SS04] Saeed Salehi & Magnus Steinby, "Varieties of Many-Sorted Recognizable Sets", submitted for publication.
Technical Report: TUCS 629 (September 2004).

In this paper, we have developed a variety theory for many-sorted algebras, recognizable subsets of many-sorted algebras, and congruences of free many-sorted algebras. Informally speaking, the theories developed in [A90] and [S92] are generalized to the many-sorted case. The notions introduced and the tools developed in [SS04] were used in the variety theory of Wilke's tree algebras in [SS06].

[A90] Almeida, J., "On Pseudovarieties, Varieties of Languages, Filters of Congruences, Pseudoidentities and Related Topics", Algebra Universalis, Vol. 27, No. 3 (1990) pages 333-350.
[S92] Steinby, M., "A Theory of Tree Language Varieties", in: Nivat, M. & Podelski, A. (eds.), Tree Automata and Languages (Le Touquet, 1990), Elsevier, Amsterdam (1992), pages 57-81.

---

[Sa05a] Saeed Salehi, "Varieties of Tree Languages", PhD Dissertation, Department of Mathematics, University of Turku, TUCS Dissertations 64, 2005.

This thesis, written under the supervision of M. Steinby at TUCS, is a monograph that contains the results of the papers [SS04] (Chapter 2), [PS05] (Chapters 3 and 5), [S05a] (Chapter 4), and [SS06] (Chapter 6). The results of the papers [Sa03] and [Sa05] are only briefed in Chapter 6 (the last section) without going to further details (to keep the thesis in a reasonable space). The paper [SS06] is completed after finishing up the thesis, so not only it covers the first two sections of Chapter 6 of [Sa05a] but also contains more and new results.