Rules and derivations in an elementary logic course

TL;DR

This paper advocates introducing the concepts of deduction rules and derivations in elementary logic courses through inductive definitions, emphasizing their foundational role and the importance of distinguishing different types of derivations.

Contribution

It proposes a strategy to teach derivations starting from inductive definitions and highlights the significance of defining derivations early in logic education.

Findings

Derivations are fundamental in logic and related fields.

Distinguishing types of derivations enhances understanding.

Early formalization of derivations benefits advanced studies.

Abstract

When teaching an elementary logic course to students who have a general scientific background but have never been exposed to logic, we have to face the problem that the notions of deduction rule and of derivation are completely new to them, and are related to nothing they already know, unlike, for instance, the notion of model, that can be seen as a generalization of the notion of algebraic structure. In this note, we defend the idea that one strategy to introduce these notions is to start with the notion of inductive definition [1]. Then, the notion of derivation comes naturally. We also defend the idea that derivations are pervasive in logic and that defining precisely this notion at an early stage is a good investment to later define other notions in proof theory, computability theory, automata theory, ... Finally, we defend the idea that to define the notion of derivation precisely, we need to distinguish two notions of derivation: labeled with elements and labeled with rule names. This approach has been taken in [2].