Classical Logic

In this chapter we will introduce Classical Logic, from both a valuational and a proof-theoretical point of view. We will start by defining some basic tools pertaining to both these frameworks, in a general fashion, so they will be useful for subsequent chapters too. Then, we will present Classical inferential Logic, through the sequent calculus LK and boolean bivaluations. We will then prove various metatheorical results about them, such as Soundness and Completeness, Compactness and Decidability. In the second half of the chapter, we will tackle the metainferential side, presenting different concepts of metainferential validity—both semantical and proof-theoretical. We will also show some metainferential versions of the metatheorems previously proved for the inferential part. We end the chapter by proving Cut-elimination and discussing some of its consequences.