Is First-order logic Turing complete? Is First-order logic also called predicate logic Turing complete?
EDIT:
If we do computation by checking if premises logically entail a conclusion. And the method is resolution .
 A: You seem to be asking whether you can use the deductive rules of first-order logic to simulate a Turing machine. One possible answer is yes, in the following sense: You can use the elements $s$ of a structure to represent steps in a computation, a series of predicates $P(s)$ to represent the state at that step, and a group of first-order axioms such as $P(s) \rightarrow Q(s+1)$ to initialize the state and govern the transitions. If you do this correctly, your Turing machine halts iff you can use these axioms to prove $(\exists s)[s$ is configured in a halting state$]$. But there are also other ways to interpret your question.
A: [Some Turing-Complete Extensions of First-Order Logic], by Antti Kuusisto, contains the following remark in the second paragraph:

A crucial weakness in the expressivity of k-th order predicate logic
  is that only a finite amount of information can be encoded by a finite
  number of quantified relations over a finite domain. Intuitively,
  there is no infinitely expandable memory available. Thus k-th order
logic is not Turing-complete.

A: Interpreting your question as is there an isomorphism between first order logic and a Turing complete system of computation/calculus, then no. The Curry-Howard Isomorphism shows it is merely isomorphic to Lambda-P, so it does need extended to be Isomorphic to something Turing complete. The more expressive Real PCF (Programming Computable Functions) extended with the existential quantifier is an example of a more expressive extension of simply typed lambda-calculus that is Turing-Complete [1][2]. This is similar to how how second-order predicate logic is more expressive than first order predicate logic and isomorphic to a more expressive computational model Lambda-P2.
One class of deductive systems isomorphic to Lambda-Calculus in general (and thus Turing-Complete) and closely related to first-order logic is the class of Hilbert-style deduction systems. This is more expressive than first-order logic because it can be used to prove meta-logical results including ones about first-order logic not provable within first-order logic. First-order logic doesn’t allow trans finite induction, but other Hilbert-style deductions can. This is similar to how general recursion is a fundamental aspect of Turing-Complete systems. This is also related to Combinatory Logic (not to be confused with Combinational Logic)
[1]: M.H. Escardó.
Real PCF extended with $\exists$ is universal.
In A. Edalat, S. Jourdan, and G. McCusker, editors, Advances in Theory and Formal Methods of Computing: Proceedings of the Third Imperial College Workshop, April 1996, pages 13-24, Christ Church, Oxford, 1996. IC Press.
[2]: https://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-374/ECS-LFCS-97-374.pdf
