21
\$\begingroup\$

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

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

Indicates that \$P\$ is false and \$Q\$ is true.

We can even place the circle around multiple sub-statements:

not (P and Q)

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)

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

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

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

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

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

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:

Łukasiewicz - Tarksi Axiom

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

Law of contra-positives

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

Practice Theorems

Here are some simple theorems you can use to practice the system:

Łukasiewicz' Second Axiom

Łukasiewicz' Second Axiom

Meredith's 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.

\$\endgroup\$
  • \$\begingroup\$ I feel like this question is better suited for puzzling \$\endgroup\$ – Conor O'Brien Jul 13 '18 at 22:06
  • 4
    \$\begingroup\$ @ConorO'Brien Why? Puzzling is mainly concerned with answering rather than optimizing. This question is very easy to answer, making it mostly golfing challenge. \$\endgroup\$ – Sriotchilism O'Zaic Jul 13 '18 at 22:07
  • \$\begingroup\$ Puzzling can very much be concerned with optimizing. I feel this challenge might find a better home on puzzling, but that's of course just my opinion \$\endgroup\$ – Conor O'Brien Jul 13 '18 at 22:10
  • 4
    \$\begingroup\$ @connorobrien proof-golf is a long established part of this community, and long may it continue. \$\endgroup\$ – Nathaniel Jul 14 '18 at 23:27
  • 1
    \$\begingroup\$ Here's a site with a fun interactive Flash applet about these sorts of expressions: markability.net \$\endgroup\$ – Woofmao Jul 16 '18 at 3:41
7
\$\begingroup\$

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)
\$\endgroup\$
4
\$\begingroup\$

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]

\$\endgroup\$
  • \$\begingroup\$ I've updated to include my full solution. Fun puzzle! Please let me know how I can improve my post. \$\endgroup\$ – Logikable Jul 13 '18 at 21:30
  • \$\begingroup\$ Generally here answers aren't hidden - the assumption being that reading the answer implies a "spoiler" to the solution. Also we have MathJax here, using \$ as the begin/end which I think would make your solution much easier to read. I hope you have a nice time here :) \$\endgroup\$ – FryAmTheEggman Jul 13 '18 at 21:44
  • \$\begingroup\$ I've updated the number of rules used (the proof remains the same). Can someone who is good at formatting please help improve my answer? \$\endgroup\$ – Logikable Jul 13 '18 at 22:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.