Deductum
In this minimalistic puzzle game, you're given a set of premises and a conclusion, and your task is to use the fundamental rules of logic to formally prove, step by step, that the conclusion follows.
Tutorials introduce you to the world of proofs and the game mechanics. The early problems are simple, but the difficulty gradually increases until eventually you might not even know where to begin. Still, every problem has a solution, and if you think deeply enough, you'll never need to guess!
- Simple controls. No timers. No distractions. Just logic.
- 111 problems to solve, including classic theorems like De Morgan's Laws and the Law of the Excluded Middle
- Sandbox mode: enter any claim (with proposition symbols A–H) and see if you can prove it!
NOTE: To run the MacOS version, double clicking may not work. Instead, try right-clicking the app and choosing 'Open' in the menu and then again 'Open' in the confirmation dialog.
Purchase
In order to download this game you must purchase it at or above the minimum price of $5 USD. You will get access to the following files:
Download demo
Development log
- Level names addedJan 11, 2026
- Version 1.0 released, with free demoMay 18, 2025
Comments
Log in with itch.io to leave a comment.
the game is great, it is fun, it give me some headache with logic, it is kind of a different interpretation of logic in algebra, gg
thank you :)
I do like this stuff. It reminds me of Terrence Tao's QED game. I would like if you would be able to undo a part of a tree, rather than just in general.
Thanks. Yeah, I remember playing through QED when I researched competition. It was a good game but didn't match my Advanced Graphics :)
Undoing a whole subtree sounds like a good idea, especially for the future first order version where proof trees are likely bigger.
Hello, the game is great, I love it so much !
Thanks! Very happy to hear that :)
I really like this game and I did buy it because I want to learn, and logic is fun. Music is good, layout good. etc.
I think it'd be helpful if you could have a notebook of some sort, as you discover the laws of logic. The first time you figure out a new thing it saves the solution, if you replay it and the solution is shorter it's over written. And when you minimize it completely you get a little note of the Law of Z discovered by Y, in XXXX
Thanks, I'm happy that you like it!
The notebook is an interesting idea. I'm imagining a sort of "proof gallery", or did you have something else in mind?
Proof gallery yeah, that's a good description. Proof gallery with a "high score." Like we fumble though it making mistakes taking way more steps than needed. That's what gets saved, the most concise proof isn't given just because we solved it. The ten step solution, then we shave it down to eight, and that's saved over, etc. When we get down to the wire with the minimum steps, we get a the name and maybe a quick blurb about it.
I love learning, but I got a goldfish brain, every time I come back I wonder how I solved the last one.
Game goes to black screen with music after loading concludes. Firefox.
Thanks for the report! Have you tried hard reloading the page (eg. ctrl-shift-r) in case it's just the download that broke? Or try in a private window. If those don't work, can you try with a different browser?
Reloading and opening with a private window have been ineffective, unfortunately. I also don't have another browser set up.
Hmm.. Does this page say your browser supports WebGL2? https://get.webgl.org/webgl2/
Also could you enter about:support in firefox location bar and find the value of WebGL 2 Driver Renderer?
What OS and Firefox version are you running?
Yes, my browser supports WebGL 2. I am running Firefox 152.0.3 on Arch Linux.
Oh, hello fellow arch user :) I tried with the same firefox version, it works for me, so my best (and so far only) guess is something goes wrong with the graphics drivers somewhere.
I uploaded a linux build of the demo, does that work?
If you want to play in browser one more thing to try is disable hardware acceleration in firefox:
Restart firefox and try once more. You probably want to restore the setting after trying, though.
music goes bip bip wooo wooo wooo
melted my brain really hard, but it was so much fun :)
Thanks! I'm very happy you liked it :)
I just bought the full game (mac) and it said the file is damaged. Any solutions, nonpop?
How did you open it? Sometimes you can't just double click but have to right-click the app and choose "Open" in the menu, and then again "Open" in the confirmation dialog. I think this is only needed once and then it works normally. Unfortunately I don't have access to a Mac anymore so I can't verify.
There's no confirmation dialogue, it just says that the file is broken and should be moved to the trash. Is your game perhaps running on 32x?
I believe it's 64-bit if that's what you mean. Can you try these steps?
Thanks very much. This helped! :)
I really enjoyed the demo! It took me a few rounds to get the hang of it, but once I did it was really fun!
Good to hear, thanks!
Is first order logic included in the later levels?
No, this is propositional logic only. I have plans for adding first order logic (likely as a separate game as it would probably need some bigger UI changes) too but haven't had time to do it yet
Loved the demo! Would really love to get a function to copypaste the deduction tree you already have, like if you proved in the left subbranch that the statement D is true, you could just drag over the same reasoning tree to the right branch if it is needed, like in the last level of the demo
Thanks! Yeah, such a function could be useful in some places but I think in *most* cases you can find a shorter sub-proof so that it's easy to copy manually ;) I'll keep it in mind for a possible future extension/v2 though!
I agree, but what would be more useful is instead of copy-pasting the same thing everywhere, you write it once and you can reuse it like a function. This will require it to be able to be extracted as a separate tree and then be referenced when needed.
Do you mean essentially like a custom "rule" (lemma) which you could then use like an ordinary rule wherever it fits? So basically a kind of template instead of a plain copy.
Yeah, could be thought of like that. A template being a custom combination of rules that you can use like a normal rule.
Here i use
P from P^Qand thenQ from P^Q, but instead of using this twice, i would make a template with both rules and it will then sayQ from (P^Q)^R. It could be a big technical hurdle to make it work correctly though, or it may end up being easy using the already existing way to create trees from rules, just replacing A, B, C with P, Q, R.And now that i think about it, functions/templates could be very useful if made persistent.
For example i want to more easily say that things are commutative. I create a new template
Q^P from P^Q. Now i can reuse this custom template everywhere like a rule.A simple solution for persintence could be that every level (at least the named ones), after solved, becomes a new rule you can use. Need some way of organizing so you can easily find them, though. If/when I add first order logic I think something like this would be very useful or the proofs might get very long.
I think this is called a lemma in most of logic. That would be nice to see.
Fun game, very repetitive though. Kind of fun to switch you brain off and just play off vibes
Thanks for the comment! Glad you're having fun :)
I don't get it, but i like it
I'll count that as success :)
it would be so convenient if we could also go forward from the premises so we don't have to prove B is true 3 times
You're right, I even had it at some point but decided to remove it to simplify the UI since not many levels seemed to need it. But you're not the first one to comment about it so maybe I was wrong...
I love backwards solving the “crab” way, but it is also very useful to solve forward. Maybe you could dynamically hide the forward-solving elements of the UI if the level doesn’t need it, but also let the player take control over it just in case i want to do something you didn’t expect.
I'll keep this idea in mind 👍
The full version does not include:
<-> (implies and vise versa)
-/> (does not imply)
<-
</-
Extra proofs:
A, A -/> B | not B
A, A <-> B | B
not A, A <-> B | not B
Thanks for the comment! I indeed dropped equivalence (<->) because I thought it would clutter the UI without bringing interesting new mechanics. Maybe I'll include it in a future version, though. I'll also add your proof suggestions to a list of possible future additions!
More proofs: A <-> B | A -> B, B -> A
A -> B | A -/> not B
A -/> B | A -> not B
not not A | B
A -> B | B -> A
A <-> B | A -> B, B -> A
A and B | A <-> B
not A and not B | A <-> B
A <-> B | A and B or not A and not B
not A <-> B | not A and B or A and not B
Level ideas:
1.
Premise: A -/> B
Prove: A -> not B
2.
Premises: A -> B, B -/> C
Prove: A -> not C
3.
Premise: A -/> not B
Prove: A -> B
4.
Premise: A <-> B
Prove: A -> B and B -> A
5.
Premise: A and B
Prove: not(A -/> B)
6.
Prove: (not A) -/> A
7.
Prove: (A and A-/> B) -> (A <-> B)