Do you ever use formal logic when working on proofs?

Question

This question has the danger of being subjective but I nevertheless think people might learn from each other's answers.

Mathematics textbooks almost never write their proofs in formal logic, but in "mathematical natural language".

What I mean is, that there are two ways to prove a statment:

1. Using natural language: "take any $\epsilon$. Now define $\delta(\epsilon)$ such that ... Then clearly, for all ..."

2. Using formal logic with logical deductive rules: $\forall x\in X\exists\delta...$. Applying logic rule $X$ gives $\exists x ...$.

Of course there is a good reason for using natural language: it is more intuitive and therefore easier to follow and easier to come up with.

However I sometimes find that using formal logical rules can clarify my thinking and help me woth proofs. I find that when I get stuck using natural language, switching to thinking about the problem in formal logic can help, and vice versa.

So I'm wondering, do you ever use formal logic while you're working to come up with a proof? Why, why not? What role does it play in your process of coming up with proofs?

Note: I'm only a relative beginner at proving theorems, since I have much more experience with applied math.

Answer 1

When I'm writing to a proof I use formal way. I do this because I find it easier to remember like this, using that way makes me think about how to write each step and thus makes me remember it better. Another advantage I think it has is that writing formally makes you read formally better which is great thing to know.

When I'm explaining something, giving hints, brainstorm etc. I prefer to use natural way, because I think that it gives you the advantages of understanding "why it is like it is" and not only the "how you get to that".

Answer 2

Basically never, it's both too slow and too hard to read. The point of learning formal logic isn't to use formal logic (unless you then go on to work in logic, where you will be writing proofs in natural language about logic), it's to train habits of thought and get you to clarify your thinking both to yourself and to others; a simple example is being able to instantly negate a universal quantifier to get an existential quantifier and vice versa (which everyone knows everyone else can do and hence which nobody will explicitly mention that they're doing). Once you've ingrained the relevant habits you don't need the formal logic anymore.

See also Terence Tao's description of the pre-rigorous, rigorous, and post-rigorous stages of learning math.

Answer 3

I mostly rely on what you call 'mathematical natural language', as it usually better 'fits' my conceptual ways to think about a problem, but there are definitely times when I work something out in formal logic to better grasp some of the details, e.g so I can see the difference between a $\forall x \exists y ...$ and a $\exists y \forall x ...$, for example.

Thus, as with most things like this, sometimes one representation is more helpful, and at other times a different representation is more helpful. Cognitively this makes sense: representations cue us to proceed in certain ways, and so different representations can cue us differently. So that's exactly why you sometimes get stuck using one representation, but 'see the light' when using the other one, and vice versa.