Chapter 1

.vscode/settings.json

@@ -1,7 +1,9 @@
 {
     "cSpell.words": [
+        "mathjax",
         "mdbook",
         "peaceiris",
+        "PMH",
         "RAIR",
     ],
     "editor.rulers": [125]

README.md

@@ -1,6 +1,8 @@
 # Existential Graph Theorem Proving in PMH
 
-A book about theorem proving in [Charles Sanders Peirce's Existential Graph System](https://en.wikipedia.org/wiki/Existential_graph#The_graphs) using the [PMH](https://github.com/RAIRLab/Peirce-My-Heart) existential graph interactive theorem prover. 
+A book about theorem proving in 
+[Charles Sanders Peirce's Existential Graph System](https://en.wikipedia.org/wiki/Existential_graph#The_graphs) 
+using the [PMH](https://github.com/RAIRLab/Peirce-My-Heart) existential graph interactive theorem prover. 
 
 Assumes that the reader has no knowledge of Propositional Calculus and no knowledge of any Existential Graphs beforehand.
 
@@ -9,8 +11,9 @@ Made with [mdBook](https://github.com/rust-lang/mdBook).
 # Testing Your Changes Locally!
 
 Install rust, cargo and mdbook.
-Then, run "mdbook build" in the **root directory** and ensure the message "Running the html backend" appears.
-
+Then, run ```mdbook build``` in the **root directory** and ensure the message "Running the html backend" appears.
+Then, in the newly created ./book/ directory on your machine, open "index.html" with your web browser of choice and determine
+if the format is to your liking.
 
 # Root Files and Folders
 

book.toml

@@ -1,6 +1,11 @@
 [book]
+title = "Existential Graph Theorem Proving in PMH"
 authors = ["James Oswald, RAIR Lab, Ryan Reilly"]
+description = "For understanding and proving with AEGs and PMH."
 language = "en"
 multilingual = false
 src = "src"
-title = "Existential Graph Theorem Proving in PMH"
+
+[output.html]
+git-repository-url = "https://github.com/RAIRLab/EG-Theorem-Proving-in-PMH"
+mathjax-support = true

src/Chapter1/atom.md

@@ -0,0 +1,46 @@
+# Chapter 1.2: The Atom
+
+Debating what exactly it means to have a cat is not in the scope of this book, but compacting such statements into equivalent
+representations certainly is.
+
+An *atom* here is an indivisible component of some statement that may be true or may be false. For example, I may say that
+
+I have a cat \\(  = C \\)
+
+This cat's name is Jerry \\(  = J \\)
+
+And change our Sheet of Assertion accordingly. This is allowed because we may replace C with "I have a cat" and we may
+replace J with "This cat's name is Jerry" at any time. They are equal!
+
+![The Jerry compaction is not displayable.](./images/JerryCompaction.png)
+
+So are these sheets! While they look different, they really do mean the same thing. So long as one clearly states what their
+atoms mean elsewhere, they may be represented as any symbol[^1], from any alphabet, or some very long 
+annoying string, if one so desires.
+
+**Why does this matter?**
+
+While the examples about Jerry are purposefully silly, the important part about them is that atoms can be either true
+or false. Jerry may be a dog, or a cat I call Jerry
+may not really be named Jerry. It is best to refer to the first sentence 
+in Chapter 1. We are concerned with *how* statements are determined as true or false, less so if they *are* true
+or false. 
+
+If you find yourself a bit confused, think about something as simple as addition. Adding two numbers and receiving their sum
+has worked for all numbers in your head. \\( 1 + 1 = 2 \\) is never going to suddenly turn into \\(1 + 1 = 43 \\) if you look
+at the equation the wrong way. There are rules that are repeatable regardless of who is using the rule, when, how and why. 
+We can plug numbers into \\( number + number = sum \\) for the rest of time and catalogue their sums if we choose. 
+Every sum received will be equal to \\( number + number \\). The point is that we are concerned
+with forming rules that work for certain parameters, and less so with applying them.
+
+We say that the statement (C and J), as in, (I have a cat and This cat's name is Jerry), 
+is true only if both C and J are true, and false otherwise. If C is false, or J is false, or both C and J are false,
+(I have a cat and This cat's name is Jerry) no longer tells the full truth, and so therefore is considered false. 
+
+Note that that "or" is similar to the word "and" in the structure of a sentence, as in it is a grammar conjunction,
+but that we cannot represent that with just The Sheet of Assertion and atoms. It still appears useful, however.
+Chapter 1.3 details how we can get this, and surprisingly construct every statement you can think of, by introducing and 
+discussing The Cut.
+
+[^1] PMH supports only single-letter, English-alphabet atoms as of version 1.0.0, but in the AEG System, generally, 
+any one atom may be represented by any symbol(s).

src/Chapter1/chapter_1.md

@@ -1,3 +1,21 @@
-# Chapter 1
+# Chapter 1: Thinking Logically with AEGs
 
-Discuss learning logic through AEGs, *without* assuming the reader knows Propositional Calculus.
+Mathematical logic concerns how one determines the truth or falsity of a statement(s). In existing logics
+(can be read as "systems of logic,") this involves large sets of notation and a significant amount of rewriting in proofs,
+which can and does get quite annoying quite quickly. 
+
+Logician Charles Peirce constructed the Existential Graph System to visualize several logics. For right now, we will discuss
+his Alpha Existential Graph System, which we will abbreviate as AEG System in reference to the system and AEGs in reference
+to Alpha Existential Graphs themselves, and we will assume you have no experience working in or understanding of other 
+logics.
+
+If the object seems intimidating, please continue still. One is able to conclude logical truths as a consequence
+of drawing ellipses and letters, which, while it sounds silly, is both true and good fun. If it is any motivation,
+all the same conclusions reachable in other, similar logics, which concern strictly truth and falsity, are reachable through
+the AEG System, even though it may seem somewhat counterintuitive at first glance that a visualization can be just as 
+powerful.
+
+To reiterate, before going into Chapter 1.1, it is **very** important to understand the first paragraph here. There are few
+numbers in these parts. While it is easy to get lost in seas of odd notation, it is helpful to remind oneself that the AEG
+System and systems similar were developed to discuss and verify, strictly, the truth or falsity of some statement and its
+components.

src/Chapter1/sheetOfAssertion.md

@@ -0,0 +1,49 @@
+# Chapter 1.1: The Sheet of Assertion
+
+For the truth or falsity of statements to be evaluated, one must have some way of asserting the truth or falsity of its 
+components.
+
+As an example, consider the sentence "I have a cat, and this cat's name is Jerry."
+While stating that he is a cat may be true,
+and while stating that he is named Jerry may be true, the overall truth or falsity of both statements together
+cannot be discussed if we had no structure to convey the statements in.
+The structure here is the sentence. It is a recognizable form we insert information into, because
+having an audience understand what they read is important.
+
+**Put bluntly, we need a place to put smaller stuff to make up bigger stuff**. 
+
+Put less bluntly, we need a place in which statements can be asserted as true and evaluated together with other 
+statements. From there, we can then proceed to determine if any incorrectness in a larger statement exists. 
+
+Since the EG System was developed during a time when a computer was an occupation and not a machine, Peirce's chosen form
+was a blank piece of paper. This form can be expanded to include any writable surface that maintains the information written.
+This includes whiteboards, blackboards and computer screens.
+Statements written on this surface are asserted as true, and if two separate statements are made,
+they are considered to be in *conjunction* with each other[^1]. To discuss this Jerry character further, the above statements
+would look like this on *The Sheet of Assertion*, our writable surface.
+
+![The Jerry discussion is not displayable.](./images/JerryDiscussion.png)
+
+As a result of the statements being considered *conjuncts*, as in they are in conjunction with each other,
+the *and* was removed. Otherwise, the sentence 
+"I have a cat, and this cat's name is Jerry," and the above Sheet of Assertion are equivalent in meaning. 
+
+Alone, this is not too powerful[^2]. 
+If, once, you were in a hurry and forgot a conjunction or two in writing something down, it could
+be said that you developed your own Sheet of Assertion. 
+
+**Why does this matter?**
+
+If we had some compact way of representing statements on the sheet, we would be able to store and evaluate the whole truth
+of some large collection of statements at once. Chapter 1.2 details this compact representation in discussing The Atom.
+
+[^1] An interesting consequence of this is that these statements do not have to be in any particular spatial relationship
+aside from being on the same sheet at the same time. 
+No statement must necessarily be visible to the eye, evidenced in PMH's Draw and Proof Modes. 
+No statement must necessarily be next to a related statement in position, either. If some Sheet of Assertion was a thousand
+miles long, a statement written at mile 0 is still in conjunction with a statement written at mile 1,000.
+
+[^2] Of note now, but not worth detailing yet, is that other logics use the symbol ∧ to denote conjunctions
+(not uppercase lambda!) This is
+one example of several in the EG System where the set of symbols was cut down. This assists in an otherwise complex 
+process of understanding what one is even looking at in all logics.

src/SUMMARY.md

@@ -3,6 +3,14 @@
 [Introduction](introduction.md)
 
 - [Thinking Logically with AEGs](./Chapter1/chapter_1.md)
+    - [The Sheet of Assertion](./Chapter1/SheetOfAssertion.md)
+    - [The Atom](./Chapter1/atom.md)
+    - [The Cut](./Chapter1/chapter_1.md)
+    - [Conjunctions between Symbols](./Chapter1/chapter_1.md)
+    - [Rules of Equivalence](./Chapter1/chapter_1.md)
+    - [Rules of Inference](./Chapter1/chapter_1.md)
+    - [What AEGs Can and Cannot Model](./Chapter1/chapter_1.md)
+    - [Conclusion](./Chapter1/chapter_1.md)
 
 - [The Propositional Calculus and AEGs](./Chapter2/chapter_2.md)
 

src/introduction.md

@@ -1,5 +1,6 @@
 # Introduction
 
-This is the open source textbook and end-user manual for theorem proving with Existential Graphs in PMH.
+This is the open source textbook and end-user manual for theorem proving with Existential Graphs in PMH. We will refer to
+the Existential Graph System as the EG System and Existential Graphs themselves as EGs from now on.
 
 If you don't know any formal logic whatsoever, don't worry! This book will explain the basics and how they relate to EGs.