We represent the well-known surprise exam paradox in constructive and computable mathematics and offer solutions. One solution is based on Brouwer’s continuity principle in constructive mathematics, and the other involves type 2 Turing computability in classical mathematics. We also discuss the backward induction paradox for extensive form games in constructive logic.

The connection between the infinite nature of Quantum Cosmology and the infinite nature of God is presented here. At the beginning of the creation process, there was a single God/Void that was divided into many Gods/Voids all filled with Dark Energy consisting of photons which were responsible for creating the Multiverses made of matter, antimatter, space, time, charge, and multiple dimensions of space. The one God initially had no material existence which along with the laws of science was a creation (...) of the powers of His infinite mind. Since the process of creation started with the Dark Energy of the Voids, the Conservation of Energy Principle applied to all of them. If the Dark Energy of each Void were to be finite, then its energy would begin to decrease as Multiverses were created, and the only solution for not violating the Conservation of Energy Principle was that the Dark Energy of each of the Voids must be infinite implying that the Voids themselves must be infinite, and with infinite amount of energy be able to create an infinite number of Multiverses. According to Mathematics, all infinite numbers are not equal, some infinities are greater than other infinities. Hence of the many infinite Voids that were initially created, some Voids were greater than others. Each Void has a Supreme Leader that we refer to as God, and therefore there exist many Gods, some Gods more powerful than other Gods. (shrink)

Twenty two treatises on Islamic ethics by eminent personalities in early Islam.

In "Intuitionistic validity in -normal Kripke structures," Buss asked whether every intuitionistic theory is, for some classical theory , that of all -normal Kripke structures for which he gave an r.e. axiomatization. In the language of arithmetic and denote PA plus Open Induction or Open LNP, and are their intuitionistic deductive closures. We show is recursively axiomatizable and , while . If proves PEM but not totality of a classically provably total Diophantine function of , then and so . A (...) result due to Wehmeier then implies . We prove is not -conservative over . If , then is not closed under MR or Friedman's translation, so range (). Both and are closed under the negative translation. (shrink)

We present an axiomatization for Basic Propositional Calculus BPC and give a completeness theorem for the class of transitive Kripke structures. We present several refinements, including a completeness theorem for irreflexive trees. The class of intermediate logics includes two maximal nodes, one being Classical Propositional Calculus CPC, the other being E1, a theory axiomatized by T → ⊥. The intersection CPC ∩ E1 is axiomatizable by the Principle of the Excluded Middle A V ∨ ⌝A. If B is a formula (...) such that → B is not derivable, then the lattice of formulas built from one propositional variable p using only the binary connectives, is isomorphically preserved if B is substituted for p. A formula → B is derivable exactly when B is provably equivalent to a formula of the form → A) →. (shrink)

Muslim scholars have had different approaches toward modern technologies. Defining the situation in various Islamic countries is dependent on knowing the approaches adopted by their scholars. These approaches create norms which can shed light on the reasons for the success and failure of access to technology and its transference. The present article sets out to analyze the views of the Qom seminary scholars in Iran about the development of modern technologies within the framework of the development sociology using the qualitative (...) methodology of grounded theory. To this end, such techniques as conducting interviews and investigating documents have been used to gather the data. The authors find four paradigm models regarding modern technologies among the Qom seminary scholars. These models are classified into two general categories: optimistic and pessimistic. In the end, an “appropriate technology” approach is introduced as an approach singled out by the researchers. (shrink)

RésuméʾAbū Saʿīd al-Siǧzī, astronome et mathématicien du ive/xe siècle, fut l'un des premiers auteurs du genre ʿilm al-hayʾa ; mais on connaît peu la genèse de cette discipline et sa relation aux autres écrits et pratiques en astronomie. Dans cet article, je présente de nouvelles découvertes permettant de préciser la biographie d'al-Siǧzī. Je décris ensuite, pour la première fois, une composition d'astronomie théorique du ive/xe siècle, la « Structure des orbes » d'al-Siǧzī, et je montre sa place dans la formation (...) de la discipline ʿilm al-hayʾa en comparant ce livre à l'ouvrage antérieur d'al-Farġānī sur la taille de la Terre et le nombre des sphères célestes. Je conclus que la Tarkīb al-aflāk d'al-Siǧzī est le plus ancien exemple connu d'un livre traitant des sujets abordés plus tard en hayʾa, et qu'il contient peutêtre la première occurrence du neuvième orbe céleste, classique dans les écrits du genre. (shrink)

Philosophy and evaluation of traditions based on the ideas of traditionalist and philosopher Seyyed Hossein Nasr, 1933-.

A latarre is a lattice with an arrow. Its axiomatization looks natural. Latarres have a nontrivial theory which permits many constructions of latarres. Latarres appear as an end result of a series of generalizations of better known structures. These include Boolean algebras and Heyting algebras. Latarres need not have a distributive lattice.

Let ℒ and ? be propositional languages over Basic Propositional Calculus, and ℳ = ℒ∩?. Weprove two different but interrelated interpolation theorems. First, suppose that Π is a sequent theory over ℒ, and Σ∪ {C⇒C′} is a set of sequents over ?, such that Π,Σ⊢C⇒C′. Then there is a sequent theory Φ over ℳ such that Π⊢Φ and Φ, Σ⊢C⇒C′. Second, let A be a formula over ℒ, and C 1, C 2 be formulas over ?, such that A∧C 1⊢C (...) 2. Then there exists a formula B over ℳ such that A⊢B and B∧C 1⊢C 2. (shrink)

We prove that Basic Arithmetic, BA, has the de Jongh property, i.e., for any propositional formula A built up of atoms p1,..., pn, BPC⊢\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\vdash}$$\end{document}A if and only if for all arithmetical sentences B1,..., Bn, BA⊢\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\vdash}$$\end{document}A. The technique used in our proof can easily be applied to some known extensions of BA.

A bounded monotone sequence of reals without a limit is called a Specker sequence. In Russian constructive analysis, Church's Thesis permits the existence of a Specker sequence. In intuitionistic mathematics, Brouwer's Continuity Principle implies it is false that every bounded monotone sequence of real numbers has a limit. We claim that the existence of Specker sequences crucially depends on the properties of intuitionistic decidable sets. We propose a schema about intuitionistic decidability that asserts “there exists an intuitionistic enumerable set that (...) is not intuitionistic decidable” and show that the existence of a Specker sequence is equivalent to ED. We show that ED is consistent with some certain well known axioms of intuitionistic analysis as Weak Continuity Principle, bar induction, and Kripke Schema. Thus, the assumption of the existence of a Specker sequence is conceivable in intuitionistic analysis. We will also introduce the notion of double Specker sequence and study the existence of them. (shrink)

Described as a gem in Islam, intellect can lead all individual and social behaviours towards balance, appeal and godliness. Given the utmost importance of protecting intellect in this divine religion, everything from eating and drinking to reading, listening and entertainment is thus considered haram [ viz. remains prohibited] if it makes threats to the health of mind and soul. In general, narcotics and substance abuse in all forms can have crushing and all-encompassing effects, that is, inflict heavy blows on the (...) body, soul, mind, willpower and religion in a person and consequently destroy life in the family and society. The continuation of life as well as the stability and survival of this holy institution accordingly depends on many factors, including addiction tendency (AT) and sexual dysfunction (SD). It is also obvious that the balance and optimal use of sexual instinct on the accepted path of religion will be the key to the family health and strength. Altogether, the role of AT and SD on intention to divorce (ITD) in Indonesian Muslim couples ( n = 450) was investigated in 2022 in this study, wherein one partner had previously attended addiction treatment centres over the last 6 months. The study results ultimately demonstrated that AT could induce SD and consequently raise ITD among Muslim couples. Contribution: The study results confirmed the harmful impacts of AT on SD among Muslim couples, which could increase their ITD. In view of this, it was suggested to promote religious teachings in the family to benefit from their positive effects. (shrink)

Avicenna introduces the primary propositions as the most fundamental principles of knowledge. However, as far as we are aware, Avicenna’s primaries have not yet been independently studied. Nor do Avicenna scholars agree on how to characterize them in the language of contemporary philosophy. It is well-known that the primaries are indemonstrable; nonetheless, it is not clear what the genealogy of the primaries is, how, epistemologically speaking, they can be distinguished from other principles, what their phenomenology is, what the cause of (...) the assent to them is, how to explain the relationship between the ‘innate [nature] of the intellect’ and the primaries and, finally, back to their indemonstrability, in what sense they are ‘indemonstrable’. We will try to fill this gap. As a corollary, we will explain why Gutas’s view [Gutas, Dimitri.... (shrink)

Basic Predicate Logic, BQC, is a proper subsystem of Intuitionistic Predicate Logic, IQC. For every formula in the language {, , , , , , }, we associate two sequences of formulas 0,1,... and 0,1,... in the same language. We prove that for every sequent , there are natural numbers m, n, such that IQC , iff BQC n m. Some applications of this translation are mentioned.

We prove that every infinite rooted narrow tree Kripke model of HA is locally PA.

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.

We give a counterexample to the claim that every provably total function of Basic Arithmetic is a polynomially bounded primitive recursive function.

Let denote a first‐order logic in a language that contains infinitely many constant symbols and also containing intuitionistic logic. By, we mean the associated logic axiomatized by the double negation of the universal closure of the axioms of plus. We shall show that if is strongly complete for a class of Kripke models, then is strongly complete for the class of Kripke models that are ultimately in.

Kolmogorov established the principle of the double negation translation by which to embed Classical Predicate Logic |${\operatorname {CQC}}$| into Intuitionistic Predicate Logic |${\operatorname {IQC}}$|⁠. We show that the obvious generalizations to the Basic Predicate Logic of [3] and to |${\operatorname {BQC}}$| of [12], a proper subsystem of |${\operatorname {IQC}}$|⁠, go through as well. The obvious generalizations of Kuroda’s embedding are shown to be equivalent to the Kolmogorov variant. In our proofs novel nontrivial techniques are needed to overcome the absence of (...) full modus ponens in Basic Predicate Logic. In [3] we argued that |${\operatorname {IQC}}$| is not the logic of constructive mathematics. Our doubts were far from new. New was that we put forward an alternative, |${\operatorname {BQC}}$|⁠. One concern is that |${\operatorname {BQC}}$| is too weak for serious mathematics, or even trivial. This paper is one step to alleviate such concerns. (shrink)

Let A be a subset of the constructive real line. What are the necessary and sufficient conditions for the set A such that A is continuously separated from other reals, i.e., there exists a continuous function f with f−1(0) = A? In this paper, we study the notions of closed sets and closure maps in constructive reverse mathematics.

In the context of intuitionistic analysis, we consider the set consisting of all continuous functions from [0,1] to such that =0 and =1, and the set consisting of ’s in where there exists x[0,1] such that . It is well-known that there are weak counterexamples to the intermediate value theorem, and with Brouwer’s continuity principle we have . However, there exists no satisfying answer to . We try to answer to this question by reducing it to a schema about intuitionistic (...) decidability that asserts “there exists an intuitionistically enumerable set that is not intuitionistically decidable”. We also introduce the notion of strong Specker double sequence, and prove that the existence of such a double sequence is equivalent to the existence of a function where. (shrink)

For the Heyting Arithmetic HA, $HA^{\text{*}} $ is defined [14, 15] as the theory $\left\{ {A|HA \vdash A^\square } \right\}$, where $A^\square $ is called the box translation of A. We characterize the ${\text{\Sigma }}_1 $-provability logic of $HA^{\text{*}} $ as a modal theory $iH_\sigma ^{\text{*}} $.

We generalize the double negation construction of Boolean algebras in Heyting algebras to a double negation construction of the same in Visser algebras. This result allows us to generalize Glivenko’s theorem from intuitionistic propositional logic and Heyting algebras to Visser’s basic propositional logic and Visser algebras.

Since the modern age the attacks against faith and religious belief have been raised. One of the major arguments against the existence of God who is described in theistic religious holy books as Almighty and all loving God come in terms of suffering in human life and the presence of evil in the world created by God. The challenge according to the critics against the religious life and faith is how a believer can be considered rational in his faith while (...) there are many suffering in human life and evil in the world. The aim of this paper is to deal with this challenge and the solution is given on the basis of Islamic teachings. There are different responses for this challenge both in Islamic theology and Christian theology. This research is limited to Quranic teachings and the main claim as one possible response and defense for the presence of evil in human life is to point out that evil plays a main role in provoking inborn knowledge of God in human nature. Keywords - life, inborn, faith, Quran, evil. (shrink)

In the Quran, the Muslim Holy book, many verses refer to the human being and in many ways issues regarding mankind are dealt with. In the Quran the possibility of doubting God’s existence is ruled out as man has a particular nature. The aim of this paper is to disclose the very basic Quranic concept concerning human nature: Fitrah. According to the Quranic understanding, mankind has its origin in God; this understanding is based on the concept of Fitrah. Fitrah is (...) considered a natural component of the human being in which God and another Truth can be perceived through man’s existential experience. (shrink)

In the Quran, mankind is mentioned in many verses with honours and dignity regarding its creation and position. The human being in some verses is honoured and respected: man is superior to angels as they bowed for Adam as the first man. Meanwhile the human being in other verses is dishonoured and devalued; being described like animals or lower beings. The aim of this paper is to deal with the Quranic perspective regarding the human being’s dignity and honour. The nature (...) of human dignity and honour in existential interpretation is seen in self—realization and self—making destination. In this regard everything in the world is in the service of man in making his destination and identification. (shrink)

We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.

We study the linear Lindenbaum algebra of Basic Propositional Calculus, called linear basic algebra.

We study the variety of Löb algebras , the algebraic structures associated with formal propositional calculus. Among other things, we prove a completeness theorem for formal propositional logic with respect to the variety of Löb algebras. We show that the variety of Löb algebras has the weak amalgamation property. Some interesting subclasses of the variety of Löb algebras, e.g. linear, faithful and strongly linear Löb algebras are introduced.

In this paper we prove a bounded translation of intuitionistic propositional logic into basic propositional logic. Our new theorem, compared with the translation theorem in [1], has the advantage that it gives an effective bound on the translation, depending on the complexity of formulas.

We introduce a Gentzen-style sequent calculus axiomatization for Basic Predicate Calculus. Our new axiomatization is an improvement of the previous axiomatizations, in the sense that it has the subformula property. In this system the cut rule is eliminated.

We study Basic algebra, the algebraic structure associated with basic propositional calculus, and some of its natural extensions. Among other things, we prove the amalgamation property for the class of Basic algebras, faithful Basic algebras and linear faithful Basic algebras. We also show that a faithful theory has the interpolation property if and only if its correspondence class of algebras has the amalgamation property.