1

Is $ (\forall x)(A \rightarrow B \land C) \rightarrow (\forall x)(A \rightarrow B) $ an absolute theorem schema ?

  • If you think 'yes', then give a proof.
  • If you think 'no', construct a counter model or prove the invalid strong generalization from it.

I wanna make sure if my answer is right.

What I have tried :

Yes!

By deduction theorem , $ (\forall x)(A \rightarrow B \land C) \vdash (\forall x)(A \rightarrow B)$

(1) $(\forall x)(A \rightarrow B \land C) $ (hypothesis)

(2) $ A \rightarrow (B \land C) $ (1, spec)

(3) $\lnot A \lor (B \land C)$ (2, 2.4.11 + Eqn)

(4) $(\lnot A \lor B) \land (\lnot A \lor C)$ (3, 2,4,23(i) + Eqn)

(5) $(\lnot A \lor B)$ (4, split)

(6) $ A \rightarrow B$ (5, 2.4.11 + Eqn)

(7) $ (\forall x)(A \rightarrow B)$ (6 + Weak generaliztion , x dnof in $\Gamma$ )

See George Tourlakis, Mathematical Logic (2008) or this post for a lists of theorems and axioms.

Community
  • 1
Out Of Bounds
  • 1,531
  • This isn't an answer but hopefully it will be helpful for future questions: When trying to figure out if what you have is a theorem or not, try to figure out what is being said instead of trying to manipulate the symbols. e.g. in this example; fix an $x$. Now if A is true, then $B\wedge{C}$ is true. So assume $A$ is true. Then $B\wedge{C}$ is true. So what can you say about the truth value of $B$? – UserB1234 Apr 14 '14 at 23:36
  • @DanulG - your semantic argument is sound, but we have to know how to interpret the statement of the problem : "is it a theorem schema ? If you think 'yes', then give a proof." We may show that it is a valid formula and then apply completenss or we must supply a derivation in the proof system (i.e.using axioms and rules of inference allowed in the system). This "decision" is OP's responsibility... – Mauro ALLEGRANZA Apr 15 '14 at 10:13
  • @MauroALLEGRANZA I was trying to give OP the tools necessary to determine whether it was a theorem schema or not on his own. He seems to have figured it out properly but seems unsure. By "try to figure out what is being said instead of trying to manipulate the symbols", I don't mean "don't come up with a formal proof". It is meant to be interpreted as, figure out what the symbols say and hence, is it possible for this to be a theorem schema? That should help guide you to the correctness of your assertions. So you know whether a proof is possible or not after that. – UserB1234 Apr 15 '14 at 11:54
  • @MauroALLEGRANZA Is my proof correct ? – Out Of Bounds Apr 15 '14 at 16:18
  • 1
    Yes, it is correct. – Mauro ALLEGRANZA Apr 15 '14 at 16:54

1 Answers1

2

Basically, DanulG's comment gives you the needed hint : the formula is valid; thus, by completeness is provable.

Your proof is sound.

Another proof can be "manufactured" starting from the fact that :

$\vDash_{TAUT} (A \rightarrow (B \land C)) \rightarrow (A \rightarrow B)$

[easy check with truth-table].

Then apply 4.2.1 Definition (Logical Axiom Schemata of Predicate Logic) [page 139] : Ax1 : partial generalization of tautologies are axioms, to have :

$\vdash (\forall x)[(A \rightarrow (B \land C)) \rightarrow (A \rightarrow B)]$.

Finally, apply Ax3 : all formulae of the form $(\forall x)(A \rightarrow B) \rightarrow ((\forall x)A \rightarrow (\forall x)B)$ are axioms, and modus ponens to get :

$\vdash (\forall x)(A \rightarrow (B \land C)) \rightarrow (\forall x)(A \rightarrow B)$.

Mauro ALLEGRANZA
  • 94,169
  • I didn't understand How did you move from step 2 to final step ? How did you apply Ax3 and modus ponens ? Also is my proof not correct ? – Out Of Bounds Apr 15 '14 at 16:44
  • @Tennisman - step 2 to last : write the Ax3 as : $⊢(∀x)[(A→(B∧C))→(A→B)] \rightarrow [(∀x)(A→(B∧C))→(∀x)(A→B)]$; it is clearly of the "form" : $(∀x)(\alpha → \beta ) → ((∀x) \alpha → (∀x) \beta)$. Step 2 is the antecedent; thus, use it to "detach" the consequebt with mp. – Mauro ALLEGRANZA Apr 15 '14 at 16:57