A Model-Theoretic Formalization of AlKhwaremis ilm alfaraid

1 Introduction

• Al-Khwārizmī’s inheritance treatment is significant for its general computational procedures across specified configurations, not only its solutions to individual numerical problems.The introduction situates inheritance within a broader principle of complete computational treatment of a delimited jurisprudential domain.Source: §1 · p. 1
• The formalization represents specified inheritance problems as finite rational linear constraint systems and analyzes them separately from their model-theoretic structure.For a fixed configuration, the resulting structure can be represented in a finite-dimensional rational coordinate space.Source: §1 · p. 1
• Linguistic ambiguity alone does not establish formal inconsistency; conclusions about a jurisprudential system require an explicit reconstruction and analysis.The paper presents Computational Fiqh as a framework for analyzing formally specifiable structures in delimited domains.Source: §1 · pp. 1–2

1.1 Contributions and non-claims

• Every configuration in the specified class is represented by a finite rational linear constraint system, and every admissible rational linear-coordinate model is isomorphic to Qd.These are the representation lemma and canonicity theorem, respectively.Source: §1.1 · p. 2
• The inheritance-relevant fragment has an exact, terminating decision procedure, but the paper does not establish full decidability of Td.The paper also distinguishes semantic completeness of Td from algorithmic decidability of finite constraint systems.Source: §1 · p. 2, §1.1 · p. 3
• The paper claims representational canonicity rather than methodological exclusivity, makes no historical claim that Al-Khwārizmī used Fourier–Motzkin, and makes domain-relative completeness conditional on a companion framework.Its contribution to Computational Fiqh is framed as a methodological interpretation.Source: §1.1 · p. 3

2 The Quranic origin of Islamic Inheritance Systems

• The Kalalah wording admits multiple semantic assignments, so contradiction under one interpretation does not establish that the inheritance axioms are inconsistent.The text identifies three possible meanings of “siblings” in each verse, yielding nine pairings, and says an interpretation must be shown uniquely compelled before its contradiction can indict the underlying system.Source: §2 · pp. 5–7
• The paper says Al-Khwārizmī had essential conceptual ingredients of algebra in the linguistic architecture of the three Quranic verses.It does not exclude the possibility of external historical influences.Source: §2 · p. 7

2.1 The respective Quranic verses and their interpretation

• Across fifteen apportionment instances, ten use definite-article formulations, three link shares to the estate by additive genitive, and two repeat the male-to-female proportion.The definite formulations present a share without syntactically tying it to the estate’s numerical value.Source: §2.1 · p. 9
• The text treats prescribed fractions as conceptually distinct from estate values, allowing relational shares to be instantiated algebraically even when overlapping shares exceed unity.Definite, unlinked fractions present shares as determinate quantities, whereas genitive constructions explicitly relate them to the estate.Source: §2.1 · p. 9

2.2 The meaning of “ma” (؇݁) and “min ma” (؇݆݁݁

• The relative pronoun “ma” denotes obscurity and totality and mathematically binds the prescribed fraction to the estate’s absolute total.Source: §2.2 · p. 10
• The distinction between “ma” and partitive “min ma” separates shares of the total estate from agreed shares drawn from a portion, enabling resolution of overlapping inheritance shares.The section presents this grammatical distinction as the mechanism for addressing complex inheritance scenarios.Source: §2.2 · p. 10

2.3 The deduced notion of a math variable

• Both unified and strict-literal readings require algebraic variables rather than basic arithmetic to resolve inheritance shares that otherwise conflict or overflow.The unified approach scales shares with X; the literal approach assigns a theoretical subset p. In the example of a husband and two sisters, the prescribed shares total 7/6 under the unified reading.Source: §2.3 · p. 10, §2.6 · p. 12

2.4 Consistence of the inheritance axioms

• The inheritance axioms avoid literal mathematical contradiction because biological and logical exclusions prevent incompatible 1/2 and 2/3 claimants from co-occurring.For example, a husband’s 1/2 share requires no children, while two or more daughters receive 2/3; a single daughter also excludes two or more daughters.Source: §2.4 · pp. 10–11

2.5 A challenge for de-mystification efforts

• The paper argues that both unified and strict-literal interpretations function without contradiction, challenging claims that the inheritance axioms are mathematically inconsistent.It says biological exclusivity safeguards the text under both interpretations and frames explaining the framework’s development as a challenge for de-mystification efforts.Source: §2.5 · p. 11

2.6 Conclusion

• The conclusion describes the verses as encoding a scalable algebraic framework for arbitrarily large finite inheritance configurations in only three verses.It also characterizes the distinct methodologies as internally consistent and logically immune through embedded biological fail-safes.Source: §2.6 · p. 12
• The conclusion says these linguistic features motivate, but do not entail, the later formal construction, which supplies a representation lemma, canonicity theorem, and decision procedure.It also characterizes the language as promoting mathematical variables and shares relative to a conceptual whole.Source: §2.6 · pp. 11–12

3.1 Inheritance configurations and the representation lemma

• An admissible allocation requires shares matching the applicable Qur’anic fractions, conservation of the estate, and a bequest no greater than one third.The allocation assigns nonnegative rational shares and a nonnegative rational bequest.Source: §3.1 · p. 12
• Each inheritance configuration is represented by a finite rational linear system whose rational solutions correspond bijectively to admissible allocations.Finite applicability cases generate separate systems; prescribed shares and conservation are equalities, while the bequest cap is an inequality.Source: §3.1 · p. 13

3.2 A worked bequest

• Fourier–Motzkin projection yields x = 8/21 for one son, with the legal cap used in forming a projection.The projected system determines x uniquely; the retained equality is consistent but unnecessary for uniqueness.Source: §3.2 · pp. 13–14
• Fourier–Motzkin elimination is a modern formal representation of the problem’s computational structure, not a claim about Al-Khwārizmī’s historical procedure.Source: §3.2 · p. 14

• The language Ld includes zero, addition, rational scalar multiplication, coordinatewise order, and distinguished basis vectors for claimant coordinates.The setup fixes d claimant coordinates for an inheritance configuration.Source: §4 · p. 14
• Admissible structures require the distinguished vectors to be linearly independent over Q and to span every element by rational linear combinations.Source: §4 · p. 14
• The order relation compares structures coordinatewise in the distinguished basis.Source: §4 · p. 14

• The canonicity theorem establishes an isomorphism preserving zero, addition, rational scalar multiplication, distinguished basis vectors, and order.Source: §5 · p. 15
• The proof uses spanning and linear independence to obtain unique rational coordinates, then establishes that the coordinate map is bijective.Source: §5 · p. 15
• Within the admissible class, Vd is unique up to isomorphism, so admissible rational linear-coordinate formalizations have allocations that coincide under the isomorphism.Source: §5 · p. 16
• Canonicity is restricted to the admissible class and does not rule out nonlinear or non-coordinatewise formalizations.The paper relates ‘awl and algebraic procedures as different presentations of the same admissible structure.Source: §5 · p. 16

6 The First-Order Theory of the Fixed-Dimensional Model

• Td contains exactly the first-order sentences in Ld that are true in the intended structure Vd.The theory is formed by collecting the sentences satisfied by Vd.Source: §6 · p. 16

6.0.1 An Explicit First-Order Axiom System

• Ad explicitly axiomatizes expressible algebraic and order-theoretic properties, including the linear independence of distinguished vectors over the fixed rational coefficient field.Rational scalars are represented by function symbols, with each nonzero rational tuple yielding a sentence requiring the corresponding combination of distinguished vectors to be nonzero.Source: §6.0.1 · pp. 16–17

6.0.2 The Expressibility Limitation of the One-Sorted Language

• The one-sorted language cannot express the spanning condition as a single first-order formula because its quantifiers cannot range over the externally fixed field Q.The full coordinatewise-order characterization likewise remains part of the specified structure rather than an additional axiom of Ad.Source: §6.0.2 · p. 18

6.0.3 Completeness of the First-Order Theory

• Td is complete by construction, a design property rather than a novel theorem, and this completeness is independent of canonicity and constraint-system decidability.For every first-order sentence, either it or its negation is true in Vd and therefore belongs to Td.Source: §6.0.3 · p. 18

6.0.4 Structure of the Formal Argument

• The section separates structural canonicity, completeness of Td, and algorithmic decidability of the inheritance-relevant fragment as distinct conclusions.Ad is not categorical: its models properly contain the externally defined admissible class, while Td is complete but not categorical in Ld.Source: §6.0.2 · p. 18, §6.0.4 · p. 19

7.1 Scope of the decidability claim

• The decidability claim covers finite existential systems of rational linear constraints generated by inheritance configurations, not the full theory Td.Every question arising from an inheritance configuration is quantifier-free and linear.Source: §7.1 · p. 19

7.1.1 Input Representation

• Every finite inheritance configuration reduces to a finite system of rational linear inequalities after legal conditions are translated into algebraic form.Equalities are replaced by pairs of inequalities.Source: §7.1.1 · pp. 19–20

7.1.2 Fourier–Motzkin Elimination

• Fourier–Motzkin elimination removes variables by replacing their lower and upper bounds with pairwise compatibility constraints while retaining zero-coefficient inequalities.The elimination preserves satisfiability over Q because rational bounds permit rational solutions at each projection step.Source: §7.1.2 · p. 20

7.1.3 The Complete Decision Procedure

• The procedure decides satisfiability by eliminating all variables and checking whether the resulting rational constant inequalities contain a contradiction.A contradiction means the original system is inconsistent; otherwise it is satisfiable.Source: §7.1.3 · p. 21

7.1.4 Correctness of the Decision Procedure

• Theorem 2 establishes that Fourier–Motzkin terminates and correctly decides whether any finite rational linear system has a rational solution.At most n elimination stages are needed for n variables.Source: §7.1.4 · p. 21

7.1.5 Reconstruction of a Solution

• When a system is satisfiable, reversing the elimination steps selects rational values within the recovered bounds and reconstructs a rational solution.If the legal constraints determine a unique allocation, reconstruction yields the same rational values for every solution.Source: §7.1.5 · p. 22

7.1.6 Determining Uniqueness

• Uniqueness is decidable by projecting the feasible set onto each coordinate and checking whether every feasible interval is a singleton.A coordinate with an unbounded or non-singleton feasible interval means the allocation is not unique; otherwise the unique rational allocation is computed exactly.Source: §7.1.6 · pp. 22–23

7.2 Complexity

• Fourier–Motzkin elimination has doubly exponential worst-case complexity because constraint counts can square at each elimination step.For typical inheritance configurations with few claimants this is acceptable; the paper selects the method for proof transparency rather than asymptotic efficiency.Source: §7.2 · p. 23
• For larger configurations, linear-programming methods or polyhedral libraries may replace Fourier–Motzkin without changing the correctness argument.The alternatives decide the same fragment.Source: §7.2 · p. 23

7.2.1 Application to the Historical Bequest

• In the historical bequest example, eliminating w yields x = 8/21 directly, without using the retained equality.The passage also states that the legal cap has already been used in forming a projected constraint.Source: §7.2.1 · p. 24

7.3 Application to an ‘Awl configuration

• For a husband and two sisters, the prescribed shares total 7/6, prompting an ‘awl computation with claimant unknowns and a scaling variable.The example sets the husband’s share at 1/2 and each sister’s share at 1/3.Source: §7.3 · p. 24
• The procedure returns the same allocation as the classical ‘awl computation, while making the derivation explicit and mechanically checkable.The algebraic representation is presented as a uniform procedure, not as a different allocation.Source: §7.3 · p. 24

7.3.1 Termination and Computational Character

• The decision procedure terminates because each Fourier–Motzkin stage eliminates a variable from the finite configuration using rational arithmetic.The resulting allocations are exact rather than numerical approximations.Source: §7.3.1 · p. 24
• The procedure decides every fixed inheritance configuration represented by finite rational linear constraints, independently of Td’s completeness by construction.The two properties concern a terminating computational procedure and the first-order theory of the intended structure, respectively.Source: §7.3.1 · p. 25

• The section records a fit with the companion framework’s notion of domain-relative computational completeness, not a theorem established here.The notion is defined and established in the companion framework.Source: §8 · p. 25
• The broader framework represents closed Fiqh chapters through exhaustive case generation, Horn-clause axiomatization, and terminating deduction.The completeness of the axiom set for the specified finite case space is established elsewhere.Source: §8 · p. 25
• Under conditions C1–C3, domain-relative computational completeness holds for the specified closed Fiqh chapter.The conditions require finite exhaustive case generation, a Horn axiom set complete for that case space, and a deductive engine complete for its specified rule class.Source: §8 · p. 25
• The analogy is methodological: both approaches represent a delimited class of jurisprudential problems explicitly and resolve its instances by a general procedure.The inheritance framework uses algebraic relations over rational quantities; the broader framework uses case generation, Horn clauses, and deduction.Source: §8 · pp. 25–26

• Every admissible rational linear realization of the fixed-claimant-coordinate structure is isomorphic to the intended model, making the representation canonical within its class.A specified inheritance problem is represented by finite rational linear constraints and solved exactly by a terminating procedure.Source: §9 · p. 26
• The inheritance-relevant existential fragment is decidable by Fourier–Motzkin elimination, while the complete first-order theory is complete by construction and is not claimed to be fully decidable.These are distinct formal properties of the fragment and the intended model’s theory.Source: §9 · p. 26
• A contradiction under one semantic interpretation establishes at most that interpretation’s failure unless linguistic evidence uniquely compels it; ambiguity alone does not establish formal inconsistency.The paper calls for making the transition from natural-language statements to formal semantics explicit so alternative interpretations can be evaluated.Source: §9 · p. 26
• The algebraic representation makes inheritance problems’ structure explicit while preserving the allocations of the pre-algebraic procedure.The representation is described as canonical within the admissible class, with questions reducing to decidable existential questions over finite rational constraint systems.Source: §9 · p. 26
• The broader analogy applies only to a specified closed Fiqh domain and its defined ontology, question space, axioms, and deductive mechanism.It does not assert universal formalization.Source: §9 · p. 26