Bi-intuitionistic logic is the result of adding the dual of intuitionistic implication to intuitionistic logic. In this note, we characterize the expressive power of this logic by showing that the first order formulas equivalent to translations of bi-intuitionistic propositional formulas are exactly those preserved under bi-intuitionistic directed bisimulations. The proof technique is originally due to Lindstrom and, in contrast to the most common proofs of this kind of result, it does not use the machinery of neither saturated models nor elementary (...) chains. (shrink)

In this contribution, we will present some results concerning the connectives of bi-intuitionistic logic in the setting of Arnold Koslow’s implication structures. Furthermore, we will present soundness and completeness results of Koslow’s implication structures with respect to bi-intuitionistic logic.

The well-known algebraic semantics and topological semantics for intuitionistic logic (Int) is here extended to Wansing's bi-intuitionistic logic (2Int). The logic 2Int is also characterised by a quasi-twist structure semantics, which leads to an alternative topological characterisation of 2Int. Later, notions of Fregean negation and of unilateralisation are proposed. The logic 2Int is extended with a ‘Fregean negation’ connective ∼, obtaining 2Int∼, and it is showed that the logic N4⋆ (an extension of Nelson's paraconsistent logic) results to be the unilateralisation (...) of 2Int∼ via ∼. The logic 2Int∼ is also characterised by a Kripke-style semantics, a twist structure semantics and a topological semantics. (shrink)

In this paper, bi-intuitionistic multilattice logic, which is a combination of multilattice logic and the bi-intuitionistic logic also known as Heyting–Brouwer logic, is introduced as a Gentzen-type sequent calculus. A Kripke semantics is developed for this logic, and the completeness theorem with respect to this semantics is proved via theorems for embedding this logic into bi-intuitionistic logic. The logic proposed is an extension of first-degree entailment logic and can be regarded as a bi-intuitionistic variant of the original classical multilattice logic (...) determined by the algebraic structure of multilattices. Similar completeness and embedding results are also shown for another logic called bi-intuitionistic connexive multilattice logic, obtained by replacing the connectives of intuitionistic implication and co-implication with their connexive variants. (shrink)

The purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int, which Wansing presents in [2016a]. There he also gives a natural deduction system for this logic, N2Int, to which SC2Int is equivalent in terms of what is derivable. What is important is that these calculi represent a kind of bilateralist reasoning, since they (...) do not only internalize processes of verifcation or provability but also the dual processes in terms of falsifcation or what is called dual provability. In [Wansing, 2017] a normal form theorem for N2Int is stated, here, I want to prove a cut-elimination theorem for SC2Int, i.e., if successful, this would extend the results existing so far. (shrink)

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, (...) semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants. (shrink)

We present a multiple-assumption multiple-conclusion system for bi-intuitionistic logic. Derivations in the systems are graphs whose edges are labelled by formulas and whose nodes are labelled by rules. We show how to embed both the standard intuitionistic and dual-intuitionistic natural deduction systems into the proposed system. Soundness and completeness are established using translations with more traditional sequent calculi for bi-intuitionistic logic.

We consider a “polarized” version of bi-intuitionistic logic [5, 2, 6, 4] as a logic of assertions and hypotheses and show that it supports a “rich proof theory” and an interesting categorical interpretation, unlike the standard approach of C. Rauszer’s Heyting-Brouwer logic [28, 29], whose categorical models are all partial orders by Crolard’s theorem [8]. We show that P.A. Melliès notion of chirality [21, 22] appears as the right mathematical representation of the mirror symmetry between the intuitionistic and co-intuitionistc sides (...) of polarized bi-intuitionism. Philosophically, we extend Dalla Pozza and Garola’s pragmatic interpretation of intuitionism as a logic of assertions [10] to bi-intuitionism as a logic of assertions and hypotheses. We focus on the logical role of illocutionary forces and justification conditions in order to provide “intended interpretations” of logical systems that classify inferential uses in natural language and remain acceptable from an intuitionistic point of view. Although Dalla Pozza and Garola originally provide a constructive interpretation of intuitionism in a classical setting, we claim that some conceptual refinements suffice to make their “pragmatic interpretation” a bona fide representation of intuitionism. We sketch a meaning-asuse interpretation of co-intuitionism that seems to fulfil the requirements of Dummett and Prawitz’s justificationist approach. We extend the Brouwer-Heyting-Kolmogorov interpretation to bi-intuitionism by regarding co-intuitionistic formulas as types of the evidence for them: if conclusive evidence is needed to justify assertions, only a scintilla of evidence suffices to justify hypotheses. (shrink)

In this article we show that bi-intuitionistic predicate logic lacks the Craig Interpolation Property. We proceed by adapting the counterexample given by Mints, Olkhovikov and Urquhart for intuitionistic predicate logic with constant domains [13]. More precisely, we show that there is a valid implication $\phi \rightarrow \psi $ with no interpolant. Importantly, this result does not contradict the unfortunately named ‘Craig interpolation’ theorem established by Rauszer in [24] since that article is about the property more correctly named ‘deductive interpolation’ (see (...) Galatos, Jipsen, Kowalski and Ono’s use of this term in [5]) for global consequence. Given that the deduction theorem fails for bi-intuitionistic logic with global consequence, the two formulations of the property are not equivalent. (shrink)

We provide a sucient frame-theoretic condition for a super bi-intuitionistic logic to have Maksimova's variable separation property. We conclude that bi-intuitionistic logic enjoys the property. Furthermore, we offer an algebraic characterization of the super-bi-intuitionistic logics with Maksimova's property.

Bi-intuitionistic logic is the union of intuitionistic and dual intuitionistic logic, and was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ‘cut-free’ sequent calculus has recently been shown to fail cut-elimination. We present a new cut-free sequent calculus for bi-intuitionistic logic, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between intuitionistic implication and dual intuitionistic exclusion, similarly to future and past modalities in (...) tense logic. Our calculus handles this interaction using derivations and refutations as first class citizens. We employ extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of refutations, and rules which compose certain refutations and derivations to form derivations. Automated deduction using terminating backward search is also possible, although this is not our main purpose. (shrink)

We prove that certain natural sequent systems for bi-intuitionistic logic have the analytic cut property. In the process we show that the (global) subformula property implies the (local) analytic cut property, thereby demonstrating their equivalence. Applying a version of Maehara technique modified in several ways, we prove that bi-intuitionistic logic enjoys the classical Craig interpolation property and Maximova variable separation property; its Halldén completeness follows.

In this paper, we introduce the notions of connexive and bi-intuitionistic multilattices and develop on their base the algebraic semantics for Kamide, Shramko, and Wansing’s connexive and bi-intuitionistic multilattice logics which were previously known in the form of sequent calculi and Kripke semantics. We prove that these logics are sound and complete with respect to the presented algebraic structures.

We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present a proof (...) search strategy which allows it to be used for automated proof search. We prove that this search strategy is terminating and complete by showing how it can be used to mimic derivations obtained from an existing calculus GBiInt for bi intuitionistic logic. As far as we know, our new calculus is the first sequent calculus for bi intuitionistic logic which uses no semantic additions like labels, which has a purely syntactic cut elimination proof, and which can be used naturally for backwards proof search. Keywords: Bi-intuitionistic logic, display calculi, proof search. (shrink)

We reconsider the pragmatic interpretation of intuitionistic logic [21] regarded as a logic of assertions and their justi cations and its relations with classical logic. We recall an extension of this approach to a logic dealing with assertions and obligations, related by a notion of causal implication [14, 45]. We focus on the extension to co-intuitionistic logic, seen as a logic of hypotheses [8, 9, 13] and on polarized bi-intuitionistic logic as a logic of assertions and conjectures: looking at the (...) S4 modal translation, we give a de nition of a system AHL of bi-intuitionistic logic that correctly represents the duality between intuitionistic and co-intuitionistic logic, correcting a mistake in previous work [7, 10]. A computational interpretation of cointuitionism as a distributed calculus of coroutines is then used to give an operational interpretation of subtraction.Work on linear co-intuitionism is then recalled, a linear calculus of co-intuitionistic coroutines is de ned and a probabilistic interpretation of linear co-intuitionism is given as in [9]. Also we remark that by extending the language of intuitionistic logic we can express the notion of expectation, an assertion that in all situations the truth of p is possible and that in a logic of expectations the law of double negation holds. Similarly, extending co-intuitionistic logic, we can express the notion of conjecture that p, de ned as a hypothesis that in some situation the truth of p is epistemically necessary. (shrink)

Intuitionistic propositional logic with Galois negations ( \(\mathsf {IGN}\) ) is introduced. Heyting algebras with Galois negations are obtained from Heyting algebras by adding the Galois pair \((\lnot,{\sim })\) and dual Galois pair \((\dot{\lnot },\dot{\sim })\) of negations. Discrete duality between GN-frames and algebras as well as the relational semantics for \(\mathsf {IGN}\) are developed. A Hilbert-style axiomatic system \(\mathsf {HN}\) is given for \(\mathsf {IGN}\), and Galois negation logics are defined as extensions of \(\mathsf {IGN}\). We give the bi-tense (...) logic \(\mathsf {S4N}_t\) which is obtained from the minimal tense extension of the modal logic \(\mathsf {S4}\) by adding tense operators. We give a new extended Gödel translation \(\tau \) and prove that \(\mathsf {IGN}\) is embedded into \(\mathsf {S4N}_t\) by \(\tau \). Moreover, every Kripke-complete Galois negation logic _L_ is embedded into its tense companion \(\tau (L)\). (shrink)

We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order with the modal accessibility relation generalize to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, and show that their (...) topology-preserving conditions are equivalent to the properties that the inverse relation and the relation are lower semi-continuous with respect to the topologies on the two models. The first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical companion logic, we use the canonical model in a second main result to characterize a Hennessy–Milner class of topological models between any pair of which there is a maximal topological bisimulation that preserve the intuitionistic semantics. (shrink)

We generalize intuitionistic tense logics to the multi-modal case by placing grammar logics on an intuitionistic footing. We provide axiomatizations for a class of base intuitionistic grammar logics as well as provide axiomatizations for extensions with combinations of seriality axioms and what we call "intuitionistic path axioms". We show that each axiomatization is sound and complete with completeness being shown via a typical canonical model construction.

We take a fresh look at the logics of informational dependence and independence of Hintikka and Sandu and Väänänen, and their compositional semantics due to Hodges. We show how Hodges’ semantics can be seen as a special case of a general construction, which provides a context for a useful completeness theorem with respect to a wider class of models. We shed some new light on each aspect of the logic. We show that the natural propositional logic carried by the semantics (...) is the logic of Bunched Implications due to Pym and O’Hearn, which combines intuitionistic and multiplicative connectives. This introduces several new connectives not previously considered in logics of informational dependence, but which we show play a very natural rôle, most notably intuitionistic implication. As regards the quantifiers, we show that their interpretation in the Hodges semantics is forced, in that they are the image under the general construction of the usual Tarski semantics; this implies that they are adjoints to substitution, and hence uniquely determined. As for the dependence predicate, we show that this is definable from a simpler predicate, of constancy or dependence on nothing. This makes essential use of the intuitionistic implication. The Armstrong axioms for functional dependence are then recovered as a standard set of axioms for intuitionistic implication. We also prove a full abstraction result in the style of Hodges, in which the intuitionistic implication plays a very natural rôle. (shrink)

In this paper, we give a possible characterization of the distributivity on bi-approximation semantics. To this end, we introduce new notions of special elements on polarities and show that the distributivity is first-order definable on bi-approximation semantics. In addition, we investigate the dual representation of those structures and compare them with bi-approximation semantics for intuitionistic logic. We also discuss that two different methods to validate the distributivity—by the splitters and by the adjointness—can be explicated with the help of the axiom (...) of choice as well. (shrink)

We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus \(\mathtt{SC2Int}\) for the bi-intuitionistic logic \(\mathtt{2Int}\). A distinctive feature of \(\mathtt{SC2Int}\) is that it makes use of two kind of sequents, one representing proofs, the other representing refutations. The structural rules of \(\mathtt{SC2Int}\), in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, mediated through (...) two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of \(\mathtt{2Int}\). By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in \(\mathtt{SC2Int}\) is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously. (shrink)

Resumen: Este artículo sostiene que algunas Meta-Picto-Poesías del Paisaje compuestas por el poeta estadounidense Gary Snyder toman como tema la pintura china del paisaje con las características de la antigua poesía china, resplandeciente de incomparable encanto artístico y sustancia cultural. La poesía de este tipo es una combinación perfecta de elementos orientales y occidentales, que integra las culturas, los pensamientos y las artes de ambas partes, cuya apreciación crea una experiencia compleja con un híbrido de formas artísticas y espacios estéticos. (...) Gary Snyder no es sólo un eco-poeta, sino también un estilista y un hombre de práctica. Sus obras poéticas revelan la relación de fomento entre literatura, cultura y naturaleza. El artículo pretende hacer un intento transcultural, interdisciplinar y multidisciplinar en la crítica de Snyder, con métodos analíticos que incluyen culturas orientales y occidentales, visiones antiguas y actuales, así como experiencias dinámicas y estáticas. (shrink)

This article discusses Abū Isḥāq al-Naẓẓām’s (d. 231/845) (one of the first Muʽtazilī thinkers); understanding of Allah-world relationship, his theory of nature (tab‘) and his view on miracles. In a proposal form, Muʽtazilī scholars accept that the miracle, which is the actual confirmation, must occur, since it is not possible for Allah to confirm His messenger (prophet) in a way that everyone can hear and in a direct word. Since the Prophet's message can be authenticated only by a miracle, Muʽtazilī (...) thinkers paid great attention to this issue, organized and formed natural theories about the universe in a way that miracles can occur. Naẓẓām explains a kind of miracle that occurs under the power of Allah, by his theory of nature called latency and occurrence (kumūn-ẓuhūr). His view of miracles is rooted in the Muʽtazilī classification of miracles. Naẓẓām argues that in the theory of nature, things are infinitely divided. He also argues that all qualities considered accident (aʽrāḍ) by other Muslim theologians are different objects as only motion and rest are the only accidents. According to him, the universe consists of objects and accidents of motion only. In each object in the universe, an unlimited number of opposing objects (sub-components) that have different effects on each other is located in the same space. Those objects in the same space are intervened (tadākhul) with each other. Kumūn refers to sub-components that are located inside the object in a state of passing into each other, and a state of balancing each other through the push-pull motion (i‘timād). Ẓuhūr is an outward movement of the sub-component from where it is located when an impact imposed outside the object interacts with one of the sub-components contained in it. Naẓẓām says that too many opposing sub-components, such as heaviness-lightness, heat-coldness contained in the object, form an internal dynamic by providing balancing each other through inside the object with the push-pull motion. The state of balance inside the object is disrupted by an external factor affecting one of the sub-components. An external thing approaching the object interacts with one of the sub-components contained in the object. Then, the affected sub-component moves out of the object and thus the state of balance inside the object is disrupted. According to the theory of kumūn-ẓuhūr, change in objects occurs when the balance within the object is disturbed. The change in the balance also occurs not by the direct intervention of Allah and the creation of accidents, but by the disruption in the balance of natures within the object. Naẓẓām, who advocates the intrinsic natures in things, has been criticized for not leaving any room for Allah’s influence on objects at least through miracles. This criticism is not correct. Naẓẓām says that the nature of objects depends on God, and it is possible for God to intervene in them at any time. According to him, Allah can force opposing objects into a union that is not in their natures. In their natures, unification can separate those by applying pull and push. In this way, Naẓẓām sees the intervention of Allah as possible in the occurrence of a situation that is the opposite of what is present in the nature of objects. In Naẓẓām's theory of kumūn-ẓuhūr, there are suppressed natures and sub-components that are in a weak state inside the actual object. Furthermore, they cannot go out in any way from the actual object. One of these suppressed natures found in the object is removed from the nature of the object by the intervention of Allah when a miracle occurs in the hands of theProphet. In this case, the miracle is not something new that Allah has created, but that Allah has disclosed a hidden sub-component that is hidden in that thing that has never appeared before. Naẓẓām’s view of miracle is something occurring under the power of the created, which Muʽtazilī scholars accept in the classification of miracles in relation to, the theory of sarfa. He suggests that the Qur'an, which he accepts under the power of the created, would not be a miracle, if the Arabs could dispute it. However, according to him, the Qur'an is a miracle because Allah prevents them from the dispute. In his understanding of sarfa, the miracles occur directly as an act of God’s divine intervention with human beings. This study investigates Naẓẓām’s view of miracles along with his theory of nature and his understanding of sarfa. (shrink)

Bilişsel Din Bilimi (CSR), dini inanç ve uygulamaların nedensel açıklamalarını sağlamayı amaçlayan din araştırmalarına bilimsel bir yaklaşımdır. CSR savunucuları, insan zihninin doğal özelliklerini ve nasıl işlediğini açıklayarak dini inançların oluşumu, kabulü, aktarımı ve yaygınlığı sürecini açıklamaya çalışırlar. Tüm insan kültürlerinde var olan ve son on yılda birçok CSR akademisyeninin dikkatini çeken dini inançlardan biri de öbür dünyaya olan inançtır. CSR araştırmacılarına göre, bu inanç, insan zihninin doğal yapılarına dayanmaktadır. Ölümden sonraki hayata olan inancı, zihinsel araçların işleyişinden kaynaklanan, yansıtıcı olmayan veya (...) sezgisel bir inanç olarak görürler. Ölümden sonra hayata inancın oluşumunu, gelişimini, yayılmasını ve aktarılmasını açıklamak için çeşitli teoriler önerdiler. Ancak bu teoriler arasında, iki teori daha geniş kabul görmüştür, sezgisel düalizm teorisi ve simülasyon kısıtlama teorisi. Sezgisel düalizm teorisi, tüm insanların iki zihinsel araca sahip olduğunu söyler: Sezgisel Biyoloji ve Sezgisel Psikoloji. Sezgisel Biyoloji, ölü bir kişinin karşısına geçip hareket edemediği için artık hayatta olmadığına inanmamızı sağlar. Sezgisel Psikoloji, ölü kişiye otomatik olarak görünmez özellikleri (arzular, düşünceler, inançlar ve duygular gibi) atfetmeye devam eder. Yukarıdaki iki zihinsel aracın aynı anda işleyişi, insan zihnini ölü kişinin bir kısmının önemsiz olduğuna ve fiziksel ölümden sonra kaldığına inandırır. Simülasyon kısıtlama teorisi, tüm insanların çevreden gelen bilgileri işlemek ve dini inançlar edinmek için zihinsel araçlara sahip olduğunu söyler. Zihinsel araçların hiçbiri, kişinin arzularının, düşüncelerinin, inançlarının ve duygularının var olmadığını hayal edemez veya simüle edemez. Bu nedenle ölü kişinin karşısındaki insan zihni, fiziksel ölümünü kolayca hayal etmesine rağmen, kişinin başka bir bölümünün (düşünceler, arzular vb.) Varlığına inanmaya devam eder. Bu teorilerin her ikisi de, öbür dünyaya inancın oluşumunu açıklamada zorluklar ve sınırlamalarla karşı karşıya görünüyor. Bunlar arasında nedensel açıklama yapamama, ölümden sonraki hayata olan inancın doğal ve rasyonel temelleri arasındaki ayrım eksikliği ve öbür dünya inancının doğaüstü temellerini göz ardı etme yer alır. İki teoriden hiçbiri öbür dünyaya inancın oluşumu için yeterli nedensel açıklama sağlamıyor gibi görünmektedir. Her iki teori de zihinsel araçların nasıl işlediğine bağlı olarak öbür dünya inançlarının oluşumu hakkında olası bir hikaye sunmaya çalışır. Ölümden sonraki hayata inanmaya yol açan sürecin yalnızca makul bir hikayesini sunarlar. Bu iki teorinin sunduğu şey, insan zihninin ve araçlarının ve bunların nasıl işlediğinin bir açıklamasıdır (nedensel açıklama değil). Bu, kendi başına, bu aletlerin öbür dünyaya bir inanç ürettiğini açıklamaz. Dolayısıyla ahirete olan inancın zihinsel araçların işleyişinin bir sonucu olduğu iddiası, zihinsel araçlar ile bu inanç arasında nedensel bir ilişki gerektirir. Bu iki teoriden hiçbiri bu nedensel ilişkiyi açıklayamaz ve yalnızca aralarındaki ilişkinin makul bir hikayesini açıklarlar. Dahası, dini inancın rasyonel temelleri ile dini inancın doğal temelleri arasındaki ayrım, ahirete inanmak veya onunla ilişkili bilişsel mekanizmaları tanımlamak için doğal bir köken bulmanın hiçbir şekilde bu inancı reddetmek veya itibarını sarsmak anlamına gelmediğini göstermektedir. Ahirete olan inancın doğal kökenleri hakkındaki bilişsel teoriler bize bu inancın rasyonel mi irrasyonel mi olduğunu gösteremez. Bu açıklamalar ancak (eğer yapabilirlerse) bize bu inancın oluşumunun ve yaygınlığının doğal köklerini gösterebilir. Ayrıca Dinsel inanç karmaşık bir kavramdır. Birincisi, doğal bir kavramdır, bu anlamda insan doğasına dayanır ve insanın bilişsel sistemleri ve zihinsel araçlarıyla ilgilidir. İkincisi, kültürel ve sosyal bir kavramdır, bu anlamda hem kültürel ve sosyal değişimden etkilenir hem de onu etkiler. Üçüncüsü, doğaüstü bir kavramdır, bu anlamda hem vahiy hem de kehanet ve insanın maddi olmayan yönüyle derinden bağlantılıdır. Öbür dünyaya inanç, her üç düzeyde açıklamayı gerektiriyor gibi görünüyor. (shrink)

This article discusses Abū ʽUthmān al-Jāḥiẓ (d. 255/869) (one of the first Muʽtazilī scholars) Allah-world relationship, his understanding of custom, and his view on miracles. The Muʻtazilī thinkers examined the problem of miracles within their concept of prophethood. They divide miracles, which they accept as the only proof of prophethood, into two: those under the power of Allah and under the power of the created. Jāḥiẓ explains these two sorts of miracles with the order in the universe established by Allah (...) and people and expresses this order with the concept of custom (ʻāda). Jāḥiẓ divides custom into three. The first of these is the “qā’im (constant) custom”, which is based on the theory of kumūn-ẓuhūr and expresses the general rules that occur as a requirement of the general functioning in the universe. According to Jāḥiẓ “qā’im (constant) custom” is that knowledgeable people are aware of the custom of the universe. This custom is an order created by Allah in the eyes of intelligent and knowledgeable people, which is continuous and therefore cannot be interrupted, and in which there is no chaos. He states that this order is realized through the natures in the objects, which are knowable to everyone. But rarely a nature in this order can be interrupted due to a situation that takes it out of the natural flow and cannot be explained by natural causes. According to him, this is proof that nature, which has the defining feature of the object, is created by the creator, and maintains its continuity based on an arranged program. However, the creator can involve in this order when necessary. In this type of custom, God’s intervention occurs by breaking the qā’im custom that continues on a regular basis. The second of these is the “regional custom”, which is not known to everyone but only known to people living in a certain area. Jāḥiẓ states that the miracle in this type of custom occurred when Allah broke the custom known to the people in the region. The third of these is “social custom” which is established by people. For Jāḥiẓ, the miracles of this kind are under the power of people. He argues that the miracle in this type of custom occurs with sarfa, that is, by God’s intervention with human’s motive or knowledge. In this study, Jāḥiẓ’s view of miracles is discussed together with his theory of nature, his understanding of custom and sarfa. (shrink)

Legal Judgment Prediction (LJP) is an essential component of legal assistant systems, which aims to automatically predict judgment results from a given criminal fact description. As a vital subtask of LJP, researchers have paid little attention to the numerical LJP, i.e., the prediction of imprisonment and penalty. Existing methods ignore numerical information in the criminal facts, making their performances far from satisfactory. For instance, the amount of theft varies, as do the prison terms and penalties. The major challenge is how (...) the model can obtain the ability of numerical comparison and magnitude perception, e.g., 400 < 500 < 800, 500 is closer to 400 than to 800. To this end, we propose a judicial knowledge-enhanced magnitude-aware reasoning architecture, called NumLJP, for the numerical LJP task. Specifically, we first implement a contrastive learning-based judicial knowledge selector to distinguish confusing criminal cases efficiently. Unlike previous approaches that employ the law article as external knowledge, judicial knowledge is a quantitative guideline in real scenarios. It contains many numerals (called anchors) that can construct a reference frame. Then we design a masked numeral prediction task to help the model remember these anchors to acquire legal numerical commonsense from the selected judicial knowledge. We construct a scale-based numerical graph using the anchors and numerals in facts to perform magnitude-aware numerical reasoning. Finally, the representations of fact description, judicial knowledge, and numerals are fused to make decisions. We conduct extensive experiments on three real-world datasets and select several competitive baselines. The results demonstrate that the macro-F1 of NumLJP improves by at least 9.53% and 11.57% on the prediction of penalty and imprisonment, respectively. (shrink)