[Question]
  [
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
[![P and Q](https://i.stack.imgur.com/d6UrV.png)](https://i.stack.imgur.com/d6UrV.png)
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:
[![not P and Q](https://i.stack.imgur.com/D3EmF.png)](https://i.stack.imgur.com/D3EmF.png)
Indicates that \$P\$ is false and \$Q\$ is true.
We can even place the circle around multiple sub-statements:
[![not (P and Q)](https://i.stack.imgur.com/F7RgN.png)](https://i.stack.imgur.com/F7RgN.png)
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
[![not (not P and Q)](https://i.stack.imgur.com/Cct9N.png)](https://i.stack.imgur.com/Cct9N.png)
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}\$. 
[![False](https://i.stack.imgur.com/9YRJ1.png)](https://i.stack.imgur.com/9YRJ1.png)
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:
[![Insertion Example](https://i.stack.imgur.com/NNNzs.png)](https://i.stack.imgur.com/NNNzs.png)
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:
[![Erasure example](https://i.stack.imgur.com/xZwt3.png)](https://i.stack.imgur.com/xZwt3.png)
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
[![Double Cut example](https://i.stack.imgur.com/eouBJ.png)](https://i.stack.imgur.com/eouBJ.png)
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:
[![Iteration example](https://i.stack.imgur.com/5PgO9.png)](https://i.stack.imgur.com/5PgO9.png)
*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](https://en.wikipedia.org/wiki/Existential_graph). If you want to read more on this, there is not a ton of literature, but the linked article is a good start.
---
# Task
Your task will be to prove the following theorem:
[![Łukasiewicz - Tarksi Axiom](https://i.stack.imgur.com/d3Pyh.png)](https://i.stack.imgur.com/d3Pyh.png)
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](https://en.wikipedia.org/wiki/List_of_Hilbert_systems#Implication_and_negation).
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](/questions/tagged/proof-golf "show questions tagged '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\$:
[Try it online!](https://tio.run/##jZJRT8IwEMff9ykuC8naTAhq4sMMJvrmsz6YUGJqV0fD1pGtCGHhs89rN8YQVLa0D9f7/@5/7c15uZBpWtexFCpTWwlRBM/ayEQWMHyAF1MonXjd6QYmoLQyQMp5voYNhTCEaTAKriDlpYEBNPGZ58UFX1vatMXNLO8E3S9iBaXhYgGF5PEcF5CABBBBQO0u8lhSNOAzZnOJb4t31kgnCuHW@fKvxlSoQqSSjK7pPdON4FCmL7mjjg9/2dgbcCl98U3kBPQ42BAbIDH5EgltWg/c78z7rbVYfTWEsJNSy3dNQtflOVVXaggI6FT/XceR@Z@3wU2eXeD6zIOgV42qauBSW44/2F32OI2bd/ynMzsHvud9rtL0Vb7ZQTsZqP1Z2c5MLlaZ1EbgpJYVFtExT3Mtd0wztirlEqvyRFZGLbYu9iETpau9zIXsWXVwijbGiLet7RiTOj5ko7eMKz1ROPEFFwZaN3VN8KP0ERd5ovQb "Haskell – Try It Online")
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:
[![Law of contra-positives](https://i.stack.imgur.com/u1jdT.png)](https://i.stack.imgur.com/u1jdT.png)
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:**
[![Example Proof 1](https://i.stack.imgur.com/lgPrY.png)](https://i.stack.imgur.com/lgPrY.png)
# Practice Theorems
Here are some simple theorems you can use to practice the system:
### Łukasiewicz' Second Axiom
[![Łukasiewicz' Second Axiom](https://i.stack.imgur.com/9eghU.png)](https://i.stack.imgur.com/9eghU.png)
### Meredith's Axiom
[![Meredith's Axiom](https://i.stack.imgur.com/3rpSS.png)](https://i.stack.imgur.com/3rpSS.png)
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.
  
[Answer]
# 19 steps
1. `(())` [double cut]
2. `(AB()(((G))))` [insertion]
3. `(AB(A)(((G))))` [iteration]
4. `(((AB(A)))(((G))))` [double cut]
5. `(((AB(A))(((G))))(((G))))` [iteration]
6. `(((AB(A))(((G))))((H(G))))` [insertion]
7. `(((AB(A))(((G)(()))))((H(G))))` [double cut]
8. `(((AB(A))(((DE()(C)(F))(G))))((H(G))))` [insertion]
9. `(((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G))))` [iteration]
10. `(((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G))))` [iteration]
11. `(((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G))))` [double cut]
12. `(((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G))))` [iteration]
13. `(((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G))))` [double cut]
14. `(((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G))))` [double cut]
15. `(((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G))))` [double cut]
16. `(((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))` [double cut]
17. `(((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))` [double cut]
18. `(((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))` [double cut]
19. `(((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))` [double cut]
# Practice theorems
### Łukasiewicz’ second axiom: 7 steps
1. `(())` [double cut]
2. `(A()(B)(C))` [insertion]
3. `(A(A(B))(B)(C))` [iteration]
4. `(A(AB(C))(A(B))(C))` [iteration]
5. `((AB(C))(A(B))((A(C))))` [double cut]
6. `((AB(C))(((A(B))((A(C))))))` [double cut]
7. `((A((B(C))))(((A(B))((A(C))))))` [double cut]
### Meredith’s axiom: 11 steps
1. `(())` [double cut]
2. `(()(D(A)(E)))` [insertion]
3. `((D(A)(E))((D(A)(E))))` [iteration]
4. `((D(A)(E))((D(A)(E(A)))))` [iteration]
5. `((D(A)(E))(((E(A))((D(A))))))` [double cut]
6. `(((E)((D(A))))(((E(A))((D(A))))))` [double cut]
7. `(((E)((C)(D(A))))(((E(A))((D(A))))))` [insertion]
8. `(((E)((C)(D(A)(C))))(((E(A))((D(A))))))` [iteration]
9. `(((E)((C)((A)(C)((D)))))(((E(A))((D(A))))))` [double cut]
10. `(((E)((C)((A)(((C)((D)))))))(((E(A))((D(A))))))` [double cut]
11. `(((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A))))))` [insertion]
# Haskell proof searcher
(What, you thought I was going to do that by hand? :-P)
This only tries insertion, double cut introduction, and iteration. So it’s still possible these solutions could be beaten using erasure, double cut elimination, or deiteration.
```
{-# LANGUAGE ViewPatterns #-}
import Control.Applicative hiding (many)
import Data.Char
import Data.Function hiding ((&))
import qualified Data.Map as M
import Data.Maybe
import qualified Data.MultiSet as S
import qualified Data.PQueue.Prio.Min as Q
import System.IO
import Text.ParserCombinators.ReadP
type Var = Char
data Part
  = Var Var
  | Not Conj
  deriving (Eq, Ord)
instance Show Part where
  show (Var s) = [s]
  show (Not c) = "(" ++ show c ++ ")"
newtype Conj = Conj
  { parts :: S.MultiSet Part
  } deriving (Eq, Ord)
instance Show Conj where
  show (Conj (S.toAscList -> [])) = ""
  show (Conj (S.toAscList -> g:gs)) =
    show g ++ concat ["" ++ show g1 | g1 <- gs]
true :: Conj
true = Conj S.empty
not_ :: Conj -> Conj
not_ = Conj . S.singleton . Not
(&) :: Conj -> Conj -> Conj
Conj as & Conj bs = Conj (S.union as bs)
intersect :: Conj -> Conj -> Conj
intersect (Conj as) (Conj bs) = Conj (S.intersection as bs)
diff :: Conj -> Conj -> Conj
diff (Conj as) (Conj bs) = Conj (S.difference as bs)
splits :: Conj -> [(Conj, Conj)]
splits =
  S.foldOccur
    (\a o bcs ->
       [ (Conj (S.insertMany a o1 bs), Conj (S.insertMany a (o - o1) cs))
       | (Conj bs, Conj cs) <- bcs
       , o1 <- [0 .. o]
       ])
    [(true, true)] .
  parts
moves :: Bool -> Conj -> [(Conj, String)]
moves ev a =
  (do (b, c) <- splits a
      andMoves ev b c) ++
  (do (p, _) <- S.toOccurList (parts a)
      partMoves ev p (Conj (S.delete p (parts a))))
andMoves :: Bool -> Conj -> Conj -> [(Conj, String)]
andMoves ev a b = [(a, "insertion") | not ev]
partMoves :: Bool -> Part -> Conj -> [(Conj, String)]
partMoves ev (Not a) b =
  [(a1 & b, why) | (a1, why) <- notMoves ev a] ++
  [ (not_ (diff a d) & b, "iteration")
  | (d, _) <- splits (intersect a b)
  , d /= true
  ]
partMoves _ (Var _) _ = []
notMoves :: Bool -> Conj -> [(Conj, String)]
notMoves ev a =
  (case S.toList (parts a) of
     [Not b] -> [(b, "double cut")]
     _ -> []) ++
  [(not_ a1, why) | (a1, why) <- moves (not ev) a]
partSat :: Part -> Bool -> M.Map Var Bool -> [M.Map Var Bool]
partSat (Var var) b m =
  case M.lookup var m of
    Nothing -> [M.insert var b m]
    Just b1 -> [m | b1 == b]
partSat (Not c) b m = conjSat c (not b) m
conjSat :: Conj -> Bool -> M.Map Var Bool -> [M.Map Var Bool]
conjSat c False m = do
  (p, _) <- S.toOccurList (parts c)
  partSat p False m
conjSat c True m = S.foldOccur (\p _ -> (partSat p True =<<)) [m] (parts c)
readConj :: ReadP Conj
readConj = Conj . S.fromList <$> many readPart
readPart :: ReadP Part
readPart =
  Var <$> satisfy isAlphaNum <|> Not <$> (char '(' *> readConj <* char ')')
parse :: String -> Maybe Conj
parse s = listToMaybe [c | (c, "") <- readP_to_S readConj s]
partSize :: Part -> Int
partSize (Var _) = 1
partSize (Not c) = 1 + conjSize c
conjSize :: Conj -> Int
conjSize c = sum [partSize p * o | (p, o) <- S.toOccurList (parts c)]
data Pri = Pri
  { dist :: Int
  , size :: Int
  } deriving (Eq, Show)
instance Ord Pri where
  compare = compare `on` \(Pri d s) -> (s + d, d)
search ::
     Q.MinPQueue Pri (Conj, [(Conj, String)])
  -> M.Map Conj Int
  -> [[(Conj, String)]]
search (Q.minViewWithKey -> Nothing) _ = []
search (Q.minViewWithKey -> Just ((pri, (a, proof)), q)) m =
  [proof | a == true] ++
  uncurry search (foldr (addMove pri a proof) (q, m) (moves True a))
addMove ::
     Pri
  -> Conj
  -> [(Conj, String)]
  -> (Conj, String)
  -> (Q.MinPQueue Pri (Conj, [(Conj, String)]), M.Map Conj Int)
  -> (Q.MinPQueue Pri (Conj, [(Conj, String)]), M.Map Conj Int)
addMove pri b proof (a, why) (q, m) =
  case M.lookup a m of
    Just d
      | d <= d1 -> (q, m)
    _
      | null (conjSat a False M.empty) ->
        ( Q.insert (Pri d1 (conjSize a)) (a, (b, why) : proof) q
        , M.insert a d1 m)
    _ -> (q, m)
  where
    d1 = dist pri + 1
prove :: Conj -> [[(Conj, String)]]
prove c = search (Q.singleton (Pri 0 (conjSize c)) (c, [])) (M.singleton c 0)
printProof :: [(Conj, String)] -> IO ()
printProof proof = do
  mapM_
    (\(i, (a, why)) ->
       putStrLn (show i ++ ". `" ++ show a ++ "`  [" ++ why ++ "]"))
    (zip [1 ..] proof)
  putStrLn ""
  hFlush stdout
main :: IO ()
main = do
  Just theorem <- parse <$> getLine
  mapM_ printProof (prove theorem)
```
[Answer]
# 22 Steps
\$\to\$`(((())(())))` [Double Cut x3]
\$\to\$`(((AB())(CDE(F)()))H(G))` [Insertion x3]
\$\to\$`(((AB(A))(CDE(F)(CD(F)))(G))H(G))` [Iteration x3]
\$\to\$`(((A((B(A))))(((((C))DE(F)(C((D(F)))))(G))))((H(G))))` [Double Cut x5]
\$\to\$`(((A((B(A))))(((((C)DE)DE(F)(C((D(F)))))(G))))((H(G))))` [Iteration]
\$\to\$`(((A((B(A))))(((((C)((D((E)))))((((((D))E(F)))(C((D(F)))))))(G))))((H(G))))` [Double Cut x5]
\$\to\$`(((A((B(A))))(((((C)((D((E)))))((((((D)E)E(F)))(C((D(F)))))))(G))))((H(G))))` [Iteration]
\$\to\$`(((A((B(A))))(((((C)((D((E)))))((((((D)E)((E(F)))))(C((D(F)))))(G))))))((H(G))))` [Double Cut]
---
A few things I learned from completing this puzzle:
* Reduce the provided representation. This involves reversing double cuts and iterations. For example, this axiom reduces to `(((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))` after reversing double cuts, and `(((AB(A))(()CDE(F)))H(G)))` after reversing iterations.
* Look for stray atoms. For example, H is used as a dummy variable, and thus can be inserted at any point.
---
# Practice Theorem Solutions:
**Solution for Łukasiewicz' Second Axiom:** [8 Steps]
\$\to\$`(())` [Double Cut]
\$\to\$`(()AB(C))` [Insertion]
\$\to\$`((AB(C))AB(C))` [Iteration]
\$\to\$`((A((B(C))))A((B))(C))` [Double Cut x2]
\$\to\$`((A((B(C))))A(A(B))(C))` [Iteration]
\$\to\$`((A((B(C))))(((A(B))((A(C))))))` [Double Cut x2]
**Solution for Meredith's Axiom:** [12 Steps]
\$\to\$`(())` [Double Cut]
\$\to\$`(()(A)D(E))` [Insertion]
\$\to\$`(((A)D(E))(A)D(E(A)))` [Iteration x2]
\$\to\$`(((((A)D))(E))(A)D(E(A)))` [Double Cut]
\$\to\$`(((((A(B))D)(C))(E))(A)D(E(A)))` [Insertion x2]
\$\to\$`(((((A(B))(C)D)(C))(E))(A)D(E(A)))` [Iteration]
\$\to\$`(((((A(B))(((C)((D)))))(C))(E))(((((A)D))(E(A)))))` [Double Cut x4]
]