Saeed Salehi

University of Tabriz
  •  124
    We respond to some of the points made by Bennet and Blanck (2022) concerning a previous publication of ours (2021).
  •  146
    We demonstrate that, in itself and in the absence of extra premises, the following argument scheme is fallacious: The sentence A says about itself that it has a property F, and A does in fact have the property F; therefore A is true. We then examine an argument of this form in the informal introduction of Gödel’s classic (1931) and examine some auxiliary premises which might have been at work in that context. Philosophically significant as it may be, that particular informal argument plays no rô…Read more
  •  11
    From Intuitionism to Many-Valued Logics Through Kripke Models
    In Mojtaba Mojtahedi, Shahid Rahman & MohammadSaleh Zarepour (eds.), Mathematics, Logic, and their Philosophies: Essays in Honour of Mohammad Ardeshir, Springer. pp. 339-348. 2021.
    Intuitionistic Propositional LogicIntuitionistic propositional logic is proved to be an infinitely many valued logicMany valued logics by Gödel Publications 1929–1936, Oxford University Press, pp 222–225, 1932), and it is proved by Jaśkowski Jaśkowski, S. to be a countably many valued logicMany valued logics. In this paper, we provide alternative proofs for these theorems by using models of Kripke :1–14, 1959). Gödel’s proof gave rise to an intermediate propositional logic, that is known nowaday…Read more
  •  30
    Tarski’s Undefinability Theorem and the Diagonal Lemma
    Logic Journal of the IGPL 30 (3): 489-498. 2022.
    We prove the equivalence of the semantic version of Tarski’s theorem on the undefinability of truth with the semantic version of the diagonal lemma and also show the equivalence of a syntactic version of Tarski’s undefinability theorem with a weak syntactic diagonal lemma. We outline two seemingly diagonal-free proofs for these theorems from the literature and show that the syntactic version of Tarski’s theorem can deliver Gödel–Rosser’s incompleteness theorem.
  •  152
    Diagonal arguments and fixed points
    Bulletin of the Iranian Mathematical Society 43 (5): 1073-1088. 2017.
    ‎A universal schema for diagonalization was popularized by N. S‎. ‎Yanofsky (2003)‎, ‎based on a pioneering work of F.W‎. ‎Lawvere (1969)‎, ‎in which the existence of a (diagonolized-out and contradictory) object implies the existence of a fixed-point for a certain function‎. ‎It was shown that many self-referential paradoxes and diagonally proved theorems can fit in that schema‎. ‎Here‎, ‎we fit more theorems in the universal‎ ‎schema of diagonalization‎, ‎such as Euclid's proof for the infinit…Read more
  •  305
    Kripke Semantics for Fuzzy Logics
    Soft Computing 22 (3). 2018.
    Kripke frames (and models) provide a suitable semantics for sub-classical logics; for example, intuitionistic logic (of Brouwer and Heyting) axiomatizes the reflexive and transitive Kripke frames (with persistent satisfaction relations), and the basic logic (of Visser) axiomatizes transitive Kripke frames (with persistent satisfaction relations). Here, we investigate whether Kripke frames/models could provide a semantics for fuzzy logics. For each axiom of the basic fuzzy logic, necessary and su…Read more
  •  191
    Theoremizing Yablo's Paradox
    with Ahmad Karimi
    To counter a general belief that all the paradoxes stem from a kind of circularity (or involve some self--reference, or use a diagonal argument) Stephen Yablo designed a paradox in 1993 that seemingly avoided self--reference. We turn Yablo's paradox, the most challenging paradox in the recent years, into a genuine mathematical theorem in Linear Temporal Logic (LTL). Indeed, Yablo's paradox comes in several varieties; and he showed in 2004 that there are other versions that are equally paradoxica…Read more
  •  188
    On Rudimentarity, Primitive Recursivity and Representability
    Reports on Mathematical Logic 55. 2020.
    It is quite well-known from Kurt G¨odel’s (1931) ground-breaking Incompleteness Theorem that rudimentary relations (i.e., those definable by bounded formulae) are primitive recursive, and that primitive recursive functions are representable in sufficiently strong arithmetical theories. It is also known, though perhaps not as well-known as the former one, that some primitive recursive relations are not rudimentary. We present a simple and elementary proof of this fact in the first part of the pap…Read more
  •  258
    From Intuitionism to Many-Valued Logics Through Kripke Models
    In Mojtaba Mojtahedi, Shahid Rahman & MohammadSaleh Zarepour (eds.), Mathematics, Logic, and their Philosophies: Essays in Honour of Mohammad Ardeshir, Springer. pp. 339-348. 2021.
    Intuitionistic Propositional Logic is proved to be an infinitely many valued logic by Gödel (Kurt Gödel collected works (Volume I) Publications 1929–1936, Oxford University Press, pp 222–225, 1932), and it is proved by Jaśkowski (Actes du Congrés International de Philosophie Scientifique, VI. Philosophie des Mathématiques, Actualités Scientifiques et Industrielles 393:58–61, 1936) to be a countably many valued logic. In this paper, we provide alternative proofs for these theorems by using model…Read more
  •  33
    Provably total functions of Basic Arithemtic
    Mathematical Logic Quarterly 49 (3): 316. 2003.
    It is shown that all the provably total functions of Basic Arithmetic BA, a theory introduced by Ruitenburg based on Predicate Basic Calculus, are primitive recursive. Along the proof a new kind of primitive recursive realizability to which BA is sound, is introduced. This realizability is similar to Kleene's recursive realizability, except that recursive functions are restricted to primitive recursives
  •  305
    ‘Sometime a paradox’, now proof: Yablo is not first order
    Logic Journal of the IGPL 30 (1): 71-77. 2022.
    Interesting as they are by themselves in philosophy and mathematics, paradoxes can be made even more fascinating when turned into proofs and theorems. For example, Russell’s paradox, which overthrew Frege’s logical edifice, is now a classical theorem in set theory, to the effect that no set contains all sets. Paradoxes can be used in proofs of some other theorems—thus Liar’s paradox has been used in the classical proof of Tarski’s theorem on the undefinability of truth in sufficiently rich langu…Read more
  •  31
    On constructivity and the Rosser property: a closer look at some Gödelean proofs
    with Payam Seraji
    Annals of Pure and Applied Logic 169 (10): 971-980. 2018.
    The proofs of Kleene, Chaitin and Boolos for Gödel's First Incompleteness Theorem are studied from the perspectives of constructivity and the Rosser property. A proof of the incompleteness theorem has the Rosser property when the independence of the true but unprovable sentence can be shown by assuming only the (simple) consistency of the theory. It is known that Gödel's own proof for his incompleteness theorem does not have the Rosser property, and we show that neither do Kleene's or Boolos' pr…Read more
  •  47
    On the diagonal lemma of Gödel and Carnap
    Bulletin of Symbolic Logic 26 (1): 80-88. 2020.
    A cornerstone of modern mathematical logic is the diagonal lemma of Gödel and Carnap. It is used in e.g. the classical proofs of the theorems of Gödel, Rosser and Tarski. From its first explication in 1934, just essentially one proof has appeared for the diagonal lemma in the literature; a proof that is so tricky and hard to relate that many authors have tried to avoid the lemma altogether. As a result, some so called diagonal-free proofs have been given for the above mentioned fundamental the…Read more
  •  32
    Herbrand consistency of some arithmetical theories
    Journal of Symbolic Logic 77 (3): 807-827. 2012.
    Gödel's second incompleteness theorem is proved for Herbrand consistency of some arithmetical theories with bounded induction, by using a technique of logarithmic shrinking the witnesses of bounded formulas, due to Z. Adamowicz [Herbrand consistency and bounded arithmetic, Fundamenta Mathematical vol. 171 (2002), pp. 279-292]. In that paper, it was shown that one cannot always shrink the witness of a bounded formula logarithmically, but in the presence of Herbrand consistency, for theories I∆₀+ …Read more
  •  137
    Decidable Formulas Of Intuitionistic Primitive Recursive Arithmetic
    Reports on Mathematical Logic 36 (1): 55-61. 2002.
    By formalizing some classical facts about provably total functions of intuitionistic primitive recursive arithmetic (iPRA), we prove that the set of decidable formulas of iPRA and of iΣ1+ (intuitionistic Σ1-induction in the language of PRA) coincides with the set of its provably ∆1-formulas and coincides with the set of its provably atomic formulas. By the same methods, we shall give another proof of a theorem of Marković and De Jongh: the decidable formulas of HA are its provably ∆1-formulas.
  •  71
    Herbrand consistency of some finite fragments of bounded arithmetical theories
    Archive for Mathematical Logic 52 (3-4): 317-333. 2013.
    We formalize the notion of Herbrand Consistency in an appropriate way for bounded arithmetics, and show the existence of a finite fragment of IΔ0 whose Herbrand Consistency is not provable in IΔ0. We also show the existence of an IΔ0-derivable Π1-sentence such that IΔ0 cannot prove its Herbrand Consistency.
  •  26
    Gödel’s Incompleteness Phenomenon—Computationally
    Philosophia Scientiae 18 23-37. 2014.
    We argue that Gödel's completeness theorem is equivalent to completability of consistent theories, and Gödel's incompleteness theorem is equivalent to the fact that this completion is not constructive, in the sense that there are some consistent and recursively enumerable theories which cannot be extended to any complete and consistent and recursively enumerable theory. Though any consistent and decidable theory can be extended to a complete and consistent and decidable theory. Thus deduction an…Read more
  •  49
    Gödel’s second incompleteness theorem: How it is derived and what it delivers
    Bulletin of Symbolic Logic 26 (3-4): 241-256. 2020.
    The proofs of Gödel (1931), Rosser (1936), Kleene (first 1936 and second 1950), Chaitin (1970), and Boolos (1989) for the first incompleteness theorem are compared with each other, especially from the viewpoint of the second incompleteness theorem. It is shown that Gödel’s (first incompleteness theorem) and Kleene’s first theorems are equivalent with the second incompleteness theorem, Rosser’s and Kleene’s second theorems do deliver the second incompleteness theorem, and Boolos’ theorem is deriv…Read more
  •  25
    Intuitionistic axiomatizations for bounded extension Kripke models
    with Mohammad Ardeshir and Wim Ruitenburg
    Annals of Pure and Applied Logic 124 (1-3): 267-285. 2003.
    We present axiom systems, and provide soundness and strong completeness theorems, for classes of Kripke models with restricted extension rules among the node structures of the model. As examples we present an axiom system for the class of cofinal extension Kripke models, and an axiom system for the class of end-extension Kripke models. We also show that Heyting arithmetic is strongly complete for its class of end-extension models. Cofinal extension models of HA are models of Peano arithmetic
  •  342
    We take an argument of Gödel's from his ground‐breaking 1931 paper, generalize it, and examine its validity. The argument in question is this: "the sentence G says about itself that it is not provable, and G is indeed not provable; therefore, G is true".
  •  341
    There May Be Many Arithmetical Gödel Sentences
    Philosophia Mathematica 29 (2). 2021.
    We argue that, under the usual assumptions for sufficiently strong arithmetical theories that are subject to Gödel’s First Incompleteness Theorem, one cannot, without impropriety, talk about *the* Gödel sentence of the theory. The reason is that, without violating the requirements of Gödel’s theorem, there could be a true sentence and a false one each of which is provably equivalent to its own unprovability in the theory if the theory is unsound.
  •  29
    Polynomially Bounded Recursive Realizability
    Notre Dame Journal of Formal Logic 46 (4): 407-417. 2005.
    A polynomially bounded recursive realizability, in which the recursive functions used in Kleene's realizability are restricted to polynomially bounded functions, is introduced. It is used to show that provably total functions of Ruitenburg's Basic Arithmetic are polynomially bounded (primitive) recursive functions. This sharpens our earlier result where those functions were proved to be primitive recursive. Also a polynomially bounded schema of Church's Thesis is shown to be polynomially bounded…Read more