# Logic: Structural Induction and Tree-method problem!

1. Sep 28, 2009

### A.Dasher

I have this challenge to do but can't seem to be able to understand it completely! I also have test right now and can't concentrate. Please help this poor soul!!! It will be appreciated!
The first question is:Let F ∈ PROP. Let (h)F be defined by the number of parentheses in the formula F.
a): Give a recursive definition of the function h: PROP -> N (natural numbers) for the number of parentheses in the formula: F= ¬(p1 v (¬p2->p1)) or in this case h(F)=4; Feel free to change the formula if you'd like.
b): Prove with structural induction, using the definition you gave in question a and the function props, that for all proposition formulas F∈ PROP:
1/2 * h(F)+1= props (F);

And the second one is a tree method:
Let A,B,C ∈PROP. Check if these meta-allegations are true or false. Use the tree-method to show if there are counterexamples for these allegations. If there are counterexamples give at least 1 valuation.
a): A->B, ¬B->C |=A->C;
b): A<->(¬B v ¬C), ¬(A -> ¬ C) |= ¬B
Thank you before hand! I really, REALLY appreciate it!

2. Sep 28, 2009

### honestrosewater

What is the function props?

What is your definition of formulas? It should be inductive and go something like this:
if x is a variable, then x is a formula.
if x and y are formulas, then ¬(y) and (y -> z) are formulas.​
And so on for whatever logical operators you have. You could start from the outermost and leftmost formula, identify what kind of formula it is (atomic, negation, implication, etc), add the corresponding number of parentheses to your counter, remove them and the operator, and repeat. Follow a branch until it contains only what kind of formulas?

I'll assume the tree method is the semantic tableau. It's been a while, but I can try. Where do you get stuck? Do you know how to set it up? You want to prove that you cannot satisfy both the premises and the negation of the conclusion. So start with
(A->B)&(¬B->C)&(¬(A->C))​
What can you get from there? (Save the disjunctions for last so you'll need fewer nodes.)