refactor

main.typ

@@ -1,253 +1,246 @@
 #set page(margin: 1cm, columns: 2)
 
+#show outline.entry.where(level: 1): it => {
+  upper(it)
+}
+
 #set heading(numbering: "1.")
 
-#show outline.entry.where(level: 1): it => {
+#set enum(numbering: "a1Ai)")
-  v(12pt, weak: true)
+#outline(indent: 1em)
-  strong(it)
-}
 
-#set enum(numbering: "a)")
+= Logical axiom schemes <logical-axiom-schemes>
 
-// #show outline.entry.where(
+$bold(L_1): B->(C->B)$
-//   level: 1
-// ): it => {
-//   v(12pt, weak: true)
-//   strong(it)
-// }
 
-#outline(indent: auto)
+$bold(L_2): (B->(C->D))->((B->C)->(B->D))$
 
-= Logical axiom schemes
+$bold(L_3): B and C->B$
 
-$bold(L_1): B→(C →B)$
+$bold(L_4): B and C->C$
 
-$bold(L_2): (B→(C →D))→((B→C)→( B→D))$
+$bold(L_5): B->(C->B and C)$
 
-$bold(L_3): B∧C→B$
+$bold(L_6): B->B or C$
 
-$bold(L_4): B∧C→C$
+$bold(L_7): C->B or C$
 
-$bold(L_5): B→(C →B∧C)$
+$bold(L_8): (B->D)->((C->D)->(B or C->D))$
 
-$bold(L_6): B→B∨C$
+$bold(L_9): (B->C)->((B->not C )-> not B)$
 
-$bold(L_7): C →B∨C$
+$bold(L_10): not B->(B->C)$
 
-$bold(L_8): (B→D)→((C →D)→(B∨C →D))$
+$bold(L_11): B or not B$
 
-$bold(L_9): (B→C)→((B→¬C )→¬B)$
+$bold(L_12): forall x F (x)->F (t) ("in particular," forall x F (x)->F(x)$)
 
-$bold(L_10): ¬B→( B→C)$
+$bold(L_13): F(t)->exists x F(x) ("in particular," F (x)->exists x F(x))$
 
-$bold(L_11): B∨¬B$
+$bold(L_14): forall x(G ->F (x))->(G->forall x F(x))$
 
-$bold(L_12): ∀x F (x)→F (t)$ (in particular, $∀x F (x)→F (x)$)
+$bold(L_15): forall x(F(x)->G)->(exists x F(x)->G)$
 
-$bold(L_13): F (t)→∃ x F( x)$ (in particular, $F (x)→∃ x F (x)$)
+= Theorems <theorems>
-
-$bold(L_14): ∀x(G →F (x))→(G→∀x F (x)) $
-
-$bold(L_15): ∀x(F (x) arrow G) arrow (exists x F (x)→G)$
-
-= Theorems
 
 == Prooving directly
 
-$[L_1, L_2, #[MP]]$:
+$[L_1, L_2, M P]$:
 
-+ $((A→B)→(A→C))→(A→(B→C))$. Be careful when assuming hypotheses: assume
++ $((A->B)->(A->C))->(A->(B->C))$. Be careful when assuming hypotheses: assume
-  (A→B)→(A→C), A, B – in this order, no other possibilities!
+  $(A->B)->(A->C), A, B$ -- in this order, no other possibilities!
-+ $(A→B)→((B→C)→(A→C))$. It's another version of the *Law of Syllogism* (by
++ $(A->B)->((B->C)->(A->C))$. It's another version of the *Law of Syllogism* (by
   Aristotle), or the transitivity property of implication.
-+ $(A→(B→C))→(B→(A→C))$. It's another version of the *Premise Permutation Law*.
++ $(A->(B->C))->(B->(A->C))$. It's another version of the *Premise Permutation
-  Explain the difference between this formula and Theorem 1.4.3(a): A→(B→C)├
+  Law*.
-  B→(A→C).
 
-== Deduction theorems
+== Deduction theorems <deduction>
 
-=== Theorem 1.5.1 (Deduction Theorem 1 AKA DT1)
+=== Theorem 1.5.1 (Deduction Theorem 1 AKA $D T 1$)
 
 If $T$ is a first order theory, and there is a proof of
-$[T, #[MP]]: A_1, A_2, dots, A_n, B├ C$, then there is a proof of
+$[T, M P]: A_1, A_2, ..., A_n, B tack.r C$, then there is a proof of
-$[L_1, L_2, T, #[MP]]: A_1, A_2, dots, A_n├ B→C$.
+$[L_1, L_2, T, M P]: A_1, A_2, ..., A_n tack.r B->C$.
 
-=== Theorem 1.5.2 (Deduction Theorem 2 AKA DT2)
+=== Theorem 1.5.2 (Deduction Theorem 2 AKA $D T 2$)
 
-If there is a proof $[T, #[MP], #[Gen]]: A_1, A_2, dots, A_n, B├ C$, where,
+If there is a proof $[T, M P, G e n]: A_1, A_2, ..., A_n, B tack.r C$, where,
 after B appears in the proof, Generalization is not applied to the variables
 that occur as free in $B$, then there is a proof of
-$[L_1, L_2, L_14, T, #[MP], #[Gen]]: A_1, A_2, dots, A_n├ B→C$.
+$[L_1, L_2, L_14, T, M P, G e n]: A_1, A_2, ..., A_n tack.r B->C$.
 
-== Conjunction
+== Conjunction <conjunction>
 
 === Theorem 2.2.1.
 
-+ (C-introduction): $[L_5, #[MP]]: A, B├ A∧B$;
++ (C-introduction): $[L_5, M P]: A, B tack.r A and B$;
-+ (C-elimination): $[L_3, L_4, #[MP]]: A∧B ├ A, A∧B ├ B$.
++ (C-elimination): $[L_3, L_4, M P]: A and B tack.r A, A and B tack.r B$.
 
 === Theorem 2.2.2.
 
-+ $[L_1, L_2, L_5, #[MP]]: (A→(B→C)) ↔ ((A→B)→(A→C))$ (extension of the axiom
++ $[L_1, L_2, L_5, M P]: (A->(B->C)) <-> ((A->B)->(A->C))$ (extension of the axiom
   L_2).
-+ $[L_1-L_4, #[MP]]: (A→B)∧( B→C)→( A→C)$ (another form of the *Law of Syllogism*,
++ $[L_1-L_4, M P]: (A->B) and (B->C)->(A->C)$ (another form of the *Law of
-  or *transitivity property of implication*).
+  Syllogism*, or *transitivity property of implication*).
 
 === Theorem 2.2.3 (properties of the conjunction connective).
 
-$[L_1- L_5, #[MP]]$:
+$[L_1-L_5, M P]$:
 
-+ $A∧B↔B∧A$ . Conjunction is commutative.
++ $A and B<->B and A$ . Conjunction is commutative.
-+ $ A∧(B∧C)↔( A∧B)∧C$. Conjunction is associative.
++ $ A and (B and C)<->( A and B) and C$. Conjunction is associative.
-+ $A∧A↔A$ . Conjunction is idempotent.
++ $A and A<->A$ . Conjunction is idempotent.
 
 === Theorem 2.2.4 (properties of the equivalence connective).
 
-$[L_1- L_5, #[MP]]$:
+$[L_1- L_5, M P]$:
 
-+ $A↔A$ (reflexivity),
++ $A<->A$ (reflexivity),
-+ $(A↔B)→(B↔A)$ (symmetry),
++ $(A<->B)->(B<->A)$ (symmetry),
-+ $(A↔B)→((B↔C) →((A↔C))$ (transitivity).
++ $(A<->B)->((B<->C) ->((A<->C))$ (transitivity).
 
-== Disjunction
+== Disjunction <disjunction>
 
 === Theorem 2.3.1
 
-+ (D-introduction)$[L_6, L_7, #[MP]]: A├ A∨B; B├ A∨B$;
++ (D-introduction)$[L_6, L_7, M P]: A tack.r A or B; B tack.r A or B$;
-+ (D-elimination) If there is a proof $[T, #[MP]]: A_1, A_2, ..., A_n, B├ D$, and
++ (D-elimination) If there is a proof $[T, M P]: A_1, A_2, ..., A_n, B tack.r D$,
-  a proof $[T, #[MP]]: A_1, A_2, ..., A_n, C├ D$, then there is a proof $[T,
+  and a proof $[T, M P]: A_1, A_2, ..., A_n, C tack.r D$, then there is a proof $[T,
-  L_1, L_2, L_8, #[MP]]: A_1, A_2, dots, A_n, B∨C ├ D$.
+  L_1, L_2, L_8, M P]: A_1, A_2, ..., A_n, B or C tack.r D$.
 
 === Theorem 2.3.2
 
-a) $[ L_5, L_6-L_8, #[MP]]: A∨B↔B∨A$ . Disjunction is commutative. b) $[L_1, L_2, L_5, L_6-L_8, #[MP]]: A∨A↔A$ .
++ $[L_5, L_6-L_8, M P]: A or B<->B or A$. Disjunction is commutative.
-Disjunction is idempotent.
++ $[L_1, L_2, L_5, L_6-L_8, M P]: A or A<->A$. Disjunction is idempotent.
 
-=== Theorem 2.3.3.
+=== Theorem 2.3.3
 
-Disjunction is associative: $[L_1, L_2, L_5, L_6-L_8, #[MP]]: A∨(B∨C)↔(
+Disjunction is associative: $[L_1, L_2, L_5, L_6-L_8, M P]: A or (B or C)<->(A or B) or C$.
-A∨B)∨C$.
 
-=== Theorem 2.3.4.
+=== Theorem 2.3.4
 
 Conjunction is distributive to disjunction, and disjunction is distributive to
 conjunction:
 
-+ $[L_1-L_8, #[MP]]: (A∧B)∨C ↔(A∨C)∧(B∨C)$ .
++ $[L_1-L_8, M P]: (A and B) or C <->(A or C) and (B or C)$ .
-+ $[L_1-L_8, #[MP]]: (A∨B)∧C ↔(A∧C)∨(B∧C)$ .
++ $[L_1-L_8, M P]: (A or B) and C <->(A and C) or (B and C)$ .
 
-=== Theorem 2.3.4.
+=== Theorem 2.3.4
 
 Conjunction is distributive to disjunction, and disjunction is distributive to
 conjunction:
 
-+ $[L_1-L_8, #[MP]]: (A∧B)∨C ↔(A∨C)∧(B∨C)$;
++ $[L_1-L_8, M P]: (A and B) or C <->(A or C) and (B or C)$;
-+ $[L_1-L_8, #[MP]]: (A∨B)∧C ↔(A∧C)∨(B∧C)$ .
++ $[L_1-L_8, M P]: (A or B) and C <->(A and C) or (B and C)$ .
 
 == Negation -- minimal logic
 
-=== Theorem 2.4.1.
+=== Theorem 2.4.1
 
 (N-elimination) If there is a proof
 
-$[T, #[MP]]: A_1, A_2, ..., A_n, B├ C$, and a proof $[T, #[MP]]: A_1, A_2, ..., A_n,
+$[T, M P]: A_1, A_2, ..., A_n, B tack.r C$, and a proof $[T, M P]: A_1, A_2, ..., A_n,
-B├ ¬C$, then there is a proof $[T, L_1, L_2, L_9, #[MP]]: A_1, A_2, ..., A_n├ ¬B$.
+B tack.r not C$, then there is a proof $[T, L_1, L_2, L_9, M P]: A_1, A_2, ..., A_n tack.r not B$.
 
-=== Theorem 2.4.2.
+=== Theorem 2.4.2
 
-a) $[L_1, L_2, L_9, #[MP]]: A, ¬B├ ¬(A→B)$. What does it mean? b) $[L_1-L_4, L_9, #[MP]]: A∧¬B→¬( A→B)$.
++ $[L_1, L_2, L_9, M P]: A, not B tack.r not (A->B)$. What does it mean?
++ $[L_1-L_4, L_9, M P]: A and not B->not (A->B)$.
 
-=== Theorem 2.4.3.
+=== Theorem 2.4.3
 
-$[L_1, L_2, L_9, #[MP]]: (A→B)→(¬B→¬A)$. What does it mean? It's the so-called
+$[L_1, L_2, L_9, M P]: (A->B)->( not B-> not A)$. What does it mean? It's the
-*Contraposition Law*.
+so-called *Contraposition Law*.
 
 Note. The following rule form of Contraposition Law is called *Modus Tollens*:
-$[L_1, L_2, L_9, #[MP]]: A→B, ¬B├ ¬A, or, frac(A→B \; ¬B, ¬A)$
+$[L_1, L_2, L_9, M P]: A->B, not B tack.r not A, or, ((A->B; not B)/(not A)$ // TODO: factcheck
 
-=== Theorem 2.4.4.
+=== Theorem 2.4.4
 
-$[L_1, L_2, L_9, #[MP]]: A→¬¬A$.
+$[L_1, L_2, L_9, M P]: A->not not A$.
 
-=== Theorem 2.4.5.
+=== Theorem 2.4.5
 
-a) $[L_1, L_2, L_9, #[MP]]: ¬¬¬A↔¬A$. b) $[L_1, L_2, L_6, L_7, L_9, #[MP]]: ¬¬( A∨¬A)$.
++ $[L_1, L_2, L_9, M P]: not not not A<-> not A$.
-What does it mean? This is a “weak form” of the *Law of Excluded Middle* that
++ $[L_1, L_2, L_6, L_7, L_9, M P]: not not ( A or not A)$.
-can be proved constructively. The formula $¬¬( A∨¬A)$ can be proved in the
+What does it mean? This is a "weak form" of the *Law of Excluded Middle* that
-constructive logic, but $A∨¬A$ can't – as we will see in Section 2.8.
+can be proved constructively. The formula $ not not ( A or not A)$ can be proved
+in the constructive logic, but $A or not A$ can't -- as we will see in
+@axiom-indempendence.
 
-=== Theorem 2.4.9.
+=== Theorem 2.4.9
 
-+ $[L_1, L_2, L_8, L_9, #[MP]]: ¬A∨¬B→¬( A∧B)$ . It's the constructive half of the
++ $[L_1, L_2, L_8, L_9, M P]: not A or not B-> not ( A and B)$ . It's the
-  so-called *First de Morgan Law*. What does it mean?
+  constructive half of the so-called *First de Morgan Law*. What does it mean?
-+ $[L_1-L_9, #[MP]]: ¬(A∨B)↔¬A∧¬B$. It's the so-called *Second de Morgan Law*.
++ $[L_1-L_9, M P]: not (A or B)<-> not A and not B$. It's the so-called *Second de
+  Morgan Law*.
 
 == Negation -- constructive logic
 
-=== Theorem 2.5.1.
+=== Theorem 2.5.1
 
-+ $[L_1, L_8, L_10, #[MP]]: ¬A∨B→( A→B)$.
++ $[L_1, L_8, L_10, M P]: not A or B->( A->B)$.
-+ $[L_1, L_2, L_6, #[MP]]: A∨B→(¬A→B) ├¬A→(A→B)$ . It means that the “natural”
++ $[L_1, L_2, L_6, M P]: A or B->( not A->B) tack.r not A->(A->B)$ . It means that
-  rule $A∨B ;¬ A ├ B$ implies $L_10$!
+  the "natural" rule $A or B ; not A tack.r B$ implies $L_10$!
 
-=== Theorem 2.5.2.
+=== Theorem 2.5.2
 
-$[L_1-L_10, #[MP]]$:
+$[L_1-L_10, M P]$:
 
-+ $(¬¬A→¬¬B)→¬¬(A→B)$. It's the converse of Theorem 2.4.7(b). Hence, $[L_1-L_10,
++ $( not not A-> not not B)-> not not (A->B)$. It's the converse of Theorem
-  #[MP]]:├ ¬¬(A→B)↔(¬¬A→¬¬B)$.
+  2.4.7(b). Hence, $[L_1-L_10,
-+ $¬¬A→(¬A→A)$. It's the converse of Theorem 2.4.6(a). Hence, [L1-L10,
+  M P]: tack.r not not (A->B)<->( not not A-> not not B)$.
-  #[MP]]: $¬¬A↔(¬A→A)$.
++ $ not not A->( not A->A)$. It's the converse of Theorem 2.4.6(a). Hence, $[L_1-L)10, M P]: not not A<->(not A->A)$.
-+ $A∨¬ A→(¬¬A→A)$ .
++ $A or not A->(not not A->A)$.
-+ $¬¬(¬¬A→A)$. What does it mean? It’s a “weak” form of the Double Negations Law –
++ $ not not (not not A->A)$. What does it mean? It’s a "weak" form of the Double
-  provable in constructive logic.
+  Negations Law -- provable in constructive logic.
 
 == Negation -- classical logic
 
 === Theorem 2.6.1. (Double Negation Law)
 
-$[L_1, L_2, L_8, L_10, L_11, #[MP]]: ¬¬A → A$. Hence, $[L_1-L_11, #[MP]]: ¬¬A ↔
+$[L_1, L_2, L_8, L_10, L_11, M P]: not not A -> A$. Hence, $[L_1-L_11, M P]: not not A <->
 A$.
 
-=== Theorem 2.6.2.
+=== Theorem 2.6.2
 
-$[L_8, L_11, #[MP]]: A→B, ¬A→B├ B$. Or, by Deduction Theorem 1, $[L_1, L_2, L_8,
+$[L_8, L_11, M P]: A->B, not A->B tack.r B$. Or, by Deduction Theorem 1, $[L_1, L_2, L_8,
-L_11, #[MP]]: (A→B)→((¬A→B)→B)$.
+L_11, M P]: (A->B)->(( not A->B)->B)$.
 
-=== Theorem 2.6.3.
+=== Theorem 2.6.3
 
-$[L_1-L_11, #[MP]]: (¬B→¬A)→(A→B)$. Hence, $[L_1-L_11, #[MP]]: (A→B) ↔ (¬B→¬A)$.
+$[L_1-L_11, M P]: ( not B-> not A)->(A->B)$. Hence, $[L_1-L_11, M P]: (A->B) <-> ( not B-> not A)$.
 
-=== Theorem 2.6.3.
+=== Theorem 2.6.3
 
 _(another one with the same number of because numbering error (it seems like it))_
 
-$[L_1-L_9, L_11, #[MP]]: ˫ ¬(A∧B)→¬A∨¬B$ . Hence, $[L_1-L_9, L_11, #[MP]]: ˫
+$[L_1-L_9, L_11, M P]: ˫ not (A and B)-> not A or not B$ . Hence, $[L_1-L_9, L_11, M P]: ˫
-¬(A∧B)↔¬A∨¬B$ .
+not (A and B)<-> not A or not B$ .
 
-=== Theorem 2.6.4.
+=== Theorem 2.6.4
 
-$[L_1-L_8, L_11, #[MP]]: (A→B)→¬ A∨B $. Hence, (I-elimination) $[L_1-L_11, #[MP]]:
+$[L_1-L_8, L_11, M P]: (A->B)-> not A or B $. Hence, (I-elimination) $[L_1-L_11, M P]:
-(A→B)↔¬ A∨B$.
+(A->B)<-> not A or B$.
 
-=== Theorem 2.6.5.
+=== Theorem 2.6.5
 
-$[L_1-L_11, #[MP]]: ¬(A→B)→A∧¬B $.
+$[L_1-L_11, M P]: not (A->B)->A and not B $.
 
-=== Theorem 2.7.1 (Glivenko's Theorem).
+=== Theorem 2.7.1 (Glivenko's Theorem)
 
-$[L_1-L_11, #[MP]]:├ A$ if and only if $[L_1-L_10, #[MP]]:├ ¬¬A$.
+$[L_1-L_11, M P]: tack.r A$ if and only if $[L_1-L_10, M P]: tack.r not not A$.
 
-== Axiom independence
+== Axiom independence <axiom-indempendence>
 
-=== Theorem 2.8.1.
+=== Theorem 2.8.1
 
-The axiom $L_9$: $(A→B)→((A→¬B)→¬A)$ can be proved in $[L_1, L_2, L_8, L_10,
+The axiom $L_9$: $(A->B)->((A-> not B)-> not A)$ can be proved in $[L_1, L_2, L_8, L_10,
-L_11, #[MP]]$.
+L_11, M P]$.
 
-=== Theorem 2.8.2.
+=== Theorem 2.8.2
 
-The axiom $L_9$ cannot be proved in $[L_1-L_8, L_10, #[MP]]$.
+The axiom $L_9$ cannot be proved in $[L_1-L_8, L_10, M P]$.
 
 == Replacement Theorem 1
 
@@ -256,7 +249,7 @@ $C$, and $o(B)$ is a propositional occurrence of $B$ in $C$. Let us denote by
 $C'$ the formula obtained from $C$ by replacing $o(B)$ by $B'$. Then, in the
 minimal logic,
 
-$[L_1-L_9, #[MP]]: B↔B'├ C↔C'$.
+$[L_1-L_9, M P]: B<->B' tack.r C<->C'$.
 
 == Replacement Theorem 2
 
@@ -264,83 +257,80 @@ Let us consider three formulas: $B$, $B'$, $C$, where $B$ is a sub-formula of
 $C$, and $o(B)$ is any occurrence of $B$ in $C$. Let us denote by $C'$ the
 formula obtained from $C$ by replacing $o(B)$ by B'. Then, in the minimal logic,
 
-$[L_1-L_9, L_12-L_15, #[MP], #[Gen]]: B↔B'├ C↔C'$.
+$[L_1-L_9, L_12-L_15, M P, G e n]: B<->B' tack.r C<->C'$.
 
-== Theorem 3.1.1.
+== Theorem 3.1.1
 
-$[L_1, L_2, L_12, L_13, #[MP]]: forall x B(x) arrow exists x B(x)$ . What does
+$[L_1, L_2, L_12, L_13, M P]: forall x B(x) -> exists x B(x)$. What does it
-it mean? It prohibits "empty domains".
+mean? It prohibits "empty domains".
 
-Theorem 3.1.2.
+== Theorem 3.1.2
 
-+ [L1, L2, L12, L14, MP, Gen]: ∀x(B→C)→(∀x B→∀xC).
++ $[L_1, L_2, L_12, L_14, M P, G e n]: forall x(B->C)->(forall x B -> forall x C)$.
-+ [L1, L2, L12-L15, MP, Gen]: ∀x(B→C)→(∃z(x+z+1=y).x B→∃z(x+z+1=y).xC).
++ $[L_1, L_2, L_12-L_15, M P, G e n]: forall x(B->C)->(exists x B->exists x C)$.
 
-== Theorems 3.1.3.
+== Theorems 3.1.3
 
-If F is any formula, then:
+If $F$ is any formula, then:
 
-+ (U-introduction) [Gen]: F(x) ├∀x F(x) .
++ (U-introduction) $[G e n]: F(x) tack.r forall x F(x)$.
-+ (U-elimination) [L12, MP, Gen]: ∀x F(x) ├F(x) . What does it mean?
++ (U-elimination) $[L_12, M P, G e n]: forall x F(x) tack.r F(x)$.
-+ (E-introduction) [L13, MP, Gen]: F(x) ├∃z(x+z+1=y).x F(x) . What does it mean?
++ (E-introduction) $[L_13, M P, G e n]: F(x) tack.r exists z(x+z+1=y).x F(x)$.
 
-== Theorems 3.1.4.
+== Theorems 3.1.4
 
-If F is any formula, and G is a formula that does not contain free occurrences
+If $F$ is any formula, and $G$ is a formula that does not contain free
-of x, then:
+occurrences of $x$, then:
 
-+ (U2-introduction) [L14, MP, Gen] G →F (x) ├G →∀x F (x) . What does it mean?
++ (U2-introduction) $[L_14, M P, G e n] G -> F (x) tack.r G -> forall x F (x)$.
-+ (E2-introduction) [L15, MP, Gen]: F (x)→G ├∃z(x+z+1=y).x F (x)→G . What does it
++ (E2-introduction) $[L_15, M P, G e n]: F(x)->G tack.r exists x F (x)->G$.
-  mean?
 
-== Theorem 3.1.5.
+== Theorem 3.1.5
 
-+ [L1, L2, L5, L12, L14, MP, Gen]: $forall x forall y B(x,y) ↔ forall y forall x B(x,y)$
++ $[L_1, L_2, L_5, L_12, L_14, M P, G e n]: forall x forall y B(x,y) <-> forall y forall x B(x,y)$
-+ [L1, L2, L5, L13, L15, MP, Gen]: $exists x exists y B(x,y) ↔ exists y exists x B(x,y)$.
++ $[L_1, L_2, L_5, L_13, L_15, M P, G e n]: exists x exists y B(x,y) <-> exists y exists x B(x,y)$.
-+ [L1, L2, L12-L15, MP, Gen]: $exists x forall y B(x,y) ↔ forall y exists x B(x,y)$.
++ $[L_1, L_2, L_12-L_15, M P, G e n]: exists x forall y B(x,y) <-> forall y exists x B(x,y)$.
 
-Theorem 3.1.6. If the formula B does not contain free occurrences of x, then
+== Theorem 3.1.6
-[L1-L2, L12-L15, MP, Gen]: (∀x B)↔B;(∃z(x+z+1=y).x B)↔B , i.e., quantifiers ∀x
+If the formula $B$ does not contain free occurrences of $x$, then
-;∃z(x+z+1=y). x can be dropped or introduced as needed.
+$[L_1-L_2, L_12-L_15, M P, G e n]: (forall x B)<->B;(exists x B)<->B$, i.e.,
+quantifiers $forall x; exists x$ can be dropped or introduced as needed.
 
-Theorem 3.2.1. In the classical logic, [L1-L15, MP, Gen]: ¬ x¬B ∀ ↔ xB.
+== Theorem 3.2.1
+In the classical logic, $[L_1-L_15, M P, G e n]: not x not B forall <-> x B$.
 
-== Theorem 3.3.1.
+== Theorem 3.3.1
 
-+ [L1-L5, L12, L14, MP, Gen]: ∀x(B∧C)↔∀x B∧∀xC .
++ $[L_1-L-5, L_12, L_14, M P, G e n]: forall x(B and C)<-> forall x B and forall x C$.
-+ [L1, L2, L6-L8, L12, L14, MP, Gen]: ├∀x B∨∀xC →∀x(B∨C) . The converse formula
++ $[L_1, L_2, L_6-L_8, L_12, L_14, M P, G e n]: tack.r forall x B or forall x C -> forall x(B or C)$.
-  ∀x(B∨C)→∀x B∨∀xC cannot be true. Explain, why.
+  The converse formula $forall x(B or C)-> forall x B or forall x C$ cannot be
+  true.
 
-== Theorem 3.3.2.
+== Theorem 3.3.2
 
-a) [L1-L8, L12-L15, MP, Gen]: ∃z(x+z+1=y).x(B∨C)↔∃z(x+z+1=y). x B∨∃z(x+z+1=y).xC
++ $[L_1-L_8, L_12-L_15, M P, G e n]: exists x(B or C)<-> exists x B or exists x C$
-. b) [L1-L5, L13-L15, MP, Gen]: ∃z(x+z+1=y).x(B∧C)→∃z(x+z+1=y). x
++ $[L_1-L_5, L_13-L_15, M P, G e n]: exists x(B and C)-> exists x B and exists C$.
-B∧∃z(x+z+1=y).xC . The converse implication ∃z(x+z+1=y).x B∧∃z(x+z+1=y). xC
+  The converse implication $exists x B and exists x C -> exists x(B and C)$ cannot
-→∃z(x+z+1=y). x(B∧C) cannot be true. Explain, why. Exercise 3.3.3. a) Prove (a→)
+  be true.
-of Theorem 3.3.2. (Hint: start by assuming B∨C , apply D-elimination, etc., and
-finish by E2-introduction.)
 
 = Three-valued logic
 
-This is a general scheme (page 74) to define a three valued logic.
-
 For example, let us consider a kind of "three-valued logic", where 0 means
-"false", 1 – "unknown" (or NULL – in terms of SQL), and 2 means "true". Then it
+"`false`", 1 -- "`unknown`" (or `NULL` -- in terms of SQL), and 2 means "true".
-would be natural to define “truth values” of conjunction and disjunction as
+Then it would be natural to define "truth values" of conjunction and disjunction
+as
 
-$A∧B=min ( A, B)$ ;
+$A and B=min ( A, B)$ ;
 
-$A∨B=max (A , B)$ .
+$A or B=max (A , B)$ .
 
-But how should we define “truth values” of implication and negation?
+But how should we define "truth values" of implication and negation?
 
 #table(
-  columns: 5, [$A$], [$B$], [$A∧B$], [$A∨B$], [$A→B$], [$0$], [$0$], [$0$], [$0$], [$i_1$], [$0$], [$1$], [$0$], [$1$], [$i_2$], [$0$], [$2$], [$0$], [$2$], [$i_3$], [$1$], [$0$], [$0$], [$1$], [$i_4$], [$1$], [$1$], [$1$], [$1$], [$i_5$], [$1$], [$2$], [$1$], [$2$], [$i_6$], [$2$], [$0$], [$0$], [$2$], [$i_7$], [$2$], [$1$], [$1$], [$2$], [$i_8$], [$2$], [$2$], [$2$], [$2$], [$i_9$],
+  columns: 5, $A$, $B$, $A and B$, $A or B$, $A->B$, $0$, $0$, $0$, $0$, $i_1$, $0$, $1$, $0$, $1$, $i_2$, $0$, $2$, $0$, $2$, $i_3$, $1$, $0$, $0$, $1$, $i_4$, $1$, $1$, $1$, $1$, $i_5$, $1$, $2$, $1$, $2$, $i_6$, $2$, $0$, $0$, $2$, $i_7$, $2$, $1$, $1$, $2$, $i_8$, $2$, $2$, $2$, $2$, $i_9$,
 )
 
-#table(
+#table(columns: 2, $A$, $not A$, $0$, $i_10$, $1$, $i_11$, $2$, $i_12$)
-  columns: 2, [$A$], [¬$A$], [$0$], [$i_10$], [$1$], [$i_11$], [$2$], [$i_12$],
-)
 
 = Model interpreation
 
@@ -350,68 +340,62 @@ But how should we define “truth values” of implication and negation?
 
 Let L be a predicate language containing:
 
-- (a possibly empty) set of object constants $c_1, dots, c_k, dots $;
+- (a possibly empty) set of object constants $c_1, ..., c_k, ... $;
-- (a possibly empty) set of function constants $f_1, dots, f_m, dots,$;
+- (a possibly empty) set of function constants $f_1, ..., f_m, ...,$;
 - (a non empty) set of predicate constants $p_1, ..., p_n, ...$.
 
 An interpretation $J$ of the language $L$ consists of the following two entities
 (a set and a mapping):
 
-+ A non-empty finite or infinite set DJ – the domain of interpretation (it will
++ A non-empty finite or infinite set DJ -- the domain of interpretation (it will
   serve first of all as the range of object variables). (For infinite domains, set
   theory comes in here.)
 + A mapping intJ that assigns:
-  - to each object constant $c_i$ – a member $#[int]_J (c_i)$ of the domain
+  - to each object constant $c_i$ -- a member $"int"_J (c_i)$ of the domain $D_J$ [contstant
-    $D_J$ [contstant corresponds to an object from domain];
+    corresponds to an object from domain];
-  - to each function constant $f_i$ – a function $#[int]_J (f_i)$ from $D_J times dots
+  - to each function constant $f_i$ -- a function $"int"_J (f_i)$ from $D_J times ... times D_J$ into $D_J$ [],
-    times D_J$ into $D_J$ [],
+  - to each predicate constant $p_i$ -- a predicate $"int"_J (p_i)$ on $D_J$.
-  - to each predicate constant $p_i$ – a predicate $#[int]_J (p_i)$ on $D_J$.
 
 Having an interpretation $J$ of the language $L$, we can define the notion of
 *true formulas* (more precisely − the notion of formulas that are true under the
 interpretation $J$).
 
-*Example.* The above interpretation of the “language about people” put in the
+*Example.* The above interpretation of the "language about people" put in the
 terms of the general definition:
 
-+ $D = {#[br], #[jo], #[pa], #[pe]}$.
++ $D = {"br", "jo", "pa", "pe"}$.
-+ $#[int]_J (#[Britney])=#[br], #[int]_J (#[John])=#[jo], #[int]_J (#[Paris])=#[pa],
++ $"int"_J ("Britney")="br", "int"_J ("John")="jo", "int"_J ("Paris")="pa", "int"_J ("Peter")="pe"$.
-  #[int]_J (#[Peter])=#[pe]$.
++ $"int"_J ("Male") = {"jo", "pe"}; "int"_J ("Female") = {"br", "pa"}$.
-+ $#[int]_J (#[Male]) = {#[jo], #[pe]}; #[int]_J (#[Female]) = {#[br], #[pa]}$.
++ $"int"_J ("Mother") = {("pa", "br"), ("pa", "jo")}; "int"_J ("Father") = {("pe", "jo"), ("pe", "br")}$.
-+ $#[int]_J (#[Mother]) = {(#[pa], #[br]), (#[pa], #[jo])}; #[int]_J (#[Father]) =
++ $"int"_J ("Married") = {("pa", "pe"), ("pe", "pa")}$.
-  {(#[pe], #[jo]), (#[pe], #[br])}$.
++ $"int"_J (=) = {("br", "br"), ("jo", "jo"), ("pa", "pa"), ("pe", "pe")}$.
-+ $#[int]_J (#[Married]) = {(#[pa], #[pe]), (#[pe], #[pa])}$.
-+ $#[int]_J (=) = {(#[br], #[br]), (#[jo], #[jo]), (#[pa], #[pa]), (#[pe],
-  #[pe])}$.
 
 === Interpretations of languages − the standard common part
 
 Finally, we define the notion of *true formulas* of the language $L$ under the
 interpretation $J$ (of course, for a fixed combination of values of their free
-variables – if any):
+variables -- if any):
 
-+ Truth-values of the formulas: $¬B , B∧C , B∨C , B →C$ [those are not examples]
++ Truth-values of the formulas: $ not B, B and C, B or C B->C$ (those are not
-  must be computed. This is done with the truth-values of $B$ and $C$
+  examples) must be computed. This is done with the truth-values of $B$ and $C$
-  by using the well-known classical truth tables (see Section 4.2).
+  by using the well-known classical truth tables (see @three-kinds-of-formulas).
 
-+ The formula $∀x B$ is true under $J$ if and only if $B(c)$ is true under $J$
++ The formula $ forall x B$ is true under $J$ if and only if $B(c)$ is true under $J$
   for all members $c$ of the domain $D_J$.
 
-+ The formula $∃x B$ is true under $J$ if and only if there is a member c of the
++ The formula $ exists x B$ is true under $J$ if and only if there is a member c
-  domain $D_J$ such that $B(c)$ is true under $J$.
+  of the domain $D_J$ such that $B(c)$ is true under $J$.
 
 *Example.* In first order arithmetic, the formula
 
-$
+$ y((x=y+y) or (x=y+y+1)) $
-  y((x= y+ y)∨( x=y+ y+1))
-$
 
 is intended to say that "x is even or odd". Under the standard interpretation S
 of arithmetic, this formula is true for all values of its free variable x.
 
-Similarly, $∀x ∀y(x+ y=y+x)$ is a closed formula that is true under this
+Similarly, $ forall x forall y(x+y=y+x)$ is a closed formula that is true under
-interpretation. The notion “a closed formula F is true under the interpretation
+this interpretation. The notion "a closed formula F is true under the
-J” is now precisely defined.
+interpretation J" is now precisely defined.
 
 *Important − non-constructivity!* It may seem that, under an interpretation, any
 closed formula is "either true or false". However, note that, for an infinite
@@ -419,22 +403,21 @@ domain DJ, the notion of "true formulas under J" is extremely non- constructive.
 
 === Example of building of an interpretation
 
-In Section 1.2, in our "language about people" we used four names of people
+In our "language about people" we used four names of people (Britney, John,
-(Britney, John, Paris, Peter) as object constants and the following predicate
+Paris, Peter) as object constants and the following predicate constants:
-constants:
 
-+ $#[Male] (x)$ − means "x is a male person";
++ $"Male" (x)$ − means "x is a male person";
-+ $#[Female] (x)$ − means "x is a female person";
++ $"Female" (x)$ − means "x is a female person";
-+ $#[Mother] (x, y)$ − means "x is mother of y";
++ $"Mother" (x, y)$ − means "x is mother of y";
-+ $#[Father] (x, y)$ − means "x is father of y";
++ $"Father" (x, y)$ − means "x is father of y";
-+ $#[Married] (x, y)$ − means "x and y are married";
++ $"Married" (x, y)$ − means "x and y are married";
 + $x=y$ − means "x and y are the same person".
 
-Now, let us consider the following interpretation of the language – a specific
+Now, let us consider the following interpretation of the language -- a specific
-“small four person world”:
+"small four person world":
 
-The domain of interpretation – and the range of variables – is: $D = {#[br],
+The domain of interpretation -- and the range of variables -- is: $D = {b r,
-#[jo], #[pa], #[pe]}$ (no people, four character strings only!).
+j o, p a, p e}$ (no people, four character strings only!).
 
 Interpretations of predicate constants are defined by the following truth
 tables:
@@ -447,7 +430,7 @@ tables:
   columns: 6, [x], [y], [Father(x,y)], [Mother(x,y)], [Married(x,y)], [x=y], [br], [br], [false], [false], [false], [true], [br], [jo], [false], [false], [false], [false], [br], [pa], [false], [false], [false], [false], [br], [pe], [false], [false], [false], [false], [jo], [br], [false], [false], [false], [false], [jo], [jo], [false], [false], [false], [true], [jo], [pa], [false], [false], [false], [false], [jo], [pe], [false], [false], [false], [false], [pa], [br], [false], [true], [false], [false], [pa], [jo], [false], [true], [false], [false], [pa], [pa], [false], [false], [false], [true], [pa], [pe], [false], [false], [true], [false], [pe], [br], [true], [false], [false], [false], [pe], [jo], [true], [false], [false], [false], [pe], [pa], [false], [false], [true], [false], [pe], [pe], [false], [false], [false], [true],
 )
 
-== Three kinds of formulas
+== Three kinds of formulas <three-kinds-of-formulas>
 
 If one explores some formula F of the language L under various interpretations,
 then three situations are possible:
@@ -481,45 +464,43 @@ tests.
 
 As an example, let us verify that the formula
 
-$
+$ forall x(p(x) or q(x))-> forall x space p(x) or forall x space q(x) $
-  ∀x( p( x)∨q( x))→∀x p(x)∨∀x q(x)
-$
 
-is not logically valid (p, q are predicate constants). Why it is not? Because
+is not logically valid ($p$, $q$ are predicate constants). Why it is not?
-the truth-values of p(x) and q(x) may behave in such a way that $p(x)∨q(x)$ is
+Because the truth-values of $p(x)$ and $q(x)$ may behave in such a way that $p(x) or q(x)$ is
-always true, but neither $forall x p(x)$, nor $forall x q(x)$ is true. Indeed,
+always true, but neither $forall x space p(x)$, nor $forall x q(x)$ is true.
-let us take the domain $D = {a, b}$, and set (in fact, we are using one of two
+Indeed, let us take the domain $D = {a, b}$, and set (in fact, we are using one
-possibilities):
+of two possibilities):
 
 #table(
   columns: 3, [x], [p(x)], [q(x)], [b], [false], [true], [a], [true], [false],
 )
 
-In this interpretation, $p(a)∨q(a) = #[true]$ , $p(b)∨q(b) = #[true]$, i.e., the
+In this interpretation, $p(a) or q(a) = #[`true`]$ , $p(b) or q(b) = #[`true`]$,
-premise $∀x( p( x)∨q(x))$ is true. But the formulas$forall p(x),
+i.e., the premise $ forall x( p( x) or q(x))$ is true. But the formulas $forall p(x)$, $forall q(x)$ both
-forall q(x)$ both are false. Hence, in this interpretation, the conclusion $∀x
+are false. Hence, in this interpretation, the conclusion $ forall x
-p(x)∨∀x q(x)$ is false, and $∀x( p( x)∨q( x))→∀x p(x)∨∀x q(x)$ is false. We have
+p(x) or forall x q(x)$ is false, and $ forall x(p(x) or q(x))-> forall x space p(x) or forall x space q(x)$ is
-built an interpretation, making the formula false. Hence, it is not logically
+false. We have built an interpretation, making the formula false. Hence, it is
-valid.
+not logically valid.
 
-On the other hand, this formula is satisfiable – there is an interpretation
+On the other hand, this formula is satisfiable -- there is an interpretation
 under which it is true. Indeed, let us take $D={a}$ as the domain of
 interpretation, and let us set $p(a)=q(a)=#[true]$. Then all the formulas
 
-$
+$ forall x(p(x) or q(x)), forall x space p(x), forall x space q( x) $
-  ∀x( p( x)∨q( x)),∀x p(x),∀x q( x)
-$
 
 become true, and so becomes the entire formula.
 
 == Gödel's Completeness Theorem
 
-*Theorem 4.3.1.* In classical predicate logic $[L_1−L_15,#[MP],#[Gen]]$ all
+=== Theorem 4.3.1
-logically valid formulas can be derived.
+In classical predicate logic $[L_1−L_15,M P,G e n]$ all logically valid formulas
+can be derived.
 
-*Theorem 4.3.3.* All formulas that can be derived in classical predicate logic
+=== Theorem 4.3.3
-$[L_1−L_15,#[MP],#[Gen]]$ are logically valid. In this logic it is not possible
+All formulas that can be derived in classical predicate logic
-to derive contradictions, it is consistent.
+$[L_1−L_15,M P,G e n]$ are logically valid. In this logic it is not possible to
+derive contradictions, it is consistent.
 
 === Gödel’s theorem usage for task solving
 
@@ -529,23 +510,23 @@ rules of inference, deduction theorem, T 2.3.1 and other helping tools, we can
 just prove that $F$ is logically valid (by showing that none of interpretations
 can make it false). If we manage to do so, then we can announce: according to
 Gödel’s theorem, $F$ is derivable in classical predicate logic
-$[L_1−L_15,#[MP],#[Gen]]$.
+$[L_1−L_15,M P,G e n]$.
 
 = Tableaux algorithm
 
 == Step 1.
 
-We will solve the task from the opposite: append to the hypotheses $F_1, dots
+We will solve the task from the opposite: append to the hypotheses $F_1, ...
-F_n$ negation of formula $G$, and obtain the set $F_1, dots, F_n, ¬G$. When you
+F_n$ negation of formula $G$, and obtain the set $F_1, ..., F_n, not G$. When
-will do homework or test, you shouldn’t forget this, because if you work with
+you will do homework or test, you shouldn’t forget this, because if you work
-the set $F_1, ..., F_n, G$, then obtained result will not give an answer whether $G$ is
+with the set $F_1, ..., F_n, G$, then obtained result will not give an answer
-derivable or not. You should keep this in mind also when the task has only one
+whether $G$ is derivable or not. You should keep this in mind also when the task
-formula, e.g., verify, whether formula $(A→B)→((B→C)→(A→C))$
+has only one formula, e.g., verify, whether formula $(A->B)->((B->C)->(A->C))$
-is derivable. Then from the beginning you should append negation in front:
+is derivable. Then from the beginning you should append negation in front: not
-¬((A→B)→((B→C)→(A→C))) and then work further. Instead of the set $F_1, dots,
+$((A->B)->((B->C)->(A->C)))$ and then work further. Instead of the set $F_1, ...,
-F_n, ¬G$ we can always check one formula $F_1∧...∧F_n∧¬G$. Therefore, our task
+F_n, not G$ we can always check one formula $F_1 and ... and F_n and not G$.
-(theoretically) is reducing to the task: given some predicate language formula
+Therefore, our task (theoretically) is reducing to the task: given some
-F, verify, whether it is satisfiable or not.
+predicate language formula F, verify, whether it is satisfiable or not.
 
 == Step 2.
 
@@ -554,33 +535,26 @@ so-called negation normal form. We can use the possibilities provided by
 Substitution theorem. First, implications are replaced with negations and
 disjunctions:
 
-$
+$ (A->B)<-> not A or B $
-  (A→B)↔¬A∨B
-$
 
 Then we apply de Morgan laws to get negations close to the atoms:
 
-$
+$ not (A or B)<-> not A and not B eq.triple not (A and B)<-> not A or not B $
-  ¬(A∨B)↔¬A∧¬B equiv \
-  ¬(A∧B)↔¬A∨¬B
-$
 
 In such way all negations are carried exactly before atoms. After that we can
 remove double negations:
 
-$
+$ not not A<->A $
-  ¬¬A↔A
-$
 
-Example: $(p→q)→q$.
+Example: $(p->q)->q$.
 
-First get rid of implications: $¬(¬p∨q)∨q$.
+First get rid of implications: $not (not p or q) or q$.
 
-Then apply de Morgan law: $(¬¬p∧¬q)∨q$.
+Then apply de Morgan law: $(not not p and not q) or q$.
 
-Then get rid of double negations: $(p∧¬q)∨q$.
+Then get rid of double negations: $(p and not q) or q$.
 
-Now we have obtained equivalent formula in negation normal form – formula only
+Now we have obtained equivalent formula in negation normal form -- formula only
 has conjunctions and disjunctions, and all negations appear only in front of
 atoms.
 
@@ -589,10 +563,10 @@ atoms.
 Next, we should build a tree, vertices of which are formulas. In the root of the
 tree we put our formula. Then we have two cases.
 
-+ If vertex is formula A∧B, then each branch that goes through this vertex is
++ If vertex is formula A and B, then each branch that goes through this vertex is
   extended with vertices A and B.
-+ If vertex is a formula A∨B, then in place of continuation we have branching into
++ If vertex is a formula A or B, then in place of continuation we have branching
-  vertex A and vertex B.
+  into vertex A and vertex B.
 
 In both cases, the initial vertex is marked as processed. Algorithm continues to
 process all cases 1 and 2 until all non-atomic vertices have been processed.
@@ -601,9 +575,9 @@ process all cases 1 and 2 until all non-atomic vertices have been processed.
 
 When the construction of the tree is finished, we need to analyze and make
 conclusions. When one branch has some atom both with and without a negation
-(e.g., $A$ and $¬A$), then it is called closed branch. Other branches are called
+(e.g., $A$ and $ not A$), then it is called closed branch. Other branches are
-open branches.
+called open branches.
 
 *Theorem.* If in constructed tree, there exists at least one open branch, then
-formula in the root is satisfiable. And vice versa – if all branches in the tree
+formula in the root is satisfiable. And vice versa -- if all branches in the
-are closed, then formula in the root is unsatisfiable.
+tree are closed, then formula in the root is unsatisfiable.