Investigation on fragments of first order branching temporal logic (Q2776809)

Various fragments of first-order computational tree logic (\textbf{FOCTL}) are investigated. The fragment of the logic with only the operator \textbf{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 \textbf{H} (always in the past) is not axiomatizable as well. The proof is done by showing that the set of valid formulae of \(\mathbf{FOCTL}_{\mathbf H}\) is \(\Pi^0_2\)-complete. The only axiomatizable fragment is the one with the next operator (\textbf{X}).