Kripke Implementation

This document describes how Mistaber implements Kripke semantics for multi-world halachic reasoning, enabling representation of different halachic authorities as "possible worlds" with inheritance and override mechanisms.

Overview

Kripke semantics provides the formal framework for: - Representing multiple halachic authorities (Mechaber, Rema, GRA, etc.) - Modeling inheritance relationships between authorities - Handling disputes (machloket) through world comparison - Supporting diamond inheritance patterns - Enabling psak (ruling) derivation based on user's tradition

World Declaration in ASP

Each halachic authority is declared as a world in ASP:

% mistaber/ontology/worlds/base.lp
world(base).

% mistaber/ontology/worlds/mechaber.lp
world(mechaber).
accessible(mechaber, base).

% mistaber/ontology/worlds/rema.lp
world(rema).
accessible(rema, base).

World Declaration Pattern

% 1. Declare the world exists
world(world_name).

% 2. Declare accessibility (inheritance) from parent(s)
accessible(world_name, parent_world).

% 3. Optionally declare safek policies
safek_policy(world_name, d_oraita, l_chumra).
safek_policy(world_name, d_rabanan, l_kula).

% 4. Include corpus files if needed
#include "../corpus/yd_87/base.lp".

The 7 Worlds and Their Relationships

Mistaber includes seven halachic worlds organized in a DAG:

World Hierarchy

                         base
                        /    \
                 mechaber    rema ←──────── gra
                    │          │              │
              sefardi_yo   ashk_mb        ashk_ah
                                    (multiple inheritance)

World Descriptions

World	Authority	Tradition	Parent(s)
base	Shulchan Aruch foundations	Universal	None (root)
mechaber	R' Yosef Karo	Sefardi	base
rema	R' Moshe Isserles	Ashkenazi	base
gra	Vilna Gaon	Litvish	base
sefardi_yo	Yalkut Yosef	Sefardi modern	mechaber
ashk_mb	Mishnah Berurah	Litvish/Ashkenazi	rema
ashk_ah	Aruch Hashulchan	Russian Ashkenazi	rema, gra

Diamond Inheritance: ashk_ah

The ashk_ah world demonstrates multiple inheritance:

% mistaber/ontology/worlds/ashk_ah.lp
world(ashk_ah).

% ashk_ah inherits from BOTH rema AND gra
accessible(ashk_ah, rema).
accessible(ashk_ah, gra).

This models how R' Yechiel Michel Epstein synthesized both traditions.

Accessibility Relation (accessible/2)

The accessible/2 predicate defines inheritance relationships:

accessible(Child, Parent).

Meaning: World Child can "see" (inherit from) world Parent.

Frame Properties

The accessibility relation has these properties:

Property	Definition	In Mistaber
Irreflexive	No accessible(W, W)	Yes - worlds don't inherit from themselves
Transitive	If A→B and B→C then A→C	Yes - via ancestor/2
Antisymmetric	If A→B then not B→A	Yes - enforced by DAG validation

Transitive Closure

The ancestor/2 predicate computes transitive inheritance:

% mistaber/engine/priorities.lp

% Direct parent is ancestor
ancestor(W_child, W_parent) :-
    world(W_child),
    world(W_parent),
    accessible(W_child, W_parent).

% Transitive closure: grandparent and beyond
ancestor(W1, W3) :-
    world(W1),
    world(W3),
    accessible(W1, W2),
    ancestor(W2, W3).

Truth Propagation (holds/2)

The core of Kripke semantics is truth propagation via holds/2:

% mistaber/ontology/worlds/kripke_rules.lp

% Local assertions hold in their world
holds(Prop, W) :-
    asserts(W, Prop),
    world(W).

% Inherit from accessible (parent) worlds
holds(Prop, W_child) :-
    accessible(W_child, W_parent),
    holds(Prop, W_parent),
    not overridden(Prop, W_child).

How Truth Flows

1. Local Assertion: If asserts(W, Prop), then holds(Prop, W)
2. Inheritance: If holds(Prop, Parent) and accessible(Child, Parent), then holds(Prop, Child) unless overridden
3. Override: If override(W, Prop, _), then inheritance is blocked

Rule Scoping (scope/2, active_in_world/2)

Rules are scoped to specific worlds:

% Rule declaration with scope
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).

Rule Activation

% mistaber/engine/priorities.lp

% A rule is active in a world if directly scoped to that world
active_in_world(R, W) :-
    rule(R),
    world(W),
    scope(R, W),
    not overridden_in(R, W).

% A rule is active in a world if scoped to an ancestor and not overridden
active_in_world(R, W) :-
    rule(R),
    world(W),
    scope(R, W_ancestor),
    ancestor(W, W_ancestor),
    not overridden_in(R, W).

Override Mechanism

override/3 Declaration

Child worlds can override parent propositions:

% mistaber/ontology/worlds/rema.lp

% Override the Mechaber's sakana ruling for fish + dairy
override(rema, sakana(M), no_sakana) :-
    is_dag_chalav_mixture(M).

override(rema, issur(achiila, M, sakana), permitted) :-
    is_dag_chalav_mixture(M).

overrides/4 for Rules

% Declare that R_child overrides R_parent in world W
overrides(R_child, R_parent, W, Override_type).

% Override types:
% - always: unconditional override
% - condition(C): override only when C holds

Override Logic

% mistaber/engine/priorities.lp

% A rule is overridden if another rule overrides it
overridden_in(R, W) :-
    rule(R),
    world(W),
    overrides(R_child, R, W, Override_type),
    active_override(R_child, R, W, Override_type).

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

Diamond Inheritance Handling

When a world inherits from multiple parents with conflicting positions, explicit priority resolution is required:

Conflict Detection

% mistaber/engine/priorities.lp

% Detect conflict: world inherits conflicting positions
conflict(W, topic(Topic)) :-
    world(W),
    world(W1),
    world(W2),
    accessible(W, W1),
    accessible(W, W2),
    W1 != W2,
    active_in_world(R1, W1),
    active_in_world(R2, W2),
    rule_concludes(R1, position(Topic, Val1)),
    rule_concludes(R2, position(Topic, Val2)),
    Val1 != Val2,
    not priority(W1, W2, W),
    not priority(W2, W1, W).

Conflict Resolution via priority/3

% Declare that W1 takes precedence over W2 in child world W
priority(W1, W2, W).

% Resolution determines the winning rule
priority_winner(R, W) :-
    world(W),
    world(W_preferred),
    world(W_less),
    accessible(W, W_preferred),
    accessible(W, W_less),
    priority(W_preferred, W_less, W),
    active_in_world(R, W_preferred),
    rule_concludes(R, position(Topic, _)),
    active_in_world(R2, W_less),
    rule_concludes(R2, position(Topic, _)),
    R != R2.

Interpretation Layer

Commentators (Shach, Taz, etc.) are NOT separate worlds. They are interpretation functions that modify rule conditions WITHIN a world:

% mistaber/engine/interpretations.lp

% Commentator declarations
commentator(shach).        % Sifsei Kohen
commentator(taz).          % Turei Zahav
commentator(pri_megadim).  % R' Yosef Teomim
commentator(pri_chadash).  % R' Chizkiyah da Silva

% Who interprets whom
interprets(shach, mechaber).
interprets(taz, mechaber).
interprets(pri_megadim, shach).
interprets(pri_megadim, taz).
interprets(pri_chadash, mechaber).

Interpretation Types

% Type 1: Adds a condition to a rule
interpretation(Comm, Rule, adds_condition(Cond)) :-
    adds_condition(Comm, Rule, Cond).

% Type 2: Removes/relaxes a condition
interpretation(Comm, Rule, removes_condition(Cond)) :-
    removes_condition(Comm, Rule, Cond).

% Type 3: Restricts scope
interpretation(Comm, Rule, restricts_to(Scope)) :-
    restricts_scope(Comm, Rule, Scope).

% Type 4: Expands scope
interpretation(Comm, Rule, expands_to(Scope)) :-
    expands_scope(Comm, Rule, Scope).

Interpretation Precedence

% Default precedence (higher number = wins in conflict)
interpretation_precedence(mechaber, taz, 1).
interpretation_precedence(mechaber, shach, 2).
interpretation_precedence(mechaber, pri_chadash, 3).

% Override precedence from config if provided
effective_precedence(Authority, Comm, Prec) :-
    config_interp_precedence(Comm, Prec),
    interprets(Comm, Authority).

File Organization

mistaber/ontology/worlds/
├── base.lp           # Root world - common halachic ground
├── mechaber.lp       # Sefardi tradition (Shulchan Aruch author)
├── rema.lp           # Ashkenazi glosses (disagreements marked)
├── gra.lp            # Vilna Gaon (independent Tier 2)
├── ashk_mb.lp        # Mishnah Berurah (Litvish)
├── ashk_ah.lp        # Aruch Hashulchan (multiple inheritance)
├── sefardi_yo.lp     # Yalkut Yosef (follows Mechaber)
└── kripke_rules.lp   # Truth propagation and override logic

mistaber/engine/
├── priorities.lp     # Rule activation, override, conflict resolution
├── interpretations.lp # Commentator interpretation layer
├── safek.lp          # Safek propagation with world awareness
├── preferences.lp    # asprin preference specification
└── kripke/           # Python support for world management
    ├── validation.py # DAG cycle detection
    └── worlds.py     # WorldManager class

Python Support

WorldManager

# mistaber/engine/kripke/worlds.py

class WorldManager:
    """Manages the world DAG for Kripke semantics."""

    def add_world(
        self,
        name: str,
        parent: Optional[str] = None,
        parents: Optional[List[str]] = None
    ) -> None:
        """Add a world to the DAG."""

    def get_parents(self, world: str) -> List[str]:
        """Get direct parents of a world."""

    def get_ancestors(self, world: str) -> List[str]:
        """Get all ancestors in BFS order."""

    def set_actual_world(self, world: str) -> None:
        """Set the designated actual world."""

WorldDAGValidator

# mistaber/engine/kripke/validation.py

class WorldDAGValidator:
    """Validates that world accessibility forms a DAG."""

    def validate(self, edges: List[Tuple[str, Optional[str]]]) -> bool:
        """
        Validate edges form a DAG.
        Uses DFS with white/gray/black coloring.
        Raises CyclicWorldError if cycle detected.
        """

Example: Fish + Dairy Machloket

The fish + dairy case demonstrates world-based machloket handling:

Mechaber's Position (sakana)

% mistaber/ontology/worlds/mechaber.lp

rule(r_bb_dag_sakana).
makor(r_bb_dag_sakana, sa("yd:87:3")).
makor(r_bb_dag_sakana, beit_yosef("yd:87")).
scope(r_bb_dag_sakana, mechaber).

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

asserts(mechaber, issur(achiila, M, sakana)) :-
    is_dag_chalav_mixture(M).

Rema's Position (no sakana)

% mistaber/ontology/worlds/rema.lp

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")).
scope(r_rema_dag_chalav_mutar, rema).

% Override the sakana ruling
override(rema, sakana(M), no_sakana) :-
    is_dag_chalav_mixture(M).

override(rema, issur(achiila, M, sakana), permitted) :-
    is_dag_chalav_mixture(M).

% Explicit permission
asserts(rema, heter(achiila, M)) :-
    is_dag_chalav_mixture(M).

asserts(rema, no_sakana(M)) :-
    is_dag_chalav_mixture(M).

% Mark as machloket
machloket(dag_chalav, mechaber, rema, M) :-
    is_dag_chalav_mixture(M).

Query Results

# Compare across worlds
results = engine.compare(
    pattern="holds(issur(achiila, M, Reason), W)",
    worlds=["mechaber", "rema"]
)

# mechaber: [{"M": "fish_cream", "Reason": "sakana"}]
# rema: []  (no issur - permitted)

Safek Handling by World

Each world can define its own safek policy:

% Base default
safek_policy(base, d_oraita, l_chumra).   % Biblical → stringent
safek_policy(base, d_rabanan, l_kula).    % Rabbinic → lenient

% Mishnah Berurah is stricter
safek_policy(ashk_mb, d_oraita, l_chumra).
safek_policy(ashk_mb, d_rabanan, l_chumra).  % Stricter than default

% Aruch Hashulchan follows standard
safek_policy(ashk_ah, d_oraita, l_chumra).
safek_policy(ashk_ah, d_rabanan, l_kula).    % More lenient than MB

Show Directives

Key predicates are shown for debugging:

#show world/1.
#show accessible/2.
#show ancestor/2.
#show holds/2.
#show asserts/2.
#show override/3.
#show overridden/2.
#show active_in_world/2.
#show overridden_in/2.
#show conflict/2.
#show priority_winner/2.
#show machloket/4.