Propositional logic in short is boolean logic as programmers would call it. It involves performing boolean operations on boolean variables and constants. In proposition logic, we call boolean variables as Atomic Propositions and the boolean expressions as Propositions.

The usual boolean operations are AND, OR and NOT represented as $\wedge$, $\vee$ and $\neg$ respectively. Some example propositions are $A \wedge B$ ie., A AND B, $\neg A \vee B$ ie., NOT(A) OR B

Tautology and proofs

What we are concerned with in a proposition is the notion of satisfiability ie., can the proposition ever be made TRUE by any assignment of boolean values to variables in it?. For example., $A \wedge B$ is satisfiable with assignment A=TRUE and B=TRUE, but $\neg A \wedge A$ is not satisfiable with any assignment.

Any proposition which isn’t satisfiable is inconsistent and any proposition which is satisfiable with every assignment is a tautology. For example., $\neg A \vee A$ is a tautology. We can also see that negation of any inconsistent proposition is a tautology and vice versa.

To verify something is satisfiable or tautology is simple, if we deal with it semantically, by applying every possible assignment of boolean values to variables and finding whether it’s tautology (but if we consider its complexity it is hard).

In first order logic we cannot verify a statement as TRUE or FALSE in this way (more on this in another post). So what we do here, is a method of derivation by encoding the semantics of the system as a set of axioms (or axiom schemas to be more accurate), along with an inference mechanism to derive the truth statements. We call the derivation a proof.

Hilbert System

Since propositional logic is simpler, we would start finding truth statements by derivation from axioms. Hilbert defined a set of axiom schemas for the propositional logic. But he didnt use AND and OR connectives. He used an operation called IMPLICATION, denoted with $\rightarrow$. For example., $X \rightarrow Y$ informally means If X is TRUE then Y is TRUE.

Any proposition on $\wedge , \vee, \neg$ can be expressed with $\rightarrow , \neg$ (It is easier to prove this by simply expressing AND, OR with IMPLICATION, NOT) and vice versa., since $A \rightarrow B \equiv (\neg A \vee B)$

Now given $A$, $B$ and $C$ be any propositions, following are Hilbert’s axioms (schemas)

We can verify all of them are tautology by writing down truth tables for it.

We also have an inference rule called Modes Ponens

Example Proof

We know $P \rightarrow P$ is a tautology, we prove it as follows,

1: Applying $A=P$, $B= P \rightarrow P$ and $C=P$ in Axiom 2 - $(P \rightarrow ((P \rightarrow P) \rightarrow P)) \rightarrow ((P \rightarrow (P \rightarrow P)) \rightarrow (P \rightarrow P))$

2: Applying $A=P$ and $B=P \rightarrow P$ in Axiom 1 - $(P \rightarrow ((P \rightarrow P) \rightarrow P))$

3: Taking $A=P \rightarrow ((P \rightarrow P) \rightarrow P)$ $B= (P \rightarrow (P \rightarrow P)) \rightarrow (P \rightarrow P)$ Modes Ponens 1 & 2 - $(P \rightarrow (P \rightarrow P)) \rightarrow (P \rightarrow P)$

4: Applying $A=P$, $B=P$ in Axiom 1 - $P \rightarrow (P \rightarrow P)$

5: Taking $A=P \rightarrow (P \rightarrow P)$ and $B=P \rightarrow P$ Modes Ponens 3 & 4 - $P \rightarrow P$

QED

Types

If we consider simplest typed programming language (or lambda calculus), the only types we need to consider are

One of the fascinating correlation of these types with propositional logic is, we can consider propositions as types and programs as proofs (Curry Howard Isomorphism).

For instance, the first two Hilbert’s Axioms are nothing but types of K and S combinator respectively, if we consider IMPLICATION as FUNCTION type,

And Modes Ponens inference rule is nothing but function application.

The last axiom in Hilbert system is bit tricky, it’s basically Proof by contradiction which can be used to prove Law of excluded middle. Constructive mathematics, on which this isomorphism relies, doesn’t allow it (Would talk more about it in seperate post). Without the negation and the last axiom, the reduced propositional logic is called Positive implicational logic.

The existence of a lambda function itself is a proof of the proposition, since lambda calculus is equivalent to SKI combinatory logic, where

$I = \lambda x.x$

$I$ has type $A \rightarrow A$ and we proved it as a tautology expressible through other axioms and our proof is nothing but $I \equiv SKK$ ie., application of Modes Ponens to the Modes Ponens of Axiom 2 and Axiom 1 with Axiom 1 again.

Hence when we are programming most of the times we are actually proving something in Propositional Logic :) .