Safek Calculus: Formal Uncertainty Handling¶

Abstract¶

We present a novel formal calculus for handling safek (uncertainty) in halachic reasoning. The calculus operates under Open World Assumption (OWA) for factual predicates while maintaining Closed World Assumption (CWA) for derived prohibitions. We formalize the classical principles of "safek d'oraita l'chumra" (Biblical doubt resolved stringently) and "safek d'rabanan l'kula" (Rabbinic doubt resolved leniently), and extend them with a treatment of sfek sfeika (compound doubt). Our key contribution is a three-layer propagation model that handles unknown predicates, safek marking, and resolution based on madrega and policy. We prove soundness of the resolution procedure and establish termination guarantees.

1. Introduction¶

1.1 The Problem of Uncertainty¶

Halachic reasoning must handle two fundamental types of uncertainty:

Safek b'Metzius (Factual Doubt): Uncertainty about physical facts
"Is this meat from a kosher animal?"
"Was the food cooked at yad soledet bo (scalding temperature)?"
Safek b'Din (Legal Doubt): Uncertainty about the applicable rule
"Does this case fall under the prohibition?"
"Which authority's opinion applies?"

Standard logic programming under CWA cannot adequately model these cases: absence of a fact implies its negation, precluding genuine uncertainty.

1.2 Classical Halachic Principles¶

The halachic tradition has developed sophisticated meta-rules for uncertainty:

Principle	Hebrew	Application
Safek d'oraita l'chumra	ספק דאורייתא לחומרא	Biblical doubt → stringent
Safek d'rabanan l'kula	ספק דרבנן לקולא	Rabbinic doubt → lenient
Sfek sfeika l'kula	ספק ספיקא לקולא	Compound doubt → lenient

1.3 Contribution¶

We provide:

A formal calculus for safek propagation compatible with ASP
OWA markers for unknown predicates
Three-layer resolution model (policy → marking → propagation)
Sfek sfeika (compound doubt) handling with independence requirements
Soundness and termination proofs

2. Preliminaries¶

2.1 Open World Semantics¶

Definition 2.1 (Three-Valued Interpretation). An interpretation 𝐼 assigns to each ground atom one of: - True (𝐼 ⊨ A): Explicitly derived - False (𝐼 ⊨ ¬A): Derived under CWA (for CWA predicates) - Unknown (𝐼 ⊨ ?A): Neither true nor false

Definition 2.2 (CWA Predicate). Predicate P is under CWA iff: $$¬P(x) \text{ derivable iff } P(x) \text{ not derivable}$$

Definition 2.3 (OWA Predicate). Predicate P is under OWA iff: $$\text{If neither } P(x) \text{ nor } ¬P(x) \text{ is derivable, then } ?P(x)$$

2.2 Madrega and Policy¶

Definition 2.4 (Madrega). The normative level 𝑚 ∈ {d_oraita, d_rabanan, minhag, chumra}.

Definition 2.5 (Safek Policy). A policy π(w, m) specifies resolution for world w and madrega m: $$π(w, m) ∈ {l_chumra, l_kula}$$

Default policies: $$π_{default}(w, d_oraita) = l_chumra$$ $$π_{default}(w, d_rabanan) = l_kula$$

3. The Safek Calculus¶

3.1 Syntax¶

Definition 3.1 (Safek Language). The safek calculus extends the base language with: - unknown(attr, x): Attribute attr of entity x is unknown - safek(status, w, act, f, ctx): Doubt about status in world w for action act on food f in context ctx - safek_resolved(w, act, f, ctx): The safek has been resolved - sfek_sfeika(w, act, f, ctx): Compound doubt (two independent doubts)

3.2 Unknown Markers¶

Definition 3.2 (Unknown Predicate). For OWA predicate P and entity x: $$unknown(P, x) \text{ iff } food(x) ∧ ¬known_P(x)$$

where known_P(x) is a helper predicate that fires when P is explicitly declared.

Example 3.1 (Unknown Food Type).

unknown(food_type, F) :-
    food(F),
    not known_food_type(F).

known_food_type(F) :- food_type(F, _).

3.3 Safek Propagation Rules¶

Rule 3.1 (Direct Safek). Unknown attribute affecting potential prohibition: $$\frac{unknown(attr, f) \quad potentially_forbidden(w, act, f, ctx)}{safek(forbidden, w, act, f, ctx)}$$

Rule 3.2 (Mixture Safek). Unknown component affecting mixture: $$\frac{contains(m, f) \quad unknown(attr, f) \quad potentially_forbidden_mixture(w, act, m, ctx)}{safek(forbidden, w, act, m, ctx)}$$

Rule 3.3 (Transitive Safek). Safek propagates through derivations: $$\frac{safek(forbidden, w, act, f_{source}, ctx) \quad derives_from_safek(w, act, f_{derived}, ctx, f_{source})}{safek(forbidden, w, act, f_{derived}, ctx)}$$

3.4 ASP Implementation¶

File: mistaber/engine/safek.lp

% Unknown markers
unknown(food_type, F) :-
    food(F),
    not known_food_type(F).

known_food_type(F) :- food_type(F, _).

% Safek from unknown food_type
safek(forbidden, W, Act, F, Ctx) :-
    world(W),
    food(F),
    unknown(food_type, F),
    potentially_forbidden(W, Act, F, Ctx).

% Safek from unknown temperature
safek(forbidden, W, Act, F, Ctx) :-
    world(W),
    food(F),
    unknown(temperature, F),
    potentially_forbidden_temperature(W, Act, F, Ctx).

% Safek from unknown mixture contents
safek(forbidden, W, Act, M, Ctx) :-
    world(W),
    mixture(M),
    unknown(contains, M),
    potentially_forbidden_mixture(W, Act, M, Ctx).

4. Safek Resolution¶

4.1 Resolution Based on Madrega¶

Definition 4.1 (Madrega-Based Resolution). Resolution depends on the normative level of the potential prohibition:

$$\frac{safek(forbidden, w, act, f, ctx) \quad madrega_of_safek(w, act, f, ctx, m) \quad π(w, m) = l_kula}{safek_resolved(w, act, f, ctx)}$$

$$\frac{safek(forbidden, w, act, f, ctx) \quad madrega_of_safek(w, act, f, ctx, m) \quad π(w, m) = l_chumra}{derives(w, forbidden(act, f, ctx))}$$

Theorem 4.1 (Resolution Completeness). Every safek is either: 1. Resolved leniently (safek_resolved) 2. Resolved stringently (derives forbidden) 3. Remains unresolved (explicitly marked)

Proof. Given safek(forbidden, w, act, f, ctx): - If madrega_of_safek is determined (d_oraita or d_rabanan): - Policy π(w, m) applies - Either l_kula (case 1) or l_chumra (case 2) - If madrega is undetermined: - Default madrega applies (d_rabanan) - Case 1 or 2 follows

If neither resolution fires, unresolved_safek/4 is derived (case 3). □

4.2 Default Madrega¶

Rule 4.1 (Default Madrega Assignment). $$\frac{safek(forbidden, w, act, f, ctx) \quad ¬explicit_madrega_of_safek(w, act, f, ctx)}{madrega_of_safek(w, act, f, ctx, d_rabanan)}$$

Rationale: Unspecified doubts are presumed rabbinic (less severe).

4.3 ASP Implementation¶

% Resolve safek d'rabanan leniently
safek_resolved(W, Act, F, Ctx) :-
    safek(forbidden, W, Act, F, Ctx),
    policy(W, safek_issur, lenient),
    madrega_of_safek(W, Act, F, Ctx, d_rabanan).

% Resolve safek d'oraita strictly
derives(W, forbidden(Act, F, Ctx)) :-
    safek(forbidden, W, Act, F, Ctx),
    policy(W, safek_issur, strict),
    madrega_of_safek(W, Act, F, Ctx, d_oraita).

% Default madrega
madrega_of_safek(W, Act, F, Ctx, d_rabanan) :-
    safek(forbidden, W, Act, F, Ctx),
    not explicit_madrega_of_safek(W, Act, F, Ctx).

5. Constraint: No Permitted from Absence with Safek¶

5.1 The Core Invariant¶

Axiom 5.1 (OWA Constraint). A food cannot be derived as permitted when unresolved safek exists: $$¬(derives(w, permitted(act, f, ctx)) ∧ safek(forbidden, w, act, f, ctx) ∧ ¬safek_resolved(w, act, f, ctx))$$

Theorem 5.1 (OWA Correctness). Under this constraint, the absence of issur with unresolved safek does not yield permission.

Proof. The integrity constraint:

:- derives(W, permitted(Act, F, Ctx)),
   safek(forbidden, W, Act, F, Ctx),
   not safek_resolved(W, Act, F, Ctx).

eliminates any stable model where permission coexists with unresolved safek. Permission requires either: - No safek exists (CWA derivation) - Safek is resolved leniently

This prevents false permission from mere absence. □

6. Sfek Sfeika (Compound Doubt)¶

6.1 Definition¶

Definition 6.1 (Sfek Sfeika). A sfek sfeika (double doubt) exists when two independent doubts combine: $$sfek_sfeika(w, act, f, ctx) \text{ iff }$$ $$\quad safek(forbidden, w, act, f, ctx) ∧ independent_doubt_count(w, act, f, ctx, n) ∧ n ≥ 2$$

Definition 6.2 (Independent Doubts). Two doubts are independent if the resolution of one does not determine the other.

6.2 Counting Independent Doubts¶

Definition 6.3 (Doubt Reason). Each doubt has a reason: $$doubt_reason(w, act, f, ctx, reason)$$

The count of independent doubts: $$independent_doubt_count(w, act, f, ctx, n) = |{r : doubt_reason(w, act, f, ctx, r)}|$$

6.3 Sfek Sfeika Resolution¶

Rule 6.1 (Sfek Sfeika L'Kula). $$\frac{sfek_sfeika(w, act, f, ctx) \quad ¬sfek_sfeika_strict(w)}{safek_resolved(w, act, f, ctx)}$$

Rationale: The Talmudic principle holds that compound independent doubts resolve leniently, even for Biblical prohibitions.

6.4 ASP Implementation¶

% Sfek sfeika detection
sfek_sfeika(W, Act, F, Ctx) :-
    safek(forbidden, W, Act, F, Ctx),
    independent_doubt_count(W, Act, F, Ctx, N),
    N >= 2.

% Count independent doubts
independent_doubt_count(W, Act, F, Ctx, N) :-
    world(W),
    safek(forbidden, W, Act, F, Ctx),
    N = #count { Reason : doubt_reason(W, Act, F, Ctx, Reason) }.

% Sfek sfeika resolved leniently
safek_resolved(W, Act, F, Ctx) :-
    sfek_sfeika(W, Act, F, Ctx),
    not sfek_sfeika_strict(W).

6.5 Example: Sfek Sfeika¶

Scenario: A mixture of unknown contents may or may not contain meat, and if it does, it may or may not have been cooked with dairy.

Doubts: 1. doubt_reason(w, eat, m, ctx, "contents_unknown"): Does it contain meat? 2. doubt_reason(w, eat, m, ctx, "cooking_unknown"): Was it cooked with dairy?

Analysis: - Two independent doubts exist - sfek_sfeika(w, eat, m, ctx) is derived - Unless sfek_sfeika_strict(w), the safek is resolved leniently

7. Safek Strength Hierarchy¶

7.1 Madrega Comparison¶

Definition 7.1 (Safek Strength). For a safek with multiple possible madregot: $$safek_stronger(w, act, f, ctx, m_1, m_2) \text{ iff }$$ $$\quad safek(forbidden, w, act, f, ctx) ∧ madrega_of_safek(w, act, f, ctx, m_1) ∧ stronger(m_1, m_2)$$

Definition 7.2 (Effective Madrega). The effective madrega is the strongest applicable: $$effective_madrega_of_safek(w, act, f, ctx, d_oraita) \text{ iff } madrega_of_safek(w, act, f, ctx, d_oraita)$$

$$effective_madrega_of_safek(w, act, f, ctx, d_rabanan) \text{ iff }$$ $$\quad madrega_of_safek(w, act, f, ctx, d_rabanan) ∧ ¬madrega_of_safek(w, act, f, ctx, d_oraita)$$

7.2 ASP Implementation¶

% Safek d'oraita is stronger
safek_stronger(W, Act, F, Ctx, d_oraita, d_rabanan) :-
    safek(forbidden, W, Act, F, Ctx),
    madrega_of_safek(W, Act, F, Ctx, d_oraita).

% Effective madrega
effective_madrega_of_safek(W, Act, F, Ctx, d_oraita) :-
    safek(forbidden, W, Act, F, Ctx),
    madrega_of_safek(W, Act, F, Ctx, d_oraita).

effective_madrega_of_safek(W, Act, F, Ctx, d_rabanan) :-
    safek(forbidden, W, Act, F, Ctx),
    madrega_of_safek(W, Act, F, Ctx, d_rabanan),
    not madrega_of_safek(W, Act, F, Ctx, d_oraita).

8. Formal Properties¶

8.1 Soundness¶

Theorem 8.1 (Soundness of Safek Resolution). The safek calculus correctly implements the halachic meta-rules:

Safek d'oraita l'chumra: Biblical doubt → forbidden
Safek d'rabanan l'kula: Rabbinic doubt → resolved (permitted)
Sfek sfeika l'kula: Compound doubt → resolved (permitted)

Proof. By case analysis on the resolution rules:

Case 1 (D'oraita): - safek(forbidden, w, act, f, ctx) holds - madrega_of_safek(w, act, f, ctx, d_oraita) holds - Policy π(w, d_oraita) = l_chumra (default or configured) - Resolution: derives(w, forbidden(act, f, ctx)) - Matches halachic principle ✓

Case 2 (D'rabanan): - safek(forbidden, w, act, f, ctx) holds - madrega_of_safek(w, act, f, ctx, d_rabanan) holds - Policy π(w, d_rabanan) = l_kula (default or configured) - Resolution: safek_resolved(w, act, f, ctx) - Matches halachic principle ✓

Case 3 (Sfek Sfeika): - sfek_sfeika(w, act, f, ctx) holds (≥2 independent doubts) - Unless sfek_sfeika_strict(w) (rare exception) - Resolution: safek_resolved(w, act, f, ctx) - Matches halachic principle ✓ □

8.2 Termination¶

Theorem 8.2 (Termination). The safek calculus terminates on finite inputs.

Proof. The calculus is stratified: 1. Layer 1: unknown/2 - derived from base facts (finite) 2. Layer 2: safek/5 - derived from unknown and potentially_forbidden (finite product) 3. Layer 3: doubt_reason/5 - explicitly declared (finite) 4. Layer 4: sfek_sfeika/4 - aggregate over finite doubt_reasons 5. Layer 5: Resolution - single derivation per safek

Each layer depends only on lower layers or finite base facts. With finite input, all layers are finite. □

8.3 Consistency¶

Theorem 8.3 (No Forbidden-Permitted Conflict). For any world w, action a, food f, context c: $$¬(derives(w, forbidden(a, f, c)) ∧ derives(w, permitted(a, f, c)))$$

Proof. The disjointness constraint (Section 5.1) prevents this directly. Any model containing both would satisfy:

:- derives(W, permitted(Act, F, Ctx)),
   safek(forbidden, W, Act, F, Ctx),
   not safek_resolved(W, Act, F, Ctx).

For non-safek cases, the ontology constraint:

:- forbidden(W, A, F, C), permitted(W, A, F, C).

applies. In both cases, contradictory models are eliminated. □

9. Three-Layer Model Summary¶

9.1 Layer 1: World-Level Policy¶

Configured per world, inherited through the world DAG:

safek_policy(base, d_oraita, l_chumra).
safek_policy(base, d_rabanan, l_kula).
safek_policy(ashk_mb, d_rabanan, l_chumra).  % More stringent tradition

9.2 Layer 2: Rule-Level Marking¶

Individual rules/facts are marked with uncertainty status:

safek_status(fact_id, safek).
safek_reason(fact_id, "eid_echad").  % Single witness testimony
safek_madrega(r_basar_bechalav, d_oraita).

9.3 Layer 3: Propagation¶

Uncertainty flows through derivations:

safek(forbidden, W, Act, F_derived, Ctx) :-
    safek(forbidden, W, Act, F_source, Ctx),
    derives_from_safek(W, Act, F_derived, Ctx, F_source).

10. Implementation Notes¶

10.1 Complete Safek Module¶

File: mistaber/engine/safek.lp

% ============================================================
% EXPLICIT UNKNOWN MARKERS
% ============================================================

unknown(food_type, F) :- food(F), not known_food_type(F).
known_food_type(F) :- food_type(F, _).

unknown(contains, M) :- mixture(M), not known_contains(M).
known_contains(M) :- contains(M, _).

unknown(temperature, F) :- food(F), not known_temperature(F).
known_temperature(F) :- temperature(F, _).

% ============================================================
% SAFEK PROPAGATION
% ============================================================

safek(forbidden, W, Act, F, Ctx) :-
    world(W), food(F),
    unknown(food_type, F),
    potentially_forbidden(W, Act, F, Ctx).

safek(forbidden, W, Act, M, Ctx) :-
    world(W), mixture(M),
    contains(M, F), unknown(food_type, F),
    potentially_forbidden_mixture(W, Act, M, Ctx).

% ============================================================
% SAFEK RESOLUTION
% ============================================================

safek_resolved(W, Act, F, Ctx) :-
    safek(forbidden, W, Act, F, Ctx),
    policy(W, safek_issur, lenient),
    madrega_of_safek(W, Act, F, Ctx, d_rabanan).

derives(W, forbidden(Act, F, Ctx)) :-
    safek(forbidden, W, Act, F, Ctx),
    policy(W, safek_issur, strict),
    madrega_of_safek(W, Act, F, Ctx, d_oraita).

madrega_of_safek(W, Act, F, Ctx, d_rabanan) :-
    safek(forbidden, W, Act, F, Ctx),
    not explicit_madrega_of_safek(W, Act, F, Ctx).

% ============================================================
% OWA CONSTRAINT
% ============================================================

:- derives(W, permitted(Act, F, Ctx)),
   safek(forbidden, W, Act, F, Ctx),
   not safek_resolved(W, Act, F, Ctx).

% ============================================================
% SFEK SFEIKA
% ============================================================

sfek_sfeika(W, Act, F, Ctx) :-
    safek(forbidden, W, Act, F, Ctx),
    independent_doubt_count(W, Act, F, Ctx, N),
    N >= 2.

independent_doubt_count(W, Act, F, Ctx, N) :-
    world(W),
    safek(forbidden, W, Act, F, Ctx),
    N = #count { Reason : doubt_reason(W, Act, F, Ctx, Reason) }.

safek_resolved(W, Act, F, Ctx) :-
    sfek_sfeika(W, Act, F, Ctx),
    not sfek_sfeika_strict(W).

References¶

Gabbay, D., Horty, J., Parent, X., van der Meyden, R., & van der Torre, L. (Eds.). (2013). Handbook of Deontic Logic and Normative Systems. College Publications.
Koons, R.C. (2017). Defeasible Reasoning. Stanford Encyclopedia of Philosophy.
Nute, D. (1994). Defeasible Logic. In Handbook of Logic in Artificial Intelligence and Logic Programming (Vol. 3, pp. 353-395). Oxford University Press.
Pollock, J.L. (1987). Defeasible Reasoning. Cognitive Science, 11(4), 481-518.
Prakken, H. (2010). An Abstract Framework for Argumentation with Structured Arguments. Argument & Computation, 1(2), 93-124.