Created: 2025-11-26 10:22 by Thom
Propositional Logic, this is one of the topics covered in the course Formal Reasoning at Radboud University, reader can be found here. It is a formal language to make sentences true or false. With propositional logic you can determine whether this is true or false: "This sentence is not true", but an application can be describing the semantics of a program. Note this is kind of a summary, if you need more look at the course guide seen here. Translating sentences To translate sentences from and to propositional logic there are some things needed, one is a dictionary these are atoms. In the Formal Reasoning course these are: R, S, RB, W, D, Out, In [1]. The next are connectives. `f ^^ g`, which translates to f /and/ g `f vv g`, which translates to f /or/ g, or both `f -> g`, to if f, then g `f harr g`, to if and only if g [2] `not f`, to not f `vv` is in this case inclusive, this means that if you have `p vv q` then both p and q are true in this case. Binding and parentheses We must define what a word is, with 3 conditions, 1. Any atomic proposition is a word. 2. If f and g are words, then so too are `(f ^^ g)`, `(f vv g)`, `(f -> g)`, `(f harr g)` , and `not f` . 3. All words are made in this way. (No additional words exist.) These in turn are called language propositions. But usually the outermost parentheses are omitted i.e. `f ^^ g` not `(f ^^ g)`. To omit them properly you must know about binding strength of the operators. This simply is the following: `not > ^^ > vv > -> > harr`. Interpreting the formula `In vv RB -> Out harr not S ^^ R`, becomes `((In vv RB) -> Out) harr (not S ^^ R)`. This is not all sadly, we also need associativity. `^^, vv, ->, harr` all are right associative. For example `p ^^ q ^^ g` must be read as `p ^^ (q ^^ g)`. Meaning and truth tables We want to be able to proof that something is true e.g. is `(p ^^ q) -> p` true? To do this we need to set the atoms to be either true or false and nothing else. The atoms `p` and `q` must be true in any model if you enumerate these truths then you are able to define the truth of `(p ^^ q) -> p`. Truth tables are used with the connectives to agree on what is true and what is not. With these truth tables the truth value can be determined for complex formula's. This is done by writing larger truth tables for all connectives. +---+---+-----------+----------+----------+------------+---------+ | f | g | `f ^^ g` | `f vv g` | `f -> g` | `f harr g` | `not f` | +---+---+-----------+----------+----------+------------+---------+ | T | T | T | T | T | T | F | | T | F | F | T | F | F | F | | F | T | F | T | T | F | T | | F | F | F | F | T | T | T | +---+---+-----------+----------+----------+------------+---------+ This is the truth table for the formula `a vv b -> a`: +---+---+----------+-----+---------------+ | a | b | `a vv b` | `a` | `a vv b -> a` | +---+---+----------+-----+---------------+ | 0 | 0 | 0 | 0 | 1 | | 0 | 1 | 1 | 0 | 0 | | 1 | 0 | 1 | 1 | 1 | | 1 | 1 | 1 | 1 | 1 | +---+---+----------+-----+---------------+ Also useful for the applications section ;) Models Truth can be seen in truth tables, whereas models assign true or false values to atoms. Where you can thus make valuations for your atoms, like: `v(a) = 0, v(b) = 1` with the formula `a vv b -> a` which has the value 0 when you look at the truth table row with the valuations. `a -> (b -> a)` is true however. To say that something is true in a certain models you use the double turnstile, or `|==` like `|== f`. In this case f is true in all models, this is also called a tautology. Something can also not be logically true, this is written with a double turnstile with a line through it [3]. Logical equivalence How can you say that two formula's are the same? This is done with logical equivalence, where formula's `f` and `g` must be true in every model `v`. This can be shown as `f -= g`, sometimes even simpler formulas can be equivalent such as `a ^^ a -= a` (having `v(a) = 1` naturally). There are some logical equivalences which are important to know of: +---------------------------------------+------------------------+ | `not (f ^^ g) -= not f vv not g` | Laws of De Morgan | | `not (f vv g) -= not f ^^ not g` | Laws of De Morgan | | `f ^^ (g vv h) -= f ^^ g vv h` | Laws of distributivity | | `f vv g ^^ h -= (f vv g) ^^ (f vv h)` | Laws of distributivity | | `not not f -= f` | Double negation | | `f -> g -= ~g -> ~f` | Contraposition | | `f -> g -= ~f vv g` | Material implication | +---------------------------------------+------------------------+ Logical consequence When speaking English the statement "the sun is shining" follows logically from the statement "it is raining and the sun is shining". In formal language we want to be able to say that `a` is a logical consequence of `a ^^ b`. A formula `g` is a logical consequence, also sometimes called a logical entailment, of the formula `f`, if `g` is true in every model for which `f` is true. You can denote this by doing `f |= g`, if it isn't then put a line through it [3]. Now we can say `|== f -> g iff f |== g`. Applications System requirements When developing hard/software systems you might have some requirements to fulfill, but because English is ambiguous you can use propositional logic to define your requirements. Complex sentences like "If the computer is within the local network or it is not within the local network but has a valid login id or it is under the use of administrator, then the Internet is accessible to the computer." can be translated to simpler formula's. Logical puzzles Puzzles made by people like Raymond Smullyan can now be solved using propositional logic. An example is the classic Knights and Knaves [4] problem. Boolean searches To search more precise you can use propositional logic in a search query. Programming Propositional logic is used in programming languages to represent and change logical expressions, which are used to control the flow of a program. For example, the conditional statements in programming languages, such as 'if-then' and 'switch-case', are based on propositional logic. At the end of the process, propositional logic is used to verify the correctness of computer programs and software systems. SAT solvers One of the bigger applications in automated reasoning is SAT solvers. Within these you use boolean formulas to solve satisfiability problems. Formula's look like this `(x ^^ y) vv (x ^^ (not z))` then assigning boolean values to x, y and z you can see if it holds. SAT solvers are used for formal verification of computer programs. For more applications look at the book Logic in Computer Science: Modelling and Reasoning about Systems by Huth and Ryan. This book also covers predicate and modal logic. [1] These are found in fr.pdf on page 3. [2] Which is often written as iff. In Dutch desda. [3] AsciiMath doesn't support this should be something like |/= f then. [4] Knights and Knaves on Wikipedia.