Mascot image.

MA0 1

Introduction to University Mathematics

Every lesson so far, in one document · 1 chapter

back to the contents

Lesson 1

Introduction to Logic

Taught

Symbols, Logic and Language

Logic is the language of mathematics. It restricts our focus to statements that are definitively true or false, thereby making human language precise. This formalisation resolves inherent ambiguities when interpreting natural expressions such as “if … then,” “or,” and “and.”

Early Greek philosophers, notably Aristotle and Chrysippus, laid the initial formal foundations but frequently struggled with the precise boundaries of semantics. It was not until the work of modern mathematicians such as Leibniz (1666), Boole (1847) and De Morgan (1847) that propositional logic was formalised.

This development introduced the core architecture of modern mathematics: formal languages, variables, operators, axioms, logical inference and proof.

Syntax and Semantics

Because logic is the formal language of mathematics, it possesses two fundamental aspects. The grammatical rules governing how symbols may be validly composed dictate its syntax, while the meaning behind a particular arrangement of those symbols is its semantics.

In mathematics, we refer to objects by giving them names. A variable is a symbol that stands in for an object that has not yet been specified. We assign a name to a particular object using the assignment operator =def\defeq. For example, writing x=def5x \defeq 5 assigns the value 55 to the variable xx. We can similarly define the golden ratio as

ϕ=def1+52.\phi \defeq \frac{1+\sqrt{5}}{2}.

The objects and variables within an expression are its terms. For instance, 55, x+2x + 2, and b24ac\sqrt{b^2 - 4ac} are all distinct terms.

Remark (On Notation).

Variables are typically denoted using single Latin or Greek letters. Common choices include:

  • Lowercase: a,b,c,i,j,k,m,n,p,q,x,y,za, b, c, i, j, k, m, n, p, q, x, y, z
  • Uppercase: A,B,C,D,M,N,P,Q,R,X,Y,ZA, B, C, D, M, N, P, Q, R, X, Y, Z
  • Greek: α,β,γ,δ,ϵ,θ,λ,μ,π,σ,τ,ϕ,ω\alpha, \beta, \gamma, \delta, \epsilon, \theta, \lambda, \mu, \pi, \sigma, \tau, \phi, \omega

Propositions and Truth Values

Mathematics, in its most basic form, is the practice of assigning truth to well-defined statements; it differs from other sciences in that its results are proven rigorously, as opposed to being hypothesized and then “confirmed” via experiements.

For these notes, most of our work amounts to taking a collection of statements which we already know to be true and using them to establish newer, more complex ones, or formulating statements whose truth or falsity we wish to determine. If we were to encounter a falsity, we would have to demonstrate that it is indeed false; so, we begin with the logic that connects what we know to what we wish to know.

The statements mathematicians study are called logical or mathematical statements or propositions, which we define as follows:

Definition 1.1 (Proposition).

A proposition is a grammatically correct declarative sentence that has a definite truth value.

By “grammatically correct,” we just mean that the words and symbols follow the rules of English (or any language you speak), and make sense.

Definition 1.2 (Truth Value).

The truth value of a proposition indicates whether the proposition is true or false. We abstract away the specific content of a statement to focus solely on its logical status, denoting ‘true’ with the symbol \top (read “top”) and ‘false’ with the symbol \bot (read “bot” or “bottom”).

The foundation of classical logic rests on the principle of bivalence, which states that every proposition is either true or false, but not both.

Example 1.3.

Some basic examples include:

  1. 2+3=52 + 3 = 5. (Truth value: \top)
  2. The integer 7 is even. (Truth value: \bot)
  3. For any real number xx, x20x^2 \geq 0. (Truth value: \top)
  4. Every even integer greater than 2 can be written as the sum of two prime numbers. (Truth value: unknown)
  5. The Earth is round. (Truth value: \top)

Example 4 is something to note: by the principle of bivalence, a sentence need not have a known truth value to qualify as a proposition; all that matters is that it makes logical sense to assign one; in fact, although the truth value of many propositions remains unknown, they are still valid propositions.

Remark.

Propositions like Example 4 are called conjectures, with Example 4 being known as the Goldbach Conjecture; in general, a conjecture is a claim believed to be true but which has not yet been proved or disproved.

By the principle of bivalence, we also see that many mathematical expressions and sentences are not propositions because they lack a definite truth value — imperative sentences (commands) and interrogative sentences (questions), for example, are naturally excluded.

Example 1.4.

The following are not propositions:

  1. x29x^2 - 9. (This is a term. Its value depends on xx, but it is not a complete sentence capable of carrying a truth value.)
  2. Solve the equation x29=0x^2 - 9 = 0. (An imperative command.)
  3. Is π\pi a rational number? (An interrogative question.)
  4. x>5x > 5. (This is something called an open sentence, but its truth value depends on the unspecified variable xx. It is a predicate, which will be addressed in later sections.)

Problem 1.1.

Suppose we say “Every even number greater than 2 can be written as the sum of two primes.” Is this a proposition?

Semantically Void and Self-Contradictory Sentences

Consider the following sentence: “The theory of relativity eats breakfast loudly.” Although it possesses a subject, verb, and adverb, the problem is that a scientific theory is an abstract concept which cannot eat; thus, because it describes a nonsensical scenario, there is no sensible way to assign a truth value to it — assigning \top is absurd, while assigning \bot would require that “The theory of relativity does not eat breakfast loudly” is a true statement, which is equally bizarre.

A more subtle challenge arises from paradoxes: sentences that are semantically meaningful but inherently are self-contradictory. Consider a page containing only the following sentence:

“The only proposition on this page is false.”

Attempting to assign a truth value to this sentence, denoted by PP, yields a contradiction:

  1. If PP is \top: Then the sentence asserts that PP is false; since it is the only proposition present, PP must evaluate to \bot, contradicting our initial assumption that PP is true.
  2. If PP is \bot: Then the sentence’s assertion that the only proposition on the page is false must itself be false. Since PP is the only proposition on the page, PP must therefore evaluate to \top, contradicting our initial assumption that PP is false.

Hence, as the sentence cannot be assigned a truth value, it is not a proposition.

Problem 1.2.

What happens if we do allow sentences like this to count as proper mathematical statements? What if we abandon the requirement that every statement we care about must be either true or false — is something fundamentally wrong, or have we simply entered a different logical universe?

In general, self-referential sentences like the one above, are quite bizarre and can produce some paradoxes that we want to disallow. By narrowing our scope strictly to propositions, we guarantee that our logical framework remains consistent, and most importantly suitable for automated reasoning and algorithmic verification (yes this is about Lean).

Problem 1.3.

Construct an example of a true proposition, a false proposition, a proposition whose truth value you do not currently know, a paradox, and a mathematical statement that is not a proposition.

Atomic Statements and the Structure of Mathematical Truth

To analyse complex (or compound) statements, we decompose them into their foundational components.

Definition 1.5 (Atomic Statement).

A statement is called atomic (or an atomic proposition) if it cannot be broken down into simpler constituent propositions.

For example, “5 is a prime number” is an atomic statement. Conversely, “5 is a prime number and 4 is an even number” is a complex statement built from two atomic components.

Remark.

We traditionally express these base components using propositional variables, denoted by lowercase letters such as p,q,r,sp, q, r, s.

By combining atomic statements into more complex structures, we can construct rigorous arguments in which certain statements support another, leading to the core mechanism of mathematics: proof.

Definition 1.6 (Proof).

A proof of a proposition is a verified logical argument demonstrating its truth. It must begin from known or assumed truths, proceed via agreed-upon valid logical steps, and be entirely verifiable by a knowledgeable reader.

As we build this mathematical architecture, the results we prove will be categorised by their structural role and intended usage:

  • Proposition: In addition to its logical meaning above, “proposition” is also commonly used as a label for a proved result, usually one of lesser or supporting importance than a theorem.
  • Theorem: A significant mathematical result.
  • Corollary: A result that follows as an immediate logical consequence of a theorem or proposition.

Logical Connectives

Thus far, we have mostly been working with atomic propositions; the next step is to combine statements into new statements using logical operators or connectives, where the truth value of the combined statement is based solely on the truth values of the original statements and on the type of logical operator facilitating the combination. These rules should make sense to you based on your understanding of the English language as a whole, but we also define them using a truth table (a table whose columns correspond to mathematical statements and their respective truth values), which lists the output truth value for every possible combination of truth values assigned to the input propositional variables.

Negation

The simplest logical operator is the negation operator, which produces the “opposite” of the original statement in the logical sense. It is actually a so-called unary operator, i.e., it does not combine statements but is merely applied to one statement. If pp is a statement, its negation, written ¬p\neg p, is the statement with the exact opposite truth value, usually produced by placing a “not” in the grammatically appropriate spot. For example, if pp is the statement “Jack is a boy,” then ¬p\neg p is the statement “Jack is not a boy,” or for another example if pp is the statement “31 is a prime number” (\top), then ¬p\neg p is the statement “31 is not a prime number” or, equivalently, “31 is composite” (\bot).

p¬p\begin{array}{c|c} p & \neg p \\ \hline \top & \bot \\ \bot & \top \end{array}

Problem 1.4.

We negated “31 is prime” to “31 is composite.” Does swapping “not prime” for “composite” work for every natural number, or did 31 get lucky?

Compound Sentences

Having seen how a unary operator acts on a single statement, we now proceed to binary logical operators, i.e., logical operators combining precisely two statements. Given two statements pp and qq, we can join them with an “and” or an “or” to build a complex statement whose truth value depends, in the way you would expect, on the truth values of pp and qq.

The conjunction of pp and qq, read ”pp and qq” and written pqp \land q, is true precisely when both pieces are true, and false otherwise.

pqpq\begin{array}{cc|c} p & q & p \land q \\ \hline \top & \top & \top\\ \top & \bot & \bot\\ \bot & \top & \bot\\ \bot & \bot & \bot \end{array}

Example 1.7.

Let pp be the proposition “2+3=5,” ss be the proposition “There exists a prime number greater than 1010010^{100},” and qq the statement “the sky is red.” Thus, because both are true, their conjunction psp \land s is true. Pairing pp with qq instead gives ”2+3=52 + 3 = 5 and the sky is red.” Here the first piece is true and the second is false, so pqp \land q is false.

Remark.

In English, conjunctions are frequently expressed using words such as “but,” “yet,” “while,” or “moreover.” The statement “A square has four sides, but a triangle has three vertices” serves the exact same logical function as a formal “and” statement.

The disjunction of pp and qq, read ”pp or qq” and written pqp \lor q, is true if at least one of the component propositions is true, and evaluates to false only when both pp and qq are false.

pqpq\begin{array}{c|c|c} p & q & p \lor q\\\hline \top & \top & \top\\ \top & \bot & \top\\ \bot & \top & \top\\ \bot & \bot & \bot \end{array}

Since both may hold at once, our “or” is what computer scientists call an inclusive or. The exclusive or, also known as XOR, on the other hand, denoted pqp \oplus q, evaluates to \top if exactly one of pp or qq is \top.

pqpq\begin{array}{c|c|c} p & q & p \oplus q\\\hline \top & \top & \bot\\ \top & \bot & \top\\ \bot & \top & \top\\ \bot & \bot & \bot \end{array}

Example 1.8.

Reusing our definitions of p,q,sp, q, s in the example block above, pqp \lor q is true, psp\lor s is true, but psp \oplus s is false.

Remark (On Ambiguity).

In everyday English, “or” is heavily context-dependent. The statement “Candidates must have a degree in mathematics or computer science” implies an inclusive or, as possessing both degrees is entirely acceptable. However, being offered “soup or a salad” with a meal implies an exclusive or, where choosing both is not an option. In mathematics, “or” strictly denotes the inclusive disjunction \lor unless specified otherwise.

Problem 1.5.

Suppose pqp \lor q is \top while pqp \land q is \bot. What do you know about pp and qq?

As you will have noted in the stated examples, logical operators can combine statements even when their meanings do not seem directly connected. While this might seem strange, adding restrictions based on content is neither needed nor helpful, because statements that appear unrelated can later become relevant within the same context. The same point applies to implications and equivalences, where the connection may initially seem even less intuitive.

”If-Then” Statements

Most statements we meet in these notes arrive as “If pp, then qq.” These are the conditional statements (or implications), written pqp \to q (or qpq \leftarrow p) and read ”pp implies qq”; within one, pp is called the hypothesis (or premise) and qq the conclusion. The logic of the implication is usually a little bit counter-intuitive to beginners so to be extra careful we can think of the statement pqp \to q to mean the same thing as “whenever pp is true, qq is also true”; i.e., pqp \to q evaluates to \bot in only one scenario: when pp is \top but qq is \bot.

Remark.

The key word here is “whenever”: pqp\to q claims that every situation in which pp is true is also one in which qq is true, so a situation where pp is false cannot violate the implication, regardless of the truth value of qq.

Example 1.9.

Consider the statement: “If the employee finishes the project by Friday (pp), then they will receive a bonus (qq)”:

  1. If pp is \top, qq is \top: The employee finishes on time and gets the bonus.
  2. If pp is \top, qq is \bot: The employee finishes on time, but does not receive the bonus. This contradicts the promise, so the statement is \bot.
  3. If pp is \bot, qq is \top: The employee misses the deadline but receives a bonus anyway (perhaps for previous good work). The original statement only specified what happens if the project is finished on time; it did not prohibit a bonus otherwise. The statement remains true.
  4. If pp is \bot, qq is \bot: The employee misses the deadline and receives no bonus. The statement remains true.

Cases 3 and 4 illustrate what is known as a vacuous truth: whenever the hypothesis is \bot, the implication places no restriction on the conclusion and therefore evaluates to \top automatically.

pqpq\begin{array}{cc|c} p & q & p \to q \\ \hline \top & \top & \top \\ \top & \bot & \bot \\ \bot & \top & \top \\ \bot & \bot & \top \end{array}

Problem 1.6.

“If 2+2=52 + 2 = 5, then 7 is prime” — true or false? What about “If 2+2=52 + 2 = 5, then 7 is composite”?

Problem 1.7.

I promise: “if it rains, I bring an umbrella.” You catch me carrying one under a cloudless sky. May you call me a liar?

Problem 1.8.

Show using a truth table that ¬p\neg p and pp \to \bot have the same truth values for every possible truth value of pp.

Another bit of confusion with these kind of statements comes from the word “implies,” as some use the word to convey some kind of causality. Take, for example the statement ”1+1=21+1=2 implies 1+2=31+2=3,” which is a true statement; many implications seem to follow this pattern, where the truth of the hypothesis seems to lead us to the truth on the conclusion, but this isnt the case in general!

Another example, “the sky being blue implies 2+2=42+2=4,” is a true statement, despite the color of the sky having nothing to do with 2+22+2 equaling 4; thus, the truth of pqp\to q, depends only on the truth values of pp and qq, regardless of if we can deduce the conclusion directly from the hypothesis (or if any meaningful connection between either even exist).

Granted, the implication pqp\to q is not really useful in situations, where the truth values of both pp and qq are already known; that is in a typical application, one tries to establish the truth of pp to prove the truth of qq (a strategy that will fail if pp happens to be false); it is important to keep in mind, that this is a consequence of the strategy not an undelying part of how conditional statements are defined.

Example 1.10.

Suppose we know that a particular bottle is stored in a wine rack. Let pp be the statement “The bottle contains red wine,” and let qq be the statement “There is at least one bottle of red wine in the rack.” A priori, we might not know whether the bottle contains red or white wine, but if we establish pp, then we can also establish qq. If instead we discover that the bottle contains white wine, then pp is false and the implication pqp\to q tells us nothing about whether qq is true or false, since there may still be some other bottle of red wine in the rack.

Finally, like conjuction, there are a plethora of ways to express implication in english; consider the implication pqp \to q, where pp is “It is raining” and qq is “The ground is wet,” assuming the implication evaluates to \top, one may also say:

  • If it rains, then the ground is wet.
  • The ground being wet is a consequence of it raining.
  • From “it is raining,” one may infer “the ground is wet.”
  • It raining is sufficient for the ground to be wet.
  • The ground being wet is necessary for it to rain.
  • It rains only if the ground is wet.

Problem 1.9.

The connectives introduced above are the standard primitives of propositional logic, but classical logic requires even fewer primitives than just these; in fact, every logical connective can be expressed using only negation and disjunction. Using this fact, express pqp\land q, and pqp\to q, only with ¬\neg and \lor, and verify each expression using a truth table. Can you find more than one expression for any of them?

Operator Precedence

Finally, before concluding this section, to preserve clarity and avoid an unreadable accumulation of parentheses in complex expressions, logical connectives adhere to a strict order of precedence. Operations are evaluated in the following hierarchy:

  1. Negation,
  2. Conjunction,
  3. Disjunction,
  4. Implication,

Under these rules, compound propositions are implicitly bracketed. For example, logical equivalence allows us to interpret expressions unambiguously without superfluous parentheses; ¬pq\neg p \lor q is the same as (¬p)q(\neg p) \lor q; likewise, pq¬rp \to q \lor \neg r means p(q(¬r))p \to (q \lor (\neg r)).

Remark.

The exclusive or lacks a universally standardised precedence level within this hierarchy; consequently, parentheses must always be explicitly written when incorporating it into compound statements.

Problem 1.10.

Consider the unparenthesised propositional formula ¬pqrp\neg p \lor q \to r \land p. First, rewrite this formula with all implicit parentheses explicitly shown, adhering strictly to the operator precedence hierarchy. Second, determine the final truth value of the formula given the assignment where pp is \top, qq is \bot, and rr is \bot.

Problem 1.11.

While multiplication distributes over addition (a×(b+c)=a×b+a×ca \times (b + c) = a \times b + a \times c), addition does not distribute over multiplication in real numbers. Provide an explicit counterexample showing that a+(b×c)(a+b)×(a+c)a + (b \times c) \neq (a + b) \times (a + c).

The Structure of Proof Systems

Having established a language of propositions, connectives, and truth tables, the natural question is: what can we actually do with all of this?

Although truth tables answer individual questions, they have several problems, one being that brute-force enumeration of every possible assignment scales poorly: a formula with nn atomic variables needs 2n2^n rows (quite obvious to see). Another, more fundamental, problem is that a truth table tells us that something is true without revealing why it is true, or how its truth connects to anything else. To patch this, we build what is called a proof system.

Formally, a proof system — pioneered by Gottlob Frege in 1879 — is a mechanism that uses axioms (assumed truths) and inference rules to mechanically derive new valid statements from existing ones. To achieve this, the system operates on two fundamental objects: statements (finite symbol strings expressing propositions) and proofs (the formal sequences justifying them). The relationship between these objects is governed by two rules:

  1. Semantics (Truth): A rule determining whether a given statement is true or false (the previous section used truth tables).
  2. Verification (Syntax): A procedure that decides if a specific string constitutes a valid proof for a given statement. This verification must be efficiently computable; a proof whose validity cannot be checked in reasonable time is useless.

The ultimate goal of a proof system is to align these two sides — ensuring that syntactic provability mirrors semantic truth. We measure this alignment through two key properties: Soundness: If a statement has a valid proof, it is true (no false statement possesses a valid proof) and Completeness: If a statement is true, a valid proof for it exists.

Remark (On Computational Efficiency).

In contrast to truth tables, verifying a formal proof requires only line-by-line pattern matching against inference rules, taking time proportional to the length of the proof itself. This fundamental asymmetry (that verifying a proof is computationally cheap even if finding one is hard) is the cornerstone of modern logic and computational complexity theory.

Example 1.11 (Primality).

Consider statements of the form “The integer nn is composite.”

  • Semantics: The statement is true if nn has a divisor dd such that 1<d<n1 < d < n.
  • Proof: A valid proof could simply be the divisor dd itself.
  • Verification: Divide nn by dd and check whether the remainder is zero.

The verification step is computationally cheap, even when finding the divisor dd is extraordinarily difficult.

Satisfiability

Before constructing proofs, we must classify propositions by the range of truth values they can assume. Not all compound propositions behave alike: some are always true, some are always false, and some depend on the assignment.

Definition 1.12 (Tautology).

A compound proposition is a tautology if it evaluates to \top under every possible assignment of truth values to its atomic variables.

Definition 1.13 (Contradiction).

A compound proposition is a contradiction if it evaluates to \bot under every possible assignment of truth values to its atomic variables.

Definition 1.14 (Contingency).

A compound proposition is a contingency if it is neither a tautology nor a contradiction; its truth value depends on the specific assignment.

A proposition is satisfiable if there exists at least one assignment under which it evaluates to \top. Every tautology and every contingency is satisfiable. A contradiction is unsatisfiable.

Example 1.15.

The proposition p¬pp \lor \neg p is a tautology (by the principle of bivalence, one of pp or ¬p\neg p must hold). The proposition p¬pp \land \neg p is a contradiction. The bare variable pp is a contingency.

To establish that a proposition is satisfiable, a single witness assignment suffices. To establish that it is unsatisfiable, one must check every assignment, which is precisely the expensive enumeration that motivates the algebraic approach developed below.

Problem 1.12.

Determine the satisfiability of (pqr)(¬p¬q¬r)(p \lor q \lor r) \land (\neg p \lor \neg q \lor \neg r). If satisfiable, provide a witness assignment. If unsatisfiable, justify your answer.

Logical Equivalence and Nonequivalence

Next, we need a way to decide when two statements are actually “the same,” at least in terms of their truth values. In particular, we may be able to prove that two statements have the same truth value for every possible assignment of the variables they contain.

From the logical operations and negation we can assemble statements of considerable complexity. Consider the formula ¬(pq)¬(pr)¬(qr).\neg(p \land q) \lor \neg(p \land r) \lor \neg(q \land r).

This is a disjunction of three terms; by the associativity of \lor (which we will prove shortly), the parentheses around the disjunction are irrelevant, and thus the formula is true exactly when at least one of the negated conjunctions is true. Now compare it with the much simpler expression ¬(pqr)\neg(p \land q \land r). Even a quick glance suggests they both express “at least one of p,q,rp,q,r is false.” Their truth tables confirm this equivalence in a single combined table:

pqr¬(pq)¬(pr)¬(qr)¬(pqr)\begin{array}{c|c|c|c|c} p & q & r & \neg(p \land q) \lor \neg(p \land r) \lor \neg(q \land r) & \neg(p \land q \land r)\\\hline \top & \top & \top & \bot & \bot\\ \top & \top & \bot & \top & \top\\ \top & \bot & \top & \top & \top\\ \top & \bot & \bot & \top & \top\\ \bot & \top & \top & \top & \top\\ \bot & \top & \bot & \top & \top\\ \bot & \bot & \top & \top & \top\\ \bot & \bot & \bot & \top & \top \end{array}

The two formulas agree on every row. This phenomenon deserves a name.

Definition 1.16 (Logical Equivalence).

Let pp and qq be statements built from the same simpler statements using ¬\neg, \land and \lor. They are logically equivalent, written pqp \equiv q, if every assignment of truth values to those simpler statements gives pp and qq the same value.

We can express this “same truth value” agreement directly in the language with a single connective.

Biconditional

Let pp and qq be statements, the biconditional, pqp \leftrightarrow q (read ”pp if and only if qq,” frequently abbreviated as “iff”) describes a relationship where two propositions strictly share the same truth value. For example, “A polygon is a triangle (pp) if and only if it has exactly three sides (qq).” If one is true, the other must be true; if one is false, the other must be false. Also note that when dealing with a biconditional pqp \leftrightarrow q, the proposition pp is said to be “necessary and sufficient” for qq.

pqpq\begin{array}{cc|c} p & q & p \leftrightarrow q \\ \hline \top & \top & \top \\ \top & \bot & \bot \\ \bot & \top & \bot \\ \bot & \bot & \top \end{array}

Equivalently, pqp \leftrightarrow q asserts both [(pq)(qp)(p \to q) \land (q \to p)]. If pp is true, then pqp \to q forces qq to be true; if pp is false, then qpq \to p forces qq to be false. Thus, in either case, pp and qq have the same truth value.

Problem 1.13.

Show using a truth table that pqp \leftrightarrow q and [(pq)(qp)(p \to q) \land (q \to p)] have the same truth values for every possible truth.

The biconditional gives us a convenient way to characterize logical equivalence. For any particular assignment, pqp \leftrightarrow q tells us whether pp and qq agree under that assignment. If they agree under every assignment, then the biconditional is always true.

Remark (Equivalence via Biconditional).

Equivalence can also be expressed in terms of a tautology: pqif and only if(pq) is a tautology.p \equiv q \quad\text{if and only if}\quad (p \leftrightarrow q) \text{ is a tautology.} This will be especially useful when we work algebraically, because it allows us to replace pqp \equiv q by the statement that pqp \leftrightarrow q reduces to \top.

The opposite situation is equally important.

Definition 1.17 (Logical Nonequivalence).

Two statements pp and qq are not logically equivalent, written p≢qp \not\equiv q, if there exists at least one assignment of truth values to their variables for which their resulting truth values differ. Such an assignment is termed a counterexample.

And thus finally, we now have all the tools to build a proof system.

Equivalence Proofs

We now introduce the axiomatic foundation that allows us to reason about propositional equivalences without enumerating truth tables. The axioms of classical propositional logic specify the algebraic behaviour of the connectives \land, \lor, and ¬\neg. Each axiom is a logical equivalence, asserting that two expressions are interchangeable in all contexts. The first five axiom pairs define a structure known as a Boolean algebra.

AxiomConjunctive FormDisjunctive FormIdentityppppComplement¬pp¬ppCommutativitypqqppqqpAssociativityp(qr)(pq)rp(qr)(pq)rDistributivityp(qr)(pq)(pr)p(qr)(pq)(pr)\begin{array}{lll} \textbf{Axiom} & \textbf{Conjunctive Form} & \textbf{Disjunctive Form} \\ \hline \text{Identity} & \top \land p \equiv p & \bot \lor p \equiv p \\ \text{Complement} & \neg p \land p \equiv \bot & \neg p \lor p \equiv \top \\ \text{Commutativity} & p \land q \equiv q \land p & p \lor q \equiv q \lor p \\ \text{Associativity} & p \land (q \land r) \equiv (p \land q) \land r & p \lor (q \lor r) \equiv (p \lor q) \lor r \\ \text{Distributivity} & p \land (q \lor r) \equiv (p \land q) \lor (p \land r) & p \lor (q \land r) \equiv (p \lor q) \land (p \lor r) \end{array}

The axioms govern only ¬\neg, \land, and \lor. To bring \to and \leftrightarrow within their reach we use the defining equivalences of the two conditional connectives, which rewrite them in terms of the core trio:

Conditional:pq¬pqBiconditional:pq(pq)(qp)(¬pq)(¬qp)\begin{aligned} \textbf{Conditional:} \quad & p \to q \equiv \neg p \lor q \\ \textbf{Biconditional:} \quad & p \leftrightarrow q \equiv (p \to q) \land (q \to p) \equiv (\neg p \lor q) \land (\neg q \lor p) \end{aligned}

Problem 1.14.

Feel free to pick any three axioms and prove them using a truth table.

From these axioms, we derive theorems. Recall Definition 1.6 : a proof begins from known truths and proceeds via valid logical steps. An equivalence proof is a chain of equivalences, each justified by an axiom, a definition, or a previously established theorem:

pp1,p1p2,,pnqpq.p \equiv p_1, \quad p_1 \equiv p_2, \quad \ldots, \quad p_n \equiv q \quad \to \quad p \equiv q.

The astute might ask: what logically permits us to stitch individual equivalences together into a single chain? Well this method relies on the principle of transitivity; we first show by truth table the closely related transitivity of implication, and then verify the transitivity of equivalence.

Let p,q,p, q, and rr be any propositions. We show that the transitivity of implication, ((pq)(qr))(pr)\bigl((p \to q) \land (q \to r)\bigr) \to (p \to r), is a tautology.

pqrpqqr(pq)(qr)pr((pq)(qr))(pr)\begin{array}{ccc|cc|c|c|c} p & q & r & p \to q & q \to r & (p \to q) \land (q \to r) & p \to r & \bigl((p \to q) \land (q \to r)\bigr) \to (p \to r) \\ \hline \top & \top & \top & \top & \top & \top & \top & \top \\ \top & \top & \bot & \top & \bot & \bot & \bot & \top \\ \top & \bot & \top & \bot & \top & \bot & \top & \top \\ \top & \bot & \bot & \bot & \top & \bot & \bot & \top \\ \bot & \top & \top & \top & \top & \top & \top & \top \\ \bot & \top & \bot & \top & \bot & \bot & \top & \top \\ \bot & \bot & \top & \top & \top & \top & \top & \top \\ \bot & \bot & \bot & \top & \top & \top & \top & \top \end{array}

The final column is \top in every row, so the formula is a tautology. Similarly, for any propositions p,q,p, q, and rr, we show that the transitivity of equivalence, ((pq)(qr))(pr)\bigl((p \leftrightarrow q) \land (q \leftrightarrow r)\bigr) \to (p \leftrightarrow r), is also a tautology.

pqrpqqr(pq)(qr)pr((pq)(qr))(pr)\begin{array}{ccc|cc|c|c|c} p & q & r & p \leftrightarrow q & q \leftrightarrow r & (p \leftrightarrow q) \land (q \leftrightarrow r) & p \leftrightarrow r & \bigl((p \leftrightarrow q) \land (q \leftrightarrow r)\bigr) \to (p \leftrightarrow r) \\ \hline \top & \top & \top & \top & \top & \top & \top & \top \\ \top & \top & \bot & \top & \bot & \bot & \bot & \top \\ \top & \bot & \top & \bot & \bot & \bot & \top & \top \\ \top & \bot & \bot & \bot & \top & \bot & \bot & \top \\ \bot & \top & \top & \bot & \top & \bot & \bot & \top \\ \bot & \top & \bot & \bot & \bot & \bot & \top & \top \\ \bot & \bot & \top & \top & \bot & \bot & \bot & \top \\ \bot & \bot & \bot & \top & \top & \top & \top & \top \end{array}

By the truth table, the transitivity of equivalence is likewise a tautology, fully justifying the chain-of-equivalences method. This method is vastly more efficient than truth tables for complex formulas (as we see below), though it requires algebraic ingenuity rather than mechanical enumeration.

Fundamental Theorems

Theorem 1.18 (Uniqueness of Complements).

For any propositions pp and qq, if pqp \land q \equiv \bot and pqp \lor q \equiv \top, then ¬pq\neg p \equiv q.

Proof.

Let pp and qq be arbitrary propositions satisfying pqp \land q \equiv \bot and pqp \lor q \equiv \top. We show that both ¬p\neg p and qq reduce to the same expression. First:

¬p¬pby Identity(¬p)by Commutativity(¬p)(pq)by assumption, pq(¬pp)(¬pq)by Distributivity(¬pq)by Complement¬pqby Identity\begin{aligned} \neg p &\equiv \top \land \neg p && \text{by Identity} \\ &\equiv (\neg p) \land \top && \text{by Commutativity} \\ &\equiv (\neg p) \land (p \lor q) && \text{by assumption, } p \lor q \equiv \top \\ &\equiv (\neg p \land p) \lor (\neg p \land q) && \text{by Distributivity} \\ &\equiv \bot \lor (\neg p \land q) && \text{by Complement} \\ &\equiv \neg p \land q && \text{by Identity} \end{aligned}

Similarly:

qqby Identityqby Commutativityq(p¬p)by Complement(qp)(q¬p)by Distributivity(pq)(¬pq)by Commutativity(¬pq)by assumption, pq¬pqby Identity\begin{aligned} q &\equiv \top \land q && \text{by Identity} \\ &\equiv q \land \top && \text{by Commutativity} \\ &\equiv q \land (p \lor \neg p) && \text{by Complement} \\ &\equiv (q \land p) \lor (q \land \neg p) && \text{by Distributivity} \\ &\equiv (p \land q) \lor (\neg p \land q) && \text{by Commutativity} \\ &\equiv \bot \lor (\neg p \land q) && \text{by assumption, } p \land q \equiv \bot \\ &\equiv \neg p \land q && \text{by Identity} \end{aligned}

Both ¬p\neg p and qq equal ¬pq\neg p \land q, hence ¬pq\neg p \equiv q.

Remark.

The symbol \blacksquare at the end of a proof is a modern substitute for the traditional Q.E.D., an initialism for the Latin phrase quod erat demonstrandum, meaning “what was to be shown.”

This theorem is the engine behind nearly every derivation that follows. It tells us that if something behaves like a complement (annihilates under \land, completes under \lor), then it is the complement. We now put it to work.

Corollary 1.19.

¬\top \equiv \neg \bot and ¬\bot \equiv \neg \top.

Proof.

By Identity, \bot \land \top \equiv \bot. By Commutativity and Identity, \bot \lor \top \equiv \top. The premises of Theorem 1.18 are satisfied with p=defp \defeq \bot and q=defq \defeq \top, yielding ¬\top \equiv \neg \bot. The second statement follows identically with p=defp \defeq \top, q=defq \defeq \bot.

Corollary 1.20 (Negative Equivalence).

For any propositions pp and qq, if pqp \equiv q, then ¬p¬q\neg p \equiv \neg q.

Proof.

Let pqp \equiv q. Then: q¬pp¬p(by assumption, then Complement),q \land \neg p \equiv p \land \neg p \equiv \bot \quad \text{(by assumption, then Complement),} and q¬pp¬p(by assumption, then Complement).q \lor \neg p \equiv p \lor \neg p \equiv \top \quad \text{(by assumption, then Complement).}

By Theorem 1.18 (with qq playing the role of pp and ¬p\neg p playing the role of qq), we conclude ¬q¬p\neg q \equiv \neg p.

Corollary 1.21.

For any propositions p,q,r,sp, q, r, s such that pqp \equiv q and rsr \equiv s:

  1. prqsp \land r \equiv q \land s
  2. prqsp \lor r \equiv q \lor s
  3. prqsp \to r \equiv q \to s
  4. prqsp \leftrightarrow r \equiv q \leftrightarrow s

Problem 1.15.

The proofs are straightforward applications of substitution and are left for the reader.

With Theorem 1.18 and its corollaries established, we can now derive the classical theorems of propositional logic.

Theorem 1.22 (Double Negation).

For any proposition pp, p¬¬pp \equiv \neg \neg p.

Proof.

By Complement (and Commutativity): ¬ppp¬p\neg p \land p \equiv p \land \neg p \equiv \bot and ¬ppp¬p\neg p \lor p \equiv p \lor \neg p \equiv \top. The premises of Theorem 1.18 are met with ¬p\neg p in the role of pp and pp in the role of qq. Therefore p¬(¬p)p \equiv \neg(\neg p).

Theorem 1.23 (Idempotence).

For any proposition pp, pppp \land p \equiv p and pppp \lor p \equiv p.

Proof.

For the conjunctive case:

pp(pp)by Identity(pp)(p¬p)by Complementp(p¬p)by Distributivitypby Complementpby Identity\begin{aligned} p \land p &\equiv (p \land p) \lor \bot && \text{by Identity} \\ &\equiv (p \land p) \lor (p \land \neg p) && \text{by Complement} \\ &\equiv p \land (p \lor \neg p) && \text{by Distributivity} \\ &\equiv p \land \top && \text{by Complement} \\ &\equiv p && \text{by Identity} \end{aligned}

The disjunctive case follows analogously:

pp(pp)by Identity(pp)(p¬p)by Complementp(p¬p)by Distributivitypby Complementpby Identity\begin{aligned} p \lor p &\equiv (p \lor p) \land \top && \text{by Identity} \\ &\equiv (p \lor p) \land (p \lor \neg p) && \text{by Complement} \\ &\equiv p \lor (p \land \neg p) && \text{by Distributivity} \\ &\equiv p \lor \bot && \text{by Complement} \\ &\equiv p && \text{by Identity} \end{aligned}

Theorem 1.24 (Domination).

For any proposition pp, p\top \lor p \equiv \top and p\bot \land p \equiv \bot.

Proof.

For the disjunctive fragment:

p(¬pp)pby Complement¬p(pp)by Associativity¬ppby Idempotence (Theorem 3)by Complement\begin{aligned} \top \lor p &\equiv (\neg p \lor p) \lor p && \text{by Complement} \\ &\equiv \neg p \lor (p \lor p) && \text{by Associativity} \\ &\equiv \neg p \lor p && \text{by Idempotence (Theorem 3)} \\ &\equiv \top && \text{by Complement} \end{aligned}

The conjunctive fragment:

p(¬pp)pby Complement¬p(pp)by Associativity¬ppby Idempotence (Theorem 3)by Complement\begin{aligned} \bot \land p &\equiv (\neg p \land p) \land p && \text{by Complement} \\ &\equiv \neg p \land (p \land p) && \text{by Associativity} \\ &\equiv \neg p \land p && \text{by Idempotence (Theorem 3)} \\ &\equiv \bot && \text{by Complement} \end{aligned}

Theorem 1.25 (Absorption).

For any propositions pp and qq, p(pq)pp \lor (p \land q) \equiv p and p(pq)pp \land (p \lor q) \equiv p.

Proof.

For the disjunctive case:

p(pq)(p)(pq)by Identityp(q)by Distributivitypby Domination (Theorem 4)pby Identity\begin{aligned} p \lor (p \land q) &\equiv (p \land \top) \lor (p \land q) && \text{by Identity} \\ &\equiv p \land (\top \lor q) && \text{by Distributivity} \\ &\equiv p \land \top && \text{by Domination (Theorem 4)} \\ &\equiv p && \text{by Identity} \end{aligned}

The conjunctive case:

p(pq)(p)(pq)by Identityp(q)by Distributivitypby Domination (Theorem 4)pby Identity\begin{aligned} p \land (p \lor q) &\equiv (p \lor \bot) \land (p \lor q) && \text{by Identity} \\ &\equiv p \lor (\bot \land q) && \text{by Distributivity} \\ &\equiv p \lor \bot && \text{by Domination (Theorem 4)} \\ &\equiv p && \text{by Identity} \end{aligned}

Theorem 1.26 (De Morgan's Laws).

For any propositions pp and qq, ¬(pq)¬p¬q\neg(p \land q) \equiv \neg p \lor \neg q and ¬(pq)¬p¬q\neg(p \lor q) \equiv \neg p \land \neg q.

Proof.

We prove ¬(pq)¬p¬q\neg(p \land q) \equiv \neg p \lor \neg q by applying Theorem 1.18 . We must show (pq)(¬p¬q)(p \land q) \land (\neg p \lor \neg q) \equiv \bot and (pq)(¬p¬q)(p \land q) \lor (\neg p \lor \neg q) \equiv \top.

The conjunctive branch:

(pq)(¬p¬q)p(q(¬p¬q))by Associativityp((q¬p)(q¬q))by Distributivityp((q¬p))by Complementp(q¬p)by Identityp(¬pq)by Commutativity(p¬p)qby Associativityqby Complementby Domination (Theorem 4)\begin{aligned} (p \land q) \land (\neg p \lor \neg q) &\equiv p \land (q \land (\neg p \lor \neg q)) && \text{by Associativity} \\ &\equiv p \land ((q \land \neg p) \lor (q \land \neg q)) && \text{by Distributivity} \\ &\equiv p \land ((q \land \neg p) \lor \bot) && \text{by Complement} \\ &\equiv p \land (q \land \neg p) && \text{by Identity} \\ &\equiv p \land (\neg p \land q) && \text{by Commutativity} \\ &\equiv (p \land \neg p) \land q && \text{by Associativity} \\ &\equiv \bot \land q && \text{by Complement} \\ &\equiv \bot && \text{by Domination (Theorem 4)} \end{aligned}

By Theorem 1.18 , ¬(pq)¬p¬q\neg(p \land q) \equiv \neg p \lor \neg q. The proof of ¬(pq)¬p¬q\neg(p \lor q) \equiv \neg p \land \neg q is analogous.

Problem 1.16.

Prove by equivalence proof that ¬(pq)¬p¬q\neg(p \lor q) \equiv \neg p \land \neg q (the second De Morgan’s Law).

Of course De Morgan’s Laws are not isolated identities; they are the first manifestation of a much broader symmetry between conjunction and disjunction. This relationship is captured by the notion of logical duality.

Definition 1.27 (Logical Duality).

Two binary logical connectives are dual when negating a compound expression built from one connective yields a formula that is logically equivalent to the compound expression built from the other connective, but with the inputs themselves negated.

Remark (Principle of Duality).

More generally, for any equivalence involving only \land, \lor, and ¬\neg, swapping every \land with \lor (and every \top with \bot) produces another valid equivalence. This is the Principle of Duality for Boolean algebra.

Conjunction and disjunction are the fundamental dual pair of classical logic. The two De Morgan’s Laws ¬(pq)¬p¬q,¬(pq)¬p¬q \neg(p \land q) \equiv \neg p \lor \neg q, \neg(p \lor q) \equiv \neg p \land \neg q show exactly that \land and \lor are dual to each other: negating an AND gives an OR of the negated parts, and negating an OR gives an AND of the negated parts.

Using this we extend the De Morgan’s Laws extend naturally to any finite number of propositions.

Corollary 1.28.

For any propositions p1,p2,,pnp_1,p_2,\ldots,p_n, ¬(p1p2pn)¬p1¬p2¬pn,\neg(p_1 \land p_2 \land \cdots \land p_n) \equiv \neg p_1 \lor \neg p_2 \lor \cdots \lor \neg p_n, and ¬(p1p2pn)¬p1¬p2¬pn.\neg(p_1 \lor p_2 \lor \cdots \lor p_n) \equiv \neg p_1 \land \neg p_2 \land \cdots \land \neg p_n.

Proof.

Since \land and \lor are dual, negating a conjunction exchanges \land for \lor while negating each of its components; hence ¬(p1pn)¬p1¬pn.\neg(p_1 \land \cdots \land p_n) \equiv \neg p_1 \lor \cdots \lor \neg p_n. By the same duality, negating a disjunction exchanges \lor for \land, giving ¬(p1pn)¬p1¬pn.\neg(p_1 \lor \cdots \lor p_n) \equiv \neg p_1 \land \cdots \land \neg p_n.

Problem 1.17.

Show that p(pq)p \land (p \to q) is a tautology, without using a truth table.

Equivalences Involving Conditionals

The defining equivalences of \to and \leftrightarrow allow us to derive every conditional equivalence by reducing implications to ¬,,\neg, \land, \lor and applying the theorems above:

pq¬pqpq¬q¬p(Contrapositive)pq¬pqpq¬(p¬q)¬(pq)p¬q\begin{aligned} p \to q &\equiv \neg p \lor q \\ p \to q &\equiv \neg q \to \neg p \quad \text{(Contrapositive)} \\ p \lor q &\equiv \neg p \to q \\ p \land q &\equiv \neg(p \to \neg q) \\ \neg(p \to q) &\equiv p \land \neg q \end{aligned} (pq)(pr)p(qr)(pr)(qr)(pq)r(pq)(pr)p(qr)(pr)(qr)(pq)r\begin{aligned} (p \to q) \land (p \to r) &\equiv p \to (q \land r) \\ (p \to r) \land (q \to r) &\equiv (p \lor q) \to r \\ (p \to q) \lor (p \to r) &\equiv p \to (q \lor r) \\ (p \to r) \lor (q \to r) &\equiv (p \land q) \to r \end{aligned} pq(pq)(qp)pq¬p¬qpq(pq)(¬p¬q)¬(pq)p¬q\begin{aligned} p \leftrightarrow q &\equiv (p \to q) \land (q \to p) \\ p \leftrightarrow q &\equiv \neg p \leftrightarrow \neg q \\ p \leftrightarrow q &\equiv (p \land q) \lor (\neg p \land \neg q) \\ \neg(p \leftrightarrow q) &\equiv p \leftrightarrow \neg q \end{aligned}

Notice the pattern in the implication equivalences: when implications share the same premise, the conclusions combine with the same connective (\land or \lor). When they share the same conclusion, the premises combine with the opposite connective. This “flip” from \land to \lor (and vice versa) is a direct consequence of the hidden negation in the definition of \to: the antecedent of an implication sits behind a ¬\neg, so De Morgan’s Laws invert the connective when premises are merged.

Contrapositive, Converse, and Inverse

Let pp and qq be mathematical statements. From an implication pqp \to q, three related conditionals arise:

  • The contrapositive ¬q¬p\neg q \to \neg p.
  • The converse qpq \to p.
  • The inverse ¬p¬q\neg p \to \neg q.

Something hinted at so far is that the direction of an implication matters: in general, reversing an implication does not preserve its truth. That is, even if pqp \to q is true, its converse qpq \to p need not be true.

Problem 1.18.

Using an equivalence proof, show that (pq)(¬q¬p)(p \to q) \equiv (\neg q \to \neg p) and (qp)(¬p¬q).(q \to p) \equiv (\neg p \to \neg q).

The first equivalence is particularly important. Since pq¬q¬p,p \to q \equiv \neg q \to \neg p, if we wish to prove pqp \to q, we may instead show ¬q¬p;\neg q \to \neg p; and this technique is one of the most useful methods of proof in mathematics (we see more of it later). However, because the converse is not determined by the truth value of the original implication whenever a mathematician proves a statement of the form pqp \to q, a natural follow-up question is whether the converse also happens to hold. This distinction is also the source of a common logical fallacy: Suppose we have established that pqp \to q; someone might object that qq does not necessarily imply pp, and therefore claim that the original argument is wrong, however, this objection confuses an implication with its converse.

Negating Conditional Statements

For the end of this specific section we ask: what does it mean for an implication itself to be false?

Recall that pqp \to q fails in exactly one situation: when pp is true and qq is false; expressing this algebraically using the conditional equivalence:

Theorem 1.29 (Negation of a Conditional).

For any propositions pp and qq, ¬(pq)p¬q.\neg(p \to q) \equiv p \land \neg q.

Proof.

¬(pq)¬(¬pq)by Conditional¬¬p¬qby De Morgan’sp¬qby Double Negation.\begin{aligned} \neg(p \to q) &\equiv \neg(\neg p \lor q) && \text{by Conditional} \\ &\equiv \neg\neg p \land \neg q && \text{by De Morgan's} \\ &\equiv p \land \neg q && \text{by Double Negation}. \end{aligned}

This has a useful interpretation: to show that an implication pqp \to q is false, one must exhibit a case in which the hypothesis pp holds but the conclusion qq fails. In other words, a counterexample to an implication is precisely a witness to p¬qp \land \neg q. It is worth distinguishing this from several superficially similar statements: neither ¬pq\neg p \to q nor p¬qp\to \neg q is the negation of pqp \to q. Anyway, we can negatate the biconditional similarly.

Theorem 1.30 (Negation of a Biconditional).

For any propositions pp and qq, ¬(pq)(p¬q)(q¬p).\neg(p \leftrightarrow q)\equiv(p \land \neg q) \lor (q \land \neg p).

Problem 1.19.

Prove the above theorem.

Thus, a biconditional is false exactly when pp and qq have different truth values; this is precisely the exclusive-or, relationship.

Equivalence Proofs in Practice

We now work through several examples that demonstrate the method and, simultaneously, show how Python can serve as a rapid sanity check.

Example 1.31.

Show that ¬(p(¬pq))¬p¬q\neg(p \lor (\neg p \land q)) \equiv \neg p \land \neg q.

¬(p(¬pq))¬p¬(¬pq)by De Morgan¬p(p¬q)by De Morgan & Double Negation(¬pp)(¬p¬q)by Distributivity(¬p¬q)by Complement¬p¬qby Identity\begin{aligned} \neg(p \lor (\neg p \land q)) &\equiv \neg p \land \neg(\neg p \land q) && \text{by De Morgan} \\ &\equiv \neg p \land (p \lor \neg q) && \text{by De Morgan \& Double Negation} \\ &\equiv (\neg p \land p) \lor (\neg p \land \neg q) && \text{by Distributivity} \\ &\equiv \bot \lor (\neg p \land \neg q) && \text{by Complement} \\ &\equiv \neg p \land \neg q && \text{by Identity} \end{aligned}

Example 1.32.

Show that (pq)(pq)(p \land q) \to (p \lor q) is a tautology.

(pq)(pq)¬(pq)(pq)by definition of (¬p¬q)(pq)by De Morgan (Theorem 6)(¬pp)(¬qq)by Associativity and Commutativityby Complementby Domination (Theorem 4)\begin{aligned} (p \land q) \to (p \lor q) &\equiv \neg(p \land q) \lor (p \lor q) && \text{by definition of $\to$} \\ &\equiv (\neg p \lor \neg q) \lor (p \lor q) && \text{by De Morgan (Theorem 6)} \\ &\equiv (\neg p \lor p) \lor (\neg q \lor q) && \text{by Associativity and Commutativity} \\ &\equiv \top \lor \top && \text{by Complement} \\ &\equiv \top && \text{by Domination (Theorem 4)} \end{aligned}

The formula reduces to \top with no surviving variables, confirming it is a tautology regardless of assignment.

Example 1.33.

Show that (pr)(qr)(pq)r(p \to r) \land (q \to r) \equiv (p \lor q) \to r.

Problem 1.20.

Prove the above result.

This result captures a natural proof strategy: to show that a disjunction implies something, it suffices to show that each disjunct separately implies it.

Example 1.34 (Negation of an Implication).

The negation of “If I think, then I am” (pqp \to q) is: ¬(pq)¬(¬pq)p¬q\neg(p \to q) \equiv \neg(\neg p \lor q) \equiv p \land \neg q by the definition of \to and De Morgan (Theorem 1.26 ). So the negation is “I think and I am not.”

Example 1.35 (XOR Distributivity).

Is \oplus distributive over \land and \lor?

The claim p(qr)(pq)(pr)p \land (q \oplus r) \equiv (p \land q) \oplus (p \land r) holds. Expanding both sides via the definition ab(a¬b)(¬ab)a \oplus b \equiv (a \land \neg b) \lor (\neg a \land b):

Left side:

p(qr)p((q¬r)(¬qr))(pq¬r)(p¬qr)p \land (q \oplus r) \equiv p \land ((q \land \neg r) \lor (\neg q \land r)) \equiv (p \land q \land \neg r) \lor (p \land \neg q \land r)

Right side:

(pq)(pr)((pq)¬(pr))(¬(pq)(pr))((pq)(¬p¬r))((¬p¬q)(pr))(pq¬p)(pq¬r)(¬ppr)(¬qpr)(pq¬r)(p¬qr)(pq¬r)(p¬qr)\begin{aligned} (p \land q) \oplus (p \land r) &\equiv ((p \land q) \land \neg(p \land r)) \lor (\neg(p \land q) \land (p \land r)) \\ &\equiv ((p \land q) \land (\neg p \lor \neg r)) \lor ((\neg p \lor \neg q) \land (p \land r)) \\ &\equiv (p \land q \land \neg p) \lor (p \land q \land \neg r) \lor (\neg p \land p \land r) \lor (\neg q \land p \land r) \\ &\equiv \bot \lor (p \land q \land \neg r) \lor \bot \lor (p \land \neg q \land r) \\ &\equiv (p \land q \land \neg r) \lor (p \land \neg q \land r) \end{aligned}

Both sides reduce to the same expression. However, p(qr)(pq)(pr)p \lor (q \oplus r) \equiv (p \lor q) \oplus (p \lor r) fails.

A single counterexample suffices: set pp \equiv \top, qq \equiv \top, rr \equiv \top.

()\top \lor (\top \oplus \top) \equiv \top \lor \bot \equiv \top()()(\top \lor \top) \oplus (\top \lor \top) \equiv \top \oplus \top \equiv \bot

Problem 1.21.

Using equivalence proofs (not truth tables), show that pq¬q¬pp \to q \equiv \neg q \to \neg p. This establishes the contrapositive equivalence from first principles.

Problem 1.22.

Show, using an equivalence proof, that (pq)(pr)p(qr)(p \to q) \lor (p \to r) \equiv p \to (q \lor r). Identify precisely where the “flip” from \lor to the structure of the result occurs, and which axiom is responsible.

Problem 1.23.

The negation of “Candidates must have a degree in mathematics or computer science” is not “Candidates must have a degree in mathematics and computer science.” Using the propositions pp = “The candidate has a degree in mathematics” and qq = “The candidate has a degree in computer science,” express the original statement formally as an implication and compute its negation. Identify the De Morgan’s Law involved.

Normal Forms

We Finish off this chapter with Normal forms.

The equivalence proofs developed demonstrate that any compound proposition can be transformed into an equivalent expression using only the core connectives ¬\neg, \land, and \lor. But this raises a question: given two arbitrary propositions, how do we determine whether they are equivalent without the algebraic ingenuity required for an equivalence proof? (excluding truth tables of course).

A normal form solves this by being a fixed structural template for propositional formulas: If two propositions are equivalent, their normal forms will be identical (after simplification). This converts the semantic question “do these formulas always agree?” into the syntactic question “do these strings match?” But before defining the two principal normal forms, we need some terminology.

Definition 1.36 (Literal).

A literal is a propositional variable or its negation. If pp is a propositional variable, then both pp and ¬p\neg p are literals.

Definition 1.37 (Clause).

A clause is a disjunction or conjunction of literals. A disjunctive clause (or simply a clause in the context of CNF) is a disjunction of literals. A conjunctive clause (or term) is a conjunction of literals.

Disjunctive Normal Form

Definition 1.38 (Disjunctive Normal Form).

A propositional formula is in Disjunctive Normal Form (DNF) if it consists of a disjunction of one or more terms, where each term is a conjunction of literals. That is, DNF has the shape:

(l1,1l1,2)(l2,1l2,2)(l_{1,1} \land l_{1,2} \land \cdots) \lor (l_{2,1} \land l_{2,2} \land \cdots) \lor \cdots

where each li,jl_{i,j} is a literal.

The structure is: OR of ANDs. Each conjunctive term describes one specific scenario under which the formula holds; the overall disjunction asserts that at least one of these scenarios is realised.

Example 1.39.

The following formulas are in DNF:

  1. (p¬q)(¬pq)(p \land \neg q) \lor (\neg p \land q). Two terms, each a conjunction of two literals.
  2. p(¬pq)p \lor (\neg p \land q). A single literal is a degenerate term (a conjunction of one literal).
  3. (p¬q¬r)(¬pqr)(p \land \neg q \land \neg r) \lor (\neg p \land q \land r).

The following formulas are not in DNF:

  1. (p¬q)¬(¬pq)(p \land \neg q) \lor \neg(\neg p \land q). The negation ¬(¬pq)\neg(\neg p \land q) is not a literal.
  2. (pq)(¬pq)(p \lor q) \land (\neg p \land q).
  3. ¬(¬pq)\neg(\neg p \lor q).

Constructing DNF from Truth Tables

Every compound proposition can be mechanically converted to DNF via its truth table via the procedure:

  1. Construct the truth table for the proposition.
  2. Identify every row where the proposition evaluates to \top.
  3. For each such row, form a conjunctive term: include the variable pp if it is assigned \top in that row, or ¬p\neg p if it is assigned \bot.
  4. Take the disjunction of all such terms.

Each term encodes exactly one satisfying assignment, and the disjunction collects them all.

Example 1.40.

Find the DNF of (pq)¬r(p \lor q) \to \neg r.

We construct the truth table:

pqr(pq)¬r\begin{array}{ccc|c} p & q & r & (p \lor q) \to \neg r \\ \hline \top & \top & \top & \bot \\ \top & \top & \bot & \top \\ \top & \bot & \top & \bot \\ \top & \bot & \bot & \top \\ \bot & \top & \top & \bot \\ \bot & \top & \bot & \top \\ \bot & \bot & \top & \top \\ \bot & \bot & \bot & \top \end{array}

Rows 2, 4, 6, 7, 8 evaluate to \top. Reading off each row:

(pq¬r)(p¬q¬r)(¬pq¬r)(¬p¬qr)(¬p¬q¬r)(p \land q \land \neg r) \lor (p \land \neg q \land \neg r) \lor (\neg p \land q \land \neg r) \lor (\neg p \land \neg q \land r) \lor (\neg p \land \neg q \land \neg r)

This is the full DNF. It can be simplified using the equivalence (pq)(p¬q)p(p \land q) \lor (p \land \neg q) \equiv p (which follows from Distributivity and Complement). Group the first two terms:

(pq¬r)(p¬q¬r)p¬r(p \land q \land \neg r) \lor (p \land \neg q \land \neg r) \equiv p \land \neg r

For the last three terms, observe that we may use Idempotence (Theorem 1.23 ) to duplicate the fifth term (¬p¬q¬r\neg p \land \neg q \land \neg r) without altering the formula. This allows two independent groupings:

(¬pq¬r)(¬p¬q¬r)¬p¬r(\neg p \land q \land \neg r) \lor (\neg p \land \neg q \land \neg r) \equiv \neg p \land \neg r(¬p¬qr)(¬p¬q¬r)¬p¬q(\neg p \land \neg q \land r) \lor (\neg p \land \neg q \land \neg r) \equiv \neg p \land \neg q

Combining:

(p¬r)(¬p¬r)(¬p¬q)¬r(¬p¬q)(p \land \neg r) \lor (\neg p \land \neg r) \lor (\neg p \land \neg q) \equiv \neg r \lor (\neg p \land \neg q)

Applying the definition of \to and De Morgan (Theorem 1.26 ) in reverse: ¬r(¬p¬q)¬r¬(pq)(pq)¬r\neg r \lor (\neg p \land \neg q) \equiv \neg r \lor \neg(p \lor q) \equiv (p \lor q) \to \neg r. The simplified DNF recovers the original formula, confirming equivalence.

Conjunctive Normal Form

Definition 1.41 (Conjunctive Normal Form).

A propositional formula is in Conjunctive Normal Form (CNF) if it consists of a conjunction of one or more clauses, where each clause is a disjunction of literals. That is, CNF has the shape:

(l1,1l1,2)(l2,1l2,2)(l_{1,1} \lor l_{1,2} \lor \cdots) \land (l_{2,1} \lor l_{2,2} \lor \cdots) \land \cdots

where each li,jl_{i,j} is a literal.

The structure is: AND of ORs, the dual of DNF. Each disjunctive clause represents a constraint that must be satisfied; the conjunction demands that every constraint holds simultaneously.

Example 1.42.

The following formulas are in CNF:

  1. (pq)(¬pq)(p \lor q) \land (\neg p \lor q).
  2. (pq¬r)(¬p¬q¬r)(p \lor q \lor \neg r) \land (\neg p \lor \neg q \lor \neg r).

The following formulas are not in CNF:

  1. (p¬q)(¬pq)(p \land \neg q) \lor (\neg p \land q).
  2. ¬(¬pq)\neg(\neg p \lor q).

Constructing CNF

There are two systematic methods for obtaining CNF.

Method 1: Algebraic manipulation. Eliminate all implications using the defining equivalences of \to and \leftrightarrow. Push negations inward using De Morgan’s Laws (Theorem 1.26 ) and Double Negation (Theorem 1.22 ). Then distribute \lor over \land using the equivalence p(qr)(pq)(pr)p \lor (q \land r) \equiv (p \lor q) \land (p \lor r) (the disjunctive form of Distributivity) until every clause is a disjunction of literals.

Method 2: Truth table (via negation of DNF). Observe that by Double Negation (Theorem 1.22 ), any proposition ϕ\phi satisfies ϕ¬(¬ϕ)\phi \equiv \neg(\neg \phi). Construct the DNF of ¬ϕ\neg \phi by reading off the rows where ϕ\phi evaluates to \bot (equivalently, where ¬ϕ\neg \phi evaluates to \top). Then negate the resulting DNF. By De Morgan’s Laws (Theorem 1.26 ), negating a disjunction of conjunctions produces a conjunction of disjunctions: precisely CNF.

Example 1.43.

Find the CNF of ¬(pq)(rp)\neg(p \to q) \lor (r \to p).

Method 1 (Algebraic):

¬(pq)(rp)¬(¬pq)(¬rp)by definition of (p¬q)(¬rp)by De Morgan and Double Negation(p¬rp)(¬q¬rp)by Distributivity(p¬r)(p¬q¬r)by Idempotence\begin{aligned} \neg(p \to q) \lor (r \to p) &\equiv \neg(\neg p \lor q) \lor (\neg r \lor p) && \text{by definition of $\to$} \\ &\equiv (p \land \neg q) \lor (\neg r \lor p) && \text{by De Morgan and Double Negation} \\ &\equiv (p \lor \neg r \lor p) \land (\neg q \lor \neg r \lor p) && \text{by Distributivity} \\ &\equiv (p \lor \neg r) \land (p \lor \neg q \lor \neg r) && \text{by Idempotence} \end{aligned}

Method 2 (Truth table):

pqr¬(pq)(rp)\begin{array}{ccc|c} p & q & r & \neg(p \to q) \lor (r \to p) \\ \hline \top & \top & \top & \top \\ \top & \top & \bot & \top \\ \top & \bot & \top & \top \\ \top & \bot & \bot & \top \\ \bot & \top & \top & \bot \\ \bot & \top & \bot & \top \\ \bot & \bot & \top & \bot \\ \bot & \bot & \bot & \top \end{array}

The formula evaluates to \bot in rows 5 and 7. Form the DNF of the negation by reading these rows: (¬pqr)(¬p¬qr),(\neg p \land q \land r) \lor (\neg p \land \neg q \land r), and simplify, thus giving (¬pqr)(¬p¬qr)¬pr(\neg p \land q \land r) \lor (\neg p \land \neg q \land r) \equiv \neg p \land r. Now negate: ¬(¬pr)p¬r\neg(\neg p \land r) \equiv p \lor \neg r by De Morgan (Theorem 1.26 ) and Double Negation (Theorem 1.22 ). This is already in CNF.

Remark.

Method 2 produced (p¬r)(p \lor \neg r), while Method 1 produced (p¬r)(p¬q¬r)(p \lor \neg r) \land (p \lor \neg q \lor \neg r). These are equivalent: the second clause in Method 1’s result is absorbed by the first via Absorption (Theorem 1.25 ), since any assignment satisfying (p¬r)(p \lor \neg r) automatically satisfies (p¬q¬r)(p \lor \neg q \lor \neg r).

The Cost of Canonicality

Normal forms guarantee a canonical structure, but this guarantee comes at a price. Converting between normal forms can cause an exponential blowup in the number of clauses.

Consider a formula already in DNF with nn terms:

(p1q1)(p2q2)(pnqn)(p_1 \land q_1) \lor (p_2 \land q_2) \lor \cdots \lor (p_n \land q_n)

To convert this to CNF, we must distribute \lor over \land repeatedly. Each application of Distributivity doubles the number of clauses. Starting with (p1q1)(p2q2)(p_1 \land q_1) \lor (p_2 \land q_2):

(p1q1)(p2q2)(p1p2)(p1q2)(q1p2)(q1q2)(p_1 \land q_1) \lor (p_2 \land q_2) \equiv (p_1 \lor p_2) \land (p_1 \lor q_2) \land (q_1 \lor p_2) \land (q_1 \lor q_2)

Two terms in DNF produce four clauses in CNF. Adjoining a third term (p3q3)(p_3 \land q_3) via disjunction and distributing again doubles to eight clauses. After nn terms, the CNF may contain up to 2n2^n clauses. The symmetric explosion occurs when converting CNF to DNF.

This exponential blowup is an intrinsic property of the normal forms themselves. It is also the reason why the satisfiability of CNF formulas (the SAT problem) occupies a central position in complexity theory: determining whether a CNF formula has a satisfying assignment is the canonical NP-complete problem, meaning that no known algorithm solves it efficiently in all cases.

Problem 1.24.

Find the DNF of p(qr)p \to (q \land r) using the truth table method. Simplify the result.

Problem 1.25.

Convert (pq)(¬pr)(p \lor q) \land (\neg p \lor r) into DNF using algebraic manipulation (Distributivity, not truth tables). Verify your result computationally.

Problem 1.26.

Find the CNF of (pq)(¬pr)(p \land q) \lor (\neg p \land r) using both methods (algebraic and truth table). Confirm that both methods yield equivalent results.

Application: Knights and Knaves

Normal forms and propositional reasoning converge naturally in logic puzzles, where the challenge is to deduce facts from constrained declarations. Consider the following scenario.

On an island, every inhabitant is either a knight (who always tells the truth) or a knave (who always lies). You encounter two inhabitants, AA and BB.

  • AA says: “B is a knight.”
  • BB says: “The two of us are of opposite types.”

Let pp denote ”AA is a knight” and qq denote ”BB is a knight.” We translate the scenario into propositional logic.

  • If AA is a knight (pp is \top): then AA‘s statement is true, so qq is \top. If AA is a knave (pp is \bot), then AA‘s statement is false, so qq is \bot. In both cases, AA‘s declaration encodes pqp \leftrightarrow q.
  • BB’s statement asserts that AA and BB are of opposite types, which means exactly one of p,qp, q is \top: this is pqp \oplus q. If BB is a knight (qq is \top), then pqp \oplus q must be \top. If BB is a knave (qq is \bot), then pqp \oplus q must be \bot. So BB‘s declaration encodes q(pq)q \leftrightarrow (p \oplus q).

The full constraint is thus (pq)(q(pq)).(p \leftrightarrow q) \land (q \leftrightarrow (p \oplus q)).

  • Case 1: Assume pp is \top. From pqp \leftrightarrow q, we get qq is \top. Then pqp \oplus q \equiv \top \oplus \top \equiv \bot. But q(pq)q \leftrightarrow (p \oplus q) \equiv \top \leftrightarrow \bot \equiv \bot. The conjunction evaluates to \bot. Contradiction.

  • Case 2: Assume pp is \bot. From pqp \leftrightarrow q, we get qq is \bot. Then pqp \oplus q \equiv \bot \oplus \bot \equiv \bot. And q(pq)q \leftrightarrow (p \oplus q) \equiv \bot \leftrightarrow \bot \equiv \top. The conjunction evaluates to \top.

Therefore both AA and BB are knaves.

Problem 1.27.

On the same island, you meet three inhabitants AA, BB, and CC. AA says: “All of us are knaves.” BB says: “Exactly one of us is a knight.” Using propositional variables pp, qq, rr for AA, BB, CC respectively, determine the types of all three inhabitants. Verify your solution computationally.

Exercises

 

Answers are checked in your browser, as often as you like. Nothing is sent anywhere and nothing is kept but your own work. A formula may be written with the symbols themselves or with ~ & | -> <-> ^, and \and, \or, \to expand as you type.

Exercise 1.1.

For each implication below, which of the four statements is its converse?

If it is raining, then the ground is wet.

answer one of these

If nn is divisible by 4, then nn is even.

answer one of these

If a function is differentiable, then it is continuous.

answer one of these

Exercise 1.2.

Construct a compound proposition in pp, qq and uu that is true exactly when:

pp is true, qq is false and uu is false.

answer formula

exactly one of pp, qq, uu is true.

answer formula

at least two of pp, qq, uu are true.

answer formula

Exercise 1.3.

The exclusive or does not distribute over conjunction: p(qu)≢(pq)(pu)p \oplus (q \land u) \not\equiv (p \oplus q) \land (p \oplus u). Give an assignment at which the two sides differ.

answer assignment
p q u

Exercise 1.4.

Write each of the following with the connectives named and no others.

¬pq\neg p \leftrightarrow q, in \oplus.

answer formula

p¬qp \leftrightarrow \neg q, in \oplus.

answer formula

pqp \leftrightarrow q, in \oplus and ¬\neg.

answer formula

Exercise 1.5.

Find the disjunctive normal form of (pq)(qr)(p \to q) \land (q \to r), simplified as far as it will go.

answer formula

Exercise 1.6.

Find the conjunctive normal form of p(qr)p \to (q \oplus r), simplified as far as it will go.

answer formula

Exercise 1.7.

The compound proposition ((¬pq)(rq))(¬sp)((\neg p \land q) \to (r \oplus q)) \lor (\neg s \leftrightarrow p) involves four propositional variables. Settle it without constructing the sixteen-row truth table.

An assignment at which it is true.

answer assignment
p q r s

An assignment at which it is false.

answer assignment
p q r s

The proposition is therefore:

answer one of these

Exercise 1.8.

On an island, knights always tell the truth and knaves always lie. Person AA says: “If I am a knight, then BB is a knight.” Determine what AA and BB are.

answer one of these

Exercises in Lean

 

The proofs below are checked in your browser. Nothing is sent anywhere, and nothing is stored but your own work. Type \to for →, \and for ∧, \< and \> for ⟨ ⟩.

Everything above this point was checked by hand. Lean is a language in which a statement and its proof are written so that a machine can check them instead, and it is what the rest of these notes will be verified in. This sheet is where we learn to write in it.

Each box below holds one statement. The grey lines are given and cannot be edited; the lines under them are ours to write, one tactic to a line. Underneath the box sits the info view, which shows what is left to prove and follows the cursor: put the caret between two lines of a proof and it reports the state at that point, which is the only way to see what a tactic has actually done.

Statements and proofs

p : Prop reads ”pp is a statement”, something that is either true or false. hp : p reads “hp is a proof of pp”, and assuming pp amounts to the same thing, since a hypothesis is a proof we were handed rather than one we made.

A goal is shown as a list of hypotheses, a turnstile, and then the statement to be proved. What stands above the ⊢ we may use; what stands after it we must reach. A proof is finished when no goals are left.

Implication

Three tactics prove everything in this part.

intro

To prove pqp \to q we may assume pp and prove qq from it. So if the goal is ⊢ p → q, then intro hp takes that assumption, names it hp, and leaves the goal ⊢ q. Several may be taken at once: intro hp hq.

exact

If a hypothesis is exactly the statement we are trying to prove, exact hp closes the goal. Note that exact p does not: p is the statement and hp is a proof of it, and it is proofs that close goals.

Example.

Three assumptions, one of which is what we want.

lean worked
1example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p := by
verified
goalGoals accomplished.

apply

apply argues backwards. If the goal is qq and we hold h : p → q, then it is enough to prove pp, so apply h replaces the goal ⊢ q with ⊢ p. It works only when the conclusion of h is the goal.

Implications also apply forwards, and read left to right: with h : p → q and hp : p, the term h hp is a proof of qq. So exact h hp closes in one line what apply h and then exact hp closes in two.

Example.

The goal is an arrow, so we may assume its left side. What we assume is never used again.

lean worked
1example (p q : Prop) (hq : q) : p  q := by
verified
goalGoals accomplished.

Example.

Backwards, in two steps. Putting exact h hp in place of both lines does the same work forwards.

lean worked
1example (p q : Prop) (h : p  q) (hp : p) : q := by
verified
goalGoals accomplished.

An arrow chain groups to the right: p → q → r is p → (q → r), so to reach rr we must supply both a pp and a qq. If h : p → q → r and the goal is ⊢ r, then apply h leaves two goals rather than one, and a tactic acts only on the first of them.

Exercise 1.9.

Every statement implies itself.

lean proof
1example (p : Prop) : p  p := by
goalp : Prop p p

Exercise 1.10.

A statement that holds goes on holding under a further assumption.

lean proof
1example (p q : Prop) : p  q  p := by
goalp q : Prop p q p

Exercise 1.11.

From pp, together with pqp \to q, reach qq.

lean proof
1example (p q : Prop) : p  (p  q)  q := by
goalp q : Prop p (p q) q

Exercise 1.12.

Implication is transitive.

lean proof
1example (p q r : Prop) : (p  q)  (q  r)  (p  r) := by
goalp q r : Prop (p q) (q r) p r

Exercise 1.13.

If rr follows from pp and qq together, and qq follows from pp, then rr follows from pp alone.

lean proof
1example (p q r : Prop) : (p  q  r)  (p  q)  (p  r) := by
goalp q r : Prop (p q r) (p q) p r

True and False

True is Lean’s \top and False is its \bot. Each is a statement like any other, and each has a tactic of its own.

trivial

trivial closes the goal ⊢ True, which asks for nothing.

Example.

The hypothesis plays no part. Nothing is needed to prove \top.

lean worked
1example (p : Prop) (hp : p) : True := by
verified
goalGoals accomplished.

exfalso

Since \bot implies everything, a proof of \bot is a proof of anything, and exfalso replaces the goal, whatever it was, with ⊢ False. It is the move to make when the hypotheses already contradict each other, because the contradiction is then the whole of what remains.

Example.

Nothing is known about qq, and nothing needs to be.

lean worked
1example (q : Prop) (h : False) : q := by
verified
goalGoals accomplished.

Exercise 1.14.

The true statement holds.

lean proof
1example : True := by
goal True

Exercise 1.15.

Anything at all implies the true statement.

lean proof
1example : False  True := by
goal False True

Exercise 1.16.

The true statement does not imply the false one.

lean proof
1example : (True  False)  False := by
goal (True False) False

Exercise 1.17.

And anything follows from the claim that it does.

lean proof
1example (p : Prop) : (True  False)  p := by
goalp : Prop (True False) p

Exercise 1.18.

From pp and a refutation of pp, any qq follows.

lean proof
1example (p q : Prop) : (p  False)  p  q := by
goalp q : Prop (p False) p q

Negation

In Lean ¬p is not a connective of its own. It is defined to be p → False, so the two are one statement and either may be given where the other is asked for. A proof of ¬p is therefore a thing that turns a proof of pp into a contradiction: intro opens a goal ⊢ ¬p exactly as it opens an arrow, and if hnp : ¬p and hp : p then hnp hp is a proof of False.

Example.

The negation is applied to the proof it refutes.

lean worked
1example (p : Prop) (hp : p) (hnp : ¬p) : False := by
verified
goalGoals accomplished.

by_contra

To prove pp by contradiction we assume ¬p\neg p and derive \bot. Where the goal is ⊢ p, by_contra hp adds hp : ¬p and changes the goal to ⊢ False. This is the one classical step available here: it is the law of excluded middle in the form of a tactic, and the exercises that need it are the ones that cannot be done without it.

Exercise 1.19.

The two readings of ¬p\neg p are one statement.

lean proof
1example (p : Prop) : ¬p  (p  False) := by
goalp : Prop ¬p p False

Exercise 1.20.

The false statement can be refuted.

lean proof
1example : ¬False := by
goal ¬False

Exercise 1.21.

A statement implies its double negation.

lean proof
1example (p : Prop) : p  ¬¬p := by
goalp : Prop p ¬¬p

Exercise 1.22.

An implication yields its contrapositive.

lean proof
1example (p q : Prop) : (p  q)  (¬q  ¬p) := by
goalp q : Prop (p q) ¬q ¬p

Exercise 1.23.

And the contrapositive yields the implication back.

lean proof
1example (p q : Prop) : (¬q  ¬p)  (p  q) := by
goalp q : Prop (¬q ¬p) p q
What the checker understands

Tactics

intro h assume the hypothesis of an implication, naming it h
exact e give the proof outright
apply f reduce the goal to the hypotheses of f
assumption close the goal with a hypothesis already present
trivial close the goal True
exfalso replace the goal with False
by_contra h assume the negation of the goal

Results you may cite

Classical.em (a : Prop), a ¬a — the law of excluded middle
Classical.byContradiction {a : Prop}, (¬a False) a — proof by contradiction; the tactic by_contra does this for you
Classical.byCases {a b : Prop}, (a b) (¬a b) b — split on whether a holds
not_not {a : Prop}, ¬¬a a — double negation
not_and_or {a b : Prop}, ¬(a b) ¬a ¬b — De Morgan
not_or {a b : Prop}, ¬(a b) ¬a ¬b — De Morgan
not_imp {a b : Prop}, ¬(a b) a ¬b
and_comm {a b : Prop}, a b b a
or_comm {a b : Prop}, a b b a

From the logical core

And.intro {a b : Prop}, a b a b
And.left {a b : Prop}, a b a
And.right {a b : Prop}, a b b
And.symm {a b : Prop}, a b b a
Or.inl {a b : Prop}, a a b
Or.inr {a b : Prop}, b a b
Or.elim {a b c : Prop}, a b (a c) (b c) c
Or.symm {a b : Prop}, a b b a
Iff.intro {a b : Prop}, (a b) (b a) (a b)
Iff.mp {a b : Prop}, (a b) a b
Iff.mpr {a b : Prop}, (a b) b a
Iff.symm {a b : Prop}, (a b) (b a)
Iff.rfl {a : Prop}, a a
Iff.trans {a b c : Prop}, (a b) (b c) (a c)
True.intro True
False.elim {a : Prop}, False a
absurd {a b : Prop}, a ¬a b
id {a : Prop}, a a
mt {a b : Prop}, (a b) ¬b ¬a
Eq.refl {α : Type} (a : α), a = a
Eq.symm {α : Type} {a b : α}, a = b b = a
Eq.trans {α : Type} {a b c : α}, a = b b = c a = c
congrArg {α : Type} {β : Type} {a b : α} (f : α β), a = b f a = f b
Exists.intro {α : Type} {p : α Prop} (w : α), p w x : α, p x
Exists.elim {α : Type} {p : α Prop} {b : Prop}, ( x : α, p x) ( y : α, p y b) b