Talk:Proof: Difference between revisions

::::: Please don't insult other users of RC; it's uncivil and will simply result in action being taken against you. You should be able to conduct discourse here without stooping so far.

::::: In general, when reasoning about infinite constructive structures (e.g., the natural numbers), you show a number of statements that are true and use mathematical induction to extrapolate to the whole infinite structure. The tricky bit is that induction is a second-order operation, and it's often easiest to have it be an axiom; the proof then consists of building the model and showing the base cases and inductive steps are true, since the assembly of that into an overall proof follows trivially from the axiomatization. I forget whether MLTT works that way though; back when I was active in the theoretical CS area, I focused far more on modal and (especially) temporal logic (which have their own special problems). –[[User:Dkf|Donal Fellows]] 09:03, 15 May 2012 (UTC)