Monday, September 26, 2011

With Conditional Proof You Never Need a Rule of Repetition

Suppose we have the rule of hypothesis introduction, conditional introduction, and conditional elimination. From just these rules of inference, in classical propositional calculus, we never need a rule of repetition, nor need CqCpq as an axiom. In other words, if those rules hold, then "q, p|-q" comes as a valid schema and CqCpq is a theorem.

1 | q hypothesis introduction
2 || p hypothesis introduction
3 ||| q hypothesis introduction
4 || Cqq 3-3 conditional introduction
5 || q 1, 4 conditional elimination
6 | Cpq 2-5 conditional introduction
7 CqCpq 1-6 conditional introduction.

No comments:

Post a Comment