Talk:Logical graph

Notes & Queries

\(\cdots\)

Place For Discussion

\(\cdots\)

Logical Equivalence Problem

Problem

Problem posted by Mike1234 on the Discrete Math List at the Math Forum.

• Required to show that \(\lnot (p \Leftrightarrow q)\) is equivalent to \((\lnot q) \Leftrightarrow p.\)

Solution

Solution posted by Jon Awbrey, using the calculus of logical graphs.

In logical graphs, the required equivalence looks like this:

      q o   o p           q o
        |   |               |
      p o   o q             o   o p
         \ /                |   |
          o               p o   o--o q
          |                  \ / 
          @         =         @

We have a theorem that says:

        y o                xy o
          |                   |
        x @        =        x @

See Logical Graph : C₂. Generation Theorem.

Applying this twice to the left hand side of the required equation, we get:

      q o   o p          pq o   o pq
        |   |               |   |
      p o   o q           p o   o q
         \ /                 \ /
          o                   o
          |                   |
          @         =         @

By collection, the reverse of distribution, we get:

          p   q
          o   o
       pq  \ / 
        o   o
         \ /
          @

But this is the same result that we get from one application of double negation to the right hand side of the required equation.

QED

Discussion

Back to the initial problem:

• Show that \(\lnot (p \Leftrightarrow q)\) is equivalent to \((\lnot q) \Leftrightarrow p.\)

We can translate this into logical graphs by supposing that we have to express everything in terms of negation and conjunction, using parentheses for negation and simple concatenation for conjunction. In this way of assigning logical meaning to graphical forms — for historical reasons called the "existential interpretation" of logical graphs — basic logical forms are given the following expressions:

The constant \(\operatorname{true}\) is written as a null character or a space.

This corresponds to an unlabeled terminal node in a logical graph. When we are thinking of it by itself, we draw it as a rooted node:

          @

The constant \(\operatorname{false}\) is written as an empty parenthesis\[(~).\]

This corresponds to an unlabeled terminal edge in a logical graph. When we are thinking of it by itself, we draw it as a rooted edge:

          o
          |
          @

The negation \(\lnot x\) is written \((x).\!\)

This corresponds to the logical graph:

          x
          o
          |
          @

The conjunction \(x \land y\) is written \(x y.\!\)

This corresponds to the logical graph:

         x y
          @

The conjunction \(x \land y \land z\) is written \(x y z.\!\)

This corresponds to the logical graph:

        x y z
          @

And so on.

The disjunction \(x \lor y\) is written \(((x)(y)).\!\)

This corresponds to the logical graph:

        x   y
        o   o
         \ /
          o
          |
          @

The disjunction \(x \lor y \lor z\) is written \(((x)(y)(z)).\!\)

This corresponds to the logical graph:

        x y z
        o o o
         \|/
          o
          |
          @

And so on.

The implication \(x \Rightarrow y\) is written \((x (y)).\!\) Reading the latter as "not \(x\!\) without \(y\!\)" helps to recall its implicational sense.

This corresponds to the logical graph:

        y o
          |
        x o
          |
          @

Thus, the equivalence \(x \Leftrightarrow y\) has to be written somewhat inefficiently as a conjunction of two implications\[(x (y)) (y (x)).\!\]

This corresponds to the logical graph:

      y o   o x
        |   |
      x o   o y
         \ /
          @

Putting all the pieces together, showing that \(\lnot (p \Leftrightarrow q)\) is equivalent to \((\lnot q) \Leftrightarrow p\) amounts to proving the following equation, expressed in the forms of logical graphs and parse strings, respectively:

      q o   o p           q o
        |   |               |
      p o   o q             o   o p
         \ /                |   |
          o               p o   o--o q
          |                  \ /
          @         =         @

( (p (q)) (q (p)) ) = (p ( (q) )) ((p)(q))

That expresses the proposed equation in the language of logical graphs. To test whether the equation holds we need to use the rest of the formal system that comes with this formal language, namely, a set of axioms taken for granted and a set of inference rules that allow us to derive the consequences of these axioms.

The formal system that we use for logical graphs has just four axioms. These are given here:

• Logical Graph Axioms

Proceeding from these axioms is a handful of very simple theorems that we tend to use over and over in deriving more complex theorems. A sample of these frequently used theorems is given here:

• C₁. Double Negation Theorem
• C₂. Generation Theorem
• C₃. Dominant Form Theorem

In my experience with a number of different propositional calculi, the logical graph picture is almost always the best way to see why a theorem is true. In the example at hand, most of the work was already done by the time we wrote down the problem in logical graph form. All that remained was to see the application of the generation and double negation theorems to the left and right hand sides of the equation, respectively.

Reflection

\(\cdots\)

Logical Graph Sandbox

More thoughts on Peirce's law

1-way version\[((a \Rightarrow b) \Rightarrow a) \Rightarrow a\]

        a o--o b
          |
          o--o a
          |
          o--o a
          |
          @         =         @

2-way version\[((a \Rightarrow b) \Rightarrow a) \Leftrightarrow a\]

        a o--o b
          |
          o--o a
          |                   a
          @         =         @

Compare with:

        a o b
          |
          o--o a
          |                   a
          @         =         @

That is:

       ab   a
        o   o
         \ /
          o
          |                   a
          @         =         @

This is the so-called absorption law, commonly written in the following ways:

\[(a \land b) \lor a \iff a\]

\[ab \lor a = a\]

Reports of my counter-intuitiveness are greatly exaggerated

We have the following theorem of classical propositional calculus:

\[(p \Rightarrow q) \lor (q \Rightarrow p)\]

The proposition may appear counter-intuitive on some ways of reading it, and it is usually excluded from the theorems of intuitionistic propositional calculi.

Read as a statement about the values of propositions — where the values \(p, q\!\) are drawn from the boolean domain \(\mathbb{B} = \{0, 1 \}\) — and written as an order law, its sense may become more sensible:

\[(p \le q) \lor (q \le p)\]

Here it is in logical graphs:

      q o   o p
        |   |
      p o   o q
        |   |
        o   o
         \ /
          o
          |
          @         =         @

Proof

      q o   o p
        |   |
      p o   o q
        |   |       q   p
        o   o       o   o       o   o         o           o
         \ /         \ /         \ /          |           |
          o        pq o        pq o        pq o           o
          |           |           |           |           |
          @     =     @     =     @     =     @     =     @     =     @

My guess as to what's going on here — why the classical and intuitionistic reasoners appear to be talking past each other on this score — is that they are really talking about two different domains of mathematical objects. That is, the variables \(p, q\!\) range over \(\mathbb{B}\) in the classical reading while they range over a space of propositions, say, \(p, q : X \to \mathbb{B}\) in the intuitionistic reading of the formulas. Just my initial guess.

On the reading \(P, Q : X \to \mathbb{B},\) another guess at what's gone awry here might be the difference between the following two statements:

\((\forall x \in X)(Px \Rightarrow Qx) \lor (Qx \Rightarrow Px)\)

\((\forall x \in X)(Px \Rightarrow Qx) \lor (\forall x \in X)(Qx \Rightarrow Px)\)

But the latter is not a theorem in anyone's philosophy, so there is really no disagreement here.

Functional quantifiers

Tables

The auxiliary notations:

\[\alpha_i f = \Upsilon (f_i, f),\!\]

\[\beta_i f = \Upsilon (f, f_i),\!\]

define two series of measures:

\[\alpha_i, \beta_i : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B},\]

incidentally providing compact names for the column headings of the next two Tables.

Table 1. Qualifiers of Implication Ordering:  \(\alpha_i f = \Upsilon (f_i \Rightarrow f)\)

\(p:\) \(q:\)	1100 1010	\(f\!\)	\(\alpha_{15}\)	\(\alpha_{14}\)	\(\alpha_{13}\)	\(\alpha_{12}\)	\(\alpha_{11}\)	\(\alpha_{10}\)	\(\alpha_9\)	\(\alpha_8\)	\(\alpha_7\)	\(\alpha_6\)	\(\alpha_5\)	\(\alpha_4\)	\(\alpha_3\)	\(\alpha_2\)	\(\alpha_1\)	\(\alpha_0\)
\(f_0\)	0000	\((~)\)																1
\(f_1\)	0001	\((p)(q)\!\)															1	1
\(f_2\)	0010	\((p) q\!\)														1		1
\(f_3\)	0011	\((p)\!\)													1	1	1	1
\(f_4\)	0100	\(p (q)\!\)												1				1
\(f_5\)	0101	\((q)\!\)											1	1			1	1
\(f_6\)	0110	\((p, q)\!\)										1		1		1		1
\(f_7\)	0111	\((p q)\!\)									1	1	1	1	1	1	1	1
\(f_8\)	1000	\(p q\!\)								1								1
\(f_9\)	1001	\(((p, q))\!\)							1	1							1	1
\(f_{10}\)	1010	\(q\!\)						1		1						1		1
\(f_{11}\)	1011	\((p (q))\!\)					1	1	1	1					1	1	1	1
\(f_{12}\)	1100	\(p\!\)				1				1				1				1
\(f_{13}\)	1101	\(((p) q)\!\)			1	1			1	1			1	1			1	1
\(f_{14}\)	1110	\(((p)(q))\!\)		1		1		1		1		1		1		1		1
\(f_{15}\)	1111	\(((~))\)	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1

Table 2. Qualifiers of Implication Ordering:  \(\beta_i f = \Upsilon (f \Rightarrow f_i)\)

\(p:\) \(q:\)	1100 1010	\(f\!\)	\(\beta_0\)	\(\beta_1\)	\(\beta_2\)	\(\beta_3\)	\(\beta_4\)	\(\beta_5\)	\(\beta_6\)	\(\beta_7\)	\(\beta_8\)	\(\beta_9\)	\(\beta_{10}\)	\(\beta_{11}\)	\(\beta_{12}\)	\(\beta_{13}\)	\(\beta_{14}\)	\(\beta_{15}\)
\(f_0\)	0000	\((~)\)	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1	1
\(f_1\)	0001	\((p)(q)\!\)		1		1		1		1		1		1		1		1
\(f_2\)	0010	\((p) q\!\)			1	1			1	1			1	1			1	1
\(f_3\)	0011	\((p)\!\)				1				1				1				1
\(f_4\)	0100	\(p (q)\!\)					1	1	1	1					1	1	1	1
\(f_5\)	0101	\((q)\!\)						1		1						1		1
\(f_6\)	0110	\((p, q)\!\)							1	1							1	1
\(f_7\)	0111	\((p q)\!\)								1								1
\(f_8\)	1000	\(p q\!\)									1	1	1	1	1	1	1	1
\(f_9\)	1001	\(((p, q))\!\)										1		1		1		1
\(f_{10}\)	1010	\(q\!\)											1	1			1	1
\(f_{11}\)	1011	\((p (q))\!\)												1				1
\(f_{12}\)	1100	\(p\!\)													1	1	1	1
\(f_{13}\)	1101	\(((p) q)\!\)														1		1
\(f_{14}\)	1110	\(((p)(y))\!\)															1	1
\(f_{15}\)	1111	\(((~))\!\)																1

Table 3. Simple Qualifiers of Propositions (n = 2)

\(p:\) \(q:\)	1100 1010	\(f\!\)	\((\ell_{11})\) \(\text{No } p \) \(\text{is } q \)	\((\ell_{10})\) \(\text{No } p \) \(\text{is }(q)\)	\((\ell_{01})\) \(\text{No }(p)\) \(\text{is } q \)	\((\ell_{00})\) \(\text{No }(p)\) \(\text{is }(q)\)	\( \ell_{00} \) \(\text{Some }(p)\) \(\text{is }(q)\)	\( \ell_{01} \) \(\text{Some }(p)\) \(\text{is } q \)	\( \ell_{10} \) \(\text{Some } p \) \(\text{is }(q)\)	\( \ell_{11} \) \(\text{Some } p \) \(\text{is } q \)
\(f_0\)	0000	\((~)\)	1	1	1	1	0	0	0	0
\(f_1\)	0001	\((p)(q)\!\)	1	1	1	0	1	0	0	0
\(f_2\)	0010	\((p) q\!\)	1	1	0	1	0	1	0	0
\(f_3\)	0011	\((p)\!\)	1	1	0	0	1	1	0	0
\(f_4\)	0100	\(p (q)\!\)	1	0	1	1	0	0	1	0
\(f_5\)	0101	\((q)\!\)	1	0	1	0	1	0	1	0
\(f_6\)	0110	\((p, q)\!\)	1	0	0	1	0	1	1	0
\(f_7\)	0111	\((p q)\!\)	1	0	0	0	1	1	1	0
\(f_8\)	1000	\(p q\!\)	0	1	1	1	0	0	0	1
\(f_9\)	1001	\(((p, q))\!\)	0	1	1	0	1	0	0	1
\(f_{10}\)	1010	\(q\!\)	0	1	0	1	0	1	0	1
\(f_{11}\)	1011	\((p (q))\!\)	0	1	0	0	1	1	0	1
\(f_{12}\)	1100	\(p\!\)	0	0	1	1	0	0	1	1
\(f_{13}\)	1101	\(((p) q)\!\)	0	0	1	0	1	0	1	1
\(f_{14}\)	1110	\(((p)(q))\!\)	0	0	0	1	0	1	1	1
\(f_{15}\)	1111	\(((~))\)	0	0	0	0	1	1	1	1

Table 4. Relation of Quantifiers to Higher Order Propositions

\(\text{Mnemonic}\)	\(\text{Category}\)	\(\text{Classical Form}\)	\(\text{Alternate Form}\)	\(\text{Symmetric Form}\)	\(\text{Operator}\)
\(\text{E}\!\) \(\text{Exclusive}\)	\(\text{Universal}\) \(\text{Negative}\)	\(\text{All}\ p\ \text{is}\ (q)\)		\(\text{No}\ p\ \text{is}\ q \)	\((\ell_{11})\)
\(\text{A}\!\) \(\text{Absolute}\)	\(\text{Universal}\) \(\text{Affirmative}\)	\(\text{All}\ p\ \text{is}\ q \)		\(\text{No}\ p\ \text{is}\ (q)\)	\((\ell_{10})\)
		\(\text{All}\ q\ \text{is}\ p \)	\(\text{No}\ q\ \text{is}\ (p)\)	\(\text{No}\ (p)\ \text{is}\ q \)	\((\ell_{01})\)
		\(\text{All}\ (q)\ \text{is}\ p \)	\(\text{No}\ (q)\ \text{is}\ (p)\)	\(\text{No}\ (p)\ \text{is}\ (q)\)	\((\ell_{00})\)
		\(\text{Some}\ (p)\ \text{is}\ (q)\)		\(\text{Some}\ (p)\ \text{is}\ (q)\)	\(\ell_{00}\!\)
		\(\text{Some}\ (p)\ \text{is}\ q\)		\(\text{Some}\ (p)\ \text{is}\ q\)	\(\ell_{01}\!\)
\(\text{O}\!\) \(\text{Obtrusive}\)	\(\text{Particular}\) \(\text{Negative}\)	\(\text{Some}\ p\ \text{is}\ (q)\)		\(\text{Some}\ p\ \text{is}\ (q)\)	\(\ell_{10}\!\)
\(\text{I}\!\) \(\text{Indefinite}\)	\(\text{Particular}\) \(\text{Affirmative}\)	\(\text{Some}\ p\ \text{is}\ q\)		\(\text{Some}\ p\ \text{is}\ y\)	\(\ell_{11}\!\)

Exercises

Express the following formulas in functional terms.

Exercise 1

\((\forall x \in X)(p(x) \Rightarrow q(x))\)

\(\prod_{x \in X} (p_x (q_x)) = 1\)

This is just the form \(\operatorname{All}\ p\ \operatorname{are}\ q,\) already covered here:

Application of Higher Order Propositions to Quantification Theory

Need to think a little more about the proposition \(p \Rightarrow q\) as a boolean function of type \(\mathbb{B}^2 \to \mathbb{B}\) and the corresponding higher order proposition of type \((\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}.\)

Exercise 2

\((\forall x \in X)(Px \Rightarrow Qx) \lor (Qx \Rightarrow Px)\)

Exercise 3

\((\forall x \in X)(Px \Rightarrow Qx) \lor (\forall x \in X)(Qx \Rightarrow Px)\)

Inquiry Into Intuitionism

Notes on a discussion with "Gribskoff" (Manuel S. Lourenço) about his artile on IntuitionisticLogic at PlanetMath.