yet another technical blog


On logic, formal verification and decision procedures - Part I

This post tries to be the enstablishment of a series that aims to introduce the use of formal methods and decision procedures in computer science and software engineering. The structure adopted strictly follows the one used in the book "The Calculus of Computation", which is the source of most of the following material.

Fundamentals of computation

A computation is any type of calculation that includes both arithmetical and non-arithmetical steps and which follows a well-defined model (e.g. an algorithm). Wikipedia

Propositional logic

Propositional logic is the first building block necessary to embark on the long journey of formal methods. As the name suggests, it handles propositions It is a statement which has a truth value, meaning it can be proved to be true or false. For a proposition to be valid, it must be possible to prove the proposition is either true or false. and are usually noted as \(P, Q, R\).


Propositional logic (from now on PL) is made of three primitive elements:

Truth values

\(\top\) (true) and \(\bot\) (false)

Propositional variables

In mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is a variable which can either be true or false. Wikipedia

They are usually denoted as \(P, Q, R, P_1, P_2, \dots\)

Logical conjectives

They are respectively: “not”, “and”, "or", "implies", "if and only if"

\[\neg, \wedge, \vee, \rightarrow, \leftrightarrow\]

Except negation which is unary, all of the aforementioned operators are binary.

These logical connectives have an aritythe number of aguments that it takes.


Formula \(G\) is a subformula of formula \(F\) if it occures syntactically within \(G\).


Semantics (from Ancient Greek: σημαντικός sēmantikós, "significant") is the study of meaning, reference, or truth. Wikipedia

In order to define the semantics of PL there must be a mechanism in place for evaluating the propositional variables. An interpretation \(I\) assigns to every propositional variable exactly one truth value.

\[I: \{P \rightarrow true, Q \rightarrow false \}\]

In the example, \(I\) assigns \(true\) to \(P\) and \(false\) to \(Q\) Given a PL formula \(F\) and an interpretation \(I\), the simplest way to compute the value (or truth value) of \(F\) is via a truth table. The readers of likely fall in categories that are very much acquainted to the process of reading and interpreting a truth table, therefore I, as of now, won't delve too much into it in favor of covering potentially more interesting By "more interesting" I mean't to say "potentially less known" What I will specify, are a couple of things in regards to notation. These notions will be further explored in future posts.

Inductive definition of PL's semantics

Truth tables, as convenient as they are a notation, are unsuitable for predicate logic (which will follow in later posts), therefore we give now an inductive definition of PL's semantics. Doing so allows us to instead of being forced to do .

Inductive definitions of sets are often informally presented by giving some rules for generating elements of the set and then adding that an object is to be in the set only if it has been generated according to the rules. An equivalent formulation is to characterize the set as the smallest set closed under the rules.

We write \(I \models F\) if \(F\) evaluates to \(true\) under \(I\) and \(I \not \models F\)To be read as "not evaluates" if it evaluates to \(false\).

Lets start by defining giving meaning to truth symbols

\[I \models \top\] \[I \not \models \bot\]

Regardless of which interpretation \(I\), \(\top\), has a value \(true\) and \(\bot\) has value \(false\).

\[I \models P, \text{ iif } I[P] = true\]