翻译 preface

.github/workflows/blank.yml

@@ -0,0 +1,36 @@
+# This is a basic workflow to help you get started with Actions
+
+name: CI
+
+# Controls when the workflow will run
+on:
+  # Triggers the workflow on push or pull request events but only for the "main" branch
+  push:
+    branches: [ "cadake" ]
+  pull_request:
+    branches: [ "cadake" ]
+
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+# A workflow run is made up of one or more jobs that can run sequentially or in parallel
+jobs:
+  # This workflow contains a single job called "build"
+  build:
+    # The type of runner that the job will run on
+    runs-on: ubuntu-latest
+
+    # Steps represent a sequence of tasks that will be executed as part of the job
+    steps:
+      # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
+      - uses: actions/checkout@v4
+
+      # Runs a single command using the runners shell
+      - name: Run a one-line script
+        run: echo Hello, world!
+
+      # Runs a set of commands using the runners shell
+      - name: Run a multi-line script
+        run: |
+          echo Add other actions to build,
+          echo test, and deploy your project.

Chap1.qmd

@@ -1,36 +1,37 @@
 # Sentential Logic
+
 \markdouble{1 Sentential Logic}
 
 Chapter 1 of *How To Prove It* introduces the following symbols of logic:
 
 ::: {style="margin: 0% 20%"}
-| Symbol | Meaning |
-|:------:|:-------:|
-| $\neg$ | not |
-| $\wedge$ | and |
-| $\vee$ | or |
-| $\to$ | if ... then |
+|      Symbol       |            Meaning            |
+|:-----------------:|:-----------------------------:|
+|      $\neg$       |              not              |
+|     $\wedge$      |              and              |
+|      $\vee$       |              or               |
+|       $\to$       |          if ... then          |
 | $\leftrightarrow$ | iff (that is, if and only if) |
 :::
 
-As we will see, Lean uses the same symbols, with the same meanings.  A statement of the form $P \wedge Q$ is called a *conjunction*, a statement of the form $P \vee Q$ is called a *disjunction*, a statement of the form $P \to Q$ is an *implication* or a *conditional* statement (with *antecedent* $P$ and *consequent* $Q$), and a statement of the form $P \leftrightarrow Q$ is a *biconditional* statement.  The statement $\neg P$ is the *negation* of $P$.
+As we will see, Lean uses the same symbols, with the same meanings. A statement of the form $P \wedge Q$ is called a *conjunction*, a statement of the form $P \vee Q$ is called a *disjunction*, a statement of the form $P \to Q$ is an *implication* or a *conditional* statement (with *antecedent* $P$ and *consequent* $Q$), and a statement of the form $P \leftrightarrow Q$ is a *biconditional* statement. The statement $\neg P$ is the *negation* of $P$.
 
 This chapter also establishes a number of logical equivalences that will be useful to us later:
 
-::: {id="prop-laws"}
-| Name | | Equivalence | |
-|:---------|:-----:|:-----:|:-----:|
+::: {#prop-laws}
+| Name |   | Equivalence |   |
+|:---------------------|:---------------:|:---------------:|:---------------:|
 | De Morgan's Laws | $\neg (P \wedge Q)$ | is equivalent to | $\neg P \vee \neg Q$ |
-|                  | $\neg (P \vee Q)$ | is equivalent to | $\neg P \wedge \neg Q$ |
+|  | $\neg (P \vee Q)$ | is equivalent to | $\neg P \wedge \neg Q$ |
 | Double Negation Law | $\neg\neg P$ | is equivalent to | $P$ |
 | Conditional Laws | $P \to Q$ | is equivalent to | $\neg P \vee Q$ |
-|                  | $P \to Q$ | is equivalent to | $\neg(P \wedge \neg Q)$ |
+|  | $P \to Q$ | is equivalent to | $\neg(P \wedge \neg Q)$ |
 | Contrapositive Law | $P \to Q$ | is equivalent to | $\neg Q \to \neg P$ |
 :::
 
-Finally, Chapter 1 of *HTPI* introduces some concepts from set theory.  A *set* is a collection of objects; the objects in the collection are called *elements* of the set.  The notation $x \in A$ means that $x$ is an element of $A$. Two sets $A$ and $B$ are equal if they have exactly the same elements.  We say that $A$ is a *subset* of $B$, denoted $A \subseteq B$, if every element of $A$ is an element of $B$.  If $P(x)$ is a statement about $x$, then $\{x \mid P(x)\}$ denotes the set whose elements are the objects $x$ for which $P(x)$ is true.  And we have the following operations on sets:
+Finally, Chapter 1 of *HTPI* introduces some concepts from set theory. A *set* is a collection of objects; the objects in the collection are called *elements* of the set. The notation $x \in A$ means that $x$ is an element of $A$. Two sets $A$ and $B$ are equal if they have exactly the same elements. We say that $A$ is a *subset* of $B$, denoted $A \subseteq B$, if every element of $A$ is an element of $B$. If $P(x)$ is a statement about $x$, then $\{x \mid P(x)\}$ denotes the set whose elements are the objects $x$ for which $P(x)$ is true. And we have the following operations on sets:
 
-::: {.quote}
+::: quote
 $A \cap B = \{x \mid x \in A \wedge x \in B\} = {}$ the *intersection* of $A$ and $B$,
 
 $A \cup B = \{x \mid x \in A \vee x \in B\} = {}$ the *union* of $A$ and $B$,