Talk:Theorem-proving
Apologies to the original author of TheoremProving, but, having proven a few theorems in my time, but I thought your claims were, basically, false, and it wasn't clear what you were trying to get at anyway...so I deleted them and left a little about what was correct and generally-accepted and -understood on the
Can anything be said in generality besides theorem proving has a tendency to go:
- Theorem: Statement of thm.
- Proof: This, that,the other, Lemma1, Lemma2, special case, QED.
- follows from two previous statements by the rule of modus ponens
Typically, proofs of all sorts make use of various inference rules, not just modus ponens. Am I not understanding something? --LMS
In the formal mathematical definition, only modus ponens is allowed, since it's all that's needed and things should be kept simple. Anything else is considered to be a shorthand for several intermediate steps. --JG
There are many formalized logics, with corresponding formal notions of proof. For proof systems which can be nicely divided into axioms and inference rules, some of them have modus ponens as the only inference rule and others do not. (To some extent, it depends on whether you are using or studying the proof system. Formalized proof systems which are actually used, as in automatic theorem proving, tend to have more complex inference rules.) --Carl Witty