Propositional logic is concerned with true and false statements and rules of inference. Propositional logic serves as a foundation for high-level mathematics. The logic operators work on true or false statements, also call well-formed formulas (wffs). The basic logic operations are
Propositional logic is based upon three axioms and the rule of Modus Ponens:
Propositional calculus was first formalized by Frege in 1879, using as his axioms Axiom 1, Axiom 2, Modus Ponens, pm2.04, con3, and the double negative theorems notnot2 and notnot1. Around 1930, Lukasiewicz simplified the system by eliminating pm2.04 which follows from Axioms 1 and 2 as you can see here. Lukasiewicz also replaced the axioms con3, notnot1, notnot2 with our Axiom 3.
The theorems of propositional calculus are also called tautologies. Tautologies can be proved very simply using truth tables, based on the true/false interpretation of propositional calculus. To do this, we assign all possible combinations of true and false to the wff variables and verify that the result always evaluates to true. This is called the semantic approach. Our approach is called the syntactic approach, in which everything is derived from axioms. A metatheorem called the Completeness Theorem for Propositional Calculus shows that the two approaches are equivalent and even provides an algorithm for automatically generating syntactic proofs from a truth table. Those proofs, however, tend to be long, and the much shorter proofs that we show here were found manually. Truth tables grow exponentially with the number of variables, but it is unknown if the same is true of proofs - an answer to this would resolve the P=NP conjecture in complexity theory.