Abstract
Leibniz’s principle—that expressions denoting the same object may be substituted without changing truth value—is an implicit warrant for transformations in school algebra. Yet familiar examples appear to violate it: \(2(x + 1)\) and \(2x + 2\) agree in value, but only the first is factorised; \(\frac{\left( x^{2} - 4 \right)}{(x - 2)}\) and \(x + 2\) agree away from \(x\ = \ 2\), but differ as partial functions on ℝ. This paper argues that such cases conflate three levels: a written expression, a typing judgement, and a denotation in a specified domain. Expressions formed in a context Γ of variable declarations constitute a typed family \(Expr_{A}(\Gamma)\), and an evaluation assigns each of them a value in a declared semantic domain, relative to an environment for Γ. A typed substitution rule then shows why a predicate about an expression form cannot receive a semantically equal value as an argument. Earlier work has already distinguished syntax from semantics and advocated explicit attention to types in mathematics teaching. The narrower contribution here is to connect student-written type declarations to an explicit substitution rule for algebra, develop that connection into a three-level instructional design, and formulate testable transfer and error-detection hypotheses.