[cubefox]

Proving things with formal calculi still relies on something like creativity, which itself isn't captured by a precise algorithm, similar to informal proofs. The advantage of learning formal proof is, I claim, purely didactic, as it gives a clear idea on what a valid inference step is in the ideal case. I don't think there is really a danger of limiting your imagination, as you will probably stop thinking in formal terms as soon as you are good in doing informal proofs.

For example, the above Stanford document on proof basics doesn't even mention elementary inference rules like modus tollens. It briefly refers to "the contrapositive", but without explaining what the contraposition rule even is. It was clearly written by someone who regards all these as too obvious to be mentioned in such a document (he only explains proof by contradiction), but they are not obvious to novices.

Anyway, your comment reminds of an interesting paper[1] by Yehuda Rav, where he defends the autonomy of informal proof with original arguments against the "formalists". You might be interested, I think your intuitions are going in a similar direction.

[1] http://sgpwe.izt.uam.mx/files/users/uami/ahg/1999_Rav.pdf

[auggierose]

Thanks for the link, looks like an interesting paper!

The thing is, formal rules can only model what you already understand. A formal rule can tell you exactly WHAT and HOW, but not WHY. But especially with basic proof rules like modus ponens, that is essential. So intuitive understanding is prior to formal rules. Of course, lots can be gained from the interplay of intuition and formality, I am the last one to deny that.

For me, that is an important issue, because I am a big proponent of doing logic on the computer, which necessarily is formal. Nevertheless, the goal here is to make logic on the computer as intuitiv as possible, something many people in the field don't seem to have a desire for. I also don't want the next generation to think exclusively in formal systems, in terms of, oh, if my formal system doesn't allow that, what I want to do must be wrong, or at least stupid. There is already enough of that going around with type theorists.

[Tainnor]

> Proving things with formal calculi still relies on something like creativity, which itself isn't captured by a precise algorithm, similar to informal proofs.

That's because first-order logic (and any system that extends it) is formally undecidable, so there can be no algorithm that, for a given statement, determines whether it is a valid theorem. If you restrict yourself to propositional logic, you gain decidability but, in the general case, it's still extremely inefficient (unless P=NP).

Of course, in order to prove these things, you have to formally develop what logic is.

[cubefox]

Yeah. Though if one is loose with the word "algorithm" one can count an advanced machine learning model (a few years from now) as such an algorithm. It wouldn't be able to prove or disprove every given first-order statement, but perhaps the vast majority below a certain length. Maybe it could decide every conjecture we are interested in.