From 54ac3bc78a453e33723ab852c6e2547c03051502 Mon Sep 17 00:00:00 2001
From: cadake <2419720664@qq.com>
Date: Mon, 23 Sep 2024 22:37:45 +0800
Subject: [PATCH 1/2] preface
---
Chap1.qmd | 29 +-
docs/Chap1.html | 507 ++++++++++++--
docs/Chap2.html | 495 ++++++++++++--
docs/IntroLean.html | 534 ++++++++++++---
docs/index.html | 625 +++++++++++++++---
docs/search.json | 177 ++++-
docs/site_libs/bootstrap/bootstrap.min.css | 12 +-
.../quarto-syntax-highlighting.css | 34 +
index.qmd | 131 +++-
9 files changed, 2171 insertions(+), 373 deletions(-)
diff --git a/Chap1.qmd b/Chap1.qmd
index 90987d1..ba4e927 100644
--- a/Chap1.qmd
+++ b/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$,
diff --git a/docs/Chap1.html b/docs/Chap1.html
index 6ec40d9..6dccde7 100644
--- a/docs/Chap1.html
+++ b/docs/Chap1.html
@@ -2,12 +2,12 @@
-
+
-How To Prove It With Lean - 1 Sentential Logic
+1 Sentential Logic – How To Prove It With Lean
@@ -47,7 +47,13 @@
"collapse-after": 3,
"panel-placement": "start",
"type": "textbox",
- "limit": 20,
+ "limit": 50,
+ "keyboard-shortcut": [
+ "f",
+ "/",
+ "s"
+ ],
+ "show-item-context": false,
"language": {
"search-no-results-text": "No results",
"search-matching-documents-text": "matching documents",
@@ -56,13 +62,43 @@
"search-more-match-text": "more match in this document",
"search-more-matches-text": "more matches in this document",
"search-clear-button-title": "Clear",
+ "search-text-placeholder": "",
"search-detached-cancel-button-title": "Cancel",
- "search-submit-button-title": "Submit"
+ "search-submit-button-title": "Submit",
+ "search-label": "Search"
}
}
+
+
+
@@ -70,11 +106,16 @@
-