[Math] Visualizing Concepts in Mathematical Logic

discrete mathematicslogic

If you were forced to speculate or offer anecdotal evidence, how would you say excellent practicioners of mathematical logic coneptually grasp statements like:

$$ \vdash ((P \rightarrow Q) \rightarrow Q) \rightarrow Q $$

…on an intuitive level?

Specifically, I'm curious if excellent practicioners will typically VISUALIZE such statements in any sort of way that doesn't involve mentally picturing the literal statement with its syntax as written above. For example, are Venn or Euler Diagrams typically a good way to go about things, or is that a bad idea in the long-run?

Personally, I know that with Analysis/Group Theory/Topology I have been successful in finding rough visualizations of pretty much every concept involved (with the understanding that mental pictures are not LITERAL representations of the relevant concepts and in fact can often be quite misleading if one is not careful with them); however, with logic I am finding this more difficult since the mathematical objects in question seem in many ways to be largely, explicitly syntactical. What this means is that the more I rougly convert formal statements into "intuitive" pictures, the more those intuitive pictures start to exactly resemble a specific interpretation which gets in the way of those sentences being explictly syntactical in nature.

As a consequence of this mess, I find myself getting confused in lacking basic intuitions over whether elementary statements are true or false before I attempt to prove them, unlike in other mathematical subjects.

In short, does anyone have any anecdotal or even speculative advice about how to be successful in visualizing (or NOT visualizing) the objects of Math Logic? How does one gain an intuitive feel for this subject?

Thanks!

Best Answer

Something that I sometimes find useful is to consider what's called the Curry-Howard Isomorphism: statements of logic correspond to the types of computer programs, and the statements are theorems if and only if the corresponding type is the type of a program that can actually exist.

In this correspondence, $A\to B$ represents the type of a function in a program that takes an argument of type $A$ and calculates a value of type $B$.

A function of type $A\to A$ is obviously possible, because the function just takes the $A$ that it got and gives it right back:

 define function f(a) {
   return a;
 }

And $A\to(B\to A)$ is also possible: the function needs to take an argument of type $A$ and then give back a function of type $B\to A$. It can do this, because it can give back a second function that ignores the $B$ that it got, and that gives back the $A$ that the first function got to begin with:

 define function f(a) {
   define function g(b) {
     return a;
   }
   return g;
 }

But in contrast, $A\to B$ is not a theorem, because how can you write a function that gets an argument of type $A$ and gives back a result of some other, completely arbitrary type? Where could it get a $B$ from if all it has is an $A$?

The isomorphism also identifies logical AND with pairing: a value of type $A\land B$ is a pair that contains both an $A$ and a $B$, and either (or both) can be extracted. It identifies logical OR with what's called a disjoint union: A value of type $A\lor B$ is either an $A$ or a $B$, but not both, and the program can tell which of the two it is. Similarly there are interpretations for negation, for constant true and false values, and so forth.

For a more elaborate example, a program that corresponds to the theorem $\lnot\lnot(P\lor\lnot P)$, see this answer.

The only catch is that not every classically true theorem corresponds to a program in a completely straightforward way. Some theorems of logic, such as $((A\to B)\to A)\to A$, (Peirce's law) don't correspond to a simple program. Instead they correspond to programs that use advanced features like continuations or exceptions.

Still it's often helpful to think of logical theorems as specifications for programs; if you can think of a program which performs the corresponding calculation, then the statement must be a theorem.

Viewed in this way, the statement you originally asked about, $((P\to Q)\to Q)\to Q$, seems quite unlikely: you need a function $f$ which gets an argument $x$, which is itself a function of type $(P\to Q)\to Q$, and $f$ needs to produce a value of type $Q$. If $f$ could call $x$, then $x$ would return the needed value. But it can't call $x$ because to do so it needs to give it an argument of type $P\to Q$, and it doesn't have one.

Related Question