Skip to content

Commit

Permalink
Supposed to have gone with previous commit
Browse files Browse the repository at this point in the history
  • Loading branch information
RyanR712 committed Dec 18, 2023
1 parent 26de9f7 commit ef185e0
Show file tree
Hide file tree
Showing 5 changed files with 53 additions and 5 deletions.
8 changes: 6 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
@@ -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.

Expand All @@ -9,7 +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
Expand Down
8 changes: 7 additions & 1 deletion src/Chapter1/chapter_1.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,16 @@ 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.
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.
Binary file added src/Chapter1/images/JerryDiscussion.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
39 changes: 38 additions & 1 deletion src/Chapter1/sheetOfAssertion.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,40 @@
# 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.
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. 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[^1].
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] Of note now, but not worth detailing yet, is that other logics use the symbol ∧ to denote conjunctions. 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 other logics.
3 changes: 2 additions & 1 deletion src/introduction.md
Original file line number Diff line number Diff line change
@@ -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.

0 comments on commit ef185e0

Please sign in to comment.