01716766

j

01716766 Montagna, Franco Pinna, G.Michele Tiezzi, Elisa B.P. Investigation on fragments of first order branching temporal logic. Math. Log. Q. 48, No.1, 51-62 (2002). 2002 Wiley-VCH, Berlin EN first-order branching temporal logic axiomatization FOCTL

doi:10.1002/1521-3870(200201)48:1<51::AID-MALQ51>3.0.CO;2-S

Various fragments of first-order computational tree logic ({\bf FOCTL}) are investigated. The fragment of the logic with only the operator {\bf F} (sometimes in the future) is not axiomatizable. This is shown by a possible embedding of arithmetic into it. The proof can be extended to first-order linear time logic. It is also proved that the logic with the past operator {\bf H} (always in the past) is not axiomatizable as well. The proof is done by showing that the set of valid formulae of $\text{\bf FOCTL}_{\bold H}$ is $\Pi^0_2$-complete. The only axiomatizable fragment is the one with the next operator ({\bf X}). Damas Gruska (Bratislava)