If the 1931 Incompleteness Theorem is correct then the much simpler expression at the end of this post equally proves that there are some sentences of predicate logic that are neither provable nor refutable.
Syntactic_Logical_Consequence (Γ proves A)
A formula A is a syntactic consequence within some formal system FS of a set Γ of formulas if there is a formal proof in FS of A from the set Γ:
Γ ⊢ FS A
Translation to Minimal Type Theory notational conventions
Γ ⊢ FS A ≡ ( Γ ⊂ FS (Γ ⊢ A) )
Named predicate (of predicate logic PL) impossible to prove and impossible to refute: G( ~∃Γ ⊂ PL (Γ ⊢ G) )