Modal Logic Foundations for Halachic Reasoning

Abstract

This document establishes the modal logic foundations for the Mistaber system. We present a Kripke semantics adapted for halachic reasoning, where possible worlds represent distinct halachic traditions (shitot) and the accessibility relation encodes authority inheritance. We prove that our accessibility relation forms a strict partial order (irreflexive, transitive, antisymmetric), ensuring the world structure is a directed acyclic graph (DAG). This foundation enables formal reasoning about how rulings propagate through chains of halachic authority while preserving the ability to override inherited positions.

1. Introduction

1.1 Motivation

Halachic discourse exhibits an inherent modal structure. Different halachic authorities (poskim) may reach different conclusions on the same question, yet these conclusions are not arbitrary---they exist within a structured space of tradition and inheritance. The Shulchan Aruch provides a baseline; the Rema glosses represent Ashkenazi tradition; later authorities inherit from and sometimes override their predecessors.

This structure maps naturally to modal logic's possible worlds semantics. Each halachic tradition constitutes a "world" where certain propositions hold. The relationship between traditions---who follows whom, who overrides whom---defines an accessibility relation between worlds.

1.2 Contribution

We provide:

1. A formal Kripke frame ⟨𝑊, 𝑅⟩ for halachic traditions
2. Proofs of the frame's structural properties (irreflexivity, transitivity, antisymmetry)
3. A satisfaction relation adapted for halachic propositions
4. Formal definitions linking modal operators to halachic concepts

2. Preliminaries

2.1 Standard Kripke Semantics

Definition 2.1 (Kripke Frame). A Kripke frame is a pair ⟨𝑊, 𝑅⟩ where: - 𝑊 is a non-empty set of possible worlds - 𝑅 ⊆ 𝑊 × 𝑊 is a binary accessibility relation

Definition 2.2 (Kripke Model). A Kripke model is a triple ⟨𝑊, 𝑅, 𝑉⟩ where: - ⟨𝑊, 𝑅⟩ is a Kripke frame - 𝑉: Prop → 𝒫(𝑊) is a valuation function assigning to each propositional variable the set of worlds where it is true

Definition 2.3 (Satisfaction Relation). The satisfaction relation ⊩ is defined inductively: - 𝑀, 𝑤 ⊩ 𝑝 iff 𝑤 ∈ 𝑉(𝑝) - 𝑀, 𝑤 ⊩ ¬φ iff 𝑀, 𝑤 ⊮ φ - 𝑀, 𝑤 ⊩ φ ∧ ψ iff 𝑀, 𝑤 ⊩ φ and 𝑀, 𝑤 ⊩ ψ - 𝑀, 𝑤 ⊩ □φ iff for all 𝑤' such that 𝑤𝑅𝑤', 𝑀, 𝑤' ⊩ φ - 𝑀, 𝑤 ⊩ ◇φ iff there exists 𝑤' such that 𝑤𝑅𝑤' and 𝑀, 𝑤' ⊩ φ

2.2 Frame Correspondence

The properties of the accessibility relation determine the logic's axioms:

Property	Definition	Corresponding Axiom
Reflexive	∀𝑤: 𝑤𝑅𝑤	T: □φ → φ
Transitive	∀𝑤,𝑤',𝑤'': (𝑤𝑅𝑤' ∧ 𝑤'𝑅𝑤'') → 𝑤𝑅𝑤''	4: □φ → □□φ
Symmetric	∀𝑤,𝑤': 𝑤𝑅𝑤' → 𝑤'𝑅𝑤	B: φ → □◇φ

3. Halachic Kripke Frames

3.1 World Structure

Definition 3.1 (Halachic World). A halachic world 𝑤 ∈ 𝑊 represents a coherent halachic tradition characterized by: - A designated authority or school of thought - A set of normative positions (rulings) - Inheritance relationships to other traditions

In Mistaber, worlds are organized into three tiers:

Tier 1 (Foundation): - base: Common ground from Shulchan Aruch

Tier 2 (Primary Authorities): - mechaber: R' Yosef Karo's rulings (Sefardi tradition) - rema: R' Moshe Isserles' glosses (Ashkenazi tradition) - gra: Vilna Gaon's positions

Tier 3 (Derivative Traditions): - ashk_mb: Ashkenazi following Mishnah Berurah - ashk_ah: Ashkenazi following Aruch HaShulchan - sefardi_yo: Sefardi following Yalkut Yosef

3.2 Accessibility as Inheritance

Definition 3.2 (Halachic Accessibility). For worlds 𝑤, 𝑤' ∈ 𝑊, we define 𝑤𝑅𝑤' (read: "𝑤 is accessible from 𝑤'" or "𝑤 inherits from 𝑤'") iff: - 𝑤 recognizes 𝑤' as a parent authority - Rulings from 𝑤' propagate to 𝑤 unless overridden

Remark. Our accessibility relation is the inverse of the typical temporal reading. If 𝑤𝑅𝑤', then 𝑤' is the parent (earlier authority) and 𝑤 is the child (later tradition). This allows inheritance to flow from parent to child.

Definition 3.3 (World Declaration). In Mistaber, worlds are declared with the world/1 predicate and accessibility with accessible/2:

world(base).
world(mechaber).
world(rema).

accessible(mechaber, base).  % mechaber inherits from base
accessible(rema, base).      % rema inherits from base

3.3 Structural Properties

Theorem 3.1 (Irreflexivity). The halachic accessibility relation 𝑅 is irreflexive: $$∀𝑤 ∈ 𝑊: ¬(𝑤𝑅𝑤)$$

Proof. A world cannot be its own authority source. Self-inheritance would create a logical paradox: a tradition would both define a ruling and inherit that ruling from itself. This is enforced by constraint:

:- accessible(W, W).

The absence of stable models containing accessible(w, w) for any w follows from the integrity constraint. □

Theorem 3.2 (Transitivity of Ancestorship). The transitive closure 𝑅⁺ of 𝑅 defines the ancestor relation: $$∀𝑤₁, 𝑤₂, 𝑤₃ ∈ 𝑊: (𝑤₁𝑅𝑤₂ ∧ 𝑤₂𝑅⁺𝑤₃) → 𝑤₁𝑅⁺𝑤₃$$

Proof. The transitive closure is computed explicitly:

ancestor(W_child, W_parent) :-
    accessible(W_child, W_parent).

ancestor(W1, W3) :-
    accessible(W1, W2),
    ancestor(W2, W3).

By structural induction on derivation length, if ancestor(w₁, w₂) and ancestor(w₂, w₃) are derivable, then ancestor(w₁, w₃) is derivable. □

Theorem 3.3 (Antisymmetry). The accessibility relation 𝑅 is antisymmetric: $$∀𝑤, 𝑤' ∈ 𝑊: (𝑤𝑅𝑤' ∧ 𝑤'𝑅𝑤) → 𝑤 = 𝑤'$$

Proof. We prove the contrapositive: if 𝑤 ≠ 𝑤', then ¬(𝑤𝑅𝑤' ∧ 𝑤'𝑅𝑤).

Suppose for contradiction that 𝑤 ≠ 𝑤' and both 𝑤𝑅𝑤' and 𝑤'𝑅𝑤. Then by transitivity, 𝑤𝑅⁺𝑤. But this contradicts Theorem 3.1 (irreflexivity extends to transitive closure for DAGs). The constraint:

:- accessible(W1, W2), accessible_transitive(W2, W1).

ensures no such pair exists in any stable model. □

Corollary 3.4 (DAG Structure). The halachic world structure ⟨𝑊, 𝑅⟩ forms a directed acyclic graph (DAG).

Proof. Immediate from irreflexivity (Theorem 3.1) and acyclicity via antisymmetry (Theorem 3.3). A cycle 𝑤₀ → 𝑤₁ → ... → 𝑤ₙ → 𝑤₀ would require 𝑤₀𝑅⁺𝑤₀, violating irreflexivity. □

4. Halachic Satisfaction

4.1 Propositions

Definition 4.1 (Halachic Proposition). A halachic proposition is one of: - issur(𝑎, 𝑓, 𝑚): Action 𝑎 on food 𝑓 is forbidden at madrega 𝑚 - heter(𝑎, 𝑓): Action 𝑎 on food 𝑓 is permitted - sakana(𝑓): Food 𝑓 presents health danger - no_sakana(𝑓): Food 𝑓 presents no health danger

4.2 Local Assertion

Definition 4.2 (Assertion). A world 𝑤 asserts proposition φ, written asserts(𝑤, φ), iff φ is a direct ruling of that tradition.

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

4.3 Holding Relation

Definition 4.3 (Holding). A proposition φ holds in world 𝑤, written holds(φ, 𝑤), iff: 1. 𝑤 directly asserts φ, or 2. φ holds in some parent 𝑤' (where 𝑤𝑅𝑤') and is not overridden in 𝑤

holds(Prop, W) :-
    asserts(W, Prop),
    world(W).

holds(Prop, W_child) :-
    accessible(W_child, W_parent),
    holds(Prop, W_parent),
    not overridden(Prop, W_child).

4.4 Override Mechanism

Definition 4.4 (Override). A proposition φ is overridden in world 𝑤 iff 𝑤 explicitly replaces it:

overridden(Prop, W) :-
    override(W, Prop, _).

Example 4.1 (Fish and Dairy). The Mechaber rules that fish with dairy is forbidden due to sakana. The Rema overrides this:

% Mechaber asserts sakana
asserts(mechaber, sakana(M)) :-
    is_dag_chalav_mixture(M).

% Rema overrides
override(rema, sakana(M), no_sakana) :-
    is_dag_chalav_mixture(M).

In rema and its descendants, holds(sakana(M), rema) is false for dag+chalav mixtures.

5. Modal Operators for Halacha

5.1 World-Relativized Operators

Definition 5.1 (World-Relativized Necessity). For world 𝑤: $$□_𝑤 φ \text{ holds iff } φ \text{ holds in } 𝑤 \text{ and all worlds accessible from } 𝑤$$

In the halachic context, □_𝑤 φ means "φ is established throughout tradition 𝑤 and all it inherits from."

Definition 5.2 (World-Relativized Possibility). For world 𝑤: $$◇_𝑤 φ \text{ holds iff } φ \text{ holds in } 𝑤 \text{ or some world accessible from } 𝑤$$

5.2 Cross-World Reasoning

Definition 5.3 (Universal Halachic Truth). A proposition φ is universally held iff: $$∀𝑤 ∈ 𝑊: \text{holds}(φ, 𝑤)$$

Definition 5.4 (Machloket). A machloket (dispute) exists on φ between worlds 𝑤₁ and 𝑤₂ iff: $$\text{holds}(φ, 𝑤₁) ∧ \text{holds}(¬φ, 𝑤₂)$$

6. Implementation Notes

6.1 ASP Encoding

The Kripke semantics is implemented in Answer Set Programming (Clingo):

File: mistaber/ontology/worlds/kripke_rules.lp

% Truth propagation
holds(Prop, W) :-
    asserts(W, Prop),
    world(W).

holds(Prop, W_child) :-
    accessible(W_child, W_parent),
    holds(Prop, W_parent),
    not overridden(Prop, W_child).

% Override mechanism
overridden(Prop, W) :-
    override(W, Prop, _).

% Transitive accessibility
accessible_transitive(W1, W2) :- accessible(W1, W2).
accessible_transitive(W1, W3) :-
    accessible(W1, W2),
    accessible_transitive(W2, W3).

6.2 World Declarations

File: mistaber/ontology/worlds/base.lp

world(base).
safek_policy(base, d_oraita, l_chumra).
safek_policy(base, d_rabanan, l_kula).

6.3 Constraint Enforcement

File: mistaber/ontology/schema/constraints.lp

% Acyclicity constraint
ancestor(W1, W2) :- inherits(W1, W2).
ancestor(W1, W3) :- inherits(W1, W2), ancestor(W2, W3).
:- ancestor(W, W).

7. Related Work

The application of modal logic to normative systems has precedent in legal informatics (Bench-Capon & Coenen, 1992) and religious knowledge representation (Abraham et al., 2011). Our contribution extends this work by:

1. Adapting Kripke semantics specifically for halachic authority hierarchies
2. Formalizing the inheritance-with-override pattern common in halachic discourse
3. Proving structural properties necessary for computational tractability

References

• Hughes, G.E., & Cresswell, M.J. (1996). A New Introduction to Modal Logic. Routledge.
• Kripke, S.A. (1963). Semantical Considerations on Modal Logic. Acta Philosophica Fennica, 16, 83-94.
• Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal Logic. Cambridge University Press.
• Bench-Capon, T.J.M., & Coenen, F.P. (1992). Isomorphism and Legal Knowledge Based Systems. Artificial Intelligence and Law, 1(1), 65-86.
• Abraham, M., Gabbay, D., & Schild, U. (2011). Analysis of the Talmudic Argumentum A Fortiori Inference Rule Using Matrix Abduction. Studia Logica.