We present the details of a formalization of Equational Predicate Logic based on a propositional version of the Leibniz rule (PSL - propositional strong Leibniz, EQN (equanimity) and TR (transitivity). All the above are "strong", i.e. they are applicable to arbitrary premises (not just absolute theorems).

It is shown that a strong no-capture Leibniz (SLCS - strong Leibniz with contextual substitution), and a weak full-capture version (WLUS - weak Leibniz with uniform substitution) are derived rules. "Weak" means that the rule is only applicable to absolutely deducible premises. We also derive general rules MON (monotonicity) and AMON (anti-monotonicity) which allow us to calculate appropriate conclusions |- C[p\A] => C[p\B] or |- C[p\A] <= C[p\B] from the assumption |- A => B.

Download paper in PDF format.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.