Reference: Shawn Hedman - A First Course in Logic, An Introduction to Model Theory, Proof Theory, Computability, and Complexity - Oxford University Press (2004)

1. Prerequicite

Atomic Formula & Formula

They are any assertion which we could assign a truth value, for example,

Symbol	Translation
A	It is raining
B	It is cloudy

Formula is an atomic formula or constructed by atomic formulas using propositional logic syntax.

Syntax

Syntax define how a formula/sentence of propositional logic is correctly constructed. There are only two primitive rules for propositional logic syntax,

1. If F is a formula, then ~F is a formula.
2. If A, B is a formula, then (A & B) is a formula.

One could add more rule like

• If A, B is a formula, then (A | B) is a formula.
• If A, B is a formula, then (A -> B) is a formula.
• If A, B is a formula, then (A <-> B) is a formula.

which are convenient but not necessary. Everything can be replaced by formula using rule 1 and 2 only.

Semantic

Semantic concerns about how to interpret a given formula/sentence, for example how should we interpret ~A & B? Is it ~(A & B) or (~A) & B?

~ has priority over &.

Semantic also deals with how to interpret each symbols, this could be represented by truth table.

A	~A
F	T
T	F

A	B	(A&B)
F	F	F
F	T	F
T	F	F
T	T	T

Since ~ and & are all the symbols that we need, this is enough to fully describe the semantic of propositional logic. Again, for convenient, we may include the precedence of other symbols and their truth tables.

Terminology

Assignment

Given a set of atomic formula S = {A1, A2, A3, ...}, an assignment A : S -> {F, T} is a function assigning true or false to element in S.

Note that S is a set of atomic formulas instead of formulas, so to write out all possible assignments in truth table (each row represents one assignment), you must start with columns of atomic formulas.

Valid formula, Tautology

A formula is valid, or a tautology if it is true under any assignment. E.g. (A | ~A)

Satisfiable

A formula is satisfiable if it is true under some assignment.

Unsatisfiable, Contradiction

A formula is unsatisfiable, or a contradiction if it is false under any assignment. E.g. (A & ~A)

Models

We say an assignment A models a formula F if A(F) = T. We write A |= F.

We say an assignment A models a set of formula F' = {F1, F2, ... } if for all i, A |= Fi. We write A |= F'.

Consequence

A formula G is a consequence of formula F if for all assignment A, A |= F then A |= G. We write F |= G.

It can be proven that F |= G if and only if F -> G is a tautology.

A formula G is a consequence of set of formula F' if for all assignment A, A |= F' then A |= G. We write F' |= G.

Equivalent

For formula F, G, if both F |= G and G |= F, we say F and G are equivalent. We write F == G. It can be proofed that F == G if and only if F <-> G is a tautology.

2. What exactly is a proof

The framework for constructing a proof consists of:

1. A formula G to be proven to be true.
2. Set of premises, denote by F' = {F1, F2, ...}
3. The assignment A that models F'.

A proof is trying to show that F' |= G. In other words, for all assignment A, if A |= F' then A |= G. Note that the exact assignment A is not important.

A universal method to show F' |= G by truth table. However this is not efficient with increasingly more premises in F'. That why a logic system is usually equipped with rules to derive formula.

3. Deriving formula

Recall from previous section that our target is to show F' |= G, i.e. G is a consequence of F. A logic system is equipped with rules that allow us to derive formula G from a set of formula F', we write F' |- G. Whenever the formula G derived is really a consequence of F', we say that the logic system is sound.

Soundness: A logic system is sound if F' |- G then F' |= G.

It is known that propositional logic is sound. This is because every single rule equipped by propositional logic is verified such that it is sound. We show for example, that the rule Modus Ponen is sound.

Modus Ponen is a rule written as {A, (A -> B)} |- B. We want to verify that {A, (A -> B)} |= B. Below is an useful proposition for the job.

Proposition: For any formula F and G, F |= G if and only if (F -> G) is a tautology.

By the above proposition, for Modus Ponen, if ((A & (A -> B)) -> B) is a tautology, then we have (A & (A -> B)) |= B. With the help of another rule call And-introduction (you may assume that it have been verified to be sound), we know that {A, (A->B)} |= (A & (A->B)). Therefore, we could draw the conclusion {A, (A -> B)} |= B if we show that ((A & (A -> B)) -> B) is a tautology. This could be done by a truth table.

A	B	(A->B)	((A & (A->B))->B)
T	T	T	T
T	F	F	T
F	T	T	T
F	F	T	T

That are many more rules than just Modus Ponen in propositional logic. Which could all be verified to be sound in a similar fashion. By verifying that all these rules are sound, we proved that propositional logic is sound. Below list some of the rule used by propositional logic. As long as a rule is sound, we could add them to the propositional logic system using as an intermediate proof step.

Name	Formula
Premise	{A} |- A
Double Negation	{A} |- ~~A
And-Introduction	{A, B} |- (A&B)
De Morgan's laws 1	{(A & B)} |- ~(~A | ~B)