Theorem: It is undecidable whether a first order logic formula is provable (or true under all possible interpretations).

Proof: Suppose there is an algorithm B that, given a first order logic and a formula in that logic, decides whether that formula is valid (holds under all possible interpretations). I will use that to give a decision algorithm for the language {(M,w) | M is the description of a Turing machine that accepts the string w}. As the latter problem is undecidable this will show that B cannot exists.

Given M and w, create a first order logic by declaring a constant , a unary function symbol a for every letter a in the alphabet, and a binary predicate f_q for every state q of M.

Consider the following interpretation of this logic: Variables x range over strings over the given alphabet,  denotes the empty string, a(w) denotes the string aw, and f_q(x,y) indicates that M, when given input w, can reach a configuration with state q, in which xy is on the tape, with x in reverse order, and the head of M points at the first position of y. Under this interpretation f_q0(,w) is certainly a true formula, as the initial configuration is surely reachable. Here q0 is the initial state, and w is a representation of w made from the constant and function symbols of the logic. Furthermore the formula x y: f_q-acc(x,y) with q-acc the acceptance state, holds iff M accepts w.

Whenever M has a transition from state q to state r, reading a, writing b, and moving right, the formula

x y: f_q(x,ay) => f_r(bx,y)

x y: f_q(cx,ay) => f_r(x,cby)

x y: f_q(,ay) => f_r(,by),

x y: f_q(x,) => f_r(bx,) 
x y: f_q(cx,) => f_r(x,cb) 
x y: f_q(,) => f_r(,b).

f_q0(,w) & T => x y: f_q-acc(x,y).

Thus, in order to decide whether or not M accepts w, it suffices to check whether or not the formula above is