LCC Volume I

Logic Cookbook

Introduction

Resources

Notation

0 \in \N and \N^+ :=\ \N \setminus \{0\}.
\varnothing denotes the empty set.

Introduction

Before we start our journey, let's ask a simple question asked by many before: "What is computation?". The answer to this question, if exists, is not short, and even if we could answer it shortly, it wouldn't be that useful. We could, however, at least try to answer it, especially by asking more questions. Of course we could look from a smaller angle, from a specific projection of all the possible angels, and could define it as a step-by-step application of some set of rules. However, it is still to broad of an answer and still doesn't give use much, not to mention correctness. Could it be continuous? It very well could be, at least to the point of implementation — if that's what we are seeking for.

Ah-ha! "What we are seeking for", another yet better question. Without doubt, there are so many (maybe too many) books on logic and computation which are somehow closely related disciplines, and depending on what you are seeking for you may go grab one but before you do that consider this piece of informative and mostly introductive work on various topics.

Our main aim in this open source work is to immerse you into this immense world of computation and thus logic. We will try to assume a general point of view to computation and logic, therefore if you are looking for bitwise operator hacks, or how to optimize your imperative program this is not the book. You will, however, learn the connection between the logic and computation.

This is an excellent resources for people who are familiar with formal mathematics, or computer scientists as they will probably grasp given concepts easier than those are not. Don't worry if you are neither as the primary audience of this work is anyone who is able to do basic reasoning and follow some mathematical symbols which will be clearly defined. We will however, assume some fundamental mathematical facts and notations that will hopefully be defined in preliminaries in the following editions.

For now you should be familiar with:

Simple set-theoric notation
Backus-Naur Form
Simple complexity classes

1.1. Lambda Calculus

We will start our journey with a very simple yet very powerful construct called the lambda calculus or \lambda-calculus. Almost every model in this work is either a generalisation of \lambda-calculus or an implementation strategy for it. This simple model of computation somehow is able to compute everything that is computable. Indeed, one might be tempted to define what computable is using the \lambda-calculus.

We will not delve much into computability; however, curious ready might want to check other related sources if interested. For now consider it as the ability to solve a given problem in a finite number of steps.

1.1.1. Def. Lambda Calculus

Simply and formally, (untyped) lambda calculus is a (high-order term) rewriting system with 3 simple types of terms. The syntax of it given in BNF is

e ::= x \mid (\lambda x.e) \mid (e \> e)

where x is a variable from any alphabet that would please us (in our case English lowercase letters x,y,z).
The second term (\lambda x.e) is called an abstraction where x is a variable and e is any \lambda-term.
Finally, third term (e \> e) is called an application which we (conventionally) apply right term e to the possibly different \lambda-term e.

Notice how whole \lambda-calculus consists of a language of lambda terms e defined as above. The \lambda sign in the abstraction term indicates the start of a function and the dot seperates the variable from the body.

It is very natural to think of lambda terms as functions over variables. With abstraction (and application) we take a single variable x which also represents a lambda term and return an another lambda term.

Until now, we have just defined how to construct lambda terms, yet other than writing down valid lambda terms we are not able to do any changes, or formally reductions on them.