# Proof from tree to steps

I'm able to get the proof in a tree form (it's invalid). Is there a method where I can transform it to steps method indicating the rules of inference and replacement?

• Being invalid, you cannot produce a proof in "rules form". – Mauro ALLEGRANZA Sep 25 '18 at 6:08
• Having said that, first step : Double Negation, followed by Conjunction elimination. This gives us S and U. With S we can apply Conditional elimination to 2nd premises followed again with U to get ¬R. Again by Conditional elim on 1st premise we get T ∨ ¬U and now we have to use Disjunction elim to generate two sub-proofs: one for T and one for ¬U. And so on... – Mauro ALLEGRANZA Sep 25 '18 at 6:12

To see what the tree method might look like as natural deduction steps note that the tree method converts conditionals into disjunctions and forms branches. To simulate the tree in natural deduction convert all conditionals in the premises to disjunctions before beginning. The following would be one way to look at the tree as a Fitch-style natural deduction:

The goal is to derive ¬(S ∧ U). The tree negates that and hopes each branch of the tree closes. To simulate that in natural deduction assume the negation of the goal and attempt to derive a contradiction (⊥). Hence I make the assumption ¬¬(S ∧ U) on line 4.

Lines 5, 6 and 7 are the part of the tree prior to the first branch.

The left side of the tree is shown in lines 8-17. The goal of this left side is to consider the case ¬T of the disjunction ¬T v U representing T => U on line 1. On the left side all branches close, that is, a contradiction was derived.

The right side of the tree is shown in lines 18-28. Not all branches close in the tree, nor do all cases lead to a contradiction in the natural deduction proof.

This shows one way to simulate what the tree was doing in natural deduction. For the proof checker and a textbook describing the natural deduction inference rules, see the links below.

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