Source Chain Formalization: Provenance Model¶

Abstract¶

Every halachic assertion must be traceable to its sources (mekorot). This document formalizes the provenance model for Mistaber, establishing the makor/2 predicate as a directed acyclic graph connecting rules to their textual sources. We define an authority ordering over sources, formalize citation chains through halachic literature, and prove a completeness theorem ensuring every derived conclusion has a well-founded source chain. The model draws from data provenance theory while adapting to the unique requirements of halachic scholarship, including primary sources (Tanakh, Talmud), codified law (Shulchan Aruch), and commentarial literature.

1. Introduction¶

1.1 The Makor Requirement¶

In halachic discourse, every legal statement requires substantiation. The Talmudic dictum "mai t'ama?" (what is the reason?) reflects the imperative that conclusions must be justified. This manifests as:

Textual Citation: Rules trace to verses, Mishnaic passages, or Talmudic discussions
Authority Chain: Later authorities cite earlier ones, creating citation networks
Explicit Attribution: Statements identify their sources explicitly

1.2 Provenance in Computational Systems¶

Data provenance---tracking the origins and transformations of data---has been extensively studied in databases (Buneman et al., 2001). Mistaber adapts these concepts to halachic knowledge:

Why-Provenance: Which sources contributed to a conclusion?
How-Provenance: What logical path connected sources to conclusion?
Where-Provenance: In which texts are the relevant passages found?

1.3 Contribution¶

We provide:

Formal provenance graph structure with the makor/2 predicate
Authority hierarchy for source classification
Citation chain semantics with transitive closure
Completeness theorem for source attribution
Conflict resolution when sources disagree

2. Preliminaries¶

2.1 Provenance Graphs¶

Definition 2.1 (Provenance Graph). A provenance graph is a DAG 𝐺 = ⟨𝑉, 𝐸, λ⟩ where: - 𝑉 is a set of nodes (data items or processes) - 𝐸 ⊆ 𝑉 × 𝑉 is a set of directed edges (derivation relation) - λ: 𝑉 → Types assigns types to nodes

Definition 2.2 (Why-Provenance). The why-provenance of node 𝑣 is the set of source nodes that contribute to 𝑣: $$why(v) = {u ∈ V : u \xrightarrow{*} v ∧ source(u)}$$

2.2 Halachic Authority Levels¶

Definition 2.3 (Authority Level). Sources are classified by authority:

Level	Name	Period	Example
1	Torah	Biblical	Shemot 23:19
2	Nevi'im/Ketuvim	Biblical	Yeshayahu 1:11
3	Mishnah	Tannaitic	Mishnah Chullin 8:1
4	Tosefta	Tannaitic	Tosefta Chullin 8:1
5	Bavli	Amoraic	Chullin 113a
6	Yerushalmi	Amoraic	Yerushalmi Chullin 8:1
7	Rishonim	Medieval	Rambam, Ma'achalot 9:1
8	Shulchan Aruch	Early Modern	SA YD 87:1
9	Acharonim	Modern	Shach YD 87:1

3. The Makor Predicate¶

3.1 Definition¶

Definition 3.1 (Makor). The makor/2 predicate relates rules to sources: $$makor(r, s)$$

where: - 𝑟 is a rule identifier - 𝑠 is a source reference

Definition 3.2 (Source Reference). A source reference 𝑠 is a structured citation: $$s = work(location)$$

Examples: - sa("yd:87:1") - Shulchan Aruch, Yoreh Deah, Siman 87, Seif 1 - rambam("maasurot:9:1") - Rambam, Hilchot Ma'achalot Asurot, Chapter 9, Halacha 1 - gemara("chullin:113a") - Talmud Bavli, Chullin, Daf 113a

3.2 Multiple Sources¶

Definition 3.3 (Multi-Source Rule). A rule may have multiple sources: $$makor(r, s_1) ∧ makor(r, s_2) ∧ ... ∧ makor(r, s_n)$$

This captures halachic practices where a ruling is supported by multiple texts.

Example 3.1 (Multiple Sources for Fish and Dairy).

rule(r_rema_dag_chalav_mutar).
makor(r_rema_dag_chalav_mutar, rema("yd:87:3")).
makor(r_rema_dag_chalav_mutar, taz("yd:87:3")).
makor(r_rema_dag_chalav_mutar, shach("yd:87:5")).

3.3 Mandatory Attribution¶

Axiom 3.1 (Makor Requirement). Every rule must have at least one source: $$∀r: rule(r) → ∃s: makor(r, s)$$

Constraint 3.1 (Enforcement).

:- rule(R), not has_makor(R).
has_makor(R) :- rule(R), makor(R, _).

4. Source Hierarchy and Authority¶

4.1 Source Type Classification¶

Definition 4.1 (Source Types). Sources are classified hierarchically:

Source
├── Primary
│   ├── Torah
│   ├── Nevi'im
│   └── Ketuvim
├── Oral Law
│   ├── Mishnah
│   ├── Tosefta
│   ├── Bavli
│   └── Yerushalmi
├── Codification
│   ├── Rishonim (Rambam, Tur, etc.)
│   └── Shulchan Aruch
└── Commentary
    ├── Early Acharonim (Shach, Taz, etc.)
    └── Later Acharonim (MB, AH, etc.)

4.2 Authority Ordering¶

Definition 4.2 (Authority Relation). For source types τ₁, τ₂: $$authority(τ_1) > authority(τ_2)$$

iff τ₁ has greater halachic authority than τ₂.

Principle 4.1 (Later Cannot Dispute Earlier of Higher Authority). A later source cannot override an earlier source of significantly higher authority without explicit justification.

4.3 Conflict Resolution¶

Definition 4.3 (Source Conflict). Sources 𝑠₁ and 𝑠₂ conflict on rule 𝑟 iff: $$supports(s_1, conclusion(r, v_1)) ∧ supports(s_2, conclusion(r, v_2)) ∧ v_1 ≠ v_2$$

Rule 4.1 (Authority-Based Resolution). $$\frac{conflict(s_1, s_2, r) \quad authority(type(s_1)) > authority(type(s_2))}{preferred(s_1, r)}$$

When sources of equal authority conflict, this becomes a machloket requiring additional resolution mechanisms (see Document 04).

5. Citation Chains¶

5.1 Direct and Transitive Citation¶

Definition 5.1 (Direct Citation). Source 𝑠₁ directly cites 𝑠₂: $$cites(s_1, s_2)$$

Definition 5.2 (Citation Chain). The transitive closure of citation: $$citation_chain(s_1, s_n) \text{ iff } ∃s_2, ..., s_{n-1}: cites(s_1, s_2) ∧ ... ∧ cites(s_{n-1}, s_n)$$

5.2 Chain Completeness¶

Definition 5.3 (Well-Founded Chain). A citation chain is well-founded iff it terminates at a primary source: $$well_founded(chain(s_1, ..., s_n)) \text{ iff } primary(s_n)$$

Axiom 5.1 (Citation Grounding). Every halachic rule should ultimately trace to primary sources: $$∀r: rule(r) → ∃s: makor(r, s) ∧ (primary(s) ∨ ∃s': citation_chain(s, s') ∧ primary(s'))$$

5.3 Example Chain¶

Example 5.1 (Basar Bechalav Chain).

Shemot 23:19 ("lo tevashel gedi bachalev imo")
    ↓ interpreted by
Chullin 113a-116b (Talmudic discussion)
    ↓ codified in
Rambam, Ma'achalot Asurot 9:1
    ↓ incorporated in
Tur, Yoreh Deah 87
    ↓ finalized in
Shulchan Aruch, Yoreh Deah 87:1
    ↓ commented on by
Shach 87:1, Taz 87:1

6. Provenance Graph Formalization¶

6.1 Graph Structure¶

Definition 6.1 (Halachic Provenance Graph). The provenance graph 𝐺_H = ⟨𝑉, 𝐸, τ, μ⟩ where: - 𝑉 = Rules ∪ Sources ∪ Conclusions - 𝐸 = makor_edges ∪ derives_edges ∪ cites_edges - τ: 𝑉 → {rule, source, conclusion} - μ: 𝐸 → {makor, derives, cites}

Definition 6.2 (Edge Types). - makor_edges: Connect rules to their sources - derives_edges: Connect premises to conclusions - cites_edges: Connect sources to earlier sources

6.2 Derivation Trees¶

Definition 6.3 (Derivation Tree). A derivation tree for conclusion 𝑐 is a tree where: - Root: 𝑐 - Internal nodes: Rules that derive 𝑐 - Leaves: Sources (mekorot)

Example 6.1 (Derivation Tree for Forbidden Chicken-Dairy).

forbidden(ashk_mb, achiila, chicken_cheese, ctx_normal)
    │
    ├── r_bb_of_achiila (Of + Chalav forbidden d'rabanan)
    │   ├── makor: sa("yd:87:3")
    │   │   └── cites: gemara("chullin:113a")
    │   │       └── cites: mishnah("chullin:8:1")
    │   │           └── cites: torah("shemot:23:19")
    │   └── madrega: d_rabanan
    │
    └── inherited from: rema → base

6.3 ASP Representation¶

% Derivation provenance
derivation(Conclusion, Rule, World) :-
    derives(World, Conclusion),
    active_in_world(Rule, World),
    rule_concludes(Rule, Conclusion).

% Source chain
source_chain(R, S) :- makor(R, S).
source_chain(R, S2) :-
    makor(R, S1),
    cites(S1, S2).
source_chain(R, S3) :-
    source_chain(R, S2),
    cites(S2, S3).

% Primary source reached
grounded(R) :-
    rule(R),
    source_chain(R, S),
    primary(S).

7. Completeness Theorem¶

7.1 Statement¶

Theorem 7.1 (Provenance Completeness). Every derivable conclusion in Mistaber has a complete provenance chain: $$∀w, c: derives(w, c) → ∃r, s: active_in_world(r, w) ∧ rule_concludes(r, c) ∧ makor(r, s)$$

7.2 Proof¶

Proof. We prove by structural induction on the derivation.

Base case (direct rule application): Let derives(w, c) be derived by a single rule application:

derives(W, Conclusion) :-
    world(W),
    active_in_world(R, W),
    rule_concludes(R, Conclusion),
    rule_conditions_met(R).

By Axiom 3.1, ∃s: makor(R, s). Thus the conclusion has provenance. ✓

Inductive case (inherited conclusion): Let derives(w, c) be inherited from parent world 𝑤': - holds(c, w) via holds(c, w') and accessible(w, w') - By induction, holds(c, w') has provenance in 𝑤' - The inheritance chain itself is traceable

Inductive case (derived from premises): Let derives(w, c) depend on premises 𝑝₁, ..., 𝑝ₙ: - By induction, each 𝑝ᵢ has provenance - The rule 𝑟 deriving 𝑐 from premises has makor(r, s) - Thus 𝑐 has provenance (combining premise provenance with rule source)

In all cases, provenance exists. □

7.3 Consequence¶

Corollary 7.1 (No Unsourced Conclusions). The constraint:

:- rule(R), not has_makor(R).

combined with the derivation semantics ensures no conclusion exists without makor.

8. Implementation Notes¶

8.1 Source Reference Formats¶

Definition 8.1 (Canonical Reference Format). Source references follow standardized formats:

Source Type	Format	Example
Torah	`torah("book:chapter:verse")`	`torah("shemot:23:19")`
Mishnah	`mishnah("tractate:chapter:mishnah")`	`mishnah("chullin:8:1")`
Bavli	`gemara("tractate:daf")`	`gemara("chullin:113a")`
Rambam	`rambam("hilchot:chapter:halacha")`	`rambam("maasurot:9:1")`
SA	`sa("section:siman:seif")`	`sa("yd:87:1")`
Rema	`rema("section:siman:seif")`	`rema("yd:87:3")`
Shach	`shach("section:siman:seif_katan")`	`shach("yd:87:1")`
Taz	`taz("section:siman:seif_katan")`	`taz("yd:87:3")`

8.2 Makor in Rule Definitions¶

File: mistaber/ontology/worlds/mechaber.lp

% Rule with source attribution
rule(r_bb_beheima_achiila).
makor(r_bb_beheima_achiila, sa("yd:87:1")).
madrega(r_bb_beheima_achiila, d_oraita).
scope(r_bb_beheima_achiila, mechaber).

asserts(mechaber, issur(achiila, M, d_oraita)) :-
    is_beheima_chalav_mixture(M).

8.3 Constraint Enforcement¶

File: mistaber/ontology/schema/constraints.lp

% Rules must have at least one makor
:- rule(R), not has_makor(R).
has_makor(R) :- rule(R), makor(R, _).

% Rules must be scoped to a world
:- rule(R), not has_scope(R).
has_scope(R) :- rule(R), scope(R, _).

8.4 Predicate Registry¶

File: mistaber/dsl/vocabulary/base.yaml

predicates:
  - name: makor
    arity: 2
    signature: [rule_id, source_ref]
    hebrew: "מקור"
    english: "Source citation for assertion"
    cwa: true
    mandatory: true
    note: "Every factual claim requires source attribution"

  - name: cites
    arity: 2
    signature: [rule_id, source_ref]
    hebrew: "מצטט"
    english: "Rule cites source"
    cwa: true
    mandatory: true

9. Explanation Generation¶

9.1 Provenance in Explanations¶

When Mistaber generates explanations, provenance is central:

RULING: Eating mixture m1 is FORBIDDEN
World: Ashkenazi (Mishnah Berurah)
Madrega: D'Oraita (Biblical)
Certainty: Vadai (Certain)

DERIVATION:
1. m1 is a mixture of basar and chalav
   ├─ m1 contains chicken (classified as: of → basar)
   └─ m1 contains milk (classified as: chalav)
2. Cooking/eating basar b'chalav is forbidden [SA YD 87:1]
3. Rule inherited: base → rema → ashk_mb

SOURCES:
• Shulchan Aruch, Yoreh Deah 87:1
• Rambam, Hilchot Ma'achalot Asurot 9:1
• Talmud Bavli, Chullin 113a

9.2 Source Chain Query¶

To retrieve the full source chain for a conclusion:

% Query: What are all sources for this conclusion?
?- derives(ashk_mb, forbidden(achiila, m1, ctx_normal)),
   derivation(forbidden(achiila, m1, ctx_normal), R, ashk_mb),
   source_chain(R, S).

The provenance model draws from:

Data provenance in databases (Buneman et al., 2001; Cheney et al., 2009)
Argumentation theory (Dung, 1995; Bench-Capon & Dunne, 2007)
Legal reasoning systems (Gordon & Walton, 2009)
Citation network analysis (Fowler et al., 2007)

Our contribution adapts these frameworks to halachic literature's unique structure of layered commentary and authority gradation.

References¶

Buneman, P., Khanna, S., & Tan, W.C. (2001). Why and Where: A Characterization of Data Provenance. Proceedings of ICDT 2001, 316-330.
Cheney, J., Chiticariu, L., & Tan, W.C. (2009). Provenance in Databases: Why, How, and Where. Foundations and Trends in Databases, 1(4), 379-474.
Dung, P.M. (1995). On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games. Artificial Intelligence, 77(2), 321-357.
Bench-Capon, T.J.M., & Dunne, P.E. (2007). Argumentation in Artificial Intelligence. Artificial Intelligence, 171(10-15), 619-641.
Gordon, T.F., & Walton, D. (2009). Proof Burdens and Standards. In Argumentation in Artificial Intelligence (pp. 239-258). Springer.
Fowler, J.H., Johnson, T.R., Spriggs, J.F., Jeon, S., & Wahlbeck, P.J. (2007). Network Analysis and the Law: Measuring the Legal Importance of Precedents at the US Supreme Court. Political Analysis, 15(3), 324-346.