Are there rules for the following in the Open Logic Project's proof checker?

Question

I'm using http://proofs.openlogicproject.org/ but can't find out what the translation of the rules are. I'm new at this, so when I try to make proofs, I know what I want the justification to be (which is required) but don't know them and couldn't find a cheat sheet online (aside from their examples, which were only so helpful.

I'm using 10 replacement rules: De Morgan, Double Neg, Commutation, Association, Distribution, Transportation, Material Implication, Material Equiv, Exportation, and tautology.

I have 8 implication rules: Mudus Ponens and Tollens, Hypo. Syll., Disjunctive Syll, Simplification, Addition, Conjunction, and Constructive Dilemma.

Some are easy: Modus ponens →E, ModusT MT, Disj Syll DS, Simplif ^E, addition vI, De Morgan DeM, Double negative DNE

I'm looking for Hypothetical Syllogism, Constructive Dilemma, Communication, association, distribution, transportation, material implication, material equiv, exportation, and tautology (even though it's useless).

I want to check my answers, but can't place it. Thanks to anyone who can help. If you knew the program online, that would make things super easy.

Answer 1

Some of the rules that might be present in another system may have to be derived separately in this proof checker as they are needed.

Here is the question:

I'm looking for Hypothetical Syll, Constructive Dilemma, Communication, association, distribution, transportation, material implication, material equiv, exportation, and tautology (even though it's useless).

1. Hypothetical Syllogism: P → Q, Q → R ∴ P → R This rule does not exist, but it is easy to derive. It involves assuming P, using conditional elimination twice and then conditional introduction:

2. Constructive Dilemma: P → Q, R → S, P ∨ R ∴ Q ∨ S This rule does not exist, but it can be derived given the premises. Consider both cases of the disjunction P ∨ R using conditional elimination and disjunction introduction to derive Q ∨ S for each case.

There is more information about the rules in the forallx text.

3. Communication: Assuming this means the commutative property for disjunction or conjunction, you can introduce a disjunct or conjunct on either side. The following can be derived: P ∧ Q ∴ Q ∧ P

4. Association: The associative property would be similar to the commutative. It is assumed that parentheses are used to pair conjuncts or disjuncts. They can be separate and then repaired in a different manner.

5. Distribution: The distribution of conjunction over disjunction: P ∨ Q, R ∴ (P ∧ R) ∨ (Q ∧ R)

6. Transposition: ∴ P → Q ↔ ¬Q → ¬P

7. Material Implication: ∴ P → Q ↔ ¬P ∨ Q

8. Exportation: ∴ [(P ∧ Q) → R] ↔ [P → (Q → R)]

9. Tautology: ∴ (P ∨ P) ↔ P Proving the simple ones can sometimes be challenging. Note that I referenced the line 2 as two separate blocks: 2-2,2-2. This took care of both cases of the disjunction elimination.

Going through the above proofs in the proof checker should also provide practice using the tool.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf