interpretation of programs using Galois connections [2]. Our fixed-point theorem allows both new results and simpler proofs of existing results as applications and corollaries. 1. It entails expressibility of the weakest precondition and the strongest postcondition, and thus the partial correctness of an imperative program, in first-order logic with a least fixed-point operator. 2. It allows a generalisation of a result by Ackermann [1] on approximating a second-order formula by first-order formulas in a direction different from the recent generalisation [8]. 3. It allows to obtain a result from a recently introduced approach to automated inductive theorem proving with tree grammars [3] as another straightforward corollary. 4. Since it incorporates abstract interpretation, it permits to considerably simplify the proof of the decidability of affine formula equations originally presented in [5]. This work is rooted in the second author's master's thesis [6]. Some of these results have been presented at the 8th Workshop on Horn Clauses for Verification and Synthesis [4].