refactor: refactor and add actions

.github/workflows/typst.yml

@@ -0,0 +1,29 @@
+name: Build Typst document
+on: [push, workflow_dispatch]
+permissions:
+  contents: write
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+      - name: Typst
+        uses: lvignoli/typst-action@main
+        with:
+          source_file: |
+            main.typ
+      - name: Upload PDF file
+        uses: actions/upload-artifact@v3
+        with:
+          name: PDF
+          path: "*.pdf"
+      - name: Get current date
+        id: date
+        run: echo "DATE=$(date +%Y-%m-%d-%H:%M)" >> $GITHUB_ENV
+      - name: Release
+        uses: softprops/action-gh-release@v1
+        if: github.ref_type == 'tag'
+        with:
+          name: "${{ github.ref_name }} — ${{ env.DATE }}"
+          files: main.pdf

.gitignore

@@ -1 +1 @@
-main.pdf
+*.pdf

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2024 Kristofers Solo
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

main.typ

@@ -1,25 +1,12 @@
-#set page(
+#set page(margin: 1cm, columns: 2)
- margin: (
-   left: 1cm,
-   right: 1cm,
-   top: 1cm,
-   bottom: 1cm,
- ),
-)
-
-
 
 #set heading(numbering: "1.")
 
-
+#show outline.entry.where(level: 1): it => {
-#show outline.entry.where(
-  level: 1
-): it => {
   v(12pt, weak: true)
   strong(it)
 }
 
-
 #set enum(numbering: "a)")
 
 // #show outline.entry.where(
@@ -31,9 +18,6 @@
 
 #outline(indent: auto)
 
-
-
-
 = Logical axiom schemes
 
 $bold(L_1): B→(C →B)$
@@ -72,28 +56,27 @@ $bold(L_15): ∀x(F (x) arrow G) arrow (exists x F (x)→G)$
 
 $[L_1, L_2, #[MP]]$:
 
-+ $((A→B)→(A→C))→(A→(B→C))$. Be careful when assuming hypotheses:
++ $((A→B)→(A→C))→(A→(B→C))$. Be careful when assuming hypotheses: assume
-  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* 
++ $(A→B)→((B→C)→(A→C))$. It's another version of the *Law of Syllogism* (by
-  (by  Aristotle),  or  the  transitivity  property  of  implication.  
+  Aristotle), or the transitivity property of implication.
-+ $(A→(B→C))→(B→(A→C))$.  It's  another  version  of  the  *Premise
++ $(A→(B→C))→(B→(A→C))$. It's another version of the *Premise Permutation Law*.
-  Permutation Law*. Explain the difference between this formula and Theorem
+  Explain the difference between this formula and Theorem 1.4.3(a): A→(B→C)├
-  1.4.3(a): A→(B→C)├ B→(A→C).
+  B→(A→C).
 
 == Deduction theorems
 
 === Theorem 1.5.1 (Deduction Theorem 1 AKA DT1)
 
 If $T$ is a first order theory, and there is a proof of
-$[T, #[MP]]: A_1, A_2, dots, A_n, B├ C$,
+$[T, #[MP]]: A_1, A_2, dots, A_n, B├ C$, then there is a proof of
- then there is a proof of
 $[L_1, L_2, T, #[MP]]: A_1, A_2, dots, A_n├ B→C$.
 
 === Theorem 1.5.2 (Deduction Theorem 2 AKA DT2)
 
-If there is a proof $[T, #[MP], #[Gen]]: A_1, A_2, dots, A_n, B├ C$,
+If there is a proof $[T, #[MP], #[Gen]]: A_1, A_2, dots, A_n, B├ C$, where,
-where, after B appears in the proof, Generalization is not applied to the
+after B appears in the proof, Generalization is not applied to the variables
-variables that occur as free in $B$, then there is a proof of
+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$.
 
 == Conjunction
@@ -105,9 +88,10 @@ $[L_1, L_2, L_14, T, #[MP], #[Gen]]: A_1, A_2, dots, A_n├ B→C$.
 
 === Theorem 2.2.2.
 
-+ $[L_1, L_2, L_5, #[MP]]: (A→(B→C)) ↔ ((A→B)→(A→C))$ (extension of the axiom L_2).
++ $[L_1, L_2, L_5, #[MP]]: (A→(B→C)) ↔ ((A→B)→(A→C))$ (extension of the axiom
-+ $[L_1-L_4, #[MP]]: (A→B)∧( B→C)→( A→C)$ (another form of the *Law of
+  L_2).
-  Syllogism*, or *transitivity property of implication*).
++ $[L_1-L_4, #[MP]]: (A→B)∧( B→C)→( A→C)$ (another form of the *Law of Syllogism*,
+  or *transitivity property of implication*).
 
 === Theorem 2.2.3 (properties of the conjunction connective).
 
@@ -125,21 +109,19 @@ $[L_1- L_5, #[MP]]$:
 + $(A↔B)→(B↔A)$ (symmetry),
 + $(A↔B)→((B↔C) →((A↔C))$ (transitivity).
 
-
 == Disjunction
 
 === Theorem 2.3.1
 
 + (D-introduction)$[L_6, L_7, #[MP]]: A├ A∨B; B├ A∨B$;
-+ (D-elimination) If there is a proof $[T, #[MP]]: A_1, A_2, ..., A_n, B├ D$,
++ (D-elimination) If there is a proof $[T, #[MP]]: A_1, A_2, ..., A_n, B├ D$, and
-  and a proof $[T, #[MP]]: A_1, A_2, ..., A_n, C├ D$, then there is a proof $[T,
+  a proof $[T, #[MP]]: A_1, A_2, ..., A_n, C├ D$, then there is a proof $[T,
   L_1, L_2, L_8, #[MP]]: A_1, A_2, dots, A_n, B∨C ├ D$.
 
-
 === Theorem 2.3.2
 
-a) $[ L_5, L_6-L_8, #[MP]]: A∨B↔B∨A$ . Disjunction is commutative.
+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$ .
-b) $[L_1, L_2, L_5, L_6-L_8, #[MP]]: A∨A↔A$ . Disjunction is idempotent.
+Disjunction is idempotent.
 
 === Theorem 2.3.3.
 
@@ -173,14 +155,12 @@ B├ ¬C$, then there is a  proof $[T, L_1, L_2, L_9, #[MP]]: A_1, A_2, ..., A_n
 
 === Theorem 2.4.2.
 
-a) $[L_1, L_2, L_9, #[MP]]: A, ¬B├ ¬(A→B)$. What does it mean?
+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)$.
-b) $[L_1-L_4, L_9, #[MP]]: A∧¬B→¬( A→B)$. 
-
 
 === Theorem 2.4.3.
 
-$[L_1, L_2, L_9, #[MP]]: (A→B)→(¬B→¬A)$. What does it mean?
+$[L_1, L_2, L_9, #[MP]]: (A→B)→(¬B→¬A)$. What does it mean? It's the so-called
-It's the so-called *Contraposition Law*.
+*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)$
@@ -191,11 +171,10 @@ $[L_1, L_2, L_9, #[MP]]: A→¬¬A$.
 
 === Theorem 2.4.5.
 
-a) $[L_1, L_2, L_9, #[MP]]: ¬¬¬A↔¬A$.
+a) $[L_1, L_2, L_9, #[MP]]: ¬¬¬A↔¬A$. b) $[L_1, L_2, L_6, L_7, L_9, #[MP]]: ¬¬( A∨¬A)$.
-b) $[L_1, L_2, L_6, L_7, L_9, #[MP]]: ¬¬( A∨¬A)$. What does it mean? This is a “weak
+What does it mean? This is a “weak form” of the *Law of Excluded Middle* that
-  form”  of  the  *Law  of  Excluded  Middle*  that  can  be  proved
+can be proved constructively. The formula $¬¬( A∨¬A)$ can be proved in the
-  constructively. The formula $¬¬( A∨¬A)$ can be proved in the constructive logic,
+constructive logic, but $A∨¬A$ can't – as we will see in Section 2.8.
-  but $A∨¬A$ can't – as we will see in Section 2.8.
 
 === Theorem 2.4.9.
 
@@ -211,7 +190,6 @@ b) $[L_1, L_2, L_6, L_7, L_9, #[MP]]: ¬¬( A∨¬A)$. What does it mean? This i
 + $[L_1, L_2, L_6, #[MP]]: A∨B→(¬A→B) ├¬A→(A→B)$ . It means that the “natural”
   rule $A∨B ;¬ A ├ B$ implies $L_10$!
 
-
 === Theorem 2.5.2.
 
 $[L_1-L_10, #[MP]]$:
@@ -221,8 +199,8 @@ $[L_1-L_10, #[MP]]$:
 + $¬¬A→(¬A→A)$. It's the converse of Theorem 2.4.6(a). Hence, [L1-L10,
   #[MP]]: $¬¬A↔(¬A→A)$.
 + $A∨¬ A→(¬¬A→A)$ .
-+ $¬¬(¬¬A→A)$. What does it mean? It’s a “weak” form of the Double Negations
++ $¬¬(¬¬A→A)$. What does it mean? It’s a “weak” form of the Double Negations Law –
-  Law – provable in constructive logic. 
+  provable in constructive logic.
 
 == Negation -- classical logic
 
@@ -236,12 +214,10 @@ A$.
 $[L_8, L_11, #[MP]]: A→B, ¬A→B├ B$. Or, by Deduction Theorem 1, $[L_1, L_2, L_8,
 L_11, #[MP]]: (A→B)→((¬A→B)→B)$.
 
-
 === Theorem 2.6.3.
 
 $[L_1-L_11, #[MP]]: (¬B→¬A)→(A→B)$. Hence, $[L_1-L_11, #[MP]]: (A→B) ↔ (¬B→¬A)$.
 
-
 === Theorem 2.6.3.
 
 _(another one with the same number of because numbering error (it seems like it))_
@@ -249,18 +225,15 @@ _(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]]: ˫
 ¬(A∧B)↔¬A∨¬B$ .
 
-
 === Theorem 2.6.4.
 
 $[L_1-L_8, L_11, #[MP]]: (A→B)→¬ A∨B $. Hence, (I-elimination) $[L_1-L_11, #[MP]]:
 (A→B)↔¬ A∨B$.
 
-
 === Theorem 2.6.5.
 
 $[L_1-L_11, #[MP]]: ¬(A→B)→A∧¬B $.
 
-
 === Theorem 2.7.1 (Glivenko's Theorem).
 
 $[L_1-L_11, #[MP]]:├ A$ if and only if $[L_1-L_10, #[MP]]:├ ¬¬A$.
@@ -276,7 +249,6 @@ L_11, #[MP]]$.
 
 The axiom $L_9$ cannot be proved in $[L_1-L_8, L_10, #[MP]]$.
 
-
 == Replacement Theorem 1
 
 Let us consider three formulas: $B$, $B'$, $C$, where $B$ is a sub-formula of
@@ -290,24 +262,20 @@ $[L_1-L_9, #[MP]]: B↔B'├ C↔C'$.
 
 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
+formula obtained from $C$ by replacing $o(B)$ by B'. Then, in the minimal logic,
-logic,
 
 $[L_1-L_9, L_12-L_15, #[MP], #[Gen]]: B↔B'├ C↔C'$.
 
-
 == Theorem 3.1.1.
 
-$[L_1, L_2, L_12, L_13, #[MP]]: forall x B(x) arrow exists x B(x)$ . What does it
+$[L_1, L_2, L_12, L_13, #[MP]]: forall x B(x) arrow exists x B(x)$ . What does
-mean? It prohibits "empty domains".
+it mean? It prohibits "empty domains".
-
 
 Theorem 3.1.2.
 
 + [L1, L2, L12, L14, MP, Gen]: ∀x(B→C)→(∀x B→∀xC).
 + [L1, L2, L12-L15, MP, Gen]: ∀x(B→C)→(∃z(x+z+1=y).x B→∃z(x+z+1=y).xC).
 
-
 == Theorems 3.1.3.
 
 If F is any formula, then:
@@ -316,13 +284,14 @@ If F is any formula, then:
 + (U-elimination) [L12, MP, Gen]: ∀x F(x) ├F(x) . What does it mean?
 + (E-introduction) [L13, MP, Gen]: F(x) ├∃z(x+z+1=y).x F(x) . What does it mean?
 
-
 == Theorems 3.1.4.
 
-If F is any formula, and G is a formula that does not contain free occurrences of x, then:
+If F is any formula, and G is a formula that does not contain free occurrences
+of x, then:
 
 + (U2-introduction) [L14, MP, Gen] G →F (x) ├G →∀x F (x) . What does it mean?
-+ (E2-introduction) [L15, MP, Gen]: F (x)→G ├∃z(x+z+1=y).x F (x)→G . What does it mean?
++ (E2-introduction) [L15, MP, Gen]: F (x)→G ├∃z(x+z+1=y).x F (x)→G . What does it
+  mean?
 
 == Theorem 3.1.5.
 
@@ -330,37 +299,34 @@ If F is any formula, and G is a formula that does not contain free occurrences o
 + [L1, L2, L5, L13, L15, MP, Gen]: $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)$.
 
-
 Theorem 3.1.6. If the formula B does not contain free occurrences of x, then
-[L1-L2,  L12-L15,  MP,  Gen]: (∀x B)↔B;(∃z(x+z+1=y).x B)↔B ,  i.e.,  quantifiers
+[L1-L2, L12-L15, MP, Gen]: (∀x B)↔B;(∃z(x+z+1=y).x B)↔B , i.e., quantifiers ∀x
-∀x ;∃z(x+z+1=y). x can be dropped or introduced as needed.
+;∃z(x+z+1=y). 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, [L1-L15, MP, Gen]: ¬ x¬B ∀ ↔ xB.
 
 == Theorem 3.3.1.
 
 + [L1-L5, L12, L14, MP, Gen]: ∀x(B∧C)↔∀x B∧∀xC .
-+ [L1, L2, L6-L8, L12, L14, MP, Gen]: ├∀x B∨∀xC →∀x(B∨C) . The converse  formula ∀x(B∨C)→∀x B∨∀xC cannot  be  true.  Explain, why.
++ [L1, L2, L6-L8, L12, L14, MP, Gen]: ├∀x B∨∀xC →∀x(B∨C) . The converse formula
-
+  ∀x(B∨C)→∀x B∨∀xC cannot be true. Explain, why.
 
 == 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 .
+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
-b) [L1-L5, L13-L15, MP, Gen]: ∃z(x+z+1=y).x(B∧C)→∃z(x+z+1=y). x B∧∃z(x+z+1=y).xC . The converse implication ∃z(x+z+1=y).x B∧∃z(x+z+1=y). xC →∃z(x+z+1=y). x(B∧C) cannot be true. Explain, why. Exercise 3.3.3. a) Prove (a→) of Theorem 3.3.2. (Hint: start by assuming B∨C , apply D-elimination, etc., and finish by E2-introduction.)
+. b) [L1-L5, L13-L15, MP, Gen]: ∃z(x+z+1=y).x(B∧C)→∃z(x+z+1=y). x
+B∧∃z(x+z+1=y).xC . The converse implication ∃z(x+z+1=y).x B∧∃z(x+z+1=y). xC
+→∃z(x+z+1=y). x(B∧C) cannot be true. Explain, why. Exercise 3.3.3. a) Prove (a→)
+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".
+"false", 1 – "unknown" (or NULL – in terms of SQL), and 2 means "true". Then it
-Then  it  would  be  natural  to  define  “truth  values”  of  conjunction  and
+would be natural to define “truth values” of conjunction and disjunction as
-disjunction as
 
 $A∧B=min ( A, B)$ ;
 
@@ -369,25 +335,11 @@ $A∨B=max (A , B)$ .
 But how should we define “truth values” of implication and negation?
 
 #table(
-  columns: 5,
+  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$],
-  [$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$],
 )
 
 #table(
-  columns: 2,
+  columns: 2, [$A$], [¬$A$], [$0$], [$i_10$], [$1$], [$i_11$], [$2$], [$i_12$],
-  [$A$], [¬$A$],
-  [$0$], [$i_10$],
-  [$1$], [$i_11$],
-  [$2$], [$i_12$],
 )
 
 = Model interpreation
@@ -402,8 +354,8 @@ Let L be a predicate language containing:
 - (a possibly empty) set of function constants $f_1, dots, f_m, dots,$;
 - (a non empty) set of predicate constants $p_1, ..., p_n, ...$.
 
-An interpretation $J$ of the language $L$ consists of the following two
+An interpretation $J$ of the language $L$ consists of the following two entities
-entities (a set and a mapping):
+(a set and a mapping):
 
 + 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
@@ -416,13 +368,12 @@ entities (a set and a mapping):
   - 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
+*true formulas* (more precisely − the notion of formulas that are true under the
-the interpretation $J$).
+interpretation $J$).
 
 *Example.* The above interpretation of the “language about people” put in the
 terms of the general definition:
 
-
 + $D = {#[br], #[jo], #[pa], #[pe]}$.
 + $#[int]_J (#[Britney])=#[br], #[int]_J (#[John])=#[jo], #[int]_J (#[Paris])=#[pa],
   #[int]_J (#[Peter])=#[pe]$.
@@ -439,8 +390,8 @@ 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):
 
-+ Truth-values of the formulas: $¬B , B∧C , B∨C , B →C$ [those are not
++ Truth-values of the formulas: $¬B , B∧C , B∨C , B →C$ [those are not examples]
-  examples] must be computed. This is done with the truth-values of $B$ and $C$
+  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).
 
 + The formula $∀x B$ is true under $J$ if and only if $B(c)$ is true under $J$
@@ -458,15 +409,13 @@ $
 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
+Similarly, $∀x ∀y(x+ y=y+x)$ is a closed formula that is true under this
-this interpretation. The notion “a closed formula F is true under the
+interpretation. The notion “a closed formula F is true under the interpretation
-interpretation J” is now precisely defined. 
+J” is now precisely defined.
 
-
+*Important − non-constructivity!* It may seem that, under an interpretation, any
-*Important − non-constructivity!* It may seem that, under an interpretation,
+closed formula is "either true or false". However, note that, for an infinite
-any closed formula is "either true or false". However, note that, for an infinite
+domain DJ, the notion of "true formulas under J" is extremely non- constructive.
-domain  DJ,  the  notion  of  "true  formulas  under  J"  is  extremely  non-
-constructive.
 
 === Example of building of an interpretation
 
@@ -491,42 +440,20 @@ Interpretations of predicate constants are defined by the following truth
 tables:
 
 #table(
-  columns: 3,
+  columns: 3, [x], [Male(x)], [Female(x)], [br], [false], [true], [jo], [true], [false], [pa], [false], [true], [pe], [true], [false],
-  [x], [Male(x)], [Female(x)],
-  [br], [false], [true],
-  [jo], [true], [false],
-  [pa], [false], [true],
-  [pe], [true], [false],
 )
 
 #table(
-  columns: 6,
+  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],
-  [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
 
-If  one  explores  some  formula  F  of  the  language  L  under  various
+If one explores some formula F of the language L under various interpretations,
-interpretations, then three situations are possible:
+then three situations are possible:
 
-+ $F$ is true in all interpretations of the language $L$. Formulas of this kind are
++ $F$ is true in all interpretations of the language $L$. Formulas of this kind
-  called *logically valid formulas* (LVF, Latv. *LVD*).
+  are called *logically valid formulas* (LVF, Latv. *LVD*).
 
 + $F$ is true in some interpretations of $L$, and false − in some other
   interpretations of $L$.
@@ -535,11 +462,10 @@ interpretations, then three situations are possible:
   *unsatisfiable formulas* (Latv. *neizpildāmas funkcijas*).
 
 Formulas that are "not unsatisfiable" (formulas of classes (a) and (b)) are
-called, of course, satisfiable formulas: a formula is satisfiable, if it is
+called, of course, satisfiable formulas: a formula is satisfiable, if it is true
-true in at least one interpretation [*satisfiable functions* (Latv. *izpildāmas
+in at least one interpretation [*satisfiable functions* (Latv. *izpildāmas
 funkcijas*)].
 
-
 === Prooving an F is LVF (Latv. LVD)
 
 First, we should learn to prove that some formula is (if really is!) logically
@@ -565,20 +491,16 @@ always true, but neither $forall x p(x)$, nor $forall x q(x)$ is true. Indeed,
 let us take the domain $D = {a, b}$, and set (in fact, we are using one of two
 possibilities):
 
-
 #table(
-  columns: 3,
+  columns: 3, [x], [p(x)], [q(x)], [b], [false], [true], [a], [true], [false],
-  [x], [p(x)], [q(x)],
-  [b], [false], [true],
-  [a], [true], [false],
 )
 
-In  this  interpretation, $p(a)∨q(a) =  #[true]$ , $p(b)∨q(b) =  #[true]$,
+In this interpretation, $p(a)∨q(a) = #[true]$ , $p(b)∨q(b) = #[true]$, i.e., the
-i.e.,  the premise $∀x( p( x)∨q(x))$ is true. But the formulas$forall p(x),
+premise $∀x( p( x)∨q(x))$ is true. But the formulas$forall p(x),
 forall q(x)$ both are false. Hence, in this interpretation, the conclusion $∀x
-p(x)∨∀x q(x)$ is false, and $∀x( p( x)∨q( x))→∀x p(x)∨∀x q(x)$ is false. We
+p(x)∨∀x q(x)$ is false, and $∀x( p( x)∨q( x))→∀x p(x)∨∀x q(x)$ is false. We have
-have built an interpretation, making the formula false. Hence, it is  not
+built an interpretation, making the formula false. Hence, it is not logically
-logically valid.
+valid.
 
 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
@@ -590,7 +512,6 @@ $
 
 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
@@ -610,7 +531,6 @@ 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]]$.
 
-
 = Tableaux algorithm
 
 == Step 1.
@@ -618,9 +538,9 @@ $[L_1−L_15,#[MP],#[Gen]]$.
 We will solve the task from the opposite: append to the hypotheses $F_1, dots
 F_n$ negation of formula $G$, and obtain the set $F_1, dots, F_n, ¬G$. When you
 will do homework or test, you shouldn’t forget this, because if you work with
-the set $F_1, ..., F_n, G$, then obtained result will not give an answer
+the set $F_1, ..., F_n, G$, then obtained result will not give an answer whether $G$ is
-whether $G$ is derivable or not. You should keep this in mind also when the
+derivable or not. You should keep this in mind also when the task has only one
-task has only one formula, e.g., verify, whether formula $(A→B)→((B→C)→(A→C))$
+formula, e.g., verify, whether formula $(A→B)→((B→C)→(A→C))$
 is derivable. Then from the beginning you should append negation in front:
 ¬((A→B)→((B→C)→(A→C))) and then work further. Instead of the set $F_1, dots,
 F_n, ¬G$ we can always check one formula $F_1∧...∧F_n∧¬G$. Therefore, our task
@@ -645,8 +565,8 @@ $
   ¬(A∧B)↔¬A∨¬B
 $
 
-In such way all negations are carried exactly before atoms.
+In such way all negations are carried exactly before atoms. After that we can
-After that we can remove double negations:
+remove double negations:
 
 $
   ¬¬A↔A
@@ -666,24 +586,24 @@ atoms.
 
 == Step 3.
 
-Next, we should build a tree, vertices of which are formulas. In the root of
+Next, we should build a tree, vertices of which are formulas. In the root of the
-the tree we put our formula. Then we have two cases.
+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
   extended with vertices A and B.
-+ If vertex is a formula A∨B, then in place of continuation we have branching
++ If vertex is a formula A∨B, then in place of continuation we have branching into
-  into vertex A and vertex B.
+  vertex A and vertex B.
 
-In both cases, the initial vertex is marked as processed. Algorithm continues
+In both cases, the initial vertex is marked as processed. Algorithm continues to
-to process all cases 1 and 2 until all non-atomic vertices have been processed.
+process all cases 1 and 2 until all non-atomic vertices have been processed.
 
 == Step 4.
 
 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
+(e.g., $A$ and $¬A$), then it is called closed branch. Other branches are called
-called open branches.
+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
+formula in the root is satisfiable. And vice versa – if all branches in the tree
-tree are closed, then formula in the root is unsatisfiable.
+are closed, then formula in the root is unsatisfiable.