Equivalences among logics of programs (Q801684)

In this paper several different first-order logics of programs such as algorithmic logic (AL), dynamic logic (DL) and logic of effective definitions (LED) are compared. The authors define a fragment Lre of constructive \(L_{\omega_ 1\omega}\), as follows: Lre contains \(\bigvee \{P_ i| \quad i\geq 1\}\) where the \(P_ i\) form an r.e. sequence of quantifier-free formulas of predicate calculus containing only finitely many free variables and Lre is closed under \(\neg\), \(\wedge\), \(\vee\), \(\exists\) and \(\forall\). They now prove that the following formal logics have the same expressibility as Lre: 1. DL of deterministic effective flowcharts without array assignments. 2. DL of deterministic effective flowcharts. 3. \(DL+\) of nondeterministic effective flowcharts without array assignments. 4. LED. 5. Logic of nondeterministic effective definitional schemes (without array assignments). 6. AL of deterministic effective flowcharts without array assignments. 7. AL of deterministic effective flowcharts without array assignments and without the iteration quantifier \(\cap.\) Finally it is shown that if some extra condition on the domain of interpretation is satisfied, also the following logics become equivalent to Lre: 8. \(DL+\) of nondeterministic effective flowcharts. 9. Logic of nondeterministic effective definitional schemes (with array assignments). 10. AL of nondeterministic effective flowcharts without the iteration quantifier \(\cap\).