Deductive Logic Expression in Mathematical Models

A conventional mathematical program is normally written as an objective and a set of equalities or inequalities. That representation is ideal for a solver, but it does not fully express why a business rule holds, which premises it needs, or what it implies. A deductive-logic representation treats every constraint as a proposition function over candidate solutions, giving domain knowledge, mathematics, and executable code a shared semantics.

1. From standard form to predicate form

A conventional linear model can be written as:

$$\begin{array}{rl}min/max& c^{\mathsf{T}}x\\ \text{s.t.}& Ax\rho b,\\ & x\in X,\end{array}$$

where each row of $\rho$ is $\le$, $=$, or $\ge$. The deductive form does not require every rule to already be a linear inequality:

$${\mathrm{opt}}_{x\in X}f(x)\text{s.t.}\underset{p\in C}{\bigwedge }p(x).$$

• $X$: the candidate universe, including variable types, domains, and modeling premises;
• $f:X\to \mathbb{R}$: the objective evaluation function;
• $C$: a set of constraint predicates;
• $p:X\to \{\mathsf{true},\mathsf{false}\}$: the truth of one domain proposition for a candidate.

The feasible set is:

$$F(C)=\{x\in X|\underset{p\in C}{\bigwedge }p(x)\}.$$

The optimum set of a minimization problem is:

$${\mathrm{Best}}_{min}(f,C)=\{x\in F(C)|\mathrm{\forall }{x}^{\prime }\in F(C),f(x)\le f(x^{\prime })\}.$$

For maximization, replace the final $\le$ with $\ge$. This definition separates “feasible” from “at least as good as every other feasible candidate,” which supports reasoning about optimality, critical constraints, and infeasibility.

2. A concrete constraint is also a predicate

A concrete mathematical-programming constraint can be represented by:

$$p=(g,\rho ,b),p(x)\equiv [g(x)\rho b],$$

where $g:X\to \mathbb{R}$ is a symbolic expression and $\rho \in \{\le ,=,\ge \}$. For example:

$$\sum _{i\in I}{w}_i{x}_i\le W$$

corresponds to:

$$p_{\mathrm{capacity}}(x)\equiv [\sum _{i\in I}{w}_i{x}_i\le W].$$

During domain analysis, the predicate can remain abstract:

$$p_{\mathrm{capacity}}(x)\equiv \text{“solution }x\text{ does not exceed resource capacity.”}$$

Formal design must prove that the concrete numerical predicate is equivalent to this domain predicate under declared premises. It is not enough to replace the sentence with a plausible formula.

3. Connectives and quantifiers

Standard logic composes domain rules:

Form	Meaning	Modeling example
$p\wedge q$	Both rules hold	Capacity and time windows both hold
$p\vee q$	At least one holds	Use an owned or outsourced resource
$\mathrm{\neg }p$	The rule does not hold	Forbid a combination
$p\Rightarrow q$	The consequent is required when the antecedent holds	An active server may carry flow
$p\iff q$	Both sides have the same meaning	An indicator matches a business state
$\mathrm{\forall }i\in I:p_i$	Every object satisfies the rule	Every demand is covered
$\mathrm{\exists }i\in I:p_i$	At least one object satisfies it	Select at least one plan

OSPF logical function symbols can compile some propositions into linear or quadratic models, but logical semantics and numerical implementation should remain separately documented. Big-M constants, auxiliaries, and bounds are compilation choices, not the domain rule itself.

4. Premises, definitions, and constraints

Distinguish three kinds of statements:

1. Premises/assumptions define the candidate universe $X$, such as nonnegative demand, unique indices, and consistent capacity units;
2. Definitions name a domain concept, such as “node assigned” being the sum of assignment variables;
3. Constraints filter feasible candidates, such as at most one server on each node.

Encoding a premise as a decision constraint can conceal invalid input data. Leaving a definition as an anonymous local expression loses cross-context reuse and traceability.

Defining an intermediate value $z$ means:

$$\mathrm{\forall }x\in X,z(x)=g(x).$$

A named intermediate value is therefore not an approximate cache. It is an equivalent definition that other predicates may reference.

5. Service-placement example

Let $x_{is}\in \{0,1\}$ indicate whether service $s$ is placed on node $i$. The Route context publishes:

$${\mathrm{NodeAssigned}}_i=\sum _{s\in S}{x}_{is},{\mathrm{ServiceAssigned}}_s=\sum _{i\in N}{x}_{is}.$$

Two domain rules become:

$$\begin{array}{rl}{p}_{\mathrm{node}}(x)& \equiv \mathrm{\forall }i\in N:{\mathrm{NodeAssigned}}_i\le 1,\\ p_{\mathrm{service}}(x)& \equiv \mathrm{\forall }s\in S:{\mathrm{ServiceAssigned}}_s\le 1.\end{array}$$

In the Bandwidth context, “a node cannot produce net outflow unless it hosts a service” is:

$$\mathrm{\forall }i\in N:\mathrm{\neg }{\mathrm{Deployed}}_i\Rightarrow {\mathrm{OutFlow}}_i=0.$$

If ${\mathrm{Deployed}}_i$ is equivalent to the binary state derived from ${\mathrm{NodeAssigned}}_i$ and $0\le {\mathrm{OutFlow}}_i\le U_i$ is known, the familiar linear form follows:

$${\mathrm{OutFlow}}_i\le U_i{\mathrm{Deployed}}_i.$$

The bound $U_i$ must be valid and justified. An arbitrary huge M can be numerically unstable and, when too small, logically nonequivalent.

6. Deduction in a knowledge base

Let $K$ be the existing predicate set and $q$ a conclusion. Define:

$$K\models q⟺\mathrm{\forall }x\in X:(\underset{p\in K}{\bigwedge }p(x))\Rightarrow q(x).$$

This relation answers:

• implication: whether existing rules entail a conclusion;
• redundancy: if $K\models q$, adding $q$ does not change the feasible region;
• conflict: if $K\models \mathrm{\neg }q$, the new rule is incompatible with current knowledge;
• equivalence: $K\models (q\iff r)$ means two expressions agree under the premises;
• refinement: an implementation predicate is more concrete while preserving required equivalence.

Consistency is satisfiability, not merely the absence of an obvious pairwise conflict:

$$\mathrm{SAT}(K)⟺\mathrm{\exists }x\in X:\underset{p\in K}{\bigwedge }p(x).$$

7. From a symbolic constraint to an executable predicate

Tests, callbacks, and diagnostics can evaluate a concrete inequality as a predicate. Floating-point code must use an explicit tolerance:

fun satisfied(
    lhs: Flt64,
    relation: Relation,
    rhs: Flt64,
    tolerance: Flt64
): Boolean = when (relation) {
    LessEqual -> lhs <= rhs + tolerance
    Equal -> abs(lhs - rhs) <= tolerance
    GreaterEqual -> lhs + tolerance >= rhs
}

Keep these concepts separate:

• exact semantics: $g(x)\rho b$ in documentation and proof;
• solver tolerance: backend primal-feasibility rules;
• business tolerance: acceptable operational deviation;
• display precision: number formatting.

One “number of displayed decimal places” cannot replace all four.

8. Traceable representation

Maintain a record for each rule:

Field	Example
Domain statement	At most one service is placed on each node
Predicate ID	route.node_assignment
Preconditions	Node and service sets are deduplicated
Formal predicate	$\mathrm{\forall }i,\sum _s{x}_{is}\le 1$
Intermediate values	${\mathrm{NodeAssigned}}_i$
Executable owner	NodeAssignmentLimit pipeline
Evidence	Boundary unit tests, model snapshot, and small known optimum

This mapping lets requirements, mathematical, code, and test reviews discuss the same semantics.

9. Boundaries of the method

• A predicate representation does not turn a general MILP into an automatically proved theorem.
• A solver's feasible status means the compiled constraints hold within numerical tolerance; it does not mean the domain rules are complete.
• Logical equivalence is meaningful only under an explicit universe $X$ and premises $K$.
• Linearizing nonlinear logic requires finite bounds and correct strict/non-strict boundary treatment.
• A callback that observes only the current candidate must handle missing values, nonintegral candidates, and solve-stage differences.

10. Next steps

• Formal design and formal verification
• DDD architecture fundamentals
• Linear logical function symbols