I will speak about the paper “A proof of completeness for continuous first-order logic” by Ben Yaacov and Pedersen. This paper gives a proof system and a proof of its completeness for the logic of metric structures we have been studying. The proof system generalizes a classical system of Łukasiewicz in a natural way, and in many ways resembles the usual proof system for classical logic. I will give an overview of the proof system and the proof of completeness, mentioning where the ideas from classical first-order logic can be imported naively; but I will place more emphasis on where things are different. For example, the completeness theorem itself gives only proofs of approximations to a semantically valid sentence.