PFPL Chapter 12 Constructive Logic

Posted on 2019-03-17 In PFPL Note 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:

$ϕ prop$ , stating $ϕ$ expresses a proposition.
$ϕ true$ , stating $ϕ $ 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 $ϕ$ expresses an unsolved problem, such as $P \overset{?}{=} 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 $ϕ prop$ and $ϕ true$ are rarely of interest by themselves, but rather in a context of a hypothetical judgment of the form $ϕ_{1} true, \dots, ϕ_{n} true ⊢ ϕ true$ . The judgment says proposition $ϕ$ is true (with proof) under the assumptions that $ϕ_{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
$\frac{}{Γ, ϕ true ⊢ ϕ true} \frac{Γ ⊢ ϕ_{1} true Γ, ϕ_{1} true ⊢ ϕ_{2} true}{Γ ⊢ ϕ_{2} true} \frac{Γ ⊢ ϕ_{2} true}{Γ, ϕ_{1} true ⊢ ϕ_{2} true}$
Two more rules are required in that we regard $Γ$ as a set of hypotheses, so that two “copies” are as good as one, and the order doesn’t matter
$\frac{Γ, ϕ_{1} true, ϕ_{1} true ⊢ ϕ_{2} true}{Γ, ϕ_{1} true ⊢ ϕ_{2} true} \frac{Γ_{1}, ϕ_{1} true, ϕ_{2} true, Γ_{2} ⊢ ϕ true}{Γ_{1}, ϕ_{2} true, ϕ_{1} true, Γ_{2} ⊢ ϕ true}$

Provability

The syntax table of constructive logic is
$\begin{aligned} Prop & τ & ::= & ⊤ & ⊤ & truth \\ ⊥ & ⊥ & falsity \\ \lor (ϕ_{1}; ϕ_{2}) & ϕ_{1} \lor ϕ_{2} & disjunction \\ \land (ϕ_{1}; ϕ_{2}) & ϕ_{1} \land ϕ_{2} & conjunction \\ \supset (ϕ_{1}; ϕ_{2}) & ϕ_{1} \supset ϕ_{2} & implication \end{aligned}$
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.
$\frac{}{Γ ⊢ ⊤ true}$

Thus there is no elimination form only introduction form.

Conjunction

$\frac{Γ ⊢ ϕ_{1} true Γ ⊢ ϕ_{2} true}{Γ ⊢ ϕ_{1} \land ϕ_{2} true} \frac{Γ ⊢ ϕ_{1} \land ϕ_{2} true}{Γ ⊢ ϕ_{1} true} \frac{Γ ⊢ ϕ_{1} \land ϕ_{2} true}{Γ ⊢ ϕ_{2} true}$

Implication

$\frac{Γ, ϕ_{1} true ⊢ ϕ_{2} true}{Γ ⊢ ϕ_{1} \supset ϕ_{2} true} \frac{Γ ⊢ ϕ_{1} \supset ϕ_{2} true Γ ⊢ ϕ_{1} true}{Γ ⊢ ϕ_{2} true}$

Falsehood

Falsehood expresses the trivially false (refutable) proposition.

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

$\frac{Γ ⊢ ⊥ true}{Γ ⊢ ϕ true}$

Disjunction

$\frac{Γ ⊢ ϕ_{1} true}{Γ ⊢ ϕ_{1} \lor ϕ_{2} true} \frac{Γ ⊢ ϕ_{2} true}{Γ ⊢ ϕ_{1} \lor ϕ_{2} true} \frac{Γ ⊢ ϕ_{1} \lor ϕ_{2} true Γ, ϕ_{1} true ⊢ ϕ true Γ, ϕ_{2} true ⊢ ϕ true}{Γ ⊢ ϕ true}$

Negnation

$\neg ϕ$ is defined as $ϕ \supset ⊥$ . As a result, $\neg ϕ true$ if $ϕ true ⊢ ⊥ true$ , which is to say that the truth of $ϕ$ is refutable.

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

A problem $ϕ$ 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 $ϕ true$ , which states that $ϕ$ has a proof, is replaced by judgment $p : ϕ$ , stating $p$ is a proof for $ϕ$ .

The hypothetical judgment form is changed into form $x_{1} : ϕ_{1}, \dots, x_{n} : ϕ_{n} ⊢ p : ϕ$ . ( $x_{i}$ stands for presumed, but unknown, proofs.)

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

The syntax table for proof terms is
$\begin{aligned} Prf p & ::= & true-I & ⟨ ⟩ & truth intro \\ and-I (p_{1}; p_{2}) & ⟨ p_{1}, p_{2} ⟩ & conj. intro \\ and-E [l] (p) & p \cdot l & conj. elim \\ and-E [r] (p) & p \cdot r & conj. elim \\ imp-I (x . p) & λ (x) p & impl. intro \\ imp-E (p_{1}; p_{2}) & p_{1} (p_{2}) & impl. elim \\ false-E (p) & abort (p) & false elim \\ or-I [l] (p) & l \cdot p & disj. intro \\ or-I [r] (p) & r \cdot p & disj. intro \\ or-E (p; x_{1} . p_{1}; x_{2} . p_{2}) & case p {l \cdot x_{1} ↪ p_{1} ∣ r \cdot x_{2} ↪ p_{2}} & disj. elim \end{aligned}$
The rules of constructive propositional logic can be restated with proof terms

Truth

$\frac{}{Γ ⊢ ⟨ ⟩ : ⊤}$

Conjunction

$\frac{Γ ⊢ p_{1} : ϕ_{1} Γ ⊢ p_{2} : ϕ_{2}}{Γ ⊢ ⟨ p_{1}, p_{2} ⟩ : ϕ_{1} \land ϕ_{2}} \frac{Γ ⊢ p_{1} : ϕ_{1} \land ϕ_{2}}{Γ ⊢ p_{1} \cdot l : ϕ_{1}} \frac{Γ ⊢ p_{1} : ϕ_{1} \land ϕ_{2}}{Γ ⊢ p_{1} \cdot r : ϕ_{2}}$

Implication

$\frac{Γ, x : ϕ_{1} ⊢ p_{2} : ϕ_{2}}{Γ ⊢ λ (x) p_{2} : ϕ_{1} \supset ϕ_{1}} \frac{Γ ⊢ p : ϕ_{1} \supset ϕ_{2} Γ ⊢ p_{1} : ϕ_{1}}{Γ ⊢ p (p_{1}) : ϕ_{2}}$

Falsehood

$\frac{Γ ⊢ p : ⊥}{Γ ⊢ abort (p) : ϕ}$

Disjunction

$\frac{Γ ⊢ p_{1} : ϕ_{1}}{Γ ⊢ l \cdot p_{1} : ϕ_{1} \lor ϕ_{2}} \frac{Γ ⊢ p_{2} : ϕ_{2}}{Γ ⊢ r \cdot p_{2} : ϕ_{1} \lor ϕ_{2}} \frac{Γ ⊢ p : ϕ_{1} \lor ϕ_{2} Γ, x_{1} : ϕ_{1} ⊢ p_{1} : ϕ Γ, x_{2} : ϕ_{2} ⊢ p_{2} : ϕ}{Γ ⊢ case p {l \cdot x_{1} ↪ p_{1} ∣ r \cdot x_{2} ↪ p_{2}} : ϕ}$

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

$\frac{Γ ⊢ p_{1} : ϕ_{1} Γ ⊢ p_{2} : ϕ_{2}}{Γ ⊢ ⟨ p_{1}, p_{2} ⟩ \cdot l \equiv p_{1} : ϕ_{1}} \frac{Γ ⊢ p_{1} : ϕ_{1} Γ ⊢ p_{2} : ϕ_{2}}{Γ ⊢ ⟨ p_{1}, p_{2} ⟩ \cdot r \equiv p_{2} : ϕ_{2}} \frac{Γ ⊢ p \cdot l : ϕ_{1} Γ ⊢ p \cdot r : ϕ_{2}}{Γ ⊢ ⟨ p \cdot l, p \cdot r ⟩ \equiv p : ϕ_{1} \land ϕ_{2}}$

Implication

$\frac{Γ, x : ϕ_{1} ⊢ p_{2} : ϕ_{2} Γ ⊢ p_{1} : ϕ_{1}}{Γ ⊢ (λ (x) p_{2}) (p_{1}) \equiv [p_{1} / x] p_{2} : ϕ_{2}} \frac{Γ ⊢ p : ϕ_{1} \supset ϕ_{2}}{Γ ⊢ λ (x) (p (x)) \equiv p : ϕ_{1} \supset ϕ_{2}}$

Disjunction

$\frac{Γ ⊢ p : ϕ_{1} \lor ϕ_{2} Γ, x_{1} : ϕ_{1} ⊢ p_{1} : ψ Γ, x_{2} : ϕ_{2} ⊢ p_{2} : ψ}{Γ ⊢ case l \cdot p {l \cdot x_{1} ↪ p_{1} ∣ r \cdot x_{2} ↪ p_{2}} \equiv [p / x_{1}] p_{1} : ψ} \frac{Γ ⊢ p : ϕ_{1} \lor ϕ_{2} Γ, x_{1} : ϕ_{1} ⊢ p_{1} : ψ Γ, x_{2} : ϕ_{2} ⊢ p_{2} : ψ}{Γ ⊢ case r \cdot p {l \cdot x_{1} ↪ p_{1} ∣ r \cdot x_{2} ↪ p_{2}} \equiv [p / x_{2}] p_{2} : ψ} \frac{Γ ⊢ p : ϕ_{1} \lor ϕ_{2} Γ, x : ϕ_{1} \lor ϕ_{2} ⊢ q : ψ}{Γ ⊢ [p / x] q \equiv case p {l \cdot x_{1} ↪ [l \cdot x_{1} / x] q ∣ r \cdot x_{2} ↪ [r \cdot x_{2} / x] q} : ψ}$

Falsehood

$\frac{Γ ⊢ p : ⊥ Γ, x : ⊥ ⊢ q : ψ}{Γ ⊢ [p / x] q \equiv abort (p) : ψ}$

Propositions as Types

$\begin{aligned} Prop & Type \\ ⊤ & unit \\ ⊥ & void \\ ϕ_{1} \land ϕ_{2} & τ_{1} \times τ_{2} \\ ϕ_{1} \lor ϕ_{2} & τ_{1} + τ_{2} \\ ϕ_{1} \supset ϕ_{2} & τ_{1} \to τ_{2} \end{aligned}$

Exercise

Law of the Excluded Middle

For $\neg \neg (ϕ \lor \neg ϕ) true$ , we can assume that $\neg (ϕ \lor \neg ϕ) true$ and derive contradiction. Then we need to prove $ϕ \lor \neg ϕ$ .

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

For $ϕ \lor \neg ϕ$ , 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 $((τ + (τ \to void)) \to void) \to void$ .

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

Double Negation Elimination

Suppose LEM holds universally, $\forall ϕ$ and assume $\neg \neg ϕ true$ , trying to derive $ϕ true$ .

By LEM, $\neg ϕ \lor ϕ true$ . If $ϕ true$ then goal reached. If $\neg ϕ true$ , we need to derive contradiction for that.

By previous problem, we can derive proof term as $λ (y) {case LEM}_{ϕ} {l \cdot y_{1} ↪ y_{1} ∣ r \cdot y_{2} ↪ case y_{2} (y) {}}$ .

General Heyting Algebra Distributivity

Consider the equivalence $ϕ \land (ψ_{1} \lor ψ_{2}) \equiv (ϕ \land ψ_{1}) \lor (ϕ \land ψ_{2}) $ .

Let $λ$ stands for left-hand side, $ρ$ for right-hand side.

Assume the equivalence is achieved. Then we can see that $ρ \leq ϕ $ and $ρ \leq ψ_{1} \lor ψ_{2} $ .

The former and latter ones are immediate, which are trivial. Thus $ρ \leq λ$ .

If we want to show $ρ \geq λ $ , we can show $ϕ \leq ρ^{ψ_{1} \lor ψ_{2}} $ . By exponential feature, $ϕ \leq ρ^{ψ_{1}} $ and $ϕ \leq ρ^{ψ_{2}} $ .

This only shows that $ϕ \land ψ_{1} \leq ρ $ and $ϕ \land ψ_{2} \leq ρ $ . Thus it is proved.

For $ϕ \lor (ψ_{1} \land ψ_{2}) \equiv (ϕ \lor ψ_{1}) \land (ϕ \lor ψ_{2}) $ , we still apply similar methods. Let $λ $ for lhs and $ρ $ for rhs.

On $ρ \leq λ $ , one can easily see that $ϕ \lor ψ_{1} \leq λ $ and $ϕ \lor ψ_{2} \leq λ $ . The rest is trivial.

On $λ \leq ρ $ , $ρ \leq ϕ \lor ψ_{1} $ and $ρ \leq ϕ \lor ψ_{2} $ . By transitive, the rest is trivial.

Boolean/Heyting Algebra De Morgen

One can see that $ϕ \supset ϕ$ in Boolean algebra as $(\neg ϕ) \lor ϕ$ . 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 $ψ$ as $\neg ϕ$ . Then only Boolean Algebra can ensure negation is always the complement of the negated.