Introduction to Dependent Types with Idris: Encoding Program Proofs in Types

© The Author(s), under exclusive license to APress Media, LLC, part of Springer Nature 2023

B. SitnikovskiIntroduction to Dependent Types with Idrishttps://doi.org/10.1007/978-1-4842-9259-4_2

2. Classical Mathematical Logic

Boro Sitnikovski¹  

(1)

Skopje, North Macedonia

 

All engineering disciplines involve some logic. The foundations of Idris, as you will see later, are based on a system that implements (or encodes) classical mathematical logic so that you can easily “map” this logic and its inference rules to computer programs.

2.1 Hierarchy of Mathematical Logic and Definitions

At its core, mathematical logic deals with mathematical concepts expressed using formal logical systems. This section looks at the hierarchy of these logical systems. The reason ...