In this short paper, the authors deal with the relative power of the formulas loop ( &agr; ) and repeat ( &agr; ) in the framework of the first-order dynamic logic. A formula loop ( &agr; ) expresses the fact that the program &agr; can diverge, whereas repeat ( &agr; ) is true whenever &agr; can be repeated indefinitely. The main result of the paper shows that the first-order dynamic logic is more expressive with repeat than with loop.

Loop and repeat enable reasoning about infinite computations. The logical apparatus which is to be used in their study is the infinitary first-order language L _{&ohgr; 1 , &ohgr;} with countable conjunction and disjunction. In fact, the first-order language dynamic logic with the inductive addition of loop is less expressive than L _{&ohgr; 1 , &ohgr;}. The authors exhibit a property expressable in first-order dynamic logic with repeat but not expressable in L _{&ohgr; 1 , &ohgr;}. Now let ϕ be a first-order formula and &agr; be a regular program ( cf., [1] ) with only first-order tests. The authors show that the validity problem for ϕ ⊃ ⌉ loop ( &agr; ) is recursively enumerable and undecidable, but that ϕ ⊃ ⌉ repeat( &agr; ) is highly undecidable, viz., &Pgr;₁¹ complete.