Les mathématiques ont beaucoup de symboles. Certains pourraient dire trop de symboles. Permet donc de faire quelques calculs avec des images.

Permet d'avoir un papier, sur lequel nous allons puiser. Pour commencer le papier est vide, on dira que c'est équivalent à ou vrai .$\top$$\textit{true}$

Si nous écrivons d'autres choses sur le papier, elles seront également vraies.

Par exemple

Indique que les revendications et Q sont vraies.$P$$Q$

Maintenant, disons que si nous dessinons un cercle autour d'une déclaration, cette déclaration est fausse. Cela représente non logique.

Par exemple:

Indique que est faux et Q est vrai.$P$$Q$

Nous pouvons même placer le cercle autour de plusieurs sous-déclarations:

Puisque la partie à l'intérieur du cercle se lit normalement comme en mettant un cercle autour d'elle, cela signifie non  ( P  et  Q ) . On peut même imbriquer des cercles$P\text{ and }Q$$\text{not }(P\text{ and }Q)$

Cela se lit comme .$\text{not }((\text{not }P)\text{ and }Q)$

Si nous dessinons un cercle sans rien, cela représente ou faux . $\bot$$\textit{false}$

Puisque l'espace vide était vrai, la négation de vrai est fausse.

Maintenant, en utilisant cette méthode visuelle simple, nous pouvons réellement représenter n'importe quelle déclaration dans la logique propositionnelle.

Preuves

La prochaine étape après avoir pu représenter des déclarations est de pouvoir les prouver. Pour les preuves, nous avons 4 règles différentes qui peuvent être utilisées pour transformer un graphe. Nous commençons toujours par une feuille vide qui, comme nous le savons, est une vérité vide de sens, puis utilisons ces différentes règles pour transformer notre feuille de papier vide en théorème.

Notre première règle d'inférence est l' insertion .

Insertion

Nous appellerons le nombre de négations entre un sous-graphique et le niveau supérieur c'est la "profondeur". L'insertion nous permet d'introduire toute déclaration que nous souhaitons à une profondeur étrange.

Voici un exemple de nous effectuant l'insertion:

Ici, nous avons choisi , mais nous pourrions tout aussi bien choisir la déclaration que nous voulions.$P$

Effacement

La prochaine règle d'inférence est l' effacement . L'effacement nous dit que si nous avons une déclaration à une profondeur uniforme, nous pouvons la supprimer entièrement.

Voici un exemple d'effacement appliqué:

$Q$$2$$P$$1$

Double coupe

Double Cut est une équivalence. Ce qui signifie que, contrairement aux inférences précédentes, il peut également être inversé. Double Cut nous dit que nous pouvons dessiner deux cercles autour de n'importe quel sous-graphique, et s'il y a deux cercles autour d'un sous-graphique, nous pouvons les supprimer tous les deux.

Voici un exemple de la double coupe utilisée

$Q$

Itération

L'itération est également une équivalence. ¹ Son inverse est appelé Deiteration Si nous avons une déclaration et une coupe au même niveau, nous pouvons copier cette déclaration à l'intérieur d'une coupe.

Par exemple:

La déitération nous permet d'inverser une itération . Une instruction peut être supprimée via Deiteration s'il en existe une copie au niveau supérieur suivant.

Ce format de représentation et de preuve n'est pas de ma propre invention. Ils sont une modification mineure d'une logique schématique appelée Alpha Graphes Existentiels . Si vous voulez en savoir plus à ce sujet, il n'y a pas une tonne de littérature, mais l'article lié est un bon début.

Tâche

Votre tâche sera de prouver le théorème suivant:

Ceci, une fois traduit en logique traditionnelle, symbolise

$((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)$.

Également connu sous le nom d' axiome Łukasiewicz-Tarski .

Cela peut sembler impliqué, mais les graphes existentiels sont très efficaces en termes de longueur de preuve. J'ai choisi ce théorème parce que je pense que c'est une longueur appropriée pour un puzzle amusant et stimulant. Si vous rencontrez des problèmes avec celui-ci, je recommanderais d'essayer d'abord quelques théorèmes plus basiques pour comprendre le système. Une liste de ceux-ci peut être trouvée au bas de l'article.

C'est une épreuve de golf donc votre score sera le nombre total d'étapes dans votre épreuve du début à la fin. Le but est de minimiser votre score.

Format

Le format de ce défi est flexible, vous pouvez soumettre des réponses dans n'importe quel format clairement lisible, y compris les formats dessinés à la main ou rendus. Cependant, pour plus de clarté, je suggère le format simple suivant:

• Nous représentons une coupe entre parenthèses, tout ce que nous coupons est placé à l'intérieur des parens. La coupe vide ne serait que ()par exemple.

• Nous représentons les atomes avec juste leurs lettres.

À titre d'exemple, voici l'énoncé d'objectif dans ce format:

(((A((B(A))))(((((C)((D((E)))))(((C((D(F))))(((E(D))((E(F))))))))(G))))((H(G))))

Ce format est agréable car il est à la fois lisible par l'homme et par la machine, donc l'inclure dans votre message serait bien.

$\LaTeX$

Essayez-le en ligne!

Quant à votre travail réel, je recommande le crayon et le papier lorsque vous vous entraînez. Je trouve que le texte n'est pas aussi intuitif que le papier en ce qui concerne les graphiques existentiels.

Exemple de preuve

Dans cet exemple de preuve, nous prouverons le théorème suivant:

$(A\rightarrow B)\rightarrow(\neg B\rightarrow \neg A)$

Preuve:

Théorèmes de pratique

Voici quelques théorèmes simples que vous pouvez utiliser pour pratiquer le système:

Deuxième Axiome de Łukasiewicz

Axiome de Meredith

^{1: La plupart des sources utilisent une version plus sophistiquée et puissante d' itération , mais pour garder ce défi simple, j'utilise cette version. Ils sont fonctionnellement équivalents.}

19 étapes

1. (()) [double coupe]
2. (AB()(((G)))) [insertion]
3. (AB(A)(((G)))) [itération]
4. (((AB(A)))(((G)))) [double coupe]
5. (((AB(A))(((G))))(((G)))) [itération]
6. (((AB(A))(((G))))((H(G)))) [insertion]
7. (((AB(A))(((G)(()))))((H(G)))) [double coupe]
8. (((AB(A))(((DE()(C)(F))(G))))((H(G)))) [insertion]
9. (((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G)))) [itération]
10. (((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G)))) [itération]
11. (((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G)))) [double coupe]
12. (((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G)))) [itération]
13. (((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G)))) [double coupe]
14. (((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G)))) [double coupe]
15. (((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G)))) [double coupe]
16. (((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [double coupe]
17. (((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [double coupe]
18. (((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [double coupe]
19. (((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [double coupe]

Théorèmes de pratique

Deuxième axiome de Łukasiewicz: 7 étapes

1. (()) [double coupe]
2. (A()(B)(C)) [insertion]
3. (A(A(B))(B)(C)) [itération]
4. (A(AB(C))(A(B))(C)) [itération]
5. ((AB(C))(A(B))((A(C)))) [double coupe]
6. ((AB(C))(((A(B))((A(C)))))) [double coupe]
7. ((A((B(C))))(((A(B))((A(C)))))) [double coupe]

Axiome de Meredith: 11 étapes

1. (()) [double coupe]
2. (()(D(A)(E))) [insertion]
3. ((D(A)(E))((D(A)(E)))) [itération]
4. ((D(A)(E))((D(A)(E(A))))) [itération]
5. ((D(A)(E))(((E(A))((D(A)))))) [double coupe]
6. (((E)((D(A))))(((E(A))((D(A)))))) [double coupe]
7. (((E)((C)(D(A))))(((E(A))((D(A)))))) [insertion]
8. (((E)((C)(D(A)(C))))(((E(A))((D(A)))))) [itération]
9. (((E)((C)((A)(C)((D)))))(((E(A))((D(A)))))) [double coupe]
10. (((E)((C)((A)(((C)((D)))))))(((E(A))((D(A)))))) [double coupe]
11. (((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A)))))) [insertion]

Chercheur d'épreuves Haskell

(Quoi, vous pensiez que j'allais le faire à la main? :-P)

Cela n'essaie que l'insertion, l'introduction en double coupe et l'itération. Il est donc toujours possible de battre ces solutions en utilisant l'effacement, la double élimination des coupures ou la déitération.

{-# 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)

22 étapes

$\to$(((())(())))

$\to$(((AB())(CDE(F)()))H(G))

$\to$(((AB(A))(CDE(F)(CD(F)))(G))H(G))

$\to$(((A((B(A))))(((((C))DE(F)(C((D(F)))))(G))))((H(G))))

$\to$(((A((B(A))))(((((C)DE)DE(F)(C((D(F)))))(G))))((H(G))))

$\to$(((A((B(A))))(((((C)((D((E)))))((((((D))E(F)))(C((D(F)))))))(G))))((H(G))))

$\to$(((A((B(A))))(((((C)((D((E)))))((((((D)E)E(F)))(C((D(F)))))))(G))))((H(G))))

$\to$(((A((B(A))))(((((C)((D((E)))))((((((D)E)((E(F)))))(C((D(F)))))(G))))))((H(G))))

Quelques choses que j'ai apprises en terminant ce puzzle:

• Réduisez la représentation fournie. Cela implique d'inverser les doubles coupes et les itérations. Par exemple, cet axiome se réduit à (((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))après avoir inversé les coupes doubles et (((AB(A))(()CDE(F)))H(G)))après avoir inversé les itérations.

• Recherchez les atomes errants. Par exemple, H est utilisé comme variable fictive et peut donc être inséré à tout moment.

Solutions théoriques de pratique:

Solution pour le deuxième axiome de Łukasiewicz: [8 étapes]

$\to$(())

$\to$(()AB(C))

$\to$((AB(C))AB(C))

$\to$((A((B(C))))A((B))(C))

$\to$((A((B(C))))A(A(B))(C))

$\to$((A((B(C))))(((A(B))((A(C))))))

Solution pour l'Axiom de Meredith: [12 étapes]

$\to$(())

$\to$(()(A)D(E))

$\to$(((A)D(E))(A)D(E(A)))

$\to$(((((A)D))(E))(A)D(E(A)))

$\to$(((((A(B))D)(C))(E))(A)D(E(A)))

$\to$(((((A(B))(C)D)(C))(E))(A)D(E(A)))

$\to$(((((A(B))(((C)((D)))))(C))(E))(((((A)D))(E(A)))))