tokenize "derivation"

rzach · rzach · commit ca7cef2003ac · 2025-09-24T11:48:21.000+02:00
diff --git a/content/first-order-logic/axiomatic-deduction/axioms-rules-propositional.tex b/content/first-order-logic/axiomatic-deduction/axioms-rules-propositional.tex
@@ -34,7 +34,7 @@
 \end{defn}
 
 \begin{defn}[Modus ponens]
-  If $!B$ and $!B \lif !A$ already occur in a derivation, then $!A$ is
+  If $!B$ and $!B \lif !A$ already occur in !!a{derivation}, then $!A$ is
   a correct inference step.
 \end{defn}
 
diff --git a/content/first-order-logic/axiomatic-deduction/deduction-theorem.tex b/content/first-order-logic/axiomatic-deduction/deduction-theorem.tex
@@ -79,7 +79,7 @@
 induction basis applies.) Then some previous steps in the
 !!{derivation} are $!C \lif !B$ and $!C$, for some !!{formula}~$!C$,
 i.e., $\Gamma \cup \{!A\} \Proves !C \lif !B$ and $\Gamma \cup \{!A\}
-\Proves !C$, and the respective derivations are shorter, so the
+\Proves !C$, and the respective !!{derivation}s are shorter, so the
 inductive hypothesis applies to them. We thus have both:
 \begin{align*}
   & \Gamma \Proves !A \lif (!C \lif !B); \\
diff --git a/content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex b/content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex
@@ -69,7 +69,7 @@
 \begin{proof}
   Suppose $\{!A\} \cup \Delta \Proves !B$. Then there is
   !!a{derivation} $!B_1$, \dots, $!B_l = !B$ from~$\{!A\} \cup
-  \Delta$. Some of the steps in that derivation will be correct
+  \Delta$. Some of the steps in that !!{derivation} will be correct
   because of a rule which refers to a prior line~$!B_i = !A$. By
   hypothesis, there is !!a{derivation} of~$!A$ from~$\Gamma$, i.e.,
   !!a{derivation}~$!A_1$, \dots, $!A_k = !A$ where every $!A_i$ is an
diff --git a/content/first-order-logic/axiomatic-deduction/proving-things-quant.tex b/content/first-order-logic/axiomatic-deduction/proving-things-quant.tex
@@ -11,7 +11,7 @@
 \olsection{\usetoken{P}{derivation} with Quantifiers}
 
 \begin{ex}
-Let us give a derivation of $(\lforall[x][!A(x)] \land
+Let us give !!a{derivation} of $(\lforall[x][!A(x)] \land
 \lforall[y][!B(y)]) \lif \lforall[x][(!A(x) \land !B(x))]$.
 
 First, note that
diff --git a/content/first-order-logic/axiomatic-deduction/proving-things.tex b/content/first-order-logic/axiomatic-deduction/proving-things.tex
@@ -27,7 +27,7 @@
 Why? Two applications of MP yield the last part, which is what we
 want.  And we easily see that $\lnot !D \lif (!D \lif !E)$ is an
 instance of \olref[prp]{ax:lnot2}, and $!E \lif (!D \lif !E)$ is an
-instance of \olref[prp]{ax:lif1}. So our derivation is:
+instance of \olref[prp]{ax:lif1}. So our !!{derivation} is:
 \begin{derivation}
   1. &  $\lnot !D \lif (!D \lif !E)$ & \olref[prp]{ax:lnot2} \\
   2. & $(\lnot !D \lif (!D \lif !E)) \lif {}$\\
@@ -68,7 +68,7 @@
 also !!{derivable}? Well, the first of these is already an instance of
 \olref[prp]{ax:lif1}, whatever we decide $!B$ to be. And $!D \lif !B$ would
 be another instance of \olref[prp]{ax:lif1} if $!B$ were $(!D \lif !D)$.
-So, our derivation is:
+So, our !!{derivation} is:
 \begin{derivation}
   1. & $!D \lif ((!D \lif !D) \lif !D)$ & \olref[prp]{ax:lif1}\\
   2. & $(!D \lif ((!D \lif !D) \lif !D)) \lif {}$\\
@@ -80,7 +80,7 @@
 \end{ex}
 
 \begin{ex}\ollabel{ex:chain}
-Sometimes we want to show that there is a derivation of some
+Sometimes we want to show that there is !!a{derivation} of some
 !!{formula} from some other !!{formula}s~$\Gamma$. For instance, let's
 show that we can !!{derive} $!A \lif !C$ from $\Gamma = \{!A \lif !B,
 !B \lif !C\}$.
diff --git a/content/first-order-logic/axiomatic-deduction/soundness.tex b/content/first-order-logic/axiomatic-deduction/soundness.tex
@@ -59,13 +59,13 @@
 \begin{proof}
 By induction on the length of the !!{derivation} of $!A$ from
 $\Gamma$. If there are no steps justified by inferences, then all
-!!{formula}s in the derivation are either instances of axioms or are
+!!{formula}s in the !!{derivation} are either instances of axioms or are
 in~$\Gamma$. By the previous proposition, all the axioms are
 \iftag{FOL}{valid}{tautologies}, and hence if $!A$ is an axiom then
 $\Gamma \Entails !A$. If $!A \in \Gamma$, then trivially $\Gamma
 \Entails !A$.
 
-If the last step of the derivation of~$!A$ is justified by modus
+If the last step of the !!{derivation} of~$!A$ is justified by modus
 ponens, then there are !!{formula}s $!B$ and $!B \lif !A$ in the
 !!{derivation}, and the induction hypothesis applies to the part of
 the !!{derivation} ending in those !!{formula}s (since they contain at
diff --git a/content/first-order-logic/natural-deduction/derivations.tex b/content/first-order-logic/natural-deduction/derivations.tex
@@ -71,7 +71,7 @@
 \RightLabel{\Intro{\land}}
 \BinaryInfC{$!D \land !C$}
 \end{prooftree}
-is also a correct derivation.
+is also a correct !!{derivation}.
 
 We can now apply another rule, say, $\Intro{\lif}$, which allows us to
 conclude a conditional and allows us to !!{discharge} any assumption
@@ -98,7 +98,7 @@
 Remember that discharging of assumptions is a permission, not a
 requirement: we don't have to discharge the assumptions. In
 particular, we can apply a rule even if the assumptions are not
-present in the derivation. For instance, the following is legal, even
+present in the !!{derivation}. For instance, the following is legal, even
 though there is no assumption~$!A$ to be !!{discharged}:
 \begin{prooftree}
   \AxiomC{$!B$}
diff --git a/content/first-order-logic/natural-deduction/identity.tex b/content/first-order-logic/natural-deduction/identity.tex
@@ -95,7 +95,7 @@
 \end{prooftree}
 The sub-!!{derivation} on the top right is completed by using its
 assumptions to show that $\eq[a][c]$ and $\eq[b][c]$. This requires two
-separate !!{derivation}s. The derivation for $\eq[a][c]$ is as
+separate !!{derivation}s. The !!{derivation} for $\eq[a][c]$ is as
 follows:
 \begin{prooftree}
 \AxiomC{$\Discharge{\lforall[y][(!A(y) \lif \eq[y][c]])}{2}$}
diff --git a/content/first-order-logic/natural-deduction/provability-consistency.tex b/content/first-order-logic/natural-deduction/provability-consistency.tex
@@ -61,7 +61,7 @@
 \end{prooftree}
 
 Now assume $\Gamma \cup \{\lnot !A\}$ is inconsistent, and let
-$\delta_1$ be the corresponding derivation of $\lfalse$ from
+$\delta_1$ be the corresponding !!{derivation} of~$\lfalse$ from
 !!{undischarged} assumptions in~$\Gamma \cup \{\lnot !A\}$. We obtain
 !!a{derivation} of~$!A$ from~$\Gamma$ alone by using~$\FalseCl$:
 \begin{prooftree}
diff --git a/content/first-order-logic/natural-deduction/proving-things-quant.tex b/content/first-order-logic/natural-deduction/proving-things-quant.tex
@@ -90,7 +90,7 @@
 violated. Since the only rule we applied that is subject to the
 eigenvariable condition was \Elim{\exists}, and the eigenvariable~$a$
 does not occur in any assumptions it depends on, this is a
-correct derivation.
+correct !!{derivation}.
 \end{ex}
 
 \begin{ex}
@@ -177,7 +177,7 @@
 \end{prooftree}
 Since we ensured at each step that the eigenvariable
 conditions were not violated, we can be confident that this
-is a correct derivation.
+is a correct !!{derivation}.
 \end{ex}
 
 \begin{ex}
diff --git a/content/first-order-logic/natural-deduction/proving-things.tex b/content/first-order-logic/natural-deduction/proving-things.tex
@@ -55,7 +55,7 @@
 \lif (!A \lif !B)$.
 
 We begin by writing the desired conclusion at the bottom of the 
-derivation.
+!!{derivation}.
 \begin{prooftree}
 \AxiomC{}
 \UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
diff --git a/content/first-order-logic/natural-deduction/soundness-identity.tex b/content/first-order-logic/natural-deduction/soundness-identity.tex
@@ -21,7 +21,7 @@
 so variable assignments are irrelevant).
 
 Suppose the last inference in !!a{derivation} is \Elim{\eq}, i.e., the
-derivation has the following form:
+!!{derivation} has the following form:
 \begin{prooftree}
   \AxiomC{$\Gamma_1$}
   \RightLabel{$\delta_1$}
diff --git a/content/first-order-logic/natural-deduction/soundness.tex b/content/first-order-logic/natural-deduction/soundness.tex
@@ -85,7 +85,7 @@
 
 \item The last inference is \Elim{\land}: There are two variants: $!A$
   or $!B$ may be inferred from the premise $!A \land !B$. Consider the
-  first case. The derivation~$\delta$ looks like this:
+  first case. The !!{derivation}~$\delta$ looks like this:
   \begin{prooftree}
     \AxiomC{$\Gamma$}
     \RightLabel{$\delta_1$}
@@ -108,7 +108,7 @@
   
 \item The last inference is \Intro{\lor}: There are two variants: $!A
   \lor !B$ may be inferred from the premise~$!A$ or the
-  premise~$!B$. Consider the first case. The derivation has the form
+  premise~$!B$. Consider the first case. The !!{derivation} has the form
   \begin{prooftree}
     \AxiomC{$\Gamma$}
     \RightLabel{$\delta_1$}
@@ -242,7 +242,7 @@
 \item The last inference is \Elim{\lor}: Exercise.
 
 \item The last inference is \Elim{\lif}. $!B$ is inferred from the
-  premises $!A \lif !B$ and~$!A$. The derivation~$\delta$ looks like this:
+  premises $!A \lif !B$ and~$!A$. The !!{derivation}~$\delta$ looks like this:
   \begin{prooftree}
     \AxiomC{$\Gamma_1$}
     \RightLabel{$\delta_1$}
diff --git a/content/first-order-logic/proof-systems/axiomatic-deduction.tex b/content/first-order-logic/proof-systems/axiomatic-deduction.tex
@@ -46,9 +46,9 @@
 The $\Proves$ relation based on axiomatic !!{derivation}s is defined
 as follows: $\Gamma \Proves !A$ iff there is !!a{derivation} with the
 !!{sentence}~$!A$ as its last formula (and $\Gamma$ is taken as the
-set of !!{sentence}s in that derivation which are justified by~(2) above).  $!A$
+set of !!{sentence}s in that !!{derivation} which are justified by~(2) above).  $!A$
 is a theorem if~$!A$ has !!a{derivation} where~$\Gamma$ is empty,
-i.e., every !!{sentence} in the derivation is justified either by (1)
+i.e., every !!{sentence} in the !!{derivation} is justified either by (1)
 or~(3). For instance, here is !!a{derivation} that shows that $\Proves
 !A  \lif (!B \lif (!B \lor !A))$:
 \begin{derivation}
diff --git a/content/first-order-logic/sequent-calculus/derivations.tex b/content/first-order-logic/sequent-calculus/derivations.tex
@@ -77,7 +77,7 @@
 \RightLabel{\LeftR{\Weakening}}
 \UnaryInf$ !C, !D \fCenter !D$
 \end{prooftree}
-is !!a{derivation}. Now we can take these two derivations, and combine
+is !!a{derivation}. Now we can take these two !!{derivation}s, and combine
 them using $\RightR{\land}$. That rule was
 \begin{prooftree}
 \Axiom$\Gamma \fCenter \Delta, !A$
diff --git a/content/first-order-logic/sequent-calculus/proving-things-quant.tex b/content/first-order-logic/sequent-calculus/proving-things-quant.tex
@@ -11,7 +11,7 @@
 \olsection{\usetoken{P}{derivation} with Quantifiers}
 
 \begin{ex}
-Give an $\Log{LK}$-derivation of the sequent $\lexists[x][\lnot !A(x)]
+Give an $\Log{LK}$-!!{derivation} of the sequent $\lexists[x][\lnot !A(x)]
 \Sequent \lnot \lforall[x][!A(x)]$.
 
 When dealing with quantifiers, we have to make sure not to violate the
@@ -79,7 +79,7 @@
 violated. Since the only rule we applied that is subject to the
 eigenvariable condition was \LeftR{\exists}, and the eigenvariable~$a$
 does not occur in its lower sequent (the end-sequent), this is a
-correct derivation.
+correct !!{derivation}.
 \end{ex}
 
 \begin{prob}
diff --git a/content/first-order-logic/sequent-calculus/proving-things.tex b/content/first-order-logic/sequent-calculus/proving-things.tex
@@ -13,9 +13,10 @@
 \olsection{Examples of \usetoken{P}{derivation}}
 
 \begin{ex}
-Give an $\Log{LK}$-derivation for the sequent $!A \land !B \Sequent !A$.
+Give an $\Log{LK}$-!!{derivation} for the sequent $!A \land !B \Sequent !A$.
 
-We begin by writing the desired end-sequent at the bottom of the derivation.
+We begin by writing the desired end-sequent at the bottom of the
+!!{derivation}.
 \begin{prooftree}
 \AxiomC{}
 \UnaryInf$!A\land !B \fCenter !A$
@@ -42,15 +43,15 @@
 \RightLabel{\LeftR{\land}}
 \UnaryInf$!A\land !B \fCenter !A$
 \end{prooftree}
-We now have a correct $\Log{LK}$-derivation of the sequent $!A \land
-!B \Sequent !A$.
+We now have a correct $\Log{LK}$-!!{derivation} of the sequent $!A
+\land !B \Sequent !A$.
 \end{ex}
 
 \begin{ex}
-Give an $\Log{LK}$-derivation for the sequent $\lnot !A \lor !B
+Give an $\Log{LK}$-!!{derivation} for the sequent $\lnot !A \lor !B
 \Sequent !A \lif !B$.
 
-Begin by writing the desired end-sequent at the bottom of the derivation.
+Begin by writing the desired end-sequent at the bottom of the !!{derivation}.
 \begin{prooftree}
 \AxiomC{}
 \UnaryInf$\lnot !A \lor !B \fCenter !A \lif !B$
@@ -151,7 +152,7 @@
 \end{ex}
 
 \begin{ex}
-Give an $\Log{LK}$-derivation of the sequent $\lnot !A \lor \lnot !B
+Give an $\Log{LK}$-!!{derivation} of the sequent $\lnot !A \lor \lnot !B
 \Sequent \lnot (!A \land !B)$
 
 Using the techniques from above, we start by writing the desired
@@ -185,7 +186,7 @@
 \RightLabel{\RightR{\lnot}}
 \UnaryInf$\lnot !A \lor \lnot !B \fCenter \lnot (!A \land !B)$
 \end{prooftree}
-Continuing to fill in the derivation, we see that we run into a problem:
+Continuing to fill in the !!{derivation}, we see that we run into a problem:
 \begin{prooftree}
 \Axiom$!A \fCenter !A$
 \RightLabel{\LeftR{\lnot}}
@@ -245,7 +246,7 @@
 \UnaryInf$\lnot !A \lor \lnot !B \fCenter \lnot (!A \land !B)$
 \end{prooftree}
 (We could have carried out the $\land$ rules lower than the $\lnot$
-rules in these steps and still obtained a correct derivation).
+rules in these steps and still obtained a correct !!{derivation}).
 \end{ex}
 
 \begin{ex}
diff --git a/content/first-order-logic/sequent-calculus/structural-rules.tex b/content/first-order-logic/sequent-calculus/structural-rules.tex
@@ -66,7 +66,7 @@ \subsection{Exchange}
 be indicated by double inference lines.
 
 The following rule, called ``cut,'' is not strictly speaking
-necessary, but makes it a lot easier to reuse and combine derivations.
+necessary, but makes it a lot easier to reuse and combine !!{derivation}s.
 \begin{defish}
 \[
 \Axiom$ \Gamma \fCenter \Delta, !A$
diff --git a/content/incompleteness/arithmetization-syntax/proofs-in-ax.tex b/content/incompleteness/arithmetization-syntax/proofs-in-ax.tex
@@ -31,7 +31,7 @@
   2. & $(!B \lif (!B \lor !A)) \lif (!A  \lif (!B \lif (!B \lor !A)))$\\
   3. & $!A  \lif (!B \lif (!B \lor !A))$
   \end{derivation}
-  The G\"odel number of this derivation would be
+  The G\"odel number of this !!{derivation} would be
   \begin{align*}
   \openTuple\, 
     & \Gn{!B \lif (!B \lor !A)}, \\
@@ -176,7 +176,7 @@
 By the previous proposition, the property $\fn{Deriv}(x)$ which holds
 iff $x$ is the code of a correct !!{derivation}~$\delta$ is primitive
 recursive. However, that definition did not take into account the set
-$\Gamma$ as an additional way to justify lines in the derivation. Our
+$\Gamma$ as an additional way to justify lines in the !!{derivation}. Our
 primitive recursive test of whether a line is justified by \QR{} also
 left out of consideration the requirement that the constant~$c$ is not
 allowed to occur in~$\Gamma$. It is possible to amend our definition so
diff --git a/content/incompleteness/arithmetization-syntax/proofs-in-lk.tex b/content/incompleteness/arithmetization-syntax/proofs-in-lk.tex
@@ -92,7 +92,7 @@
 
 \begin{explain}
 Having settled on a representation of !!{derivation}s, we must also
-show that we can manipulate such derivations primitive recursively,
+show that we can manipulate such !!{derivation}s primitive recursively,
 and express their essential properties and relations so.  Some
 operations are simple: e.g., given a G\"odel number~$p$ of
 !!a{derivation}, $\fn{EndSeq}(p) = (p)_{(p)_0+1}$ gives us the G\"odel
@@ -264,7 +264,7 @@
 $\Gamma_0 \Sequent !A$ is primitive recursive.
 
 By the previous proposition, the property $\fn{Deriv}(x)$ which holds
-iff $x$ is the code of a correct derivation~$\pi$ in $\Log{LK}$ is
+iff $x$ is the code of a correct !!{derivation}~$\pi$ in $\Log{LK}$ is
 primitive recursive.  If $x$ is such a code, then $\fn{EndSequent}(x)$
 is the code of the end-sequent of~$\pi$, and so
 $(\fn{EndSequent}(x))_0$ is the code of the left side of the end
diff --git a/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex b/content/incompleteness/arithmetization-syntax/proofs-in-nd.tex
@@ -319,7 +319,7 @@
   primitive recursive.
 
   By \olref{prop:deriv}, the property $\fn{Deriv}(x)$ which holds iff
-  $x$ is the G\"odel number of a correct derivation~$\delta$ in
+  $x$ is the G\"odel number of a correct !!{derivation}~$\delta$ in
   natural deduction is primitive recursive. Thus we can define
   $\Prf[\Gamma](x, y)$ by
   \begin{align*}
diff --git a/content/incompleteness/introduction/historical-background.tex b/content/incompleteness/introduction/historical-background.tex
@@ -170,10 +170,10 @@
 of proving these systems to be consistent.  He was aided in this
 project by several of his students, in particular Bernays, Ackermann,
 and later Gentzen. The basic idea for accomplishing this goal was to
-cast the question of the possibility of a derivation of an
+cast the question of the possibility of !!{derivation} of an
 inconsistency in mathematics as a combinatorial problem about possible
 sequences of symbols, namely possible sequences of sentences which
-meet the criterion of being a correct derivation of, say, $!A \land
+meet the criterion of being a correct !!{derivation} of, say, $!A \land
 \lnot !A$ from the axioms of an axiom system for arithmetic, analysis,
 or set theory.  A proof of the impossibility of such a sequence of
 symbols would---since it is itself a mathematical proof---be
@@ -193,7 +193,7 @@
 property is called \emph{complete}. Of course, for any given sentence
 it might still be a difficult task to determine which of the two
 alternatives holds.  But in principle there should be a method to do
-so.  In fact, for the axiom and derivation systems considered by
+so.  In fact, for the axiom and !!{derivation} systems considered by
 Hilbert, completeness would imply that such a method exists---although
 Hilbert did not realize this.  The second way to interpret the
 question would be this stronger requirement: that there be a
diff --git a/content/incompleteness/representability-in-q/c-representable.tex b/content/incompleteness/representability-in-q/c-representable.tex
@@ -142,7 +142,7 @@
 
 \begin{proof}
 Let us do 1 and part of 2, informally (i.e., only giving hints as to
-how to construct the formal derivation).
+how to construct the formal !!{derivation}).
 
 For part 1, by the definition of $<$, we need to prove $\lnot
 \lexists[y][\eq[(y'+x)][0]]$ in $\Th{Q}$, which is equivalent (using
diff --git a/content/incompleteness/representability-in-q/minimization-representable.tex b/content/incompleteness/representability-in-q/minimization-representable.tex
@@ -74,7 +74,7 @@
 
 \begin{proof}
 We give the proof informally (i.e., only giving hints as to
-how to construct the formal derivation).
+how to construct the formal !!{derivation}).
 
 We have to prove $\lnot a < \Obj 0$ for an arbitrary~$a$. By the
 definition of $<$, we need to prove $\lnot
diff --git a/content/incompleteness/representability-in-q/representable-comp.tex b/content/incompleteness/representability-in-q/representable-comp.tex
@@ -88,7 +88,7 @@
 m) = \Gn{!A_f(\num{n_0}, \dots, \num{n_k}, \num{m})}$.
 
 Now, consider the relation~$R(n_0, \dots, n_k, s)$ which holds if
-$(s)_0$ is the G\"odel number of a derivation from~$\Th{Q}$ of
+$(s)_0$ is the G\"odel number of !!a{derivation} from~$\Th{Q}$ of
 $!A_f(\num{n_0}, \dots, \num{n_k}, \num{(s)_1})$:
 \[
 R(n_0, \dots, n_k, s) \quad\text{iff}\quad \Prf[\Th{Q}]((s)_0, A(n_0,
diff --git a/content/intuitionistic-logic/propositions-as-types/reduction.tex b/content/intuitionistic-logic/propositions-as-types/reduction.tex
@@ -42,8 +42,9 @@
 out.'' In general, we see that the conclusion of $\Elim{\land}$ is
 always the formula on one side of the conjunction, and the premises of
 $\Intro{\land}$ requires both sides of the conjunction, thus if we
-need a derivation of either side, we can simply use that derivation
-without introducing the conjunction followed by eliminating it.
+need !!a{derivation} of either side, we can simply use that
+!!{derivation} without introducing the conjunction followed by
+eliminating it.
 
 Thus in general we have
 \begin{gather*}
diff --git a/content/intuitionistic-logic/propositions-as-types/terms-to-proofs.tex b/content/intuitionistic-logic/propositions-as-types/terms-to-proofs.tex
diff --git a/content/intuitionistic-logic/soundness-completeness/soundness-nd.tex b/content/intuitionistic-logic/soundness-completeness/soundness-nd.tex
diff --git a/content/lambda-calculus/church-rosser/beta-eta-reduction.tex b/content/lambda-calculus/church-rosser/beta-eta-reduction.tex
diff --git a/content/lambda-calculus/church-rosser/beta-reduction.tex b/content/lambda-calculus/church-rosser/beta-reduction.tex
diff --git a/content/lambda-calculus/church-rosser/parallel-beta-eta-reduction.tex b/content/lambda-calculus/church-rosser/parallel-beta-eta-reduction.tex
diff --git a/content/lambda-calculus/church-rosser/parallel-beta-reduction.tex b/content/lambda-calculus/church-rosser/parallel-beta-reduction.tex
diff --git a/content/lambda-calculus/syntax/alpha.tex b/content/lambda-calculus/syntax/alpha.tex
diff --git a/content/normal-modal-logic/axioms-systems/introduction.tex b/content/normal-modal-logic/axioms-systems/introduction.tex
diff --git a/content/normal-modal-logic/axioms-systems/logics-proofs.tex b/content/normal-modal-logic/axioms-systems/logics-proofs.tex
diff --git a/content/second-order-logic/syntax-and-semantics/syntax-and-semantics.tex b/content/second-order-logic/syntax-and-semantics/syntax-and-semantics.tex
diff --git a/content/sets-functions-relations/relations/trees.tex b/content/sets-functions-relations/relations/trees.tex
diff --git a/content/turing-machines/undecidability/verification.tex b/content/turing-machines/undecidability/verification.tex
