PFPL Chapter 12 Constructive Logic

Posted on In Disqus:

This part is not shown on PFPL preview version.

What is Constructive Logic

Constructive logic codifies the principles of mathematical reasoning as it is actually practiced.

In mathematics, a proposition is judged true exactly when it has a proof, and false exactly when refutation occurs. Since there’re always, and will always be, unsolved problems, we can’t expect in general a proposition be either true or false.

Constructive Semantics

Constructive logic is concerned with 2 judgments:

  • $\phi\text{ prop}$, stating $\phi$ expresses a proposition.
  • $\phi \text{ true}$, stating $\phi​$ is a true proposition.

What distinguishes constructive from non-constructive logic is that proposition is not conceived of merely a truth value, but instead as a problem statement whose solution, if it has one, is given by a proof.

Truth with Proof

Identifying truth with proof has some consequences. One cannot say that a proposition is either true or false. There exists a chaos state indicating there’s no proof for it.

In this sense, constructive logic is a logic of positive, or affirmative, information. One must have explicit evidence in the form of a proof or refutation to prove the truth or falsity of the proposition.

Decidable or Undecidable

It’s clear that not every proposition is either true or false. If $\phi$ expresses an unsolved problem, such as $\text{P} \stackrel{?}{=} \text{NP}$, since we have no proof nor refutation for it. Such problem is undecidable, precisely because it hasn’t been solved.

My Personal Fav

The constructive attitude is simply to accept the situation as inevitable, and make out peace with that.

When faced with a problem, we have no choice but to roll up our sleeves and try to prove it or refute it. There is not guarantee of success! Life is hard, but we muddle though somehow.

Constructive Logic

Judgments $\phi \text{ prop}$ and $\phi \text{ true}$ are rarely of interest by themselves, but rather in a context of a hypothetical judgment of the form $\phi_1\text{ true},\dots,\phi_n\text{ true}\vdash \phi\text{ true}$. The judgment says proposition $\phi$ is true (with proof) under the assumptions that $\phi_i$ are true (with proofs).

The structural properties of the hypothetical judgment, when specialized to constructive logic, define what we mean by reasoning under hypotheses
$$
\dfrac{}{\Gamma,\phi\text{ true}\vdash \phi\text{ true}}\\
\dfrac{\Gamma \vdash \phi_1 \text{ true}\phantom{“”}\Gamma,\phi_1\text{ true}\vdash \phi_2\text{ true}}{\Gamma \vdash \phi_2\text{ true}}\\
\dfrac{\Gamma \vdash \phi_2\text{ true}}{\Gamma,\phi_1\text{ true}\vdash \phi_2\text{ true}}
$$
Two more rules are required in that we regard $\Gamma$ as a set of hypotheses, so that two “copies” are as good as one, and the order doesn’t matter
$$
\dfrac{\Gamma,\phi_1\text{ true},\phi_1\text{ true}\vdash\phi_2\text{ true}}{\Gamma,\phi_1\text{ true}\vdash \phi_2\text{ true}}\\
\dfrac{\Gamma_1,\phi_1\text{ true},\phi_2\text{ true},\Gamma_2\vdash\phi\text{ true}}{\Gamma_1,\phi_2\text{ true},\phi_1\text{ true},\Gamma_2\vdash\phi\text{ true}}
$$

Provability

The syntax table of constructive logic is
$$
\begin{align}
\text{Prop}&&\tau&&::=&&\top&&\top&&\text{truth}\\
&&&&&&\bot&&\bot&&\text{falsity}\\
&&&&&&\vee(\phi_1;\phi_2)&&\phi_1\vee\phi_2&&\text{disjunction}\\
&&&&&&\wedge(\phi_1;\phi_2)&&\phi_1\wedge\phi_2&&\text{conjunction}\\
&&&&&&\supset(\phi_1;\phi_2)&&\phi_1\supset\phi_2&&\text{implication}
\end{align}
$$
The connectives of propositional logic are given meaning by rules that define

  • what constitutes a “direct” proof of propositional formed form that connective
  • how to exploit existence of such proof in an “indirect” proof of another proposition.

These are called introduction and elimination rules for the connectives.

The principle of conservation of proof states that these rules are inverse to one another: the elimination cannot extract more information than information we put it by introduction rule, and vise versa.

Truth

Truth proposition is trivially true, no information goes into proving it, no information can be obtained from it.
$$
\dfrac{}{\Gamma \vdash \top \text{ true}}
$$

Thus there is no elimination form only introduction form.

Conjunction

$$
\dfrac{\Gamma \vdash \phi_1 \text{ true}\phantom{“”}\Gamma \vdash \phi_2\text{ true}}{\Gamma \vdash \phi_1 \wedge \phi_2\text{ true}}\\
\dfrac{\Gamma \vdash \phi_1 \wedge \phi_2 \text{ true}}{\Gamma \vdash \phi_1\text{ true}}\\
\dfrac{\Gamma \vdash \phi_1 \wedge \phi_2 \text{ true}}{\Gamma \vdash \phi_2\text{ true}}\\
$$

Implication

$$
\dfrac{\Gamma,\phi_1\text{ true}\vdash \phi_2\text{ true}}{\Gamma \vdash \phi_1\supset\phi_2\text{ true}}\\
\dfrac{\Gamma \vdash \phi_1\supset\phi_2\text{ true}\phantom{“”}\Gamma \vdash \phi_1\text{ true}}{\Gamma \vdash \phi_2\text{ true}}
$$

Falsehood

Falsehood expresses the trivially false (refutable) proposition.

Thus there is no introduction form since no judgment supports falsehood, only elimination form.

$$
\dfrac{\Gamma \vdash \bot \text{ true}}{\Gamma \vdash \phi\text{ true}}
$$

Disjunction

$$
\dfrac{\Gamma \vdash \phi_1 \text{ true}}{\Gamma \vdash \phi_1 \vee \phi_2 \text{ true}}\\
\dfrac{\Gamma \vdash \phi_2 \text{ true}}{\Gamma \vdash \phi_1 \vee \phi_2 \text{ true}}\\
\dfrac{\Gamma \vdash \phi_1 \vee \phi_2 \text{ true}\phantom{“”}\Gamma,\phi_1\text{ true}\vdash \phi\text{ true}\phantom{“”}\Gamma,\phi_2\text{ true}\vdash \phi\text{ true}}{\Gamma \vdash \phi\text{ true}}
$$

Negnation

$\neg \phi$ is defined as $\phi \supset \bot$. As a result, $\neg \phi\text{ true}$ if $\phi\text{ true}\vdash \bot \text{ true}$, which is to say that the truth of $\phi$ is refutable.

Since constructive truth is defined to be the existence of proof, the implied semantics of negation is strong.

A problem $\phi$ is open exactly when neither affirm it or refute it. In contrast, classical conception of tuth assigns a fixed truth value to each proposition.

Proof Terms

The key to propositions-as-types principles is to make explicit the forms of proof.

Basic judgment $\phi\text{ true}$, which states that $\phi$ has a proof, is replaced by judgment $p:\phi$, stating $p$ is a proof for $\phi$.

The hypothetical judgment form is changed into form $x_1:\phi_1,\dots,x_n:\phi_n\vdash p:\phi$. ($x_i$ stands for presumed, but unknown, proofs.)

We again let $\Gamma​$ range over such hypothesis lists, subject to the restriction that no variable occurs more than once.

The syntax table for proof terms is
$$
\begin{align}
\text{Prf }p&&::=&&\text{true-I}&&\langle \rangle&&\text{truth intro}\\
&&&&\text{and-I}(p_1;p_2)&&\langle p_1,p_2 \rangle&&\text{conj. intro}\\
&&&&\text{and-E}\lbrack l\rbrack(p)&&p\cdot l&&\text{conj. elim}\\
&&&&\text{and-E}\lbrack r\rbrack(p)&&p\cdot r&&\text{conj. elim}\\
&&&&\text{imp-I}(x.p)&&\lambda(x)p&&\text{impl. intro}\\
&&&&\text{imp-E}(p_1;p_2)&&p_1(p_2)&&\text{impl. elim}\\
&&&&\text{false-E}(p)&&\text{abort}(p)&&\text{false elim}\\
&&&&\text{or-I}\lbrack l\rbrack(p)&&l\cdot p&&\text{disj. intro}\\
&&&&\text{or-I}\lbrack r\rbrack(p)&&r\cdot p&&\text{disj. intro}\\
&&&&\text{or-E}(p;x_1.p_1;x_2.p_2)&&\text{case }p\lbrace l\cdot x_1\hookrightarrow p_1 \shortmid r\cdot x_2\hookrightarrow p_2\rbrace &&\text{disj. elim}
\end{align}
$$
The rules of constructive propositional logic can be restated with proof terms

Truth

$$
\dfrac{}{\Gamma \vdash \langle \rangle :\top}
$$

Conjunction

$$
\dfrac{\Gamma \vdash p_1:\phi_1\phantom{“”}\Gamma \vdash p_2:\phi_2}{\Gamma \vdash \langle p_1,p_2\rangle :\phi_1 \wedge \phi_2}\\
\dfrac{\Gamma \vdash p_1 :\phi_1 \wedge \phi_2}{\Gamma \vdash p_1\cdot l:\phi_1}\\
\dfrac{\Gamma \vdash p_1 :\phi_1 \wedge \phi_2}{\Gamma \vdash p_1\cdot r:\phi_2}
$$

Implication

$$
\dfrac{\Gamma,x:\phi_1 \vdash p_2:\phi_2}{\Gamma \vdash \lambda(x)p_2:\phi_1\supset \phi_1}\\
\dfrac{\Gamma \vdash p:\phi_1\supset \phi_2\phantom{“”}\Gamma \vdash p_1 :\phi_1}{\Gamma \vdash p(p_1):\phi_2}
$$

Falsehood

$$
\dfrac{\Gamma \vdash p:\bot}{\Gamma \vdash \text{abort}(p):\phi}
$$

Disjunction

$$
\dfrac{\Gamma \vdash p_1:\phi_1}{\Gamma \vdash l\cdot p_1 :\phi_1 \vee \phi_2}\\
\dfrac{\Gamma \vdash p_2:\phi_2}{\Gamma \vdash r\cdot p_2 :\phi_1 \vee \phi_2}\\
\dfrac{\Gamma \vdash p:\phi_1 \vee \phi_2\phantom{“”}\Gamma,x_1:\phi_1\vdash p_1:\phi\phantom{“”}\Gamma,x_2:\phi_2\vdash p_2:\phi}{\Gamma \vdash \text{case }p\lbrace l\cdot x_1\hookrightarrow p_1 \shortmid r\cdot x_2\hookrightarrow p_2\rbrace :\phi}
$$

Proof Dynamics

Proof terms in constructive logic are given a dynamics by Gentzen’s Principle, stating that elimination forms are inverse to the introduction forms.

One aspect of Gentzen’s Principle is the principle of conservation of proof.

Conjunction

$$
\dfrac{\Gamma \vdash p_1:\phi_1\phantom{“”}\Gamma\vdash p_2:\phi_2}{\Gamma \vdash \langle p_1,p_2\rangle\cdot l\equiv p_1:\phi_1}\\
\dfrac{\Gamma \vdash p_1:\phi_1\phantom{“”}\Gamma\vdash p_2:\phi_2}{\Gamma \vdash \langle p_1,p_2\rangle\cdot r\equiv p_2:\phi_2}\\
\dfrac{\Gamma \vdash p\cdot l:\phi_1\phantom{“”}\Gamma \vdash p\cdot r:\phi_2}{\Gamma \vdash \langle p\cdot l,p\cdot r \rangle \equiv p:\phi_1\wedge\phi_2}
$$

Implication

$$
\dfrac{\Gamma,x:\phi_1\vdash p_2:\phi_2\phantom{“”}\Gamma\vdash p_1:\phi_1}{\Gamma \vdash (\lambda(x)p_2)(p_1)\equiv \lbrack p_1/x \rbrack p_2:\phi_2}\\
\dfrac{\Gamma\vdash p:\phi_1\supset\phi_2}{\Gamma \vdash \lambda(x)(p(x))\equiv p:\phi_1\supset\phi_2}
$$

Disjunction

$$
\dfrac{\Gamma\vdash p:\phi_1\vee\phi_2\phantom{“”}\Gamma,x_1:\phi_1\vdash p_1:\psi\phantom{“”}\Gamma,x_2:\phi_2\vdash p_2:\psi}{\Gamma \vdash \text{case }l\cdot p \lbrace l\cdot x_1\hookrightarrow p_1 \shortmid r\cdot x_2\hookrightarrow p_2\rbrace \equiv \lbrack p/x_1\rbrack p_1:\psi}\\
\dfrac{\Gamma\vdash p:\phi_1\vee\phi_2\phantom{“”}\Gamma,x_1:\phi_1\vdash p_1:\psi\phantom{“”}\Gamma,x_2:\phi_2\vdash p_2:\psi}{\Gamma \vdash \text{case }r\cdot p \lbrace l\cdot x_1\hookrightarrow p_1 \shortmid r\cdot x_2\hookrightarrow p_2\rbrace \equiv \lbrack p/x_2\rbrack p_2:\psi}\\
\dfrac{\Gamma \vdash p:\phi_1\vee\phi_2\phantom{“”}\Gamma,x:\phi_1\vee\phi_2\vdash q:\psi}{\Gamma\vdash\lbrack p/x \rbrack q\equiv \text{case } p \lbrace l\cdot x_1\hookrightarrow \lbrack l\cdot x_1/x \rbrack q \shortmid r\cdot x_2\hookrightarrow \lbrack r\cdot x_2/x \rbrack q\rbrace:\psi}
$$

Falsehood

$$
\dfrac{\Gamma\vdash p:\bot\phantom{“”}\Gamma,x:\bot\vdash q:\psi}{\Gamma\vdash\lbrack p/x \rbrack q\equiv\text{abort}(p):\psi}
$$

Propositions as Types

$$
\begin{align}
\text{Prop}&&\text{Type}\\
\top&&\text{unit}\\
\bot&&\text{void}\\
\phi_1\wedge\phi_2&&\tau_1 \times \tau_2\\
\phi_1\vee\phi_2&&\tau_1+\tau_2\\
\phi_1\supset\phi_2&&\tau_1\to\tau_2
\end{align}
$$

Exercise

Law of the Excluded Middle

For $\neg\neg (\phi\vee\neg\phi)\text{ true}$, we can assume that $\neg(\phi\vee\neg\phi)\text{ true}$ and derive contradiction. Then we need to prove $\phi\vee\neg\phi$.

Plausible: LEM cannot be expected to hold for a general $\phi$.

For $\phi \vee \neg\phi$, it suffices to prove one of its disjuncts. The following steps seems to be trivial.

Formally, we can see that the type of the proposition is $((\tau+(\tau\to\text{void}))\to\text{void})\to\text{void}$.

Thus we can construct proof term as $\lambda(x) x(r\cdot \lambda(y)x(l\cdot y))$.

Double Negation Elimination

Suppose LEM holds universally, $\forall \phi$ and assume $\neg\neg \phi\text{ true}$, trying to derive $\phi\text{ true}$.

By LEM, $\neg\phi\vee \phi\text{ true}$. If $\phi\text{ true}$ then goal reached. If $\neg \phi \text{ true}$, we need to derive contradiction for that.

By previous problem, we can derive proof term as $\lambda(y)\text{ case LEM}_\phi \lbrace l\cdot y_1 \hookrightarrow y_1 \shortmid r \cdot y_2 \hookrightarrow \text{case }y_2(y)\lbrace \rbrace \rbrace$.

General Heyting Algebra Distributivity

Consider the equivalence $\phi \wedge (\psi_1\vee \psi_2)\equiv (\phi \wedge \psi_1) \vee(\phi \wedge\psi_2)​$.

Let $\lambda$ stands for left-hand side, $\rho$ for right-hand side.

Assume the equivalence is achieved. Then we can see that $\rho \le \phi​$ and $\rho \le \psi_1 \vee \psi_2​$.

The former and latter ones are immediate, which are trivial. Thus $\rho \le \lambda$.

If we want to show $\rho \geq \lambda​$, we can show $\phi \leq \rho ^{\psi_1\vee \psi_2}​$. By exponential feature, $\phi \le \rho^{\psi_1}​$ and $\phi \leq \rho^{\psi_2}​$.

This only shows that $\phi \wedge\psi_1 \le \rho​$ and $\phi \wedge\psi_2\le\rho​$. Thus it is proved.

For $\phi \vee (\psi_1 \wedge\psi_2) \equiv (\phi \vee\psi_1) \wedge (\phi\vee\psi_2)​$, we still apply similar methods. Let $\lambda​$ for lhs and $\rho​$ for rhs.

On $\rho \leq \lambda​$, one can easily see that $\phi \vee \psi_1 \le \lambda​$ and $\phi \vee \psi_2 \le \lambda​$. The rest is trivial.

On $\lambda \le \rho​$, $\rho \le \phi\vee\psi_1​$ and $\rho \le \phi \vee \psi_2​$. By transitive, the rest is trivial.

Boolean/Heyting Algebra De Morgen

One can see that $\phi \supset \phi$ in Boolean algebra as $(\neg \phi) \vee \phi$. Then it is consistent to adjoin LEM to constructive logic.

According to definition, the first de Morgan duality law can be proved by any Heyting Algebra.

The second one might encounter the case $\psi$ as $\neg \phi$. Then only Boolean Algebra can ensure negation is always the complement of the negated.