[auggierose]

I like your analogy with riding a bike: If you want to ride a bike, what is more important, learning how to ACTUALLY DO IT, or to learn the physical and mechanical rules underlying it? Furthermore, technical knowledge will always be incomplete (and that applies also to logic in a very technical sense), while once you learnt how to ride a bike, your knowledge, in a way, is complete.

[cubefox]

A lot of things can be learned simply by practice, without any theory, but many things at least benefit from learning it in a more principled way. That's not feasible for riding bikes, since this relies on the the motor cortex, which doesn't understand and benefit from explicit knowledge about the physics of bike movement. Writing proofs is more intellectual, it benefits from principled understanding.

[auggierose]

Finding theorems and proofs is not intellectual at all, it is like riding a bike. You are probably not going to prove anything new and interesting by approaching it from an intellectual angle. You CAN turn it into an intellectual exercise, and at some point it is very beneficial to do so, for meta-mathematical insights. Just like it is beneficial to learn the physics and mechanics of cycling, if you want to construct bikes. It's also very helpful when you are wondering about the technical veracity of your theorems and proofs. It's not that helpful if you want to FIND those theorems and proofs in the first place. Starting out with a fixed rule system also has the danger of limiting your imagination about what's possible, given that no fixed rule system is ever going to be enough.

[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.