Scholarlink

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 \(\mathbf {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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Classical Logic

  • 章节

  • 发表日期：

    2026年

查看全文
  • Bruno Da Ré,
  • Damián Szmuc,
  • Paula Teijeiro

摘要

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 \(\mathbf {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.