About systems of equations, X-separability, and left-invertibility in the \(\lambda\)-calculus (Q752684)

A system S of equations in \(\lambda\)-calculus is said to be solvable in the theory T iff there exists a suitable simultaneous substitution of the unknown that makes the equations of S theorems of T. For any finite system and within any semi-sensible T (e.g., \(\beta\), \(\beta\eta\), \(H^*)\) a necessary condition for T-solvability is given. A class of systems for which this condition becomes also sufficient is shown. A typical result is the constructive characterization of T-solvability of systems having the shape \(\{xx=N_ 0\), \(xM_ 1=N_ 1\),..., \(xM_ n=N_ n\}\) where the \(M_ i\) are closed \(\lambda\)-terms and the \(N_ i\) are x-free \(\beta\eta\)-normal forms.