Is FOL equivalent to CL logic?

[elvilio]

From 1: That every first-order theory has a coherent conservative extension is regarded by some as obvious (and trivial)...

A positive formula, also known as a “coherent formula”, is a first-order formula built up from atoms (amongst which we include equations) using conjunction, disjunction, and existential quantification.

Maybe there is an equivalent formulation from 2 for the positive formula (coherent formula), but couldn't access the resource.

[...] translation from FOL to CL is not necessarily constructive. The problem of provability in CL is semi-decidable.

In 1 it is then proved that another logic, called CL2, is equivalent to CL, and transofmations are provided.

From 3: Every first-order theory has a coherent conservative extension, i.e., any first-order theory can be translated into CL, possibly with additional predicate symbols. This translation process is called “coherentisation” or, sometimes, “geometrisation”.

For coherentisation see 4.

In our case the logic need to not have negation and universal quantification because of the temporal specifications, but for each atom FOL could be used and translated, but translation could not be feasable.

Bibliography:

1. Dyckhoff, R., Negri, S: Geometrization of first-order logic
2. Rothmaler, P.: Introduction to model theory
3. Janičić, P., Narboux, J.: Theorem Proving as Constraint Solving with Coherent Logic
4. Dyckhoff, R.: Invited Talk: Coherentisation of First-Order Logic

In syntesys, FOL != CL