Showing 1–31 of 31 results for author: Salehi, S

Fast Inexact Bilevel Optimization for Analytical Deep Image Priors

Authors: Mohammad Sadegh Salehi, Tatiana A. Bubba, Yury Korolev

Abstract: The analytical deep image prior (ADP) introduced by Dittmer et al. (2020) establishes a link between deep image priors and classical regularization theory via bilevel optimization. While this is an elegant construction, it involves expensive computations if the lower-level problem is to be solved accurately. To overcome this issue, we propose to use adaptive inexact bilevel optimization to solve A… ▽ More The analytical deep image prior (ADP) introduced by Dittmer et al. (2020) establishes a link between deep image priors and classical regularization theory via bilevel optimization. While this is an elegant construction, it involves expensive computations if the lower-level problem is to be solved accurately. To overcome this issue, we propose to use adaptive inexact bilevel optimization to solve ADP problems. We discuss an extension of a recent inexact bilevel method called the method of adaptive inexact descent of Salehi et al.(2024) to an infinite-dimensional setting required by the ADP framework. In our numerical experiments we demonstrate that the computational speed-up achieved by adaptive inexact bilevel optimization allows one to use ADP on larger-scale problems than in the previous literature, e.g. in deblurring of 2D color images. △ Less

Submitted 11 March, 2025; v1 submitted 13 February, 2025; originally announced February 2025.

Comments: 12 pages, 7 figures. Accepted to the 10th International Conference on Scale Space and Variational Methods in Computer Vision (SSVM 2025)

Bilevel Learning with Inexact Stochastic Gradients

Authors: Mohammad Sadegh Salehi, Subhadip Mukherjee, Lindon Roberts, Matthias J. Ehrhardt

Abstract: Bilevel learning has gained prominence in machine learning, inverse problems, and imaging applications, including hyperparameter optimization, learning data-adaptive regularizers, and optimizing forward operators. The large-scale nature of these problems has led to the development of inexact and computationally efficient methods. Existing adaptive methods predominantly rely on deterministic formul… ▽ More Bilevel learning has gained prominence in machine learning, inverse problems, and imaging applications, including hyperparameter optimization, learning data-adaptive regularizers, and optimizing forward operators. The large-scale nature of these problems has led to the development of inexact and computationally efficient methods. Existing adaptive methods predominantly rely on deterministic formulations, while stochastic approaches often adopt a doubly-stochastic framework with impractical variance assumptions, enforces a fixed number of lower-level iterations, and requires extensive tuning. In this work, we focus on bilevel learning with strongly convex lower-level problems and a nonconvex sum-of-functions in the upper-level. Stochasticity arises from data sampling in the upper-level which leads to inexact stochastic hypergradients. We establish their connection to state-of-the-art stochastic optimization theory for nonconvex objectives. Furthermore, we prove the convergence of inexact stochastic bilevel optimization under mild assumptions. Our empirical results highlight significant speed-ups and improved generalization in imaging tasks such as image denoising and deblurring in comparison with adaptive deterministic bilevel methods. △ Less

Submitted 11 March, 2025; v1 submitted 16 December, 2024; originally announced December 2024.

Comments: Accepted to the 10th International Conference on Scale Space and Variational Methods in Computer Vision (SSVM 2025)

An Adaptively Inexact Method for Bilevel Learning Using Primal-Dual Style Differentiation

Authors: Lea Bogensperger, Matthias J. Ehrhardt, Thomas Pock, Mohammad Sadegh Salehi, Hok Shing Wong

Abstract: We consider a bilevel learning framework for learning linear operators. In this framework, the learnable parameters are optimized via a loss function that also depends on the minimizer of a convex optimization problem (denoted lower-level problem). We utilize an iterative algorithm called `piggyback' to compute the gradient of the loss and minimizer of the lower-level problem. Given that the lower… ▽ More We consider a bilevel learning framework for learning linear operators. In this framework, the learnable parameters are optimized via a loss function that also depends on the minimizer of a convex optimization problem (denoted lower-level problem). We utilize an iterative algorithm called `piggyback' to compute the gradient of the loss and minimizer of the lower-level problem. Given that the lower-level problem is solved numerically, the loss function and thus its gradient can only be computed inexactly. To estimate the accuracy of the computed hypergradient, we derive an a-posteriori error bound, which provides guides for setting the tolerance for the lower-level problem, as well as the piggyback algorithm. To efficiently solve the upper-level optimization, we also propose an adaptive method for choosing a suitable step-size. To illustrate the proposed method, we consider a few learned regularizer problems, such as training an input-convex neural network. △ Less

Submitted 7 June, 2025; v1 submitted 9 December, 2024; originally announced December 2024.

On a fallacy concerning I-am-unprovable sentences: what to take home from Goedel's introduction

Authors: Kaave Lajevardi, Saeed Salehi

Abstract: 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 certain 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 Goedel's classic (1931) and examine some auxiliary premises which might have been at… ▽ More 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 certain 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 Goedel'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 role in Goedel's technical results. Going deeper into the issue and investigating truth conditions of Goedelian sentences (i.e., those sentences which are provably equivalent to their own unprovability) will provide us with insights regarding the philosophical debate on the truth of Goedelian sentences of systems--a debate which is at least as old as Dummett (1963). △ Less

Submitted 11 November, 2023; originally announced November 2023.

Comments: 14 pages

MSC Class: 03F40

On Chaitin's Heuristic Principle and Halting Probability

Authors: Saeed Salehi

Abstract: It would be a heavenly reward if there were a method of weighing theories and sentences in such a way that a theory could never prove a heavier sentence (Chaitin's Heuristic Principle). Alas, no satisfactory measure has been found so far, and this dream seemed too good to ever come true. In the first part of this paper, we attempt to revive Chaitin's lost paradise of heuristic principle as much as… ▽ More It would be a heavenly reward if there were a method of weighing theories and sentences in such a way that a theory could never prove a heavier sentence (Chaitin's Heuristic Principle). Alas, no satisfactory measure has been found so far, and this dream seemed too good to ever come true. In the first part of this paper, we attempt to revive Chaitin's lost paradise of heuristic principle as much as logic allows. In the second part, which is a joint work with M. Jalilvand and B. Nikzad, we study Chaitin's well-known constant Omega, and show that this number is not a probability of halting the randomly chosen input-free programs under any infinite discrete measure. We suggest some methods for defining the halting probabilities by various measures. △ Less

Submitted 15 June, 2024; v1 submitted 23 October, 2023; originally announced October 2023.

Comments: 22 pages (two parts)

MSC Class: 03F40; 68Q30; 60A10; 28A05; 68Q04; 03D10

Soundness does not come for free (if at all)

Authors: Kaave Lajevardi, Saeed Salehi

Abstract: We respond to some of the points made by Bennet and Blanck (2022) concerning a previous publication of ours (2021). We respond to some of the points made by Bennet and Blanck (2022) concerning a previous publication of ours (2021). △ Less

Submitted 20 October, 2023; originally announced October 2023.

Comments: 7 pages

An adaptively inexact first-order method for bilevel optimization with application to hyperparameter learning

Authors: Mohammad Sadegh Salehi, Subhadip Mukherjee, Lindon Roberts, Matthias J. Ehrhardt

Abstract: Various tasks in data science are modeled utilizing the variational regularization approach, where manually selecting regularization parameters presents a challenge. The difficulty gets exacerbated when employing regularizers involving a large number of hyperparameters. To overcome this challenge, bilevel learning can be employed to learn such parameters from data. However, neither exact function… ▽ More Various tasks in data science are modeled utilizing the variational regularization approach, where manually selecting regularization parameters presents a challenge. The difficulty gets exacerbated when employing regularizers involving a large number of hyperparameters. To overcome this challenge, bilevel learning can be employed to learn such parameters from data. However, neither exact function values nor exact gradients with respect to the hyperparameters are attainable, necessitating methods that only rely on inexact evaluation of such quantities. State-of-the-art inexact gradient-based methods a priori select a sequence of the required accuracies and cannot identify an appropriate step size since the Lipschitz constant of the hypergradient is unknown. In this work, we propose an algorithm with backtracking line search that only relies on inexact function evaluations and hypergradients and show convergence to a stationary point. Furthermore, the proposed algorithm determines the required accuracy dynamically rather than manually selected before running it. Our numerical experiments demonstrate the efficiency and feasibility of our approach for hyperparameter estimation on a range of relevant problems in imaging and data science such as total variation and field of experts denoising and multinomial logistic regression. Particularly, the results show that the algorithm is robust to its own hyperparameters such as the initial accuracies and step size. △ Less

Submitted 8 April, 2025; v1 submitted 19 August, 2023; originally announced August 2023.

A Reunion of Godel, Tarski, Carnap, and Rosser

Authors: Saeed Salehi

Abstract: We unify Godel's First Incompleteness Theorem (1931), Tarski's Undefinability Theorem (1933), Godel-Carnap's Diagonal Lemma (1934), and Rosser's (strengthening of Godel's first) Incompleteness Theorem (1936), whose proofs resemble much and use almost the same technique. We unify Godel's First Incompleteness Theorem (1931), Tarski's Undefinability Theorem (1933), Godel-Carnap's Diagonal Lemma (1934), and Rosser's (strengthening of Godel's first) Incompleteness Theorem (1936), whose proofs resemble much and use almost the same technique. △ Less

Submitted 15 October, 2022; v1 submitted 10 October, 2022; originally announced October 2022.

Comments: 7 pages

MSC Class: 03F40

On Godel's "Much Weaker" Assumption

Authors: Saeed Salehi

Abstract: Godelian sentences of a sufficiently strong and recursively enumerable theory, constructed in Godel's 1931 groundbreaking paper on the incompleteness theorems, are unprovable if the theory is consistent; however, they could be refutable. These sentences are independent when the theory is so-called omega-consistent; a notion introduced by Godel, which is stronger than (simple) consistency, but ``mu… ▽ More Godelian sentences of a sufficiently strong and recursively enumerable theory, constructed in Godel's 1931 groundbreaking paper on the incompleteness theorems, are unprovable if the theory is consistent; however, they could be refutable. These sentences are independent when the theory is so-called omega-consistent; a notion introduced by Godel, which is stronger than (simple) consistency, but ``much weaker'' than soundness. Godel goes to great lengths to show in detail that omega-consistency is stronger than consistency, but never shows, or seems to forget to say, why it is much weaker than soundness. In this paper, we study this proof-theoretic notion and compare some of its properties with those of consistency and (variants of) soundness. △ Less

Submitted 20 September, 2022; v1 submitted 15 September, 2022; originally announced September 2022.

Comments: 7 pages

MSC Class: 03F40; 03F30

On the Truth of Gödelian and Rosserian Sentences

Authors: Ziba Assadi, Saeed Salehi

Abstract: There is a longstanding debate in the logico-philosophical community as to why the Gödelian sentences of a consistent and sufficiently strong theory are true. The prevalent argument seems to be something like this: since every one of the Gödelian sentences of such a theory is equivalent to the theory's consistency statement, even provably so inside the theory, the truth of those sentences follows… ▽ More There is a longstanding debate in the logico-philosophical community as to why the Gödelian sentences of a consistent and sufficiently strong theory are true. The prevalent argument seems to be something like this: since every one of the Gödelian sentences of such a theory is equivalent to the theory's consistency statement, even provably so inside the theory, the truth of those sentences follows from the consistency of the theory in question. So, Gödelian sentences of consistent theories should be true. In this paper, we show that Gödelian sentences of only sound theories are true; and there is a long road from consistency to soundness, indeed a hierarchy of conditions which are satisfied by some theories and falsified by others. We also study the truth of Rosserian sentences and provide necessary and sufficient conditions for the truth of Rosserian (and also Gödelian) sentences of theories. △ Less

Submitted 1 September, 2020; originally announced September 2020.

Comments: 10 pages

MSC Class: 03F40

Journal ref: Journal of Logic and Computation 32:4 (2022) 729--740

Tarski's Undefinability Theorem and Diagonal Lemma

Authors: Saeed Salehi

Abstract: We prove the equivalence of the semantic version of Tarski's theorem on the undefinability of truth with a semantic version of the Diagonal Lemma, and also show the equivalence of syntactic 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 syntactic Tarski's theorem can deliver G… ▽ More We prove the equivalence of the semantic version of Tarski's theorem on the undefinability of truth with a semantic version of the Diagonal Lemma, and also show the equivalence of syntactic 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 syntactic Tarski's theorem can deliver Gödel-Rosser's Incompleteness Theorem. △ Less

Submitted 15 September, 2020; v1 submitted 1 September, 2020; originally announced September 2020.

Comments: 8 pages

MSC Class: 03F40; 03A05; 03F30; 03C40

Journal ref: Logic Journal of the IGPL 30:3 (2022) 489--498

From Intuitionism to Many-Valued Logics through Kripke Models

Authors: Saeed Salehi

Abstract: Intuitionistic Propositional Logic is proved to be an infinitely many valued logic by Kurt Gödel (1932), and it is proved by Stanisław Jaśkowski (1936) to be a countably many valued logic. In this paper, we provide alternative proofs for these theorems by using models of Saul Kripke (1959). Gödel's proof gave rise to an intermediate propositional logic (between intuitionistic and classical), that… ▽ More Intuitionistic Propositional Logic is proved to be an infinitely many valued logic by Kurt Gödel (1932), and it is proved by Stanisław Jaśkowski (1936) to be a countably many valued logic. In this paper, we provide alternative proofs for these theorems by using models of Saul Kripke (1959). Gödel's proof gave rise to an intermediate propositional logic (between intuitionistic and classical), that is known nowadays as Gödel or the Gödel-Dummet Logic, and is studied by fuzzy logicians as well. We also provide some results on the inter-definablility of propositional connectives in this logic. △ Less

Submitted 20 August, 2020; originally announced August 2020.

Comments: 10 pages, to appear in: Mathematics, Logic, and their Philosophies---Essays in Honor of Mohammad Ardeshir (Springer)

Journal ref: M. Mojtahedi & Sh. Rahman & M.S. Zarepour (eds.), Mathematics, Logic, and their Philosophies: Essays in Honour of Mohammad Ardeshir, Springer (2021) pp. 339--348

Axiomatic (and Non-Axiomatic) Mathematics

Authors: Saeed Salehi

Abstract: Axiomatizing mathematical structures and theories is an objective of Mathematical Logic. Some axiomatic systems are nowadays mere definitions, such as the axioms of Group Theory; but some systems are much deeper, such as the axioms of Complete Ordered Fields with which Real Analysis starts. Groups abound in mathematical sciences, while by Dedekind's theorem there exists only one complete ordered f… ▽ More Axiomatizing mathematical structures and theories is an objective of Mathematical Logic. Some axiomatic systems are nowadays mere definitions, such as the axioms of Group Theory; but some systems are much deeper, such as the axioms of Complete Ordered Fields with which Real Analysis starts. Groups abound in mathematical sciences, while by Dedekind's theorem there exists only one complete ordered field, up to isomorphism. Cayley's theorem in Abstract Algebra implies that the axioms of group theory completely axiomatize the class of permutation sets that are closed under composition and inversion. In this article, we survey some old and new results on the first-order axiomatizability of various mathematical structures. We will also review identities over addition, multiplication, and exponentiation that hold in the set of positive real numbers. △ Less

Submitted 19 August, 2020; originally announced August 2020.

Comments: 10 pages

MSC Class: 03C05; 03C10; 03C35; 03D35; 03F40

Journal ref: Rocky Mountain Journal of Mathematics 52:4 (2022) 1157--1176

Sometime a Paradox, Now Proof: Non-First-Order-izability of Yablo's Paradox

Authors: Saeed Salehi

Abstract: Paradoxes are interesting puzzles in philosophy and mathematics, and they could be even more fascinating, when turned into proofs and theorems. For example, Liar's paradox can be translated into a propositional tautology, and Barber's paradox turns into a first-order tautology. Russell's paradox, which collapsed Frege's foundational framework, is now a classical theorem in set theory, implying tha… ▽ More Paradoxes are interesting puzzles in philosophy and mathematics, and they could be even more fascinating, when turned into proofs and theorems. For example, Liar's paradox can be translated into a propositional tautology, and Barber's paradox turns into a first-order tautology. Russell's paradox, which collapsed Frege's foundational framework, is now a classical theorem in set theory, implying that no set of all sets can exist. Paradoxes can be used in proofs of some other theorems; Liar's paradox has been used in the classical proof of Tarski's theorem on the undefinability of truth in sufficiently rich languages. This paradox (and also Richard's paradox) appears implicitly in Gödel's proof of his celebrated first incompleteness theorem. In this paper, we study Yablo's paradox from the viewpoint of first and second order logics. We prove that a formalization of Yablo's paradox (which is second-order in nature) is non-first-order-izable in the sense of George Boolos (1984). △ Less

Submitted 1 July, 2020; v1 submitted 5 August, 2019; originally announced August 2019.

Comments: 6 pages

MSC Class: Yablo's Paradox; Non-first-orderizability

Journal ref: Logic Journal of the IGPL 30:1 (2022) 71--77

On the Notions of Rudimentarity, Primitive Recursivity and Representability of Functions and Relations

Authors: Saeed Salehi

Abstract: It is quite well-known from Kurt Godel's (1931) ground-breaking result on the 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… ▽ More It is quite well-known from Kurt Godel's (1931) ground-breaking result on the 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 paper. In the second part, we review some possible notions of representability of functions studied in the literature, and give a new proof of the equivalence of the weak representability with the (strong) representability of functions in sufficiently strong arithmetical theories. Our results shed some new light on the notions of rudimentary, primitive recursive, and representable functions and relations, and clarify, hopefully, some misunderstandings and confusing errors in the literature. △ Less

Submitted 1 March, 2020; v1 submitted 1 July, 2019; originally announced July 2019.

Comments: 18 pages

MSC Class: 03F40; 03D20; 03F30

Journal ref: Reports on Mathematical Logic 55 (2020) 73--85

First-Order Continuous Induction, and a Logical Study of Real Closed Fields

Authors: Saeed Salehi, Mohammadsaleh Zarza

Abstract: Over the last century, the principle of "induction on the continuum" has been studied by different authors in different formats. All of these different readings are equivalent to one of the three versions that we isolate in this paper. We also formalize those three forms (of "continuous induction") in first-order logic and prove that two of them are equivalent and sufficiently strong to completely… ▽ More Over the last century, the principle of "induction on the continuum" has been studied by different authors in different formats. All of these different readings are equivalent to one of the three versions that we isolate in this paper. We also formalize those three forms (of "continuous induction") in first-order logic and prove that two of them are equivalent and sufficiently strong to completely axiomatize the first-order theory of the real closed (ordered) fields. We show that the third weaker form of continuous induction is equivalent with the Archimedean property. We study some equivalent axiomatizations for the theory of real closed fields and propose a first-order scheme of the fundamental theorem of algebra as an alternative axiomatization for this theory (over the theory of ordered fields). △ Less

Submitted 11 April, 2019; v1 submitted 1 November, 2018; originally announced November 2018.

Comments: 20 pages -- Keywords: First-Order Logic, Complete Theories, Axiomatizing the Field of Real Numbers, Continuous Induction, Real Closed Fields

MSC Class: 03B25; 03C35; 03C10; 12L05

Journal ref: Bulletin of the Iranian Mathematical Society 46:1 (2020) 225--243

On Decidability of the Ordered Structures of Numbers

Authors: Ziba Assadi, Saeed Salehi

Abstract: The ordered structures of natural, integer, rational and real numbers are studied here. It is known that the theories of these numbers in the language of order are decidable and finitely axiomatizable. Also, their theories in the language of order and addition are decidable and infinitely axiomatizable. For the language of order and multiplication, it is known that the theories of $\mathbb{N}$ and… ▽ More The ordered structures of natural, integer, rational and real numbers are studied here. It is known that the theories of these numbers in the language of order are decidable and finitely axiomatizable. Also, their theories in the language of order and addition are decidable and infinitely axiomatizable. For the language of order and multiplication, it is known that the theories of $\mathbb{N}$ and $\mathbb{Z}$ are not decidable (and so not axiomatizable by any computably enumerable set of sentences). By Tarski's theorem, the multiplicative ordered structure of $\mathbb{R}$ is decidable also; here we prove this result directly and present an axiomatization. The structure of $\mathbb{Q}$ in the language of order and multiplication seems to be missing in the literature; here we show the decidability of its theory by the technique of quantifier elimination and after presenting an infinite axiomatization for this structure we prove that it is not finitely axiomatizable. △ Less

Submitted 14 February, 2018; v1 submitted 15 September, 2017; originally announced September 2017.

Comments: 17 pages

MSC Class: 03B25; 03C10; 03D35; 03C65

Journal ref: Soft Computing 23:11 (2019) 3615--3626

On Axiomatizability of the Multiplicative Theory of Numbers

Authors: Saeed Salehi

Abstract: The multiplicative theory of a set of numbers (which could be natural, integer, rational, real or complex numbers) is the first-order theory of the structure of that set with (solely) the multiplication operation (that set is taken to be multiplicative, i.e., closed under multiplication). In this paper we study the multiplicative theories of the complex, real and (positive) rational numbers. These… ▽ More The multiplicative theory of a set of numbers (which could be natural, integer, rational, real or complex numbers) is the first-order theory of the structure of that set with (solely) the multiplication operation (that set is taken to be multiplicative, i.e., closed under multiplication). In this paper we study the multiplicative theories of the complex, real and (positive) rational numbers. These theories (and also the multiplicative theories of natural and integer numbers) are known to be decidable (i.e., there exists an algorithm that decides whether a given sentence is derivable form the theory); here we present explicit axiomatizations for them and show that they are not finitely axiomatizable. For each of these sets (of complex, real and [positive] rational numbers) a language, including the multiplication operation, is introduced in a way that it allows quantifier elimination (for the theory of that set). △ Less

Submitted 14 February, 2018; v1 submitted 15 July, 2017; originally announced July 2017.

Comments: 18 pages

MSC Class: 03B25; 03C10; 03D35; 03C65

Journal ref: Fundamenta Informaticae 159 (2018) 279--296

Computation in Logic and Logic in Computation

Authors: Saeed Salehi

Abstract: The theory of addition in the domains of natural (N), integer (Z), rational (Q), real (R) and complex (C) numbers is decidable, so is the theory of multiplication in all those domains. By Godel's Incompleteness Theorem the theory of addition and multiplication is undecidable in the domains of N, Z and Q, though Tarski proved that this theory is decidable in the domains of R and C. The theory of mu… ▽ More The theory of addition in the domains of natural (N), integer (Z), rational (Q), real (R) and complex (C) numbers is decidable, so is the theory of multiplication in all those domains. By Godel's Incompleteness Theorem the theory of addition and multiplication is undecidable in the domains of N, Z and Q, though Tarski proved that this theory is decidable in the domains of R and C. The theory of multiplication and order (x,<) behaves differently in the above mentioned domains of numbers. By a theorem of Robinson, addition is definable by multiplication and order in the domain of natural numbers, thus the theory (N;x,<) is undecidable. By a classical theorem in mathematical logic, addition is not definable in terms of multiplication and order in R. In this paper, we extend Robinson's theorem to the domain of integers (Z) by showing the definability of addition in (Z;x,<), this implies that (Z;x,<) is undecidable. We also show the decidability of (Q;x,<) by the method of quantifier elimination. Whence, addition is not definable in (Q;x,<). △ Less

Submitted 20 December, 2016; originally announced December 2016.

Comments: Invited Conference Paper at the Institute for Advanced Studies in Basic Sciences, Gavazangh, Zanjan, Iran (http://www.universal-publishers.com/book.php?method=ISBN&book=161233623X)

MSC Class: 03B25; 03C10; 03D35; 03F40; 11U05

Journal ref: B. Sadeghi-Bigham (ed.), Proceedings of the Third International Conference on Contemporary Issues in Computer and Information Sciences (CICIS 2012), Brown Walker Press, USA (2012) pp. 580--583

Axiomatizing Mathematical Theories: Multiplication

Authors: Saeed Salehi

Abstract: Axiomatizing mathematical structures is a goal of Mathematical Logic. Axiomatizability of the theories of some structures have turned out to be quite difficult and challenging, and some remain open. However axiomatization of some mathematical structures are now classical theorems in Logic, Algebra and Geometry. In this paper we will study the axiomatizability of the theories of multiplication in t… ▽ More Axiomatizing mathematical structures is a goal of Mathematical Logic. Axiomatizability of the theories of some structures have turned out to be quite difficult and challenging, and some remain open. However axiomatization of some mathematical structures are now classical theorems in Logic, Algebra and Geometry. In this paper we will study the axiomatizability of the theories of multiplication in the domains of natural, integer, rational, real, and complex numbers. We will review some classical theorems, and will give some new proofs for old results. We will see that some structures are missing in the literature, thus leaving it open whether the theories of that structures are axiomatizable (decidable) or not. We will answer one of those open questions in this paper. △ Less

Submitted 20 December, 2016; originally announced December 2016.

Comments: A Conference Paper at Sharif University of Technology, 25-27 December 2012, Tehran

MSC Class: 03B25; 03C10; 03D35; 03F40; 11U05; 12L05

Journal ref: A. Kamali-Nejad (ed.), Proceedings of Frontiers in Mathematical Sciences, Fundamental Education Publications, Iran (2012) pp. 165--176

On Constructivity and the Rosser Property: a closer look at some Gödelean proofs

Authors: Saeed Salehi, Payam Seraji

Abstract: 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 incomple… ▽ More 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' proofs. However, we show that a variant of Chaitin's proof can have the Rosser property. The proofs of Gödel, Rosser and Kleene are constructive in the sense that they explicitly construct, by algorithmic ways, the independent sentence(s) from the theory. We show that the proofs of Chaitin and Boolos are not constructive, and they prove only the mere existence of the independent sentences. △ Less

Submitted 14 February, 2018; v1 submitted 8 December, 2016; originally announced December 2016.

Comments: 12 pages -- to appear in the Annals of Pure and Applied Logic

MSC Class: 03F40; 03F30; 03D32

Journal ref: Annals of Pure and Applied Logic 169:10 (2018) 971--980

Kripke Semantics for Fuzzy Logics

Authors: Parvin Safari, Saeed Salehi

Abstract: 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 co… ▽ More 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 sufficient conditions are sought for Kripke frames/models which satisfy them. It turns out that the only fuzzy logics (logics containing the Basic Fuzzy Logic) which are sound and complete with respect to a class of Kripke frames/models are the extensions of the Gödel Logic (or the super-intuitionistic logic of Dummett), indeed this logic is sound and strongly complete with respect to reflexive, transitive and connected (linear) Kripke frames (with persistent satisfaction relations). This provides a semantic characterization for the Gödel Logic among (propositional) fuzzy logics. △ Less

Submitted 10 December, 2016; v1 submitted 14 July, 2016; originally announced July 2016.

Comments: Soft Computing (2016)

MSC Class: 03B52; 03F50; 03F55; 03A20

Journal ref: Soft Computing 22:3 (2018) 839--844

On Arithmetical Truth of the Self-Referential Sentences

Authors: Kaave Lajevardi, Saeed Salehi

Abstract: 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. 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. △ Less

Submitted 14 February, 2018; v1 submitted 14 July, 2016; originally announced July 2016.

Comments: 7 pages

MSC Class: 00A30; 03A05; 03B30; 03F40

Journal ref: Theoria 85:1 (2019) 8--17

Theorems of Tarski's Undefinability and Godel's Second Incompleteness-Computationally

Authors: Saeed Salehi

Abstract: We present a version of Gödel's Second Incompleteness Theorem for recursively enumerable consistent extensions of a fixed axiomatizable theory, by incorporating some bi-theoretic version of the derivability conditions. We also argue that Tarski's theorem on the Undefinability of Truth is Gödel's First Incompleteness Theorem relativized to definable oracles; a unification of these two theorems is g… ▽ More We present a version of Gödel's Second Incompleteness Theorem for recursively enumerable consistent extensions of a fixed axiomatizable theory, by incorporating some bi-theoretic version of the derivability conditions. We also argue that Tarski's theorem on the Undefinability of Truth is Gödel's First Incompleteness Theorem relativized to definable oracles; a unification of these two theorems is given. △ Less

Submitted 10 November, 2019; v1 submitted 1 September, 2015; originally announced September 2015.

Comments: 12 pages

MSC Class: 03F40; 03B25; 03D35; 03A05

Godel-Rosser's Incompleteness Theorems for Non-Recursively Enumerable Theories

Authors: Saeed Salehi, Payam Seraji

Abstract: Godel's First Incompleteness Theorem is generalized to definable theories, which are not necessarily recursively enumerable, by using a couple of syntactic-semantic notions, one is the consistency of a theory with the set of all true $Π_n$-sentences or equivalently the $Σ_n$-soundness of the theory, and the other is $n$-consistency the restriction of $ω$-consistency to the $Σ_n$-formulas. It is al… ▽ More Godel's First Incompleteness Theorem is generalized to definable theories, which are not necessarily recursively enumerable, by using a couple of syntactic-semantic notions, one is the consistency of a theory with the set of all true $Π_n$-sentences or equivalently the $Σ_n$-soundness of the theory, and the other is $n$-consistency the restriction of $ω$-consistency to the $Σ_n$-formulas. It is also shown that Rosser's Incompleteness Theorem does not generally hold for definable non-recursively enumerable theories, whence Godel-Rosser's Incompleteness Theorem is optimal in a sense. Though the proof of the incompleteness theorem using the $Σ_n$-soundness assumption is constructive, it is shown that there is no constructive proof for the incompleteness theorem using the $n$-consistency assumption, for $n\!>\!2$. △ Less

Submitted 10 December, 2016; v1 submitted 9 June, 2015; originally announced June 2015.

Comments: Journal of Logic and Computation (2016) "Gödel-Rosser's Incompleteness Theorem, generalized and optimized for definable theories"

MSC Class: 03F40; 03F30; 03D35; 03D25

Journal ref: Journal of Logic and Computation 27:5 (2017) 1391--1397

Theoremizing Yablo's Paradox

Authors: Ahmad Karimi, Saeed Salehi

Abstract: 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 i… ▽ More 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 paradoxical. Formalizing these versions of Yablo's paradox, we prove some theorems in LTL. This is the first time that Yablo's paradox(es) become new(ly discovered) theorems in mathematics and logic. △ Less

Submitted 1 June, 2014; originally announced June 2014.

Comments: Preprint; all comments/suggestions are most welcome!

MSC Class: 03B44; 03A05

Diagonalizing by Fixed-Points

Authors: Ahmad Karimi, Saeed Salehi

Abstract: A universal schema for diagonalization was popularized by N. S. Yanofsky (2003) 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 E… ▽ More A universal schema for diagonalization was popularized by N. S. Yanofsky (2003) 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 theorem on the infinitude of the primes and new proofs of Boolos (1997) for Cantor's theorem on the non-equinumerosity of a set with its powerset. Then, in Linear Temporal Logic, we show the non-existence of a fixed-point in this logic whose proof resembles the argument of Yablo's paradox. Thus, Yablo's paradox turns for the first time into a genuine mathematico-logical theorem in the framework of Linear Temporal Logic. Again the diagonal schema of the paper is used in this proof, and also it is shown that G. Priest's inclosure schema (1997) can fit in our universal diagonal/fixed-point schema. We also show the existence of dominating (Ackermann-like) functions (which dominate a given countable set of functions---like primitive recursives) using the schema. △ Less

Submitted 10 December, 2016; v1 submitted 4 March, 2013; originally announced March 2013.

Comments: to appear by the title "Diagonal Arguments and Fixed Points", The Bulletin of the Iranian Mathematical Society (2016) http://bims.iranjournals.ir/

MSC Class: 18A10; 18A15; 03B44; 03A05

Journal ref: Bulletin of the Iranian Mathematical Society 43:5 (2017) 1073--1088

Godel's Incompleteness Phenomenon - Computationally

Authors: Saeed Salehi

Abstract: We argue that Godel's completeness theorem is equivalent to completability of consistent theories, and Godel'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 d… ▽ More We argue that Godel's completeness theorem is equivalent to completability of consistent theories, and Godel'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 and consistency are not decidable in logic, and an analogue of Rice's Theorem holds for recursively enumerable theories: all the non-trivial properties of such theories are undecidable. △ Less

Submitted 10 December, 2016; v1 submitted 30 November, 2012; originally announced November 2012.

MSC Class: 03B25; 03D35; 03F40

Journal ref: Philosophia Scientiæ 18:3 (2014) 23--37

Herbrand Consistency of Some Finite Fragments of Bounded Arithmetical Theories

Authors: Saeed Salehi

Abstract: We formalize the notion of Herbrand Consistency in an appropriate way for bounded arithmetics, and show the existence of a finite fragment of ${\rm IΔ_0}$ whose Herbrand Consistency is not provable in the thoery ${\rm IΔ_0}$. We also show the existence of an ${\rm IΔ_0}-$derivable $Π_1-$sentence such that ${\rm IΔ_0}$ cannot prove its Herbrand Consistency. We formalize the notion of Herbrand Consistency in an appropriate way for bounded arithmetics, and show the existence of a finite fragment of ${\rm IΔ_0}$ whose Herbrand Consistency is not provable in the thoery ${\rm IΔ_0}$. We also show the existence of an ${\rm IΔ_0}-$derivable $Π_1-$sentence such that ${\rm IΔ_0}$ cannot prove its Herbrand Consistency. △ Less

Submitted 10 December, 2016; v1 submitted 9 October, 2011; originally announced October 2011.

MSC Class: 03F40; 03F25; 03F30

Journal ref: Archive for Mathematical Logic 52:3 (2013) 317--333

Separating Bounded Arithmetics by Herbrand Consistency

Authors: Saeed Salehi

Abstract: The problem of $Π_1-$separating the hierarchy of bounded arithmetic has been studied in the paper. It is shown that the notion of Herbrand Consistency, in its full generality, cannot $Π_1-$separate the theory ${\rm IΔ_0+\bigwedge_jΩ_j}$ from ${\rm IΔ_0}$; though it can $Π_1-$separate ${\rm IΔ_0+Exp}$ from ${\rm IΔ_0}$. This extends a result of L. A. Kołodziejczyk (2006), by showing the unprovabili… ▽ More The problem of $Π_1-$separating the hierarchy of bounded arithmetic has been studied in the paper. It is shown that the notion of Herbrand Consistency, in its full generality, cannot $Π_1-$separate the theory ${\rm IΔ_0+\bigwedge_jΩ_j}$ from ${\rm IΔ_0}$; though it can $Π_1-$separate ${\rm IΔ_0+Exp}$ from ${\rm IΔ_0}$. This extends a result of L. A. Kołodziejczyk (2006), by showing the unprovability of the Herbrand Consistency of ${\rm IΔ_0}$ in the theory ${\rm IΔ_0+\bigwedge_jΩ_j}$. △ Less

Submitted 10 December, 2016; v1 submitted 2 August, 2010; originally announced August 2010.

Comments: Published by Oxford University Press. arXiv admin note: text overlap with arXiv:1005.2654

MSC Class: Primary 03F30; 03F25; Secondary 03F05; 03F40

Journal ref: Journal of Logic and Computation 22:3 (2012) 545--560

Herbrand Consistency of Some Arithmetical Theories

Authors: Saeed Salehi

Abstract: 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, \textit{Fundamenta Mathematicae} 171 (2002) 279--292]. In that paper, it was shown that one cannot always shrink the witness o… ▽ More 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, \textit{Fundamenta Mathematicae} 171 (2002) 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 ${\rm IΔ_0+Ω_m}$ with $m\geqslant 2$, any witness for any bounded formula can be shortened logarithmically. This immediately implies the unprovability of Herbrand consistency of a theory $T\supseteq {\rm IΔ_0+Ω_2}$ in $T$ itself. In this paper, the above results are generalized for ${\rm IΔ_0+Ω_1}$. Also after tailoring the definition of Herbrand consistency for ${\rm IΔ_0}$ we prove the corresponding theorems for ${\rm IΔ_0}$. Thus the Herbrand version of Gödel's second incompleteness theorem follows for the theories ${\rm IΔ_0+Ω_1}$ and ${\rm IΔ_0}$. △ Less

Submitted 10 December, 2016; v1 submitted 15 May, 2010; originally announced May 2010.

MSC Class: Primary 03F40; 03F30; Secondary 03F05; 03H15

Journal ref: The Journal of Symbolic Logic 77:3 (2012) 807--827