Источник / закреплённая редакция

The Open Logic Text

Источник пакета logic.methods · The Open Logic Text (Open Logic Project), commit 1e960be

work
urn:logic:clir:methods#OPEN_LOGIC
номер
The Open Logic Text (Open Logic Project), commit 1e960be
вид
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
язык
en
официальность
official
материализация
PINNED_OFFICIAL_BYTES
жизненный цикл
adopted: 2026-08-14

Публикации

URIТипdocumentHashПолучено
https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/induction/induction.texapplication/x-tex; charset=utf-8sha256:a473475ad8fdd83af7da9474e389385d9b3fc9b0fe3673fbb7dc9c6a413df5af2026-09-08T00:00:00Z

Фрагменты — 1

content/methods/induction/induction.tex · section · на него ссылаются: 8

en · official · sha256:621e792077ccf2d458e3afa40ab1b3ca4ba65337a4de3a726059bb2fdbde15b8EN

% 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}

Ссылаются нормы: 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
язык
en
официальность
official
материализация
PINNED_OFFICIAL_BYTES
жизненный цикл
adopted: 2026-08-14

Публикации

URIТипdocumentHashПолучено
https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/induction/induction-on-N.texapplication/x-tex; charset=utf-8sha256:30a7fe3bf67517b5744d826eeb819782d399cf28a018313f5a7eff12843fe2222026-09-08T00:00:00Z

Фрагменты — 1

content/methods/induction/induction-on-N.tex · section · на него ссылаются: 2

en · official · sha256:7c909ee315b414a82b62a1bf34fccddeb91dc54c3f9bd3045ccf0ef73182a57fEN

% 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}

Ссылаются нормы: 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
язык
en
официальность
official
материализация
PINNED_OFFICIAL_BYTES
жизненный цикл
adopted: 2026-08-14

Публикации

URIТипdocumentHashПолучено
https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/induction/structural-induction.texapplication/x-tex; charset=utf-8sha256:f57f94a62ed4aab37f569b5d56430b3756ee6e3a5281a0488cae5c233f2a62d82026-09-08T00:00:00Z

Фрагменты — 1

content/methods/induction/structural-induction.tex · section · на него ссылаются: 1

en · official · sha256:2a35051885b790a50ee726b2f2bdf94fecbb4c3143325497329ab8a48bd616d9EN

% 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}

Ссылаются нормы: 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
язык
en
официальность
official
материализация
PINNED_OFFICIAL_BYTES
жизненный цикл
adopted: 2026-08-14

Публикации

URIТипdocumentHashПолучено
https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/inference-patterns.texapplication/x-tex; charset=utf-8sha256:dec51f23018334023107ecfaa7a2f31fdf964b2b0cb7aebaeeb4e1688ed6dd312026-09-08T00:00:00Z

Фрагменты — 8

content/methods/proofs/inference-patterns.tex#Conditional Proof · subsection · на него ссылаются: 8

en · official · sha256:485319001698c005ce2c5cecc7ed4f4db28dd4d876ab6615fdd0d1e94ec7decdEN

\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.''

Ссылаются нормы: 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 · на него ссылаются: 6

en · official · sha256:645cc8681d965c364a09c4e228376c3b857ac79bd3d769962ef097c5df368841EN

\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}

Ссылаются нормы: 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 · на него ссылаются: 5

en · official · sha256:6073feed398a28d8a6a874ec173bfcace2c6a4e4d00ddc0cb587204b65e1fef2EN

\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}

Ссылаются нормы: 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 · на него ссылаются: 5

en · official · sha256:b26bf852ffe423d8ae64cba4f33388a9d1098c27d3f535c3ac799fa19711bc5dEN

\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$).

Ссылаются нормы: 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 · на него ссылаются: 4

en · official · sha256:17a7dc63299618aa3494755d5afb4933f1ce813271fb4df18aa62b89bbfd2f25EN

\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).

Ссылаются нормы: M_DISJUNCTION_PROOF, ST_ORP_1, ST_ORP_2, ST_ORP_3

content/methods/proofs/inference-patterns.tex#Universal Claims · subsection · на него ссылаются: 11

en · official · sha256:741c3ec90929b67254c5791983913060506fb15e9109261a2daf4851460d85c3EN

\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}

Ссылаются нормы: 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 · на него ссылаются: 4

en · official · sha256:b8cb77d7086ccd051f0975d81e035d68bc29f75ced25d9803715070b16bf8ccfEN

\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).

Ссылаются нормы: M_CONJUNCTION_USE, ST_ANDU_1, ST_ANDU_2, ST_ANDU_3

content/methods/proofs/inference-patterns.tex#Using Existence Claims · subsection · на него ссылаются: 5

en · official · sha256:7a2342700d7026d835068ec7de157fc077f990b839e30525bd7b99a048b323c3EN

\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?

Ссылаются нормы: 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
язык
en
официальность
official
материализация
PINNED_OFFICIAL_BYTES
жизненный цикл
adopted: 2026-08-14

Публикации

URIТипdocumentHashПолучено
https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/introduction.texapplication/x-tex; charset=utf-8sha256:ae06d0471d8f4c8565a11f9dbd7bb77513f837bb495032b6356cafbaa319ad832026-09-08T00:00:00Z

Фрагменты — 1

content/methods/proofs/introduction.tex · section · на него ссылаются: 6

en · official · sha256:0efff70c58f6862639a3b6e903a05e91f3a0511d9c2d8a3a82a6c0ed63c6ad83EN

% 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}

Ссылаются нормы: 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
язык
en
официальность
official
материализация
PINNED_OFFICIAL_BYTES
жизненный цикл
adopted: 2026-08-14

Публикации

URIТипdocumentHashПолучено
https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/proof-by-contradiction.texapplication/x-tex; charset=utf-8sha256:3eda384520d99069031c01f168564f639980118e7fd145ca105e8092fbe438dd2026-09-08T00:00:00Z

Фрагменты — 1

content/methods/proofs/proof-by-contradiction.tex · section · на него ссылаются: 15

en · official · sha256:ae73e61f00f1ba507dc3f7f8f329f99069e62243011c294534b92007151046b8EN

% 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}

Ссылаются нормы: 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
язык
en
официальность
official
материализация
PINNED_OFFICIAL_BYTES
жизненный цикл
adopted: 2026-08-14

Публикации

URIТипdocumentHashПолучено
https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/starting-proofs.texapplication/x-tex; charset=utf-8sha256:84908cb7ef78b1ec62e2ccc41376d5bc039c6e44e1855c386d7b112c69d5ce642026-09-08T00:00:00Z

Фрагменты — 1

content/methods/proofs/starting-proofs.tex · section

en · official · sha256:799594b8602ea5cb51ad49353f411b65a5b7884a2521954fae3ec94ef5a5a9beEN

% 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
язык
en
официальность
official
материализация
PINNED_OFFICIAL_BYTES
жизненный цикл
adopted: 2026-08-14

Публикации

URIТипdocumentHashПолучено
https://raw.githubusercontent.com/OpenLogicProject/OpenLogic/1e960beff9ed7835bf3e3f1335e21af3439cd107/content/methods/proofs/using-definitions.texapplication/x-tex; charset=utf-8sha256:0496b9489f10eb402e2eb91b503c7b522c2e73349e1481ceb9781f2e191a3bce2026-09-08T00:00:00Z

Фрагменты — 1

content/methods/proofs/using-definitions.tex · section

en · official · sha256:9471b38c98324ae757108f4dbe0b20a5bb06291d7dce8d3915a30c4fd4e83002EN

% 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}

Хэш рядом с текстом — sha256 его точных байтов. Он и есть проверка того, что показанный текст совпадает с закреплённым в пакете: расхождение роняет статику оракула.