Existential Golf

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

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.¹ 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

Your task will be to prove the following theorem:

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\$:

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:

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

^{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 1

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 2

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]