0

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.

  • I'm solving natural deductions if it's worth anything. – Mick Jul 28 at 22:18
  • "Communication" ? Maybe Commutation... – Mauro ALLEGRANZA Jul 29 at 8:52
2

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:

enter image description here

  1. 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.

enter image description here

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

  1. 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

enter image description here

  1. 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.

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

enter image description here

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

enter image description here

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

enter image description here

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

enter image description here

  1. 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.

enter image description here

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

  • Thank you @Frank Hubeny much appreciated for your help – Mick Jul 29 at 3:54

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.