proposition-restriction.md

The Subtle Difference Between Quantifier and Predicate Restriction

In logic, we often need to make propositions (P) about a domain but then would like to restrict the domain to specific subsets (S) while reusing the proposition.

Quantifier and Predicate Restriction are the two common approaches to domain restriction, explained below.

IRL Example

Imagine you're implementing type checking in a programming language compiler. You need to verify that "all function calls have matching parameter types" - a seemingly straightforward rule. But how you express this constraint in logic can have profound implications for your compiler's correctness. Should you write "for all function calls, the parameter types match" or "for all expressions, if it is a function call, then its parameter types match"? While these might appear equivalent, choosing the wrong formulation could lead to subtle bugs that slip through your type checking phase. The wrong formulation could allow malformed programs to compile or reject valid ones.

Quantifier Restriction

This approach modifies the quantifier itself, explicitly stating which elements we care about:

Existential: $\exists x \in S : P(x)$

Universal: $\forall x \in S : P(x)$

Consider talking about odd numbers with the proposition "for all x, x is odd" represented as $\forall x : P(x)$. Using universal quantifier restriction it becomes $\forall x \in S : P(x)$ with S being the set {1,3,5} which means "for all x where x is one, three, or five, x is odd."

Predicate Restriction

Here, we use logical operators to combine our domain predicate with our main predicate:

Existential: $\exists x : x \in S \wedge P(x)$

Universal: Two possibilities...

• Using implication: $\forall x : x \in S \rightarrow P(x)$
• Using conjunction: $\forall x : x \in S \wedge P(x)$

Similarly to our previous example but using predicate restricion with implication it becomes $\forall x : x \in S \rightarrow P(x)$ which means "for all x, if x is one, three, or five then x is odd"

The Subtle Difference

At first glance, these might seem like mere syntactic variations. However, there's a profound difference in how they handle elements outside our intended domain S:

1. Quantifier restriction simply ignores elements outside S
2. Predicate restriction evaluates them, leading to:
   • For existential: false when x S
   • For universal with implication: true when x S (vacuously)
   • For universal with conjunction: false when x S

This distinction means these forms aren't truly equivalent. We cannot freely convert between them through algebraic manipulation, as they make fundamentally different claims about the domain.

Verification Capabilities and Domain Restrictions

The way we handle domain restrictions in practice often depends on our verification tools. Some systems can enforce domain constraints before runtime through type systems or formal proofs, while others must rely on runtime checks. These different capabilities fundamentally affect which restriction approach is most appropriate.

For systems with strong pre-runtime verification (like dependent types):

1. Quantifier restriction is ideal, mapping naturally to type-level constraints
2. Neither form of predicate restriction is suitable:
   • Implication leads to vacuous truths that can hide errors
   • Conjunction forces unnecessary reasoning about impossible cases
   • Both obscure the fundamental intent that we're only interested in elements from our domain

For example, in Idris the type system ensures length properties at compile time - it's impossible to construct invalid inputs.

-- Vector is a type-level list with length
data Vec : Nat -> Type -> Type
-- Length is part of type, impossible to call with wrong length
append : Vec n a -> Vec m a -> Vec (n + m) a

For systems without pre-runtime verification:

1. Predicate restriction with conjunction becomes valuable, as it enforces defensive programming through explicit runtime validation
2. This "forced" handling of out-of-domain cases provides runtime safety in the absence of compile-time guarantees
3. Predicate restriction with implication remains problematic, as its vacuous truths can hide runtime errors

For example, in Python the length properties must be explicitly checked at runtime because the type system isn't expressive enough to encode them.

def append(xs: List[int], ys: List[int], n: int, m: int) -> List[int]:
    # Runtime checks enforced by conjunction of conditions
    if len(xs) == n and len(ys) == m:
        return xs + ys
    raise ValueError("Length mismatch")

Key Takeaway

The distinction between quantifier restriction ($\forall x \in S : P(x))$ and predicate restriction ($\forall x : x \in S \rightarrow P(x)$ or $\forall x : x \in S \wedge P(x))$ has significant ramifications in both theory and practice:

1. When formalizing mathematics, these approaches make different claims about elements outside our domain of interest
2. In implementation, this manifests as a choice between:
   • Encoding domain constraints in types, where invalid states become unrepresentable
   • Encoding domain constraints in predicates, where invalid states must be handled explicitly
3. This choice directly impacts verification strategy:
   • Quantifier restriction pushes verification to compile time, requiring sophisticated type systems
   • Predicate restriction typically moves verification to runtime, requiring explicit checks

The seemingly simple choice between these formulations thus fundamentally shapes how we can reason about and verify our systems.

Anyways

How do you handle domain restrictions in your coding projects? Let's discuss! Share your experiences or questions below!

#LogicInProgramming #TypeSystems #SoftwareEngineering #ProgrammingConcepts #DomainRestriction #CompilerDesign #ProgrammingLanguages