A Model-Theoretic Formalization of AlKhwaremis ilm alfaraid

Abstract

This paper presents a model theoretic and computational formalization of AlKhwarizmis treatment of inheritance within the framework of Computational Fiqh. We first show that every inheritance configuration in a specified class is representable as a finite system of rational linear equalities and inequalities, and that such systems are decided exactly by Fourier Motzkin elimination over Q. We then define the fixed dimensional inheritance structure Vd with distinguished claimant coordinates, and prove that every admissible rational linear coordinate realization is isomorphic to Vd, this establishes the algebraic representation as canonical within that class. The complete first order theory Td of Vd is shown to be complete by construction and is explicitly distinguished from the decidability of the inheritance relevant fragment. The methodological principle is then related to a broader formalization of closed Fiqh domains via exhaustive case generation, Horn clause axiomatization, and terminating deduction, yielding domain relative computational completeness.