In this chapter, we introduce the language of first-order logic, on which we may base precise thinking, speaking, and writing, in computer science and all other kinds of scientific disciplines. We present first-order logic as a formal language in the spirit of the previous chapter by an abstract syntax based on which the intuitive interpretation of the various phrases is explained. We will then equip the language with some sort of “type system” to identify the well-formed phrases, and give these phrases a formal semantics, first for the subset of “propositional logic” and then for the full language. Based on this semantics, we investigate which syntactic transformations preserve the meanings of formulas and which formulas always denote “true” statements.