Propositional Logic: Logical consequence and consistency
Normal forms of logical formulas
Functional completeness A set of connectives is called functionally complete if any formula from propositional logic is equivalent to a formula using only connectives from .
The set is functionally complete.
The set is functionally complete.
We denote the exclusive disjunction connective with the symbol (or ); the truth table of this connective is:
We define the neither connective with symbol via the truth table below
The collection is functionally complete.
Normal forms A literal is a propositional letter or a negation of a propositional letter. We define the following normal forms of logical formulas.
Disjunctive normal form
A logic formula is in disjunctive normal form if is a disjunction of conjunctions of literals, i.e., has the following form
A disjunctive normal form is full if each propositional variable occurs exactly once in each disjunction part.
Examples of formulas in normal form:
are in disjunctive normal form:
Conjunctive normal form
A logical formula is in conjunctive normal form if is a conjunction of disjunctions of literals, i.e., has the following form
Examples of formulas in normal form:
are in cconjunctive normal form:
Algebraic normal form
A logical formula is in algebraic normal form if is an exclusive disjunction of conjunctions of propositional variables or an exclusive disjunction of verum with such a formula, i.e., has the following form
Examples of formulas in algebraic normal form:
are in algebraic normal form:
Transformations of logical formulas into normal form usually proceed through a series of applications of well-known tautologies such as De Morgan's rules, distributivity rules, and double negation. Every logical formula is logically equivalent with exactly one complete disjunctive normal form (except for associative and distributive rules)
The algebraic normal form is the simplest normal form because it is not necessary to work with literals, but only with propositional variables and the verum connective. Also, logically equivalent formulas have the same algebraic normal form. This makes it easier to check logical equivalence in an 'automatic theorem prover' than with the full disjunctive normal form.