Main Question: Does every language used in mathematics (such as mathematical symbols and English to describe formulas, theorems, definition, proofs, and etc.) can be translated (or reduced) to first-order (predicate) language? Sub Question: Does every informal proof can be formalized (that is, to be a formal proof)? (Note that: the mathematical proofs in publications such as papers and books, in general, are informal proofs.) Related Question: (1) Did the logicism project of Russell and Whitehead in Principia Mathematica fail? If failed, then why? (2) What is the implication of Godel's Incompleteness Theorem to the logicism activity? * I would be really grateful if anyone suggest me good, authoritative reference books that answer or discuss these questions.