I like playing around with formal logic, but when proving things about synthetic geometry in the usual kinds of formal logic, you sometimes have to spend time proving things that would be obvious from a diagram. It's often stated that diagrams can't be part of a formal proof because they can deceive you into thinking you've proved false things, such as the infamous proof that all triangles are isosceles. But in all the false proofs using diagrams I've seen, the problem was that the diagram didn't consider all possible cases. There's no reason a system of logic using diagrams couldn't be made just as sound as regular predicate logic.

So I've started reading PDF related, which describes such a system of diagrams for proving things about geometry. It's a short book made from an edited version of his PhD thesis. Apparently people have also been studying systems of diagrammatic reasoning not specific to geometry such as Venn diagrams and similar systems, including proving various soundness results about them. One criticism I've seen about the system in the book is that the number of cases you have to draw can be very large, and you can see one instance of that in the book in Figure 9. But at least the operation that leads to Figure 9 is not something you'd normally do in a proof, so I don't know yet how much of a problem case explosion is in practice. I'm hopeful that this system can and will be improved upon, and that in general diagrams will become a more common tool in formal proofs.

Here's the "all triangles are isosceles" proof in case you haven't seen it, taken from https://jdh.hamkins.org/all-triangles-are-isosceles/:

>Consider an arbitrary triangle △ABC. Let Q be the intersection of the angle bisector (blue) at ∠A and the perpendicular bisector (green) of BC at midpoint P.

>Drop perpendiculars from Q to AB at R and to AC at S. Because P is the midpoint of BC and PQ is perpendicular, we deduce BQ ≅ CQ by the Pytha*****an theorem. Since AQ is the angle bisector of ∠A, the triangles AQR and AQS are similar, and since they share a hypotenuse, they are congruent. It follows that AR ≅ AS and also QR ≅ QS. Therefore △BQR is congruent to △CQS by the hypotenuse-leg congruence theorem. So RB ≅ SC. And therefore, AB ≅ AR+RB ≅ AS+SC ≅ AC, and so the triangle is isosceles, as desired. QED

P112860
Colon *****ed up the link:
https://jdh.hamkins.org/all-triangles-are-isosceles/
This false proof was originally devised by W. W. Rouse Ball in Mathematical Recreations and Essays (1892).

Using formal logic only works when you already correctly know the relationships between things.

1+1=2 works for apples, but that logic doesn't work for things like radians that are cyclic instead of linear, it doesn't work for shadows, it doesn't work for a lot of stuff.

So logics are specific to objects, and to learn the logic of an object, it's relationship with other things, you have to observe it first to know it applies.

Science is testing hypothesis about relationships, but the actual formulation of relationships still relies on obeservations to deduce a pattern of relationships between objects. The reason formulas in math and physics seem to always work is just because those are the ones that were tested and worked repeatedly in different situations, not because there are some unviolatable rules that can be extrapolated indefinitely to deduce everything.

Formal logic requires you to get your premises correct, to get the correct conclusion. I also imagine it's pretty limited, but it's such a boring subject I didn't look deep enough into it to find out. I don't remember being able to describe time dependent relationships in formal logic, for instance.

All the formulas and rules we make up to describe the relationships we see have the possibility of hidden variables or factors that aren't accounted for that could change outcomes in a given situation. This always exists as a possibility because in real systems we can't test every possible situation.

Maybe if you have the right quest item in your inventory, an object will behave differently, because there was a hidden variable.

The way that our brains work, taking repeatedly observed things as the norm, you probably wouldn't notice when a relationship between objects was unusual, then it would become an accepted scientific fact. Magnets used to be magic rocks and extremely abnormal in the natural world. Magnetism was a hidden variable that has become an accepted scientific fact.

Rubbing iron with a magnet can make the iron magnetic, then tapping the iron a few times causes it to loose its magnetism. You don't think that's an usual relationship? What other things can you change the state of and transfer properties to like that? You can't rub a piece of wood with a rock to make it heavier, then tap it to make it lighter.

Magnetism only makes sense because people repeatedly observed it and assembled some rules to reliably describe its behavior, but for most of mankind's existence it was a hidden variable.

And magnetism can change the outcomes of other systems.

Magnetize a few parts in a mechanical clock and your formulas for the mechanics of a mechanical clock won't work anymore.

Mechanical clocks don't work the same if you stick a magnet in them and exert forces on the parts, magnetism was a hidden variable.

When he starts covering the SAS theorem you start seeing case explosion become a real problem. Pic related is just some of the diagrams that occur in one step of a proof of one case of the theorem. You can't even state the theorem in his system without breaking it down into a lot of needless cases, because the theorem involves two triangles and you have to draw every possible way the two triangles can intersect.

But it's also pretty clear that this could be massively improved upon. An obvious improvement would be to add a way to say that two figures, each depicted in its own diagram, exist in a plane without caring about how or whether the figures intersect. One improvement he suggests himself but does not implement is combining his diagrams with the usual sentential systems of logic. Making his diagrams into propositions that could be combined with logical connectives could be a good way to implement the capability I want. The way his system works, multiple diagrams always represent different cases, like propositions connected with "or". If we could connect them with "and" instead, we could represent the two triangles on different diagrams and say that both exist somewhere in the plane.

As for the sort of case explosion shown in the attached pic, it seems suboptimal even by his existing rules. You would get fewer cases if you constructed the new triangle using multiple steps. You'd still need to be able to depict two figures without saying how they intersect to get the cases down to a reasonable level.