Global vs Local Validity¶

This document clarifies the relationship between global satisfiability of the questionnaire and per-item implication checks. We formalize both notions and prove what is (and is not) equivalent, with practical consequences for validation.

Motivation¶

When analyzing questionnaires, we can check constraints at two levels:

Per-item level: For each item \(I_i\), check if its postcondition \(Q_i\) can be violated when its precondition \(P_i\) holds
Global level: Check if there exists at least one assignment that satisfies all item constraints simultaneously

These are not equivalent concepts, and understanding their precise relationship is crucial for correct questionnaire validation.

Setup¶

Let \(B\) denote the conjunction of all base constraints in the questionnaire (domains of outcomes and any initialization constraints). For each item \(I_i\), let \(P_i\) be its precondition and \(Q_i\) its postcondition, expressed as Boolean formulas over the answer variables \(\mathbf{S} = (S_1,\dots,S_n)\).

Global Satisfiability¶

Define the global formula:

\[ G := B \wedge \bigwedge_{i=1}^n \bigl(P_i \Rightarrow Q_i\bigr) \]

We say the questionnaire passes the global satisfiability check if \(\mathrm{SAT}(G)\) holds.

Interpretation: There exists at least one assignment to all variables that:

Satisfies all domain constraints (\(B\))
For each item, if its precondition holds, its postcondition also holds

Per-Item Invariants¶

For an item \(I_i\), define:

\[ W_i := B \wedge P_i \wedge \lnot Q_i \]

\[ F_i := B \wedge P_i \wedge Q_i \]

Key Relations¶

The following facts capture the exact relationship between the global check and the per-item checks.

Theorem: Soundness of Per-Item Validity for Global Satisfiability¶

Theorem: If \(\mathrm{SAT}(B)\) and for every \(i\) we have \(\mathrm{UNSAT}(W_i)\), then \(\mathrm{SAT}(G)\).

Informal statement: If the base constraints are satisfiable and every item's postcondition is per-item valid (cannot be violated), then the global formula is satisfiable.

Complete Formal Proof

Assume \(\mathrm{SAT}(B)\) and \(\mathrm{UNSAT}(W_i)\) for all \(i \in \{1, \ldots, n\}\), where \(W_i = B \wedge P_i \wedge \lnot Q_i\).

Step 1: Transform unsatisfiability to entailment for each item.

For each \(i\), we have \(\mathrm{UNSAT}(B \wedge P_i \wedge \lnot Q_i)\).

By definition of unsatisfiability:

\[ \nexists \mathbf{a} : \mathbf{a} \models (B \wedge P_i \wedge \lnot Q_i) \]

Equivalently, by the quantifier negation rule (i.e., \(\neg \exists x \, P(x) \equiv \forall x \, \neg P(x)\)):

\[ \forall \mathbf{a} : \mathbf{a} \not\models (B \wedge P_i \wedge \lnot Q_i) \]

By the definition of satisfaction for conjunction (an assignment fails to satisfy a conjunction if it fails to satisfy at least one conjunct), this means for all assignments \(\mathbf{a}\):

\[ \mathbf{a} \not\models B \text{ or } \mathbf{a} \not\models P_i \text{ or } \mathbf{a} \not\models \lnot Q_i \]

Note that \(\mathbf{a} \not\models \lnot Q_i\) is equivalent to \(\mathbf{a} \models Q_i\) (by double negation).

Rewriting the disjunction using the logical equivalence \((\neg A \vee \neg B \vee C) \equiv ((A \wedge B) \Rightarrow C)\), we get: for all assignments \(\mathbf{a}\):

\[ \text{if } \mathbf{a} \models B \wedge P_i, \text{ then } \mathbf{a} \models Q_i \]

By the semantic deduction theorem, this is precisely the definition of:

\[ B \wedge P_i \models Q_i \]

Applying the deduction theorem again (moving \(P_i\) to the right):

\[ B \models (P_i \Rightarrow Q_i) \]

Step 2: Combine entailments for all items.

We have established that \(B \models (P_i \Rightarrow Q_i)\) for each \(i \in \{1, \ldots, n\}\).

By the monotonicity of entailment: if \(B \models \phi_i\) for each \(i\), then \(B \models \bigwedge_i \phi_i\).

Therefore:

\[ B \models \bigwedge_{i=1}^n (P_i \Rightarrow Q_i) \]

Step 3: Construct a model for \(G\).

By hypothesis, \(\mathrm{SAT}(B)\), so there exists an assignment \(\mathbf{a}\) such that \(\mathbf{a} \models B\).

From Step 2, we have \(B \models \bigwedge_{i=1}^n (P_i \Rightarrow Q_i)\).

By the definition of semantic entailment, every model of \(B\) is also a model of \(\bigwedge_{i=1}^n (P_i \Rightarrow Q_i)\).

Since \(\mathbf{a} \models B\), we have \(\mathbf{a} \models \bigwedge_{i=1}^n (P_i \Rightarrow Q_i)\).

Therefore:

\[ \mathbf{a} \models B \wedge \bigwedge_{i=1}^n (P_i \Rightarrow Q_i) = G \]

Hence, \(\mathrm{SAT}(G)\). ∎

Practical implication: Per-item validation provides a sufficient condition for global consistency. If each item's postcondition passes individual validity checks (\(\mathrm{UNSAT}(W_i)\)), we can conclude the questionnaire is globally consistent without performing the more expensive global SAT check.

Additional Key Facts¶

Fact (Per-Item Constraint Does Not Imply Global Unsatisfiability): If \(\mathrm{SAT}(W_i)\) for some \(i\), it does not follow that \(\mathrm{UNSAT}(G)\).

Explanation: The witness for \(\mathrm{SAT}(W_i)\) shows that there exists a model where \(P_i\) holds but \(Q_i\) is violated. However, the global check asks whether there exists a (possibly different) model that satisfies all implications simultaneously.

The existence of a violating model for some \(i\) does not preclude the existence of a different model that avoids all violations.

Per-Item Violation but Global Satisfiability

Voting Eligibility Survey:

\(I_1\): "Age" with \(S_1 \in [0, 120]\)
\(I_2\): "Eligible to vote?" with \(P_2 = (S_1 \geq 18)\), \(Q_2 = (S_1 \geq 18)\)
\(I_3\): "Driver's license?" with \(P_3 = (S_1 \geq 16)\), \(Q_3 = (S_2 = 1 \Rightarrow S_1 \geq 18)\)

Analysis:

For item 2: \(W_2 = B \wedge (S_1 \geq 18) \wedge \lnot(S_1 \geq 18)\) is UNSAT (since \(P_2 \equiv Q_2\))
For item 3: \(W_3 = B \wedge (S_1 \geq 16) \wedge \lnot(S_2 = 1 \Rightarrow S_1 \geq 18)\) is SAT
Violating witness: \(S_1 = 17, S_2 = 1\) (17-year-old claims to be eligible to vote)

Global check:

\(G\) is still SAT with assignment \(S_1 = 18, S_2 = 1\)
The violation witness (\(S_1 = 17, S_2 = 1\)) is just one possible assignment
Other assignments (e.g., \(S_1 = 18, S_2 = 1\) or \(S_1 = 17, S_2 = 0\)) satisfy all constraints

Conclusion: Finding a per-item violation does not prove global unsatisfiability.

Fact (Base Unsatisfiability Is Invisible to Per-Item Checks): If \(\mathrm{UNSAT}(B)\), then \(\mathrm{UNSAT}(G)\), yet every \(W_i\) is also UNSAT (trivially).

Explanation: If the base constraints \(B\) are unsatisfiable (e.g., contradictory domain constraints), then every formula containing \(B\) is also unsatisfiable, including all \(W_i\) and \(G\).

Per-item checks will report all postconditions as "TAUTOLOGICAL" (since \(W_i\) is always UNSAT), masking the deeper problem that the base system has no valid states.

Unsatisfiable Base Constraints

Survey with Contradictory Domains:

\(I_1\): "Age in years" with domain \(S_1 \in [0, 120]\)
\(I_2\): "Age in months" with domain \(S_2 \in [0, 100]\)
Base constraint adds: \(S_2 = 12 \times S_1\)

Problem:

For \(S_1 = 10\) years, we need \(S_2 = 120\) months
But domain constraint requires \(S_2 \leq 100\)
Therefore \(B\) is UNSAT for ages > 8.33 years

Per-item checks:

All \(W_i\) are UNSAT (because \(B\) is UNSAT)
System reports all postconditions as "TAUTOLOGICAL"
Misleading result: The real problem is unsatisfiable base constraints, not valid postconditions

Recommendation: Always verify \(\mathrm{SAT}(B)\) first before interpreting per-item results.

Formal Characterization¶

The global satisfiability problem is:

\[ \mathrm{SAT}\Bigl( B \wedge \bigwedge_{i} (\lnot P_i \lor Q_i) \Bigr) \]

which is equivalent to checking the existence of a model of \(B\) that avoids all per-item counterexamples simultaneously:

\[ \mathrm{SAT}\Bigl( B \wedge \bigwedge_{i} \lnot (P_i \land \lnot Q_i) \Bigr) \]

By contrast, the per-item constraint witness checks, for each \(i\), the existence of a counterexample model:

\[ \mathrm{SAT}(B \wedge P_i \wedge \lnot Q_i) \]

Key difference:

Global check: ∃ model satisfying all implications simultaneously
Per-item check: For each item, ∃ a model violating that item's implication

Existence of any violating model for some \(i\) does not preclude the existence of a different model that satisfies all implications. Hence there is no equivalence in general.

Consequences for Implementation¶

What Per-Item Checks Guarantee¶

If \(B\) is SAT and all items have \(\mathrm{UNSAT}(W_i)\) (i.e., all postconditions are per-item valid), then the global formula \(G\) is SAT.

Sufficient condition: Per-item validity + SAT base ⟹ global satisfiability

This theorem provides a computationally efficient validation strategy: per-item checks are typically much faster than global satisfiability checks, especially for large questionnaires.

What Per-Item Checks Do Not Guarantee¶

Detecting an INVALID item (some \(\mathrm{SAT}(W_i)\)) is not a proof that \(G\) is UNSAT
A violation witness shows one problematic assignment exists
Other assignments may still satisfy all constraints simultaneously
All items per-item valid does not prove \(G\) is SAT unless \(\mathrm{SAT}(B)\) is also established
If base constraints are unsatisfiable, all per-item checks trivially pass
Must verify \(\mathrm{SAT}(B)\) first to avoid misleading results

When Global Check Is Needed¶

To decide \(\mathrm{SAT}(G)\) exactly, one must check:

\[ \mathrm{SAT}\Bigl( B \wedge \bigwedge_i (\lnot P_i \lor Q_i) \Bigr) \]

Per-item checks provide actionable diagnostics (finding specific violating assignments) and yield a sufficient condition for global satisfiability when combined with a SAT base. However, they are neither necessary nor sufficient to characterize global satisfiability in general.

Practical Validation Strategy¶

Given these relationships, a sound validation strategy proceeds in layers:

Layer 1: Base Constraint Check

Verify \(\mathrm{SAT}(B)\) first
If UNSAT: Report fundamental design error in domain constraints
If SAT: Proceed to per-item analysis

Layer 2: Per-Item Analysis

For each item \(i\):
Check precondition reachability: ALWAYS, NEVER, or CONDITIONAL
Check postcondition status: VACUOUS, TAUTOLOGICAL, CONSTRAINING, or INFEASIBLE
Report specific violating assignments as diagnostics
Flag NEVER-reachable items and INFEASIBLE postconditions as design errors

Layer 3: Global Consistency (Optional)

If high confidence is needed, perform global check:
Solve \(\mathrm{SAT}(G)\) to confirm at least one valid completion path exists
If UNSAT despite per-item validity, investigate inter-item conflicts
If SAT, optionally report witness assignment as example valid survey path

This layered strategy balances computational efficiency with validation thoroughness.

Practical Validation Heuristic

For most questionnaires:

If \(\mathrm{SAT}(B)\) and all items pass per-item checks (\(\mathrm{UNSAT}(W_i)\)), the questionnaire is valid
Global check is only needed when:
- Extra confidence is required (critical surveys)
- Some per-item violations exist but you suspect global consistency
- Debugging complex inter-item dependencies

Visual Summary¶

graph TD
    A[Base Constraints B] --> B{SAT?}
    B -->|UNSAT| C[All W_i are UNSAT<br/>G is UNSAT<br/>❌ Broken base system]
    B -->|SAT| D{All W_i UNSAT?}
    D -->|Yes| E[G is SAT ✅<br/>Questionnaire consistent<br/>Per-item checks sufficient]
    D -->|No| F{Some W_i SAT}
    F --> G{Check SAT of G}
    G -->|SAT| H[G is SAT ✅<br/>Despite per-item violations,<br/>global path exists]
    G -->|UNSAT| I[G is UNSAT ❌<br/>No valid completion path]