Existential Golf
Math has a lot of symbols. Some might say too many symbols. So lets do some math with pictures.
Lets have a paper, which we will draw on. To start the paper is empty, we will say that is equivalent to \$\top\$ or \$\textit{true}\$.
If we write other things on the paper they will also be true.
For example
Indicates that the claims \$P\$ and \$Q\$ are true.
Now let us say that if we draw a circle around some statement that statement is false. This represents logical not.
For example:
Indicates that \$P\$ is false and \$Q\$ is true.
We can even place the circle around multiple sub-statements:
Since the part inside the circle normally reads as \$P\text{ and }Q\$ by putting a circle around it it means \$\text{not }(P\text{ and }Q)\$. We can even nest circles
This reads as \$\text{not }((\text{not }P)\text{ and }Q)\$.
If we draw a circle with nothing in it, that represents \$\bot\$ or \$\textit{false}\$.
Since empty space was true, then the negation of true is false.
Now using this simple visual method we can actually represent any statement in propositional logic.
Proofs
The next step after being able to represent statements is being able to prove them. For proofs we have 4 different rules that can be used to transform a graph. We always start with an empty sheet which as we know is a vacuous truth and then use these different rules to transform our empty sheet of paper into a theorem.
Our first inference rule is Insertion.
Insertion
We will call the number of negations between a sub-graph and the top level it's "depth". Insertion allows us to introduce any statement we wish at an odd depth.
Here is an example of us performing insertion:
Here we chose \$P\$, but we could just as well choose any statement we wanted.
Erasure
The next inference rule is Erasure. Erasure tells us that if we have a statement that is at a even depth we can remove it entirely.
Here is an example of erasure being applied:
Here we erased the \$Q\$, because it was \$2\$ levels nested. Even if we wanted to we could not have erased \$P\$ because it is \$1\$ level nested.
Double Cut
Double Cut is an equivalence. Which means, unlike the previous inferences it can also be reversed. Double Cut tells us that we can draw two circles around any sub-graph, and if there are two circles around a sub-graph we can remove them both.
Here is an example of the Double Cut being used
Here we use Double Cut on \$Q\$.
Iteration
Iteration is a equivalence as well.1 It's reverse is called Deiteration If we have a statement and a cut on the same level, we can copy that statement inside of a cut.
For example:
Deiteration allows us to reverse an Iteration. A statement can be removed via Deiteration if there exists a copy of it at the next level up.
This format of representation and proof is not of my own invention. They are a minor modification of a diagrammatic logic are called Alpha Existential Graphs. If you want to read more on this, there is not a ton of literature, but the linked article is a good start.
Task
Ok now for the task. Your task will be to prove the following theorem:
Need to check it is an appropriate level of difficulty, Currently my naïve solution is 23 steps
This, when translated into traditional logic symbolization is
\$((A\to(B\to A))\to(((\neg C\to(D\to\neg E))\to((C\to(D\to F))\to((E\to D)\to(E\to F))))\to G)]\to(H\to G)\$.
Also known as the Łukasiewicz-Tarski Axiom.
It may seem involved but existential graphs are very efficient when it comes to proof length. I selected this theorem because I do think it is an appropriate length for a fun and challenging puzzle. If you are having trouble with this one I would recommend trying some more basic theorems first to get the hang of the system. A list of these can be found at the bottom of the post.
This is proof-golf so your score will be the total number of steps in your proof from start to finish. The goal is to minimize your score.
Format
The format for this challenge is flexible you can submit answers in any format that is clearly readable, including hand-drawn or rendered formats. However for clarity I suggest the following simple format:
We represent a cut with parentheses, whatever we are cutting is put inside of the parens. The empty cut would just be
()for example.We represent atoms with just their letters.
As an example here is the goal statement in this format:
(((A((B(A))))(((((C)((D((E)))))(((C((D(F))))(((E(D))((E(F))))))))(G))))((H(G))))
This format is nice because it is both human and machine readable, so including it in your post would be nice.
If you want some nice(ish) diagrams here is some code that converts this format to LaTeX:
As for your actual work I recommend pencil and paper when working out. I find that text just isn't as intuitive as paper when it comes to existential graphs.
Example proof
In this example proof we will prove the following theorem:
Now this may seem alien to you at first but if we translate this into traditional logic notation we get \$(A\rightarrow B)\rightarrow(\neg B\rightarrow \neg A)\$, also known as the law of contra-positives.
Proof:
Practice Theorems
Here are some simple theorems you can use to practice the system:
Łukasiewicz' Second Axiom
Meredith's Axiom
Add more theorems!
There is a some work I need to do before this challenge is ready to go. I figured I put it up even if it's not quite ready yet. All criticisms, suggestions and the such are of course welcome even if the challenge is not quite complete
1: Most sources use a more sophisticated and powerful version of Iteration, but to keep this challenge simple I am using this version. They are functionally equivalent.
