# Visualizing Concepts in Mathematical Logic

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!

-

2
Use a truth table. – Brian Jan 15 at 2:39
One obstruction I have (but maybe others don't) is that $P \rightarrow Q$ being true whenever $P$ is false immediately doesn't sync of up with my intuition. For example, consider: If I had been born with blue eyes, I would have proved Goldbach's Conjecture by age 13. Now, since I was born with brown eyes, this statement is "true." But, since we are talking intuition here, I believe in a strong way that the preceding statement is false. Relatedly, you might check out: A Counterexample to Modus Ponens. Vann McGee. The Journal of Philosophy, jstor.org/stable/2026276. – B.D Jan 15 at 2:42
– MJD Jan 15 at 2:49
– B.D Jan 15 at 2:56
A mathematician was once asked, what do you see then you read $f(x,y)=0$? He replied, "I see $f(x,y)=0$". So it depends, some mathematicians are more geometric, some more algebraic. – alancalvitti Jan 15 at 3:00
show 2 more comments

## 2 Answers

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.

-
"But in contrast, A→B is not a theorem, because how can you write a function that gets and argument of type A and gives back a result of some other, completely arbitrary type?" I'm not sure I follow this without a very precise definition of "type". It is quite common to write a program that returns a different kind of data than it was given. – Austin Mohr Jan 15 at 3:05
1. Yes, you are quite right, and if you are interested, I suggest you follow this up, because I think the subject is fascinating. 2. To write a program that returns a different sort of data than it receives requires that your language have some built-in function or operator for converting one to the other, something like C's `atoi` function which converts strings to integers. Such a built-in function of type `string→int` is analogous to having a contextual assumption in the logic, on the left-hand side of the $\vdash$. – MJD Jan 15 at 3:09

1
3. Even in the presence of such built-in functions, $A\to B$ is impossible, because $B$ is completely unconstrained. You may be able to write a program that takes a value of one type and returns a value of another, but you can't write a program that returns a value of a completely arbitrary type. If your function takes a `string` and returns an `int`, I can object that I didn't want an `int`, I wanted a `(int\to(double, string))\to array of float`, and your function doesn't produce one. – MJD Jan 15 at 3:12

I think part of what makes excellent practitioners excellent is that they have many different intuitive representations of the things they work with, and can switch between them effortlessly according to what works well in a given situations. The important thing is to not stick with a single visualization and use that for everything, but to be familiar with a range of possibilities that you can quickly test to see if one of them is helpful for the task at hand.

The Curry-Howard isomorphism (see MJD's answers) is great to know, especially if you already have (functional) programming experience. Closely related to it is the intuitionistic conception of proofs as conversational games, an informal version of which is often used to explain the semantics of quantifiers to beginning students ("the adversary chooses an $\epsilon>0$ and then we have to produce a $\delta>0$ such that ..."). This can be extended to propositional connectives: If we want to prove $P\land Q$, the adversary chooses whether he wants to see our proof of $P$ or of $Q$, but to prove $P\lor Q$, we get to choose which of the proofs to present. If we must prove $P\to Q$, the adversary starts by giving us his proof of $P$, and afterwards we must prove $Q$.

More specifically visual, Venn diagrams can indeed be useful, but become cumbersome if there are many propositional letters. Personally I often find it surprisingly helpful simply to visualize the abstract syntax tree of a formula instead of its linear written syntax. This is related to (but distinct from) visualizing a propositional formula as a Boolean circuit containing gates and wires.

Even something as primitive as truth tables can be helpful for some purposes. For example, my best intuition about how the possible two-variable Boolean functions relate to each other is in terms of two-dimensional truth tables: $$\begin{array}{c|cc} \to & 0 & 1 \\ \hline 0 & 1 & 1 \\ 1 & 0 & 1 \end{array} \quad \begin{array}{c|cc} \land & 0 & 1 \\ \hline 0 & 0 & 0 \\ 1 & 0 & 1 \end{array} \quad \begin{array}{c|cc} \oplus & 0 & 1 \\ \hline 0 & 0 & 1 \\ 1 & 1 & 0 \end{array} \quad \begin{array}{c|cc} \text{a} & 0 & 1 \\ \hline 0 & 0 & 0 \\ 1 & 1 & 1 \end{array} \quad \ldots$$ where, for example "$\to$" and "$\land$" is similar because their truth tables both have a wedge of three identical squares with an odd one in one of the corners. I can make one into the other by flipping and inverting, which tells me that an AND gate can become an IMPLIES gate by adding inverters to some of the inputs and outputs, and vice versa.

-
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 51, "mathjax_display_tex": 2, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9427041411399841, "perplexity_flag": "head"}