Source / pinned edition
The Open Logic Text
Source of package logic.methods · The Open Logic Text (Open Logic Project), commit 1e960be
- work
- urn:logic:clir:methods#OPEN_LOGIC
- number
- The Open Logic Text (Open Logic Project), commit 1e960be
- kind
- urn:logic:clir:methods#treatise
content/methods/induction/induction.tex at commit 1e960be (master, 2026-08-14)
- edition
- urn:logic:clir:methods#OLP_MTH_INDUCTION_INDUCTION_ED
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- adopted: 2026-08-14
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/induction/induction.tex | application/x-tex; charset=utf-8 | sha256:a473475ad8fdd83af7da9474e389385d9b3fc9b0fe3673fbb7dc9c6a413df5af | 2026-09-08T00:00:00Z |
Fragments — 1
content/methods/induction/induction.tex · section · referenced by: 8
en · official · sha256:621e792077ccf2d458e3afa40ab1b3ca4ba65337a4de3a726059bb2fdbde15b8
% Part: methods
% Chapter: induction
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olchapter{mth}{ind}{Induction}
\olimport{introduction}
\olimport{induction-on-N}
\olimport{strong-induction}
\olimport{inductive-definitions}
\olimport{structural-induction}
\olimport{relations}
\OLEndChapterHook
\end{document}Referencing norms: M_INDUCTION, RunsOver, ST_IND_1, ST_IND_2, ST_IND_3, ST_IND_4, method_over_structure, runs_over
content/methods/induction/induction-on-N.tex at commit 1e960be (master, 2026-08-14)
- edition
- urn:logic:clir:methods#OLP_MTH_INDUCTION_INDUCTION_ON_N_ED
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- adopted: 2026-08-14
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/induction/induction-on-N.tex | application/x-tex; charset=utf-8 | sha256:30a7fe3bf67517b5744d826eeb819782d399cf28a018313f5a7eff12843fe222 | 2026-09-08T00:00:00Z |
Fragments — 1
content/methods/induction/induction-on-N.tex · section · referenced by: 2
en · official · sha256:7c909ee315b414a82b62a1bf34fccddeb91dc54c3f9bd3045ccf0ef73182a57f
% Part: methods
% Chapter: induction
% Section: induction-on-N
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{mth}{ind}{inN}
\olsection{Induction on~$\Nat$}
In its simplest form, induction is a technique used to prove results
for all natural numbers. It uses the fact that by starting from $0$
and repeatedly adding~$1$ we eventually reach every natural number. So
to prove that something is true for every number, we can (1)~establish
that it is true for $0$ and (2)~show that whenever it is true for a
number~$n$, it is also true for the next number~$n+1$. If we
abbreviate ``number~$n$ has property $P$'' by $P(n)$ (and ``number~$k$
has property $P$'' by $P(k)$, etc.), then a proof by induction that
$P(n)$ for all $n \in \Nat$ consists of:
\begin{enumerate}
\item a proof of $P(0)$, and
\item a proof that, for any~$k$, if $P(k)$ then $P(k+1)$.
\end{enumerate}
To make this crystal clear, suppose we have both (1) and~(2). Then
(1) tells us that $P(0)$ is true. If we also have~(2), we know in
particular that if $P(0)$ then $P(0+1)$, i.e., $P(1)$. This follows
from the general statement ``for any~$k$, if $P(k)$ then $P(k+1)$'' by
putting~$0$ for~$k$. So by modus ponens, we have that~$P(1)$. From (2)
again, now taking $1$ for~$n$, we have: if $P(1)$ then~$P(2)$. Since
we've just established~$P(1)$, by modus ponens, we have~$P(2)$. And so
on. For any number~$n$, after doing this $n$~times, we eventually
arrive at~$P(n)$. So (1) and~(2) together establish~$P(n)$ for any $n
\in \Nat$.
Let's look at an example. Suppose we want to find out how many
different sums we can throw with $n$ dice. Although it might seem
silly, let's start with $0$ dice. If you have no dice there's only one
possible sum you can ``throw'': no dots at all, which sums to~$0$. So
the number of different possible throws is~$1$. If you have only one
die, i.e., $n=1$, there are six possible values, $1$ through~$6$. With
two dice, we can throw any sum from $2$ through $12$, that's $11$
possibilities. With three dice, we can throw any number from $3$ to
$18$, i.e., $16$ different possibilities. $1$, $6$, $11$, $16$: looks
like a pattern: maybe the answer is $5n+1$? Of course, $5n+1$ is the
maximum possible, because there are only $5n+1$ numbers between $n$,
the lowest value you can throw with $n$ dice (all $1$'s) and $6n$, the
highest you can throw (all $6$'s).
\begin{thm}
With $n$ dice one can throw all $5n+1$ possible values between $n$
and $6n$.
\end{thm}
\begin{proof}
Let $P(n)$ be the claim: ``It is possible to throw any number between
$n$ and~$6n$ using $n$~dice.'' To use induction, we prove:
\begin{enumerate}
\item The \emph{induction basis} $P(1)$, i.e., with just one die,
you can throw any number between $1$ and $6$.
\item The \emph{induction step}, for all $k$, if $P(k)$ then~$P(k+1)$.
\end{enumerate}
(1) Is proved by inspecting a $6$-sided die. It has all 6 sides, and
every number between $1$ and~$6$ shows up one on of the sides. So it
is possible to throw any number between $1$ and~$6$ using a single
die.
To prove (2), we assume the antecedent of the conditional, i.e.,
$P(k)$. This assumption is called the \emph{inductive hypothesis}. We
use it to prove~$P(k+1)$. The hard part is to find a way of thinking
about the possible values of a throw of $k+1$ dice in terms of the
possible values of throws of $k$~dice plus of throws of the extra
$k+1$-st die---this is what we have to do, though, if we want to use
the inductive hypothesis.
The inductive hypothesis says we can get any number between $k$
and~$6k$ using $k$~dice. If we throw a~$1$ with our $(k+1)$-st die,
this adds $1$ to the total. So we can throw any value between $k+1$
and $6k+1$ by throwing $k$~dice and then rolling a~$1$ with the
$(k+1)$-st die. What's left? The values $6k+2$ through $6k+6$. We
can get these by rolling $k$ $6$s and then a number between $2$ and
$6$ with our $(k+1)$-st die. Together, this means that with $k+1$ dice
we can throw any of the numbers between $k+1$ and $6(k+1)$, i.e.,
we've proved~$P(k+1)$ using the assumption~$P(k)$, the inductive
hypothesis.
\end{proof}
Very often we use induction when we want to prove something about a
series of objects (numbers, sets, etc.) that is itself defined
``inductively,'' i.e., by defining the $(n+1)$-st object in terms of
the $n$-th. For instance, we can define the sum~$s_n$ of the natural
numbers up to~$n$ by
\begin{align*}
s_0 & = 0\\
s_{n+1} & = s_n + (n+1)
\end{align*}
This definition gives:
\begin{align*}
s_0 & = 0,\\
s_1 & = s_0 + 1 && = 1,\\
s_2 & = s_1 + 2 && = 1 + 2 = 3\\
s_3 & = s_2 + 3 && = 1 + 2 + 3 = 6, \text{ etc.}
\end{align*}
Now we can prove, by induction, that $s_n = n(n+1)/2$.
\begin{prop}
$s_n = n(n+1)/2$.
\end{prop}
\begin{proof}
We have to prove (1) that $s_0 = 0\cdot(0 + 1)/2$ and (2) if $s_k =
k(k+1)/2$ then $s_{k+1} = (k+1)(k+2)/2$. (1) is obvious. To prove
(2), we assume the inductive hypothesis: $s_k = k(k+1)/2$. Using it,
we have to show that $s_{k+1} = (k+1)(k+2)/2$.
What is $s_{k+1}$? By the definition, $s_{k+1} = s_k + (k+1)$. By
inductive hypothesis, $s_k = k(k+1)/2$. We can substitute this into
the previous equation, and then just need a bit of arithmetic of
fractions:
\begin{align*}
s_{k+1} & = \frac{k(k+1)}{2} + (k+1) = {}\\
& = \frac{k(k+1)}{2} + \frac{2(k+1)}{2} = {}\\
& = \frac{k(k+1) + 2(k+1)}{2} = {}\\
& = \frac{(k+2)(k+1)}{2}.
\end{align*}
\end{proof}
The important lesson here is that if you're proving something about
some inductively defined sequence $a_n$, induction is the obvious way
to go. And even if it isn't (as in the case of the possibilities of
dice throws), you can use induction if you can somehow relate the case
for~$k+1$ to the case for~$k$.
\end{document}Referencing norms: NATURAL_NUMBERS, P_INDUCTION_N
content/methods/induction/structural-induction.tex at commit 1e960be (master, 2026-08-14)
- edition
- urn:logic:clir:methods#OLP_MTH_INDUCTION_STRUCTURAL_INDUCTION_ED
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- adopted: 2026-08-14
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/induction/structural-induction.tex | application/x-tex; charset=utf-8 | sha256:f57f94a62ed4aab37f569b5d56430b3756ee6e3a5281a0488cae5c233f2a62d8 | 2026-09-08T00:00:00Z |
Fragments — 1
content/methods/induction/structural-induction.tex · section · referenced by: 1
en · official · sha256:2a35051885b790a50ee726b2f2bdf94fecbb4c3143325497329ab8a48bd616d9
% Part: methods
% Chapter: induction
% Section: structural-induction
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{mth}{ind}{sti}
\olsection{Structural Induction}
So far we have used induction to establish results about all natural
numbers. But a corresponding principle can be used directly to prove
results about all !!{element}s of an inductively defined set. This
often called \emph{structural} induction, because it depends on the
structure of the inductively defined objects.
Generally, an inductive definition is given by (a)~a list of
``initial'' !!{element}s of the set and (b)~a list of operations which
produce new !!{element}s of the set from old ones. In the case of nice
terms, for instance, the initial objects are the letters. We only have
one operation: the operations are
\begin{align*}
o(s_1, s_2) = & [s_1 \circ s_2]
\end{align*}
You can even think of the natural numbers~$\Nat$ themselves as being
given by an inductive definition: the initial object is~$0$, and the
operation is the successor function~$x + 1$.
In order to prove something about all elements of an inductively
defined set, i.e., that every !!{element} of the set has a
property~$P$, we must:
\begin{enumerate}
\item Prove that the initial objects have~$P$
\item Prove that for each operation~$o$, if the arguments have~$P$,
so does the result.
\end{enumerate}
For instance, in order to prove something about all nice terms, we
would prove that it is true about all letters, and that it is true
about $[s_1 \circ s_2]$ provided it is true of $s_1$ and $s_2$
individually.
\begin{prop}
The number of $[$ equals the number of $]$ in any nice term~$t$.
\end{prop}
\begin{proof}
We use structural induction. Nice terms are inductively defined, with
letters as initial objects and the operation $o$ for constructing new
nice terms out of old ones.
\begin{enumerate}
\item The claim is true for every letter, since the number of $[$ in a
letter by itself is~$0$ and the number of $]$ in it is also~$0$.
\item Suppose the number of $[$ in $s_1$ equals the number of $]$, and
the same is true for $s_2$. The number of $[$ in $o(s_1, s_2)$, i.e., in
$[s_1 \circ s_2]$, is the sum of the number of $[$ in $s_1$ and
$s_2$ plus one. The number of $]$ in $o(s_1, s_2)$ is the sum of the number
of $]$ in $s_1$ and $s_2$ plus one. Thus, the number of $[$ in $o(s_1, s_2)$
equals the number of $]$ in $o(s_1,s_2)$.
\end{enumerate}
\end{proof}
\begin{prob}
Prove by structural induction that no nice term starts with~$]$.
\end{prob}
Let's give another proof by structural induction: a proper initial
segment of a string~$t$ of symbols is any string~$s$ that agrees with
$t$ symbol by symbol, read from the left, but $t$ is longer. So,
e.g., $[a \circ {}$ is a proper initial segment of $[a \circ b]$, but
neither are $[b \circ {}$ (they disagree at the second symbol) nor $[a
\circ b]$ (they are the same length).
\begin{prop}\ollabel{prop:initial}
Every proper initial segment of a nice term~$t$ has more $[$'s than
$]$'s.
\end{prop}
\begin{proof}
By induction on~$t$:
\begin{enumerate}
\item $t$ is a letter by itself: Then $t$ has no proper initial segments.
\item $t = [s_1 \circ s_2]$ for some nice terms $s_1$ and~$s_2$. If $r$ is
a proper initial segment of $t$, there are a number of
possibilities:
\begin{enumerate}
\item $r$ is just $[$: Then $r$ has one more $[$ than it does~$]$.
\item $r$ is $[r_1$ where $r_1$ is a proper initial segment
of~$s_1$: Since $s_1$ is a nice term, by induction hypothesis, $r_1$
has more $[$ than $]$ and the same is true for $[r_1$.
\item $r$ is $[s_1$ or $[s_1 \circ {}$: By the previous result, the
number of $[$ and $]$ in~$s_1$ are equal; so the number of $[$
in $[s_1$ or $[s_1 \circ {}$ is one more than the number of~$]$.
\item $r$ is $[s_1 \circ r_2$ where $r_2$ is a proper initial segment
of~$s_2$: By induction hypothesis, $r_2$ contains more $[$ than
$]$. By the previous result, the number of $[$ and of
$]$ in~$s_1$ are equal. So the number of $[$ in $[s_1 \circ r_2$
is greater than the number of~$]$.
\item $r$ is $[s_1 \circ s_2$: By the previous result, the number of
$[$ and $]$ in $s_1$ are equal, and the same for~$s_2$. So there
is one more $[$ in $[s_1 \circ s_2$ than there are~$]$.
\end{enumerate}
\end{enumerate}
\end{proof}
\end{document}Referencing norms: P_STRUCTURAL_INDUCTION
content/methods/proofs/inference-patterns.tex at commit 1e960be (master, 2026-08-14)
- edition
- urn:logic:clir:methods#OLP_MTH_PROOFS_INFERENCE_PATTERNS_ED
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- adopted: 2026-08-14
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/inference-patterns.tex | application/x-tex; charset=utf-8 | sha256:dec51f23018334023107ecfaa7a2f31fdf964b2b0cb7aebaeeb4e1688ed6dd31 | 2026-09-08T00:00:00Z |
Fragments — 8
content/methods/proofs/inference-patterns.tex#Conditional Proof · subsection · referenced by: 8
en · official · sha256:485319001698c005ce2c5cecc7ed4f4db28dd4d876ab6615fdd0d1e94ec7decd
\subsection{Conditional Proof}
Many theorems you will encounter are in conditional form (i.e., show
that if $p$ holds, then $q$ is also true). These cases are nice and
easy to set up---simply assume the antecedent of the conditional (in
this case, $p$) and prove the conclusion~$q$ from it. So if your
theorem reads, ``If $p$ then $q$,'' you start your proof with ``assume
$p$'' and at the end you should have proved~$q$.
Conditionals may be stated in different ways. So instead of ``If $p$
then $q$,'' a theorem may state that ``$p$ only if $q$,'' ``$q$ if
$p$,'' or ``$q$, provided $p$.'' These all mean the same and require
assuming $p$ and proving~$q$ from that assumption. Recall that a
biconditional (``$p$ if and only if (iff) $q$'') is really two
conditionals put together: if $p$ then $q$, and if $q$ then~$p$. All
you have to do, then, is two instances of conditional proof: one for
the first conditional and another one for the second. Sometimes,
however, it is possible to prove an ``iff'' statement by chaining
together a bunch of other ``iff'' statements so that you start with
``$p$'' an end with ``$q$''---but in that case you have to make sure
that each step really is an ``iff.''
Referencing norms: M_IMPLICATION_PROOF, MethodUsesRule, ST_IMP_1, ST_IMP_2, ST_IMP_3, ST_IMP_4, ST_IMP_5, method_uses_rule
content/methods/proofs/inference-patterns.tex#Proof by Cases · subsection · referenced by: 6
en · official · sha256:645cc8681d965c364a09c4e228376c3b857ac79bd3d769962ef097c5df368841
\subsection{Proof by Cases}
Suppose you have a disjunction as an assumption or as an already
established conclusion---you have assumed or proved that $p$ or $q$ is
true. You want to prove $r$. You do this in two steps: first you
assume that $p$ is true, and prove~$r$, then you assume that $q$ is
true and prove~$r$ again. This works because we assume or know that
one of the two alternatives holds. The two steps establish that either
one is sufficient for the truth of~$r$. (If both are true, we have
not one but two reasons for why $r$~is true. It is not necessary to
separately prove that $r$~is true assuming both $p$ and~$q$.) To
indicate what we're doing, we announce that we ``distinguish cases.''
For instance, suppose we know that $x \in B \cup C$. $B \cup C$ is
defined as $\Setabs{x}{x \in B \text{ or } x \in C}$. In other words,
by definition, $x \in B$ or $x \in C$. We would prove that $x \in A$
from this by first assuming that $x \in B$, and proving $x \in A$ from
this assumption, and then assume $x \in C$, and again prove $x \in A$
from this. You would write ``We distinguish cases'' under the
assumption, then ``Case (1): $x \in B$'' underneath, and ``Case (2):
$x \in C$ halfway down the page. Then you'd proceed to fill in the top
half and the bottom half of the page.
Proof by cases is especially useful if what you're proving is itself
disjunctive. Here's a simple example:
\begin{prop}
Suppose $B \subseteq D$ and $C \subseteq E$. Then $B \cup C \subseteq
D \cup E$.
\end{prop}
\begin{proof}
Assume (a) that $B \subseteq D$ and (b) $C \subseteq E$. By
definition, any $x \in B$ is also $\in D$ (c) and any $x \in C$ is
also $\in E$ (d). To show that $B \cup C \subseteq D \cup E$, we
have to show that if $x \in B \cup C$ then $x \in D \cup E$ (by
definition of $\subseteq$). $x \in B \cup C$ iff $x \in B$ or $x \in
C$ (by definition of~$\cup$). Similarly, $x \in D \cup E$ iff $x \in
D$ or $x \in E$. So, we have to show: for any $x$, if $x \in B$ or
$x \in C$, then $x \in D$ or $x \in E$.
\begin{quote}
So far we've only unpacked definitions!{} We've reformulated our
proposition without $\subseteq$ and $\cup$ and are left with trying
to prove a universal conditional claim. By what we've discussed
above, this is done by assuming that $x$ is something about which we
assume the ``if'' part is true, and we'll go on to show that the
``then'' part is true as well. In other words, we'll assume that $x
\in B$ or $x \in C$ and show that $x \in D$ or $x \in
E$.\footnote{This paragraph just explains what we're doing---it's
not part of the proof, and you don't have to go into all this
detail when you write down your own proofs.}
\end{quote}
Suppose that $x \in B$ or $x \in C$. We have to show that $x \in D$
or $x \in E$. We distinguish cases.
Case 1: $x \in B$. By (c), $x \in D$. Thus, $x \in D$ or $x \in
E$. (Here we've made the inference discussed in the preceding
subsection!)
Case 2: $x \in C$. By (d), $x \in E$. Thus, $x \in D$ or $x \in E$.
\end{proof}
Referencing norms: M_CASES, ST_CASE_1, ST_CASE_2, ST_CASE_3, ST_CASE_4, ST_CASE_5
content/methods/proofs/inference-patterns.tex#Proving an Existence Claim · subsection · referenced by: 5
en · official · sha256:6073feed398a28d8a6a874ec173bfcace2c6a4e4d00ddc0cb587204b65e1fef2
\subsection{Proving an Existence Claim}
When asked to prove an existence claim, the question will usually be
of the form ``prove that there is an~$x$ such that $\dots x \dots$'',
i.e., that some object that has the property described by ``$\dots x
\dots$''. In this case you'll have to identify a suitable object and show
that it has the required property. This sounds straightforward, but a
proof of this kind can be tricky. Typically it involves
\emph{constructing} or \emph{defining} an object and proving that the
object so defined has the required property. Finding the right object
may be hard, proving that it has the required property may be hard,
and sometimes it's even tricky to show that you've succeeded in
defining an object at all!{}
Generally, you'd write this out by specifying the object, e.g., ``let
$x$ be \dots'' (where \dots{} specifies which object you have in
mind), possibly proving that $\dots$ in fact describes an object that
exists, and then go on to show that $x$ has the property~$Q$. Here's a
simple example.
\begin{prop}
Suppose that $x \in B$. Then there is an~$A$ such that $A \subseteq
B$ and $A \neq \emptyset$.
\end{prop}
\begin{proof}
Assume $x \in B$. Let $A = \{x\}$.
\begin{quote}
Here we've defined the set~$A$ by enumerating its
!!{element}s. Since we assume that $x$ is an object, and we can
always form a set by enumerating its !!{element}s, we don't have
to show that we've succeeded in defining a set~$A$ here. However,
we still have to show that $A$ has the properties required by the
proposition. The proof isn't complete without that!{}
\end{quote}
Since $x \in A$, $A \neq \emptyset$.
\begin{quote}
This relies on the definition of $A$ as $\{x\}$ and the obvious
facts that $x \in \{x\}$ and $x \notin \emptyset$.
\end{quote}
Since $x$ is the only !!{element} of~$\{x\}$, and $x \in B$, every
!!{element} of~$A$ is also !!a{element} of~$B$. By definition
of~$\subseteq$, $A \subseteq B$.
\end{proof}
Referencing norms: M_EXISTENCE_WITNESS, ST_EXW_1, ST_EXW_2, ST_EXW_3, ST_EXW_4
content/methods/proofs/inference-patterns.tex#Proving a Conjunction · subsection · referenced by: 5
en · official · sha256:b26bf852ffe423d8ae64cba4f33388a9d1098c27d3f535c3ac799fa19711bc5d
\subsection{Proving a Conjunction}
Sometimes what you'll be asked to prove will have the form of a
conjunction; you will be asked to ``prove $p$ and $q$.'' In this case,
you simply have to do two things: prove $p$, and then prove $q$. You
could divide your proof into two sections, and for clarity, label
them. When you're making your first notes, you might write ``(1) Prove
$p$'' at the top of the page, and ``(2) Prove $q$'' in the middle of
the page. (Of course, you might not be explicitly asked to prove a
conjunction but find that your proof requires that you prove a
conjunction. For instance, if you're asked to prove that $D = E$ you
will find that, after unpacking the definition of~$=$, you have to
prove: every !!{element} of~$D$ is !!a{element} of~$E$
\emph{and} every !!{element} of~$E$ is !!a{element} of~$D$).
Referencing norms: M_CONJUNCTION_PROOF, ST_ANDP_1, ST_ANDP_2, ST_ANDP_3, ST_ANDP_4
content/methods/proofs/inference-patterns.tex#Proving a Disjunction · subsection · referenced by: 4
en · official · sha256:17a7dc63299618aa3494755d5afb4933f1ce813271fb4df18aa62b89bbfd2f25
\subsection{Proving a Disjunction}
When what you are proving takes the form of a disjunction (i.e., it is
an statement of the form ``$p$ or $q$''), it is enough to show that
one of the disjuncts is true. However, it basically never happens
that either disjunct just follows from the assumptions of your
theorem. More often, the assumptions of your theorem are themselves
disjunctive, or you're showing that all things of a certain kind have
one of two properties, but some of the things have the one and others
have the other property. This is where proof by cases is
useful (see below).
Referencing norms: M_DISJUNCTION_PROOF, ST_ORP_1, ST_ORP_2, ST_ORP_3
content/methods/proofs/inference-patterns.tex#Universal Claims · subsection · referenced by: 11
en · official · sha256:741c3ec90929b67254c5791983913060506fb15e9109261a2daf4851460d85c3
\subsection{Universal Claims}
Using a universal claim is simple: if something is true for anything,
it's true for each particular thing. So if, say, the hypothesis of
your proof is $A \subseteq B$, that means (unpacking the definition
of~$\subseteq$), that, for every $x \in A$, $x \in B$. Thus, if you
already know that $z \in A$, you can conclude $z \in B$.
Proving a universal claim may seem a little bit tricky. Usually these
statements take the following form: ``If $x$ has~$P$, then it
has~$Q$'' or ``All $P$s are $Q$s.'' Of course, it might not fit this
form perfectly, and it takes a bit of practice to figure out what
you're asked to prove exactly. But: we often have to prove that all objects
with some property have a certain other property.
The way to prove a universal claim is to introduce names or variables,
for the things that have the one property and then show that they also
have the other property. We might put this by saying that to prove
something for \emph{all}~$P$s you have to prove it for an
\emph{arbitrary}~$P$. And the name introduced is a name for an
arbitrary~$P$. We typically use single letters as these names for
arbitrary things, and the letters usually follow conventions: e.g., we
use $n$ for natural numbers, $!A$ for !!{formula}s, $A$ for sets, $f$
for functions, etc.
The trick is to maintain generality throughout the proof. You start by
assuming that an arbitrary object (``$x$'') has the property~$P$, and
show (based only on definitions or what you are allowed to assume)
that $x$ has the property~$Q$. Because you have not stipulated what
$x$ is specifically, other that it has the property $P$, then you can
assert that everything with $P$ has the property~$Q$. In short, $x$ is a
stand-in for \emph{all} things with property~$P$.
\begin{prop}
For all sets $A$ and $B$, $A \subseteq A \cup B$.
\end{prop}
\begin{proof}
Let $A$ and $B$ be arbitrary sets. We want to show that $A
\subseteq A \cup B$. By definition of $\subseteq$, this amounts to:
for every $x$, if $x \in A$ then $x \in A \cup B$. So let $x \in A$
be an arbitrary !!{element} of~$A$. We have to show that $x \in A
\cup B$. Since $x \in A$, $x \in A$ or $x \in B$. Thus, $x \in
\Setabs{x}{x \in A \lor x \in B}$. But that, by definition of $\cup
$, means $x \in A \cup B$.
\end{proof}
Referencing norms: M_COUNTEREXAMPLE, M_UNIVERSAL, ST_CEX_1, ST_CEX_2, ST_CEX_3, ST_CEX_4, ST_UNI_1, ST_UNI_2, ST_UNI_3, ST_UNI_4, ST_UNI_5
content/methods/proofs/inference-patterns.tex#Using a Conjunction · subsection · referenced by: 4
en · official · sha256:b8cb77d7086ccd051f0975d81e035d68bc29f75ced25d9803715070b16bf8ccf
\subsection{Using a Conjunction}
Perhaps the simplest inference pattern is that of drawing as
conclusion one of the conjuncts of a conjunction. In other words: if
we have assumed or already proved that $p$ and~$q$, then we're
entitled to infer that~$p$ (and also that~$q$). This is such a basic
inference that it is often not mentioned. For instance, once we've
unpacked the definition of $D = E$ we've established that every
!!{element} of~$D$ is !!a{element} of~$E$ and vice versa. From this
we can conclude that every !!{element} of~$E$ is !!a{element} of~$D$
(that's the ``vice versa'' part).
Referencing norms: M_CONJUNCTION_USE, ST_ANDU_1, ST_ANDU_2, ST_ANDU_3
content/methods/proofs/inference-patterns.tex#Using Existence Claims · subsection · referenced by: 5
en · official · sha256:7a2342700d7026d835068ec7de157fc077f990b839e30525bd7b99a048b323c3
\subsection{Using Existence Claims}
Suppose you know that some existence claim is true (you've proved it,
or it's a hypothesis you can use), say, ``for some~$x$, $x \in A$'' or
``there is an $x \in A$.'' If you want to use it in your proof, you
can just pretend that you have a name for one of the things which your
hypothesis says exist. Since $A$ contains at least one thing, there
are things to which that name might refer. You might of course not be
able to pick one out or describe it further (other than that it is
$\in A$). But for the purpose of the proof, you can pretend that you
have picked it out and give a name to it. It's important to pick a
name that you haven't already used (or that appears in your
hypotheses), otherwise things can go wrong. In your proof, you
indicate this by going from ``for some $x$, $x \in A$'' to ``Let $a
\in A$.'' Now you can reason about~$a$, use some other hypotheses, etc.,
until you come to a conclusion, $p$. If $p$ no longer mentions~$a$, $p$ is
independent of the asusmption that $a \in A$, and you've shown that it
follows just from the assumption ``for some $x$, $x \in A$.''
\begin{prop}
If $A \neq \emptyset$, then $A \cup B \neq \emptyset$.
\end{prop}
\begin{proof}
Suppose $A \neq \emptyset$. So for some $x$, $x \in A$.
\begin{quote}
Here we first just restated the hypothesis of the
proposition. This hypothesis, i.e., $A \neq \emptyset$, hides an
existential claim, which you get to only by unpacking a few
definitions. The definition of $=$ tells us that $A = \emptyset$
iff every $x \in A$ is also $\in \emptyset$ and every $x \in
\emptyset$ is also $\in A$. Negating both sides, we get: $A \neq
\emptyset$ iff either some $x \in A$ is $\notin \emptyset$ or some
$x \in \emptyset$ is $\notin A$. Since nothing is $\in \emptyset$,
the second disjunct can never be true, and ``$x \in A$ and $x
\notin \emptyset$'' reduces to just $x \in A$. So $x \neq
\emptyset$ iff for some $x$, $x \in A$. That's an existence
claim. Now we use that existence claim by introducing a name for
one of the !!{element}s of~$A$:
\end{quote}
Let $a \in A$.
\begin{quote}
Now we've introduced a name for one of the things~$\in A$. We'll
continue to argue about~$a$, but we'll be careful to only assume
that $a \in A$ and nothing else:
\end{quote}
Since $a \in A$, $a \in A \cup B$, by definition of~$\cup$. So for
some $x$, $x \in A \cup B$, i.e., $A \cup B \neq \emptyset$.
\begin{quote}
In that last step, we went from ``$a \in A \cup B$'' to ``for some
$x$, $x \in A \cup B$.'' That doesn't mention $a$ anymore, so we
know that ``for some $x$, $x \in A \cup B$'' follows from ``for
some $x$, $x \in A$ alone.'' But that means that $A \cup B \neq
\emptyset$.
\end{quote}
\end{proof}
It's maybe good practice to keep bound variables like ``$x$'' separate
from hypothetical names like $a$, like we did. In practice, however, we
often don't and just use $x$, like so:
\begin{quote}
Suppose $A \neq \emptyset$, i.e., there is an $x \in A$. By definition
of $\cup$, $x \in A \cup B$. So $A \cup B \neq \emptyset$.
\end{quote}
However, when you do this, you have to be extra careful that you use
different $x$'s and $y$'s for different existential claims. For
instance, the following is \emph{not} a correct proof of ``If $A \neq
\emptyset$ and $B \neq \emptyset$ then $A \cap B \neq \emptyset$''
(which is not true).
\begin{quote}
Suppose $A \neq \emptyset$ and $B \neq \emptyset$. So for some $x$, $x
\in A$ and also for some $x$, $x \in B$. Since $x \in A$ and $x \in
B$, $x \in A \cap B$, by definition of~$\cap$. So $A \cap B \neq
\emptyset$.
\end{quote}
Can you spot where the incorrect step occurs and explain why the
result does not hold?
Referencing norms: M_EXISTENCE_USE, ST_EXU_1, ST_EXU_2, ST_EXU_3, ST_EXU_4
content/methods/proofs/introduction.tex at commit 1e960be (master, 2026-08-14)
- edition
- urn:logic:clir:methods#OLP_MTH_PROOFS_INTRODUCTION_ED
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- adopted: 2026-08-14
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/introduction.tex | application/x-tex; charset=utf-8 | sha256:ae06d0471d8f4c8565a11f9dbd7bb77513f837bb495032b6356cafbaa319ad83 | 2026-09-08T00:00:00Z |
Fragments — 1
content/methods/proofs/introduction.tex · section · referenced by: 6
en · official · sha256:0efff70c58f6862639a3b6e903a05e91f3a0511d9c2d8a3a82a6c0ed63c6ad83
% Part: methods
% Chapter: proofs
% Section: introduction
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{mth}{prf}{int}
\olsection{Introduction}
Based on your experiences in introductory logic, you might be
comfortable with !!a{derivation} system---probably a natural deduction or
Fitch style !!{derivation} system, or perhaps a proof-tree system. You probably
remember doing proofs in these systems, either proving !!a{formula}
or show that a given argument is valid. In order to do this, you
applied the rules of the system until you got the desired end
result. In reasoning \emph{about} logic, we also prove things, but in
most cases we are not using !!a{derivation} system. In fact, most of the
proofs we consider are done in English (perhaps, with some symbolic
language thrown in) rather than entirely in the language of
first-order logic. When constructing such proofs, you might at first
be at a loss---how do I prove something without !!a{derivation} system? How
do I start? How do I know if my proof is correct?
Before attempting a proof, it's important to know what a proof is and
how to construct one. As implied by the name, a \emph{proof} is meant
to show that something is true. You might think of this in terms of a
dialogue---someone asks you if something is true, say, if every prime
other than two is an odd number. To answer ``yes'' is not enough; they
might want to know \emph{why}. In this case, you'd give them a proof.
In everyday discourse, it might be enough to gesture at an answer, or
give an incomplete answer. In logic and mathematics, however, we want
rigorous proof---we want to show that something is true beyond \emph{any}
doubt. This means that every step in our proof must be justified, and
the justification must be cogent (i.e., the assumption you're using is
actually assumed in the statement of the theorem you're proving, the
definitions you apply must be correctly applied, the justifications
appealed to must be correct inferences, etc.).
Usually, we're proving some statement. We call the statements we're
proving by various names: propositions, theorems, lemmas, or
corollaries. A proposition is a basic proof-worthy statement:
important enough to record, but perhaps not particularly deep nor
applied often. A theorem is a significant, important proposition. Its
proof often is broken into several steps, and sometimes it is named
after the person who first proved it (e.g., Cantor's Theorem, the
L\"owenheim--Skolem theorem) or after the fact it concerns (e.g., the
completeness theorem). A lemma is a proposition or theorem that is
used in the proof of a more important result. Confusingly,
sometimes lemmas are important results in themselves, and also named
after the person who introduced them (e.g., Zorn's Lemma). A corollary
is a result that easily follows from another one.
A statement to be proved often contains assumptions that clarify
which kinds of things we're proving something about. It might begin
with ``Let $!A$ be !!a{formula} of the form $!B \lif !C$'' or
``Suppose $\Gamma \Proves !A$'' or something of the sort. These are
\emph{hypotheses} of the proposition, theorem, or lemma, and you may
assume these to be true in your proof. They restrict what we're
proving, and also introduce some names for the objects we're
talking about. For instance, if your proposition begins with ``Let
$!A$ be !!a{formula} of the form $!B \lif !C$,'' you're proving
something about all formulas of a certain sort only (namely,
conditionals), and it's understood that $!B \lif !C$ is an arbitrary
conditional that your proof will talk about.
\end{document}Referencing norms: DescribedStep, StepTextFromName, described_step, method_mode, step_is_description, step_text
content/methods/proofs/proof-by-contradiction.tex at commit 1e960be (master, 2026-08-14)
- edition
- urn:logic:clir:methods#OLP_MTH_PROOFS_PROOF_BY_CONTRADICTION_ED
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- adopted: 2026-08-14
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/proof-by-contradiction.tex | application/x-tex; charset=utf-8 | sha256:3eda384520d99069031c01f168564f639980118e7fd145ca105e8092fbe438dd | 2026-09-08T00:00:00Z |
Fragments — 1
content/methods/proofs/proof-by-contradiction.tex · section · referenced by: 15
en · official · sha256:ae73e61f00f1ba507dc3f7f8f329f99069e62243011c294534b92007151046b8
% Part: methods
% Chapter: proofs
% Section: proof-by-contradiction
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{mth}{prf}{con}
\olsection{Proof by Contradiction}
In the first instance, proof by contradiction is an inference pattern
that is used to prove negative claims. Suppose you want to show that
some claim~$p$ is \emph{false}, i.e., you want to show~$\lnot p$. The
most promising strategy is to (a) suppose that $p$~is true, and (b)
show that this assumption leads to something you know to be false.
``Something known to be false'' may be a result that conflicts
with---contradicts---$p$ itself, or some other hypothesis of the
overall claim you are considering. For instance, a proof of ``if $q$
then $\lnot p$'' involves assuming that $q$~is true and proving~$\lnot
p$ from it. If you prove $\lnot p$ by contradiction, that means
assuming $p$ in addition to~$q$. If you can prove $\lnot q$ from $p$,
you have shown that the assumption~$p$ leads to something that
contradicts your other assumption~$q$, since $q$~and $\lnot q$ cannot
both be true. Of course, you have to use other inference patterns in
your proof of the contradiction, as well as unpacking definitions.
Let's consider an example.
\begin{prop}
If $A \subseteq B$ and $B = \emptyset$, then $A$ has no !!{element}s.
\end{prop}
\begin{proof}
Suppose $A \subseteq B$ and $B = \emptyset$. We want to show that
$A$ has no !!{element}s.
\begin{quote}
Since this is a conditional claim, we assume the antecedent and
want to prove the consequent. The consequent is: $A$ has no
!!{element}s. We can make that a bit more explicit: it's not the
case that there is an~$x \in A$.
\end{quote}
$A$ has no !!{element}s iff it's not the case that there is an~$x$
such that $x \in A$.
\begin{quote}
So we've determined that what we want to prove is really a
negative claim~$\lnot p$, namely: it's not the case that there is
an $x \in A$. To use proof by contradiction, we have to assume the
corresponding positive claim~$p$, i.e., there is an $x \in A$, and
prove a contradiction from it. We indicate that we're doing a
proof by contradiction by writing ``by way
of contradiction, assume'' or even just ``suppose not,'' and then state
the assumption~$p$.
\end{quote}
Suppose not: there is an $x \in A$.
\begin{quote}
This is now the new assumption we'll use to obtain a
contradiction. We have two more assumptions: that $A \subseteq B$
and that $B = \emptyset$. The first gives us that $x \in B$:
\end{quote}
Since $A \subseteq B$, $x \in B$.
\begin{quote}
But since $B = \emptyset$, every !!{element} of $B$ (e.g., $x$)
must also be !!a{element} of~$\emptyset$.
\end{quote}
Since $B = \emptyset$, $x \in \emptyset$. This is a contradiction,
since by definition $\emptyset$ has no !!{element}s.
\begin{quote}
This already completes the proof: we've arrived at what we need (a
contradiction) from the assumptions we've set up, and this means
that the assumptions can't all be true. Since the first two
assumptions ($A \subseteq B$ and $B = \emptyset$) are not
contested, it must be the last assumption introduced (there is an
$x \in A$) that must be false. But if we want to be thorough, we
can spell this out.
\end{quote}
Thus, our assumption that there is an $x \in A$ must be false, hence,
$A$ has no !!{element}s by proof by contradiction.
\end{proof}
Every positive claim is trivially equivalent to a negative claim: $p$
iff $\lnot\lnot p$. So proofs by contradiction can also be used to
establish positive claims ``indirectly,'' as follows: To prove~$p$,
read it as the negative claim $\lnot\lnot p$. If we can prove a
contradiction from $\lnot p$, we've established $\lnot\lnot p$ by
proof by contradiction, and hence~$p$.
In the last example, we aimed to prove a negative claim, namely that
$A$ has no !!{element}s, and so the assumption we made for the purpose
of proof by contradiction (i.e., that there is an $x \in A$) was a
positive claim. It gave us something to work with, namely the
hypothetical $x \in A$ about which we continued to reason until we got
to $x \in \emptyset$.
When proving a positive claim indirectly, the assumption you'd make
for the purpose of proof by contradiction would be negative. But very
often you can easily reformulate a positive claim as a negative claim,
and a negative claim as a positive claim. Our previous proof would
have been essentially the same had we proved ``$A = \emptyset$''
instead of the negative consequent ``$A$ has no !!{element}s.'' (By
definition of $=$, ``$A = \emptyset$'' is a general claim, since it
unpacks to ``every !!{element} of~$A$ is an !!{element} of~$\emptyset$
and vice versa''.) But it is easily seen to be equivalent to the
negative claim ``not: there is an $x \in A$.''
So it is sometimes easier to work with $\lnot p$ as an assumption than
it is to prove~$p$ directly. Even when a direct proof is just as
simple or even simpler (as in the next examples), some people prefer to
proceed indirectly. If the double negation confuses you, think of a
proof by contradiction of some claim as a proof of a contradiction
from the \emph{opposite} claim. So, a proof by contradiction of $\lnot
p$ is a proof of a contradiction from the assumption~$p$; and proof by
contradiction of~$p$ is a proof of a contradiction from~$\lnot p$.
\begin{prop}
$A \subseteq A \cup B$.
\end{prop}
\begin{proof}
We want to show that $A \subseteq A \cup B$.
\begin{quote}
On the face of it, this is a positive claim: every $x \in A$ is
also in $A \cup B$. The negation of that is: some $x \in A$ is
$\notin A \cup B$. So we can prove the claim indirectly by
assuming this negated claim, and showing that it leads to a
contradiction.
\end{quote}
Suppose not, i.e., $A \nsubseteq A \cup B$.
\begin{quote}
We have a definition of $A \subseteq A \cup B$: every $x \in A$ is
also $\in A \cup B$. To understand what $A \nsubseteq A \cup B$
means, we have to use some elementary logical manipulation on the
unpacked definition: it's false that every $x \in A$ is also $\in
A \cup B$ iff there is \emph{some}~$x \in A$ that is $\notin C$.
(This is a place where you want to be very careful: many students'
attempted proofs by contradiction fail because they analyze the
negation of a claim like ``all $A$s are $B$s'' incorrectly.) In
other words, $A \nsubseteq A \cup B$ iff there is an $x$ such that
$x \in A$ and $x \notin A \cup B$. From then on, it's easy.
\end{quote}
So, there is an $x \in A$ such that $x \notin A \cup B$. By
definition of $\cup$, $x \in A \cup B$ iff $x \in A$ or $x \in
B$. Since $x \in A$, we have $x \in A \cup B$. This contradicts the
assumption that $x \notin A \cup B$.
\end{proof}
\begin{prob}
Prove \emph{indirectly} that $A \cap B \subseteq A$.
\end{prob}
\begin{prop}
If $A \subseteq B$ and $B \subseteq C$ then $A \subseteq C$.
\end{prop}
\begin{proof}
Suppose $A \subseteq B$ and $B \subseteq C$. We want to show $A
\subseteq C$.
\begin{quote}
Let's proceed indirectly: we assume the negation of what we want
to etablish.
\end{quote}
Suppose not, i.e., $A \nsubseteq C$.
\begin{quote}
As before, we reason that $A \nsubseteq C$ iff not every $x \in A$
is also $\in C$, i.e., some $x \in A$ is $\notin C$. Don't worry,
with practice you won't have to think hard anymore to unpack
negations like this.
\end{quote}
In other words, there is an~$x$ such that $x \in A$ and $x \notin C$.
\begin{quote}
Now we can use this to get to our contradiction. Of course, we'll
have to use the other two assumptions to do it.
\end{quote}
Since $A \subseteq B$, $x \in B$. Since $B \subseteq C$, $x \in
C$. But this contradicts $x \notin C$.
\end{proof}
\begin{prop}
If $A \cup B = A \cap B$ then $A = B$.
\end{prop}
\begin{proof}
Suppose $A \cup B = A \cap B$. We want to show that $A = B$.
\begin{quote}
The beginning is now routine:
\end{quote}
Assume, by way of contradiction, that $A \neq B$.
\begin{quote}
Our assumption for the proof by contradiction is that $A \neq
B$. Since $A = B$ iff $A \subseteq B$ an $B \subseteq A$, we get
that $A \neq B$ iff $A \nsubseteq B$ \emph{or} $B \nsubseteq
A$. (Note how important it is to be careful when manipulating
negations!{}) To prove a contradiction from this disjunction, we
use a proof by cases and show that in each case, a contradiction
follows.
\end{quote}
$A \neq B$ iff $A \nsubseteq B$ or $B \nsubseteq A$. We distinguish
cases.
\begin{quote}
In the first case, we assume $A \nsubseteq B$, i.e., for some $x$,
$x \in A$ but $\notin B$. $A \cap B$ is defined as those
!!{element}s that $A$ and $B$ have in common, so if something
isn't in one of them, it's not in the intersection. $A \cup B$ is
$A$ together with $B$, so anything in either is also in the
union. This tells us that $x \in A \cup B$ but $x \notin A \cap
B$, and hence that $A \cap B \neq A \cup B$.
\end{quote}
Case 1: $A \nsubseteq B$. Then for some $x$, $x \in A$ but $x \notin
B$. Since $x \notin B$, then $x \notin A \cap B$. Since $x \in A$,
$x \in A \cup B$. So, $A \cap B \neq A \cup B$, contradicting the
assumption that $A \cap B = A \cup B$.
Case 2: $B \nsubseteq A$. Then for some $y$, $y \in B$ but $y \notin
A$. As before, we have $y \in A \cup B$ but $y \notin A \cap B$, and
so $A \cap B \neq A \cup B$, again contradicting $A \cap B = A \cup
B$.
\end{proof}
\end{document}Referencing norms: M_CLASSICAL_CONTRADICTION, M_NEGATION_INTRO, NeedsPrincipleAt, PrincipleFree, ST_CIP_1, ST_CIP_2, ST_CIP_3, ST_CIP_4, ST_CIP_5, ST_NEG_1, ST_NEG_2, ST_NEG_3, ST_NEG_4, needs_principle_at, principle_free
content/methods/proofs/starting-proofs.tex at commit 1e960be (master, 2026-08-14)
- edition
- urn:logic:clir:methods#OLP_MTH_PROOFS_STARTING_PROOFS_ED
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- adopted: 2026-08-14
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/starting-proofs.tex | application/x-tex; charset=utf-8 | sha256:84908cb7ef78b1ec62e2ccc41376d5bc039c6e44e1855c386d7b112c69d5ce64 | 2026-09-08T00:00:00Z |
Fragments — 1
content/methods/proofs/starting-proofs.tex · section
en · official · sha256:799594b8602ea5cb51ad49353f411b65a5b7884a2521954fae3ec94ef5a5a9be
% Part: methods
% Chapter: proofs
% Section: starting-proofs
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{mth}{prf}{str}
\olsection{Starting a Proof}
But where do you even start?
You've been given something to prove, so this should be the last thing that
is mentioned in the proof (you can, obviously, \emph{announce} that you're
going to prove it at the beginning, but you don't want to use it as an
assumption). Write what you are trying to prove at the bottom of a fresh
sheet of paper---this way you don't lose sight of your goal.
Next, you may have some assumptions that you are able to use (this
will be made clearer when we talk about the \emph{type} of proof you
are doing in the next section). Write these at the top of the page and
make sure to flag that they are assumptions (i.e., if you are assuming
$p$, write ``assume that $p$,'' or ``suppose that $p$''). Finally,
there might be some definitions in the question that you need to know.
You might be told to use a specific definition, or there might be
various definitions in the assumptions or conclusion that you are
working towards. \emph{Write these down and ensure that you understand
what they mean.}
How you set up your proof will also be dependent upon the form of the
question. The next section provides details on how to set up your proof
based on the type of sentence.
\end{document}content/methods/proofs/using-definitions.tex at commit 1e960be (master, 2026-08-14)
- edition
- urn:logic:clir:methods#OLP_MTH_PROOFS_USING_DEFINITIONS_ED
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- adopted: 2026-08-14
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/using-definitions.tex | application/x-tex; charset=utf-8 | sha256:0496b9489f10eb402e2eb91b503c7b522c2e73349e1481ceb9781f2e191a3bce | 2026-09-08T00:00:00Z |
Fragments — 1
content/methods/proofs/using-definitions.tex · section
en · official · sha256:9471b38c98324ae757108f4dbe0b20a5bb06291d7dce8d3915a30c4fd4e83002
% Part: methods
% Chapter: proofs
% Section: using-definitions
\documentclass[../../../include/open-logic-section]{subfiles}
\begin{document}
\olfileid{mod}{prf}{def}
\olsection{Using Definitions}
We mentioned that you must be familiar with all definitions that may
be used in the proof, and that you can properly apply them. This is a
really important point, and it is worth looking at in a bit more
detail. Definitions are used to abbreviate properties and relations so
we can talk about them more succinctly. The introduced abbreviation is
called the \emph{definiendum}, and what it abbreviates is the
\emph{definiens}. In proofs, we often have to go back to how the
definiendum was introduced, because we have to exploit the logical
structure of the definiens (the long version of which the defined term
is the abbreviation) to get through our proof. By unpacking
definitions, you're ensuring that you're getting to the heart of where
the logical action is.
We'll start with an example. Suppose you want to prove the following:
\begin{prop}
For any sets $A$ and $B$, $A \cup B = B \cup A$.
\end{prop}
In order to even start the proof, we need to know what it means for
two sets to be identical; i.e., we need to know what the ``$=$'' in
that equation means for sets. Sets are defined to be identical
whenever they have the same !!{element}s. So the definition we have
to unpack is:
\begin{defn}
Sets $A$ and $B$ are \emph{identical}, $A = B$, iff every !!{element}
of~$A$ is !!a{element} of~$B$, and vice versa.
\end{defn}
This definition uses $A$ and~$B$ as placeholders for arbitrary
sets. What it defines---the \emph{definiendum}---is the expression
``$A = B$'' by giving the condition under which $A = B$ is true. This
condition---``every !!{element} of~$A$ is !!a{element} of~$B$, and
vice versa''---is the \emph{definiens}.\footnote{In this particular
case---and very confusingly!---when $A = B$, the sets $A$ and $B$
are just one and the same set, even though we use different letters
for it on the left and the right side. But the ways in which that
set is picked out may be different, and that makes the definition
non-trivial.} The definition specifies that $A = B$ is true if, and
only if (we abbreviate this to ``iff'') the condition holds.
When you apply the definition, you have to match the $A$ and $B$ in
the definition to the case you're dealing with. In our case, it means
that in order for $A \cup B = B \cup A$ to be true, each $z \in A \cup
B$ must also be in $B \cup A$, and vice versa. The expression $A \cup
B$ in the proposition plays the role of~$A$ in the definition, and $B
\cup A$ that of~$B$. Since $A$ and $B$ are used both in the definition
and in the statement of the proposition we're proving, but in
different uses, you have to be careful to make sure you don't mix up
the two. For instance, it would be a mistake to think that you could
prove the proposition by showing that every !!{element} of~$A$ is
!!a{element} of~$B$, and vice versa---that would show that $A = B$,
not that $A \cup B = B \cup A$. (Also, since $A$ and $B$ may be any
two sets, you won't get very far, because if nothing is assumed about
$A$ and~$B$ they may well be different sets.)
Within the proof we are dealing with set-theoretic notions such as
union, and so we must also know the meanings of the symbol $\cup$ in
order to understand how the proof should proceed. And sometimes,
unpacking the definition gives rise to further definitions to
unpack. For instance, $A \cup B$ is defined as $\Setabs{z}{z \in A
\text{ or } z \in B}$. So if you want to prove that $x \in A \cup
B$, unpacking the definition of $\cup$ tells you that you have to
prove $x \in \Setabs{z}{z \in A \text{ or } z \in B}$. Now you also
have to remember that $x \in \Setabs{z}{\dots z\dots}$ iff $\dots
x\dots$. So, further unpacking the definition of the
$\Setabs{z}{\dots z \dots}$ notation, what you have to show is: $x \in
A$ or $x \in B$. So, ``every !!{element} of $A \cup B$ is also
!!a{element} of $B \cup A$'' really means: ``for every $x$, if $x \in
A$ or $x \in B$, then $x \in B$ or $x \in A$.'' If we fully
unpack the definitions in the proposition, we see that what we have to
show is this:
\begin{prop}
For any sets $A$ and $B$: (a) for every $x$, if $x \in A$ or $x \in
B$, then $x \in B$ or $x \in A$, and (b) for every $x$, if $x \in B$
or $x \in A$, then $x \in A$ or $x \in B$.
\end{prop}
What's important is that unpacking definitions is a necessary part of
constructing a proof. Properly doing it is sometimes difficult: you
must be careful to distinguish and match the variables in the
definition and the terms in the claim you're proving. In order to be
successful, you must know what the question is asking and what all the
terms used in the question mean---you will often need to unpack more
than one definition. In simple proofs such as the ones below, the
solution follows almost immediately from the definitions
themselves. Of course, it won't always be this simple.
\begin{prob}
Suppose you are asked to prove that $A \cap B \neq \emptyset$. Unpack
all the definitions occurring here, i.e., restate this in a way that
does not mention ``$\cap$'', ``='', or ``$\emptyset$''.
\end{prob}
\end{document}The hash beside the text is the sha256 of its exact bytes. It is the check that the text shown matches the one pinned in the package: a divergence fails the oracle’s static analysis.