Expressing 3-SAT in first-order logic
There has been a lot of work on formalizing mathematics, and in all of this work one needs to express definitions, theorems and proofs within the logic that one is using for formalization.

This is always quite involved. 

To describe the statement that 3SAT is NP-complete, we will need a version of first-order logic with a term language that will allow us to express notions of languages, time complexity, Turing machines, polynomial-time reducibility, propositional logic and conjunctive normal forms.

Once we have an appropriate term language, we will need to describe 3SAT and NP-completeness in it. This requires us to be able to express the definitions of these notions, and this in turn involves the definition of first-order predicates that correspond to these notions and the notions that were used to define them.

Let us take a brief look at a part of this construction - this should convince you that this is indeed fairly involved. A language $L$ is NP-complete if


$L \in \mathrm{NP}$
For every $L' \in \mathrm{NP}$ we have that $L'$ polynomial-time reduces to $L$


We define a predicate $NPC(x)$ which holds if the following conjunction holds for $x$


$x$ is a language in $\mathrm{NP}$
for every $y$, if $y$ is a language in $\mathrm{NP}$, then $y$ polynomial-time reduces to $x$


We therefore need a predicate $NP(x)$ that captures that $x$ is a language in $\mathrm{NP}$, and we need a predicate $PTR(x,y)$ that captures that $y$ polynomial-time reduces to $x$. If we have these, then we can define

$$ NPC(x) = NP(x) \wedge \forall y. NP(y) \Rightarrow PTR(x,y) $$

The definition $NP(x)$ must capture the following


$x$ is a language.
There exists a nondeterministic Turing machine $M$ with polynomial-time complexity such that for all $w$, $M$ will accept $w$ if and only if $w$ is an element of $x$.


And this in turn requires us to define predicates $L(x)$, which must describe that $x$ is a language, $TM(y)$ which must describe that $y$ is a nondeterministic Turing machine, $ACC(m,w)$ which must describe that $m$ is a Turing machine that accepts string $w$, $TC(x,c)$ which describes that $x$ is a Turing machine within $c$ steps and $POL(c,p,n)$ which describes that $c$ is bounded by the polynomial $p(n)$.

Once we have defined these, we may have needed to introduce and define further predicates. And once this has been done, we need to define $PTR(x,y)$. Here, we can make use of some of the predicates that we already have, but we also need to introduce some new ones as well.

I hope that this outlines that this process of formalization is a involved and not entirely trivial task, and I hope this also explains why I do not present the entire construction of the first-order formula here.