Post by Thane9009 in Deductum (with free demo) comments

Viewing post in Deductum (with free demo) comments

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

nonpop203 days ago

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!

Thane9009203 days ago

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)

itch.io

Viewing post in Deductum (with free demo) comments