Last modified on 13 July 2009, at 14:18

Logic for Computer Scientists/Propositional Logic/Preliminaries

PreliminariesEdit

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.

Figure1simplecircut.png