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.
Table of contents
- Propositional logic
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 and are usually noted as \(P, Q, R\)
Propositional logic (from now on PL) is made of three primitive elements:
Truth values
They are values indicating whether a proposition is true or false.
\(\top\) (true) and \(\bot\) (false)
For example given the following proposition a truth value can be assigned to it:
“Dogs can fly” is 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. the number of arguments required is called arity.
type
PrimitiveElements {.pure.} = enum
True,
False,
Not,
And,
Or,
Implies,
Iif,
Models
Subformula
Formula \(G\) is a subformula of formula \(F\) if it occures syntactically within \(G\).
Semantics
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 are 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 things. 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, therefore we give now an inductive definition of PL’s semantics.
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 characterizing 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\) 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\) is used, \(\top\) has a value \(true\) and \(\bot\) has value \(false\).
\[I \models P, \text{ iif } I[P] = true\]Next, the definition of propositional variables:
\[I \not \models P, \text{ iif } I[P] = false\]This is the base case of the inductive definition. The inductive step is made of the combinations of the following more complex formuales:
\[\begin{align*} & I \models \neg F, & \; \text{ iif } I \not \models F \\ & I \models F_1 \wedge F_2, & \; \text{ iif } I \models F_1 \text{ and } I \models F_2 \\ & I \models F_1 \vee F_2, & \; \text{ iif } I \models F_1 \text{ or } I \models F_2\\ & I \models F_1 \rightarrow F_2, & \; \text{ iif, if } I \models F_1 \text{ then } \models I \models F_2 \\ & I \models F_1 \leftrightarrow F_2, & \; \text{ iif } I \models F_1 \text{ and } I \models F_2, \text{ or } I \not \models F_1 \text{ and } I \not \models F_2 \\ \end{align*}\]Satisfiability and Validity
Here follow two fundamental properties that are of interest in the study of formulaes
Satisfiability
A formula \(F\) is said to be satisfiable if and only if there exists an interpretation \(I\) such that
\[I \models F\]Validity
A formula \(F\) is valid if and only if for all interpretation \(I\)
\[I\models F\]They are often times interchangeable to a certain degree, one gives information about the other. Thanks to the semantics of negation they can be proven to be dual. This allows us to choose whatever is most comfortable for a given task. As anyone might have guessed at this point, it is very interesting to determine whether a formulae is satisfiable and/or valid.
Equivalence and Implication
Two formulae \(F_1\) and \(F_2\) are equivalent if they evaluate to the same truth value under all interpretations \(I\). That is, for all interpretations \(I\), \(I \models F_1 \leftrightarrow I\models F_2\).
Formula \(F_1\) implies formula \(F_2\) if \(I \models F_2\) for every interpretation \(I\) such that \(I\models F_1\).
Substitution
A substitution \(\sigma\) is a mapping from formulae to formulae:
\[\sigma: \{F_1 \rightarrow G_1, \dots, F_n \rightarrow G_n \}\]The domain of \(\sigma\) is:
\[domain(\sigma): \{F_1, \dots, F_n \}\]The range of \(\sigma\) is:
\[range(\sigma): \{G_1, \dots, G_n \}\]Replacements occur all at once.
Substitution of Equivalent Formulae
Consider substitution
\[\sigma: \{F_1 \rightarrow G_1, \dots, F_n \rightarrow G_n \}\]such that for each \(i, F_i \leftrightarrow, G_i\) . Then \(F \leftrightarrow F_{\sigma}\)
which means that given a formula and a substitution, if each part of the derived formula is equivalent to its substitution, the derived formula is equivalent to the starting one.
One very mathematically interesting thing is that proving the validity of a PL formula \(F\) proves the validity of an infinite set of formulae, the set of all formulaes that can be derived via a variable substitution
Valid Template
If \(F\) is valid and \(G = F_{\sigma}\) for some variable substitution \(\sigma\), then \(G\) is valid.
Normal Forms
A normal form of formulae is a syntactic restriction such that for every formula of the logic, there is an equivalent formula in the normal form. Three normal forms are particularly important for PL.
Negation normal form (NNF)
A NNF requires that \(\neg, \wedge, \vee\) be the only connectives and that negations appear only in literals
Disjuntive normal form (DNF)
A formula is in DNF if it is a disjunction of conjunction of literals
\[\bigvee_i \bigwedge_j\text{ for literals }\mathcal{l}_{i,j}\]Conjuctive normal form (CNF)
A formula is in CNF if it is a conjunction of disjunction literals. This is the dual of DNF
\[\bigwedge_i \bigvee_j \text{ for literals }\mathcal{l}_{i,j}\]« Start
Inchworm theory »