Feb 4, 2026
Everything in classical mathematics is expressed in terms of first order logic. FOL extends propositional logic by adding statements that can be quantification over propositions parameterized by variables. There are many logics aside from first-order predicate logic but they all share the notion that a proof of ‘If P then Q’ starts with the proposition ‘P’ and uses the axioms and rules of inference for that logic to produce ‘Q’. More precisely, the proof demonstrates that assuming P is true then Q is true. More compactly, we also say P implies Q and write P\rightarrow Q.
A logic is sound if the axioms and rules of inference cannot be used to produce a false statement. A logic is complete if every true statement can be proved using the axioms and rules of inference. A logic is not consistent if a statement and its negation can be proved. A logic is decidable if there is an algorithm to prove every true statement.
If this makes you think a proof is similar to a computation Curry and Howard beat you to it. Howard noticed the axiom system
was in one-to-one correspondence with the \lambda-calculus combinators
Mathematicians use a vocabulary even more impoverished than that of a sailor. Proposition logic uses the words not, and, or, and implies. The mathematical symbols for these words are \neg, \wedge, \vee, and \rightarrow. If P is a proposition then \neg P is true if P is false and \neg P is false if P is true. The words ‘and’ and ‘or’ have the usual meaning. The odd man out is ‘implies’.
The mathematical definition of P implies Q is not P or Q, so {P\rightarrow Q} is defined as {(\neg P)\vee Q}.
Exercise. Show P implies Q is true if P is false.
You would not be the only one to think this is a bit odd. Mathematicians must use common words to define things. The choice of the word ‘implies’ should not be construed to mean P ‘causes’ Q.
Exercise. Show if P is true and P\rightarrow Q is true then Q is true.
We say P and Q are equivalent if P\equiv Q is true if and only if P and Q are both P and Q are true or both P and Q are false.
The symbol \equiv indicates a tautology. For any values of P and Q both sides are either both true or both false.
New words can be defined it terms of these.
For example we define equivalent by
All of these word can be defined in terms of nand, the negation of and, P\uparrow Q \equiv \neg(P\wedge Q).
Exercise, Show \neg P \equiv P\uparrow P.
Hint: If P is true then P and P is true. If P is false then P and P is false.
Exercise. Show P\wedge Q \equiv \neg(P\uparrow Q).
Hint: That is the definition of nand.
Exercise. Show P\vee Q \equiv \neg(\neg P \wedge\neg Q)..
Here is the recipe for all well-formed formulas.
A proposition is a WFF.
If \phi is a WFF then \neg \phi is a WFF.
If \phi and \psi are WFFs then \phi\uparrow\psi is a WFF.
We use lower-case Greek letters for WFFs built from these rules.
We use parentheses to indicate the order in which the rules were applied. For example, \neg P \uparrow Q could be either (\neg P)\uparrow Q (apply rule 2 to P and rule 3 to that and Q) or \neg(P\uparrow Q) (apply rule 3 to P and Q then rule 2 to that).
One way to establish a tautology is to evaluate both sides for all possible truth values of propositions. If there are n propositions on each side then 2^n calculations are required.
A more parsimonious approach is to posit axioms and use rules of inference. The axioms of propositional logic are
The only rule of inference is modus ponens (a means to advance) that from \phi and \phi\rightarrow\psi we can infer \psi. A proof of \phi\rightarrow\psi consists of starting with \phi we can use axioms and modus ponens to infer \psi.
George Boole showed how to reduce propositional logic to algebraic equations, thus laying the foundation for computer science. Given a set S we can consider the algebra of functions from subsets of S to \{0,1\}. Given \{P\colon S\to\{0, 1\}}} define 1_P(s) = 1 if s\in P and 1_P(s) = 0 if s\not\in P.
In first order logic propositions can be parameterized variables.