Tutorial 3: Understanding Worlds

This tutorial explains Mistaber's multi-world Kripke semantics - the formal foundation that allows modeling different halachic authorities and their relationships.

Learning Objectives

• Understand what "worlds" represent in Mistaber
• Learn the world inheritance hierarchy (DAG)
• Use world-specific queries
• Understand the override mechanism

Prerequisites

• Tutorial 2: Your First Query completed
• Basic understanding of halachic authority structure

Estimated Time

20 minutes

Steps

Step 1: What is a "World"?

In Mistaber, a world represents a coherent halachic perspective - typically the rulings of a particular posek (halachic authority) or tradition.

Think of each world as answering the question: "According to [authority], what is the halacha?"

The seven built-in worlds are:

World	Authority	Tradition
base	Core Shulchan Aruch	Universal foundations
mechaber	R' Yosef Karo	Sefardi (Shulchan Aruch)
rema	R' Moshe Isserles	Ashkenazi (Mapah)
gra	Vilna Gaon	Litvish (Biur HaGra)
sefardi_yo	R' Ovadia Yosef	Contemporary Sefardi
ashk_mb	Chofetz Chaim	Mishnah Berurah
ashk_ah	R' Yechiel Michel Epstein	Aruch Hashulchan

Step 2: The World Hierarchy (DAG)

Worlds form a Directed Acyclic Graph (DAG) where child worlds inherit from parent worlds:

                         base
                        /    \
                 mechaber    rema -------- gra
                    |          |       \    /
               sefardi_yo   ashk_mb   ashk_ah

This hierarchy reflects reality: - base contains universally accepted foundations - mechaber and rema both inherit from base but differ on some rulings - gra provides independent analysis (inherits from base only) - sefardi_yo follows the mechaber - ashk_mb follows the rema - ashk_ah synthesizes both rema and gra (multiple inheritance)

Step 3: Query the World Structure

Let's explore the world structure programmatically:

from pathlib import Path
from mistaber.engine import HsrsEngine

engine = HsrsEngine(Path("mistaber/ontology"))

# List all worlds
worlds = engine.query("world(W)")
print("All worlds:")
for w in worlds:
    print(f"  - {w['W']}")

# Show inheritance relationships
print("\nInheritance (accessible/2):")
accessible = engine.query("accessible(Child, Parent)")
for a in accessible:
    print(f"  {a['Child']} inherits from {a['Parent']}")

Output:

All worlds:
  - base
  - mechaber
  - rema
  - gra
  - sefardi_yo
  - ashk_mb
  - ashk_ah

Inheritance (accessible/2):
  mechaber inherits from base
  rema inherits from base
  gra inherits from base
  sefardi_yo inherits from mechaber
  ashk_mb inherits from rema
  ashk_ah inherits from rema
  ashk_ah inherits from gra

Step 4: Understand holds/2 - Truth in Worlds

The holds(Property, World) predicate indicates that a property is true in a specific world.

Properties can hold in a world in two ways: 1. Direct assertion: The world explicitly declares it via asserts(World, Property) 2. Inheritance: The property holds in an accessible (parent) world

from pathlib import Path
from mistaber.engine import HsrsEngine

engine = HsrsEngine(Path("mistaber/ontology"))

# What does mechaber directly assert?
print("Mechaber directly asserts:")
asserts = engine.query("asserts(mechaber, P)")
for a in asserts[:5]:  # First 5
    print(f"  {a['P']}")

# What holds in mechaber (includes inherited)?
print("\nHolds in mechaber:")
holds = engine.query("holds(P, mechaber)")
# Many results - these include both local and inherited

Step 5: The Override Mechanism

When a child world disagrees with a parent, it uses override/3:

% In rema.lp - Override mechaber's fish+dairy ruling
override(rema, sakana(M), no_sakana) :-
    is_dag_chalav_mixture(M).

This prevents the parent's ruling from being inherited. Let's see this in action:

from pathlib import Path
from mistaber.engine import HsrsEngine

engine = HsrsEngine(Path("mistaber/ontology"))

# Create a fish + dairy scenario
scenario = """
food(salmon).
food(butter).
food_type(salmon, dag).
food_type(butter, chalav).
mixture(fish_butter).
contains(fish_butter, salmon).
contains(fish_butter, butter).
"""

# Check mechaber's view
mechaber_result = engine.analyze(scenario, world="mechaber")
mechaber_atoms = mechaber_result["atoms"]

# Check rema's view
rema_result = engine.analyze(scenario, world="rema")
rema_atoms = rema_result["atoms"]

# Compare
print("Mechaber on fish+dairy:")
for a in mechaber_atoms:
    if "fish_butter" in a and ("sakana" in a or "issur" in a or "heter" in a):
        print(f"  {a}")

print("\nRema on fish+dairy:")
for a in rema_atoms:
    if "fish_butter" in a and ("sakana" in a or "issur" in a or "heter" in a):
        print(f"  {a}")

Expected output:

Mechaber on fish+dairy:
  holds(sakana(fish_butter),mechaber)
  holds(issur(achiila,fish_butter,sakana),mechaber)

Rema on fish+dairy:
  holds(heter(achiila,fish_butter),rema)
  holds(heter(bishul,fish_butter),rema)
  holds(no_sakana(fish_butter),rema)

Step 6: Safek Policies Per World

Worlds can have different policies for handling doubt (safek):

from pathlib import Path
from mistaber.engine import HsrsEngine

engine = HsrsEngine(Path("mistaber/ontology"))

# Query safek policies
policies = engine.query("safek_policy(World, Level, Resolution)")
print("Safek policies by world:")
for p in policies:
    print(f"  {p['World']}: {p['Level']} -> {p['Resolution']}")

Output:

Safek policies by world:
  base: d_oraita -> l_chumra
  base: d_rabanan -> l_kula
  ashk_mb: d_oraita -> l_chumra
  ashk_mb: d_rabanan -> l_chumra    # MB is stricter!
  ashk_ah: d_oraita -> l_chumra
  ashk_ah: d_rabanan -> l_kula      # AH follows standard

The key difference: - Mishnah Berurah (ashk_mb): Treats safek d'rabanan strictly (l_chumra) - Aruch Hashulchan (ashk_ah): Treats safek d'rabanan leniently (l_kula)

Step 7: Compare Rulings Across All Worlds

Use the compare method to see how all worlds rule on an issue:

from pathlib import Path
from mistaber.engine import HsrsEngine

engine = HsrsEngine(Path("mistaber/ontology"))

# Compare fish+dairy ruling across all Tier 2 worlds
comparison = engine.compare(
    "holds(sakana(fish_dairy_mix), W)",
    worlds=["mechaber", "rema", "gra"]
)

print("Fish+dairy sakana ruling:")
for world, results in comparison.items():
    has_sakana = len(results) > 0
    print(f"  {world}: {'sakana' if has_sakana else 'no sakana'}")

Step 8: Minhag Regions

Each world is associated with a geographic tradition:

from pathlib import Path
from mistaber.engine import HsrsEngine

engine = HsrsEngine(Path("mistaber/ontology"))

regions = engine.query("minhag_region(World, Region)")
print("World minhag regions:")
for r in regions:
    print(f"  {r['World']}: {r['Region']}")

Output:

World minhag regions:
  rema: ashkenaz
  gra: ashkenaz_litvish
  ashk_mb: ashkenaz_litvish
  ashk_ah: ashkenaz_russian
  sefardi_yo: sefardi_edot_hamizrach

The Kripke Rules

The inheritance mechanism is implemented in 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).

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

This simple set of rules implements: 1. Local truth: What a world asserts, holds in that world 2. Inheritance: What holds in a parent also holds in children 3. Override: Children can block inheritance with explicit override

Exercises

Exercise 1: Trace Inheritance

For ashk_mb, trace back all ancestors. What do they inherit from each world?

Solution

engine = HsrsEngine(Path("mistaber/ontology"))

# ashk_mb -> rema -> base
print("ashk_mb accessibility chain:")
accessible = engine.query("accessible_transitive(ashk_mb, Ancestor)")
for a in accessible:
    print(f"  ashk_mb can access: {a['Ancestor']}")

Result: `ashk_mb` -> `rema` -> `base`

Exercise 2: Find All Machloket

Query for mixtures where mechaber and rema disagree:

Solution

engine = HsrsEngine(Path("mistaber/ontology"))

machloket = engine.query("machloket(Topic, mechaber, rema, Item)")
print("Disputes between Mechaber and Rema:")
for m in machloket:
    print(f"  Topic: {m['Topic']}, Item: {m['Item']}")

Exercise 3: Create a Custom Scenario

Create a scenario where the difference between ashk_mb and ashk_ah safek policies matters.

Hint

Create a scenario with unknown food type, which triggers safek. The two worlds handle safek d'rabanan differently.

What You've Learned

• Worlds represent coherent halachic perspectives
• The world hierarchy forms a DAG with inheritance
• holds(P, W) means property P is true in world W
• override/3 prevents inheritance of specific properties
• Different worlds can have different safek policies
• The Kripke rules implement inheritance and override

Next Steps

Continue to Tutorial 4: Writing Rules to learn how to author your own halachic rules.

Quick Reference

# Query all worlds
engine.query("world(W)")

# Query inheritance
engine.query("accessible(Child, Parent)")

# Query what holds in a specific world
engine.query("holds(P, mechaber)")

# Query direct assertions
engine.query("asserts(mechaber, P)")

# Query overrides
engine.query("override(W, Prop, Reason)")

# Query safek policies
engine.query("safek_policy(W, Level, Resolution)")