Logic for Computer Scientists/Propositional Logic/Preliminaries

Preliminaries

As a running example consider the simple digital circuit in figure 1 consisting of an or-gate ($or1$) and two inverters ($inv1$ and $inv2$). The system description is given by the following propositional formulae, where the formulae are labeled in order to facilitate recognition of corresponding parts in figure 1. The mnemonic used in the names within the formulae is the following:

• The symbols $\lor$, $\land$ and $\lnot$ denote "or", "and" and "not" respectively.
• $i1$ and $i2$ are denoting inputs in the or-gate, $i$ an inverter and $o$ denotes the output of a gate.
• $high$ is a predicate which is intended to denote the fact, that the value specified by its arguments is "of high voltage", i.e. is on.
• $ab$ is a predicate which stands for "is abnormal", i.e. the expression $\lnot (ab(inv1))$ can be read as "the inverter one is not abnormal."

$OR1:{\lnot (ab(or1))\to high(or1,o)\leftrightarrow (high(or1,i1)\lor high(or1,i2))}$
$INV1:{\lnot (ab(inv1))\to high(inv1,o)\leftrightarrow \lnot (high(inv1,i))}$
$INV2:{\lnot (ab(inv2))\to high(inv2,o)\leftrightarrow \lnot (high(inv2,i))}$
$CONN1:{high(inv1,o)\leftrightarrow high(or1,i1)}$
$CONN2:{high(inv2,o)\leftrightarrow high(or1,i2)}$

These formulae contain labels which express their intended meaning: OR1 stands for a formula describing the function of the or-gate, IN1 ind IN2 are describing the (identical) behavior of the two inverters: CONN1 and CONN2 are specifying the way the inputs of the or-gate are connected with the outputs of the inverters. Note, that in this description the inputs and outputs of the system are not yet defined. We observe from the graphical description that both inputs of the circuit have low voltage and the output also has low voltage, i.e. we could state this by the formulae $\lnot high(inv1,i),\;\lnot high(inv2,i),\;$ $\lnot high(or1,o)$

This example demonstrates how a proposition like $high(inv1,o)$ can be used to formally describe the behaviour of an electronic circuit. Note that $high(inv1,o)$ can be read intuitively as “the output of inverter 1 is high”, and of course this sentence can be further simplified by ignoring the phrase structure and by understanding it as a simple string: “the_output_of_inverter_1_ is_high”. If we would proceed with the other propositions in the same manner we would get formulae like this:

the_output_of_inverter_1_is_high $\leftrightarrow$ the_input_of_inverter_1_is_high

This formula consists of two propositions which are connected via a double arrow. It is easy to see that formulae get rather lengthy by this way and hence we can further abbreviate the propositions by simpler strings like $P_{1}$ or $P_{2}$, which results in a formula $P_{1}\leftrightarrow P_{2}$. It should be clear by the above argumentation that this formula carries for our purposes the same information as $high(or1,i1)\leftrightarrow high(inv1,o)$. The only difference is that with the latter form some intuition is associated with the reader -- for our formal logical framework this is irrelevant and we will focus on arbitrary propositions.

In the following we will systematically avoid any intuition to real world meaning in the design of our language. We will focus solely on the study of the logical aspects, which can be expressed by our language and not to a certain intended meaning. In other words, our previous introduction of the logical formulae, which described the toy electronic circuit was too much oriented on a interpretation, which was triggered by the picture.

We will introduce the syntax of propositional logic by a very simple inductive definition and then we specify a formal semantics by another single definition.