For any argument form in the language of propositional logic, the tree for that argument

Question

For any argument form in the language of propositional logic, the tree for that argument ...

1. always closes after a finite number of steps
2. can always be completed after a finite number of steps
3. can sometimes be closed only after an infinite number of steps
4. can sometimes be completed only after an infinite number of steps

Which of the option is true? 1, 2, 3 or 4? My attempt:

My logic instructor told me infinite set of formulas are not allowed. He also told me infinite length formulas are not allowed.

Therefore, I can only deal with finite sets of finite length formulas.

There is no way to get an infinite step tree with a finite set of finite length formulas. (Not exactly sure about this)

Therefore every tree must be able to be completed in a finite number of steps.

Option 2 is my answer.

Could someone check the reasoning for my argument?

Answer 1

I found it surprisingly hard to find a good general reference about truth trees but here is one: http://pegasus.cc.ucf.edu/~stanlick/truthtrees.htm

A truth tree is a mechanical method of checking the validity of an argument in symbolic logic. You start with the premises and the negation of the conclusion, and check to see if any possible interpretation does not lead to a contradiction. If the negation of the conclusion is inconsistent with the premises under all interpretations, the argument is valid (by definition).

What makes a truth tree work is that every step in a truth tree decomposes a more complex branch into either one or two branches of a lesser order of complexity. When a branch reaches the base level of complexity (a single statement, represented by a single letter or the negation of a single letter) it can be evaluated as either consistent with everything above it (open) or inconsistent (closed).

From the list of options, we can rule out #1 immediately, because some arguments (invalid ones) do not lead to closed trees.

To rule out number 3 and 4 we reason as follows: Any finite argument (a finite set of finite premises and a finite conclusion) will have a finite order of complexity. Since each decomposition of the tree reduces the complexity of a given branch, and adds at most two branches of lesser orders of complexity, only a finite amount of branches can be ever generated for any finite initial level of complexity, and all branches must eventually reach the base level of complexity in a finite number of steps. Therefore every tree must complete in a finite amount of time.

Answer 2

Yes, it looks fine to me.

You could make your third sentence more convincing by explaining the relation between the length of the formula (what would be a good measure?) and the size of the tree.

Answer 3

Option 2 is correct. One could also use resolution. If there's a clause p∨¬q and another clause q∨r, one can conclude p∨r. If there's no such pair of clauses, the set is satisfiable. Otherwise one gets a smaller set of clauses and since it's finite one will finish after a finite number of steps (possibly arriving at a contradiction).