# a property of truth-value semantics for intuitionistic propositional logic

In this entry, we show the following: if $\neg A$ is a tautology of $V_{n}$, then $\neg A$ is a theorem. First, we need the following lemma, which is the intuitionistic version of one for classical propositional logic, found here. Given an interpretation $v$, define

$v[A]\textrm{ is }\left\{\begin{array}[]{ll}\neg A&\textrm{if }v(A)=0,\\ \neg\neg A&\textrm{otherwise.}\end{array}\right.$

It is easy to see that for any $A$, $v(v[A])=n$ for any $v$, so that $v[A]$ is always true. In addition, we have the following table:

$v(A)$ $v[A]$ $v(B)$ $v[B]$ $v(A\land B)$ $v[A\land B]$ $v(A\lor B)$ $v[A\lor B]$ $v(A\to B)$ $v[A\to B]$
$0$ $\neg A$ $0$ $\neg B$ $0$ $\neg(A\land B)$ $0$ $\neg(A\lor B)$ $0$ $\neg\neg(A\to B)$
$0$ $\neg A$ $\neq 0$ $\neg\neg B$ $0$ $\neg(A\land B)$ $\neq 0$ $\neg\neg(A\lor B)$ $n$ $\neg\neg(A\to B)$
$\neq 0$ $\neg\neg A$ $0$ $\neg B$ $0$ $\neg(A\land B)$ $\neq 0$ $\neg\neg(A\lor B)$ $0$ $\neg(A\to B)$
$\neq 0$ $\neg\neg A$ $\neq 0$ $\neg\neg B$ $\neq 0$ $\neg\neg(A\land B)$ $\neq 0$ $\neg\neg(A\lor B)$ $\neq 0$ $\neg\neg(A\to B)$

The proofs of the following lemmas use instances of the theorem schemas below (proofs here):

$1$ $2$ $3$
$(C\to D)\to(\neg D\to\neg C)$ $\neg\neg\neg C\to\neg C$ $C\to\neg\neg C$
###### Lemma 1.

$v[A],v[B]\vdash v[A\land B]$.

###### Proof.

Since $\vdash A\land B\to A$ and $\vdash A\land B\to B$, by modus ponens and instances of the theorem schema 1 above, we have $\vdash\neg A\to\neg(A\land B)$ and $\vdash\neg B\to\neg(A\land B)$. This proves the first three cases.

For the last case, we start with the axiom $A\to(B\to A\land B)$, or $A\vdash B\to A\land B$ by the deduction theorem. Apply modus ponens twice to instances of schema 1, we get $A\vdash\neg\neg B\to\neg\neg(A\land B)$, or $\neg\neg B\vdash A\to\neg\neg(A\land B)$ by the deduction theorem twice. Again, applying modus ponens twice to instances of 1, we have $\neg\neg B\vdash\neg\neg A\to\neg\neg\neg\neg(A\land B)$, or $\neg\neg B,\neg\neg A\vdash\neg\neg\neg\neg(A\land B)$ by the deduction theorem. One application of modus ponens to an instance of schema 2, we have $\neg\neg B,\neg\neg A\vdash\neg\neg(A\land B)$, as desired. ∎

###### Lemma 2.

$v[A],v[B]\vdash v[A\lor B]$.

###### Proof.

Since $\vdash A\to A\lor B$ and $\vdash B\to A\lor B$, by modus ponens twice to instances of the schema 1, we have $\vdash\neg\neg A\to\neg\neg(A\lor B)$ and $\vdash\neg\neg B\to\neg\neg(A\lor B)$. This settles the last three cases.

For the first case, we use the axiom $(A\to\perp)\to((B\to\perp)\to((A\lor B)\to\perp))$, which is just $\neg A\to(\neg B\to\neg(A\lor B))$, or $\neg A,\neg B\vdash\neg(A\lor B)$ by the deduction theorem twice. ∎

###### Lemma 3.

$v[A],v[B]\vdash v[A\to B]$.

###### Proof.

For the first two, all we need is $\neg A\vdash\neg\neg(A\to B)$. To see this, we have deduction

$A\to\perp,A,\perp,\perp\to B,B,$

so $\neg A,A\vdash B$, or $\neg A\vdash A\to B$ by the deduction theorem. Since $(A\to B)\to\neg\neg(A\to B)$ is an instance of schema 3, by modus ponens, $\neg A\vdash\neg\neg(A\to B)$ as desired.

For the third, by the deduction theorem, it is enough to show $\neg\neg A,\neg B,A\to B\vdash\perp$. Now,

$\neg A\to\perp,\neg B,A\to B,(A\to B)\to(\neg B\to\neg A),\neg B\to\neg A,\neg A,\perp$

is a deduction of $\perp$ from $\neg\neg A,\neg B$, and $A\to B$, where $(A\to B)\to(\neg B\to\neg A)$ is a theorem.

For the last, all we need to show is $\neg\neg B\vdash\neg\neg(A\to B)$. We start with $B\to(A\to B)$, which is an axiom. Applying modus ponens twice to instances of 1, we have $\vdash\neg\neg B\to\neg\neg(A\to B)$, or $\neg\neg B\vdash\neg\neg(A\to B)$. ∎

###### Lemma 4.

Suppose $p_{1},\ldots,p_{n}$ are all the propositional variables in a wff $A$. Then

$v[p_{1}],\ldots,v[p_{m}]\vdash v[A].$
###### Proof.

We use induction on the number $n$ of primitive logical connectives ($\land,\lor$, and $\to$) in $A$. If $n=0$, then $A$ is either $\perp$ or a propositional variable $p$. If $A$ is $\perp$, then $\perp\vdash\perp$, or $\vdash\neg\perp$, or $\vdash v[\perp]$. If $A$ is $p$, then clearly $v[p]\vdash v[p]$. Now, if $A$ has $n+1$ connectives, and is either $B\land C$, $B\lor C$, or $B\to C$, then $B$ and $C$ has no more than $n$ connectives. By induction,

$v[p_{{i(1)}}],\ldots,v[p_{{i(s)}}]\vdash v[B]\qquad\mbox{and}\qquad v[p_{{j(1)% }}],\ldots,v[p_{{j(t)}}]\vdash v[C]$

or

$v[p_{1}],\ldots,v[p_{m}]\vdash v[B]\qquad\mbox{and}\qquad v[p_{1}],\ldots,v[p_% {m}]\vdash v[C]$

By the first three lemmas above, $v[B],v[C]\vdash v[A]$, so by modus ponens twice,

$v[p_{1}],\ldots,v[p_{m}]\vdash v[A].$

∎

We are now ready for the main result:

###### Theorem 1.

If $A$ is a tautology of $V_{n}$, then $\vdash\neg\neg A$.

###### Proof.

Let $v$ be any interpretation, then $v[p_{1}],\ldots,v[p_{m}]\vdash v[A]$ by the last lemma, where $p_{1},\ldots,p_{m}$ are all the propositional variables in $A$. Since $A$ is a tautology,

$v[p_{1}],\ldots,v[p_{m}]\vdash\neg\neg A.$

If $m=0$, then we are done. Otherwise, let $v_{1}$ and $v_{2}$ be two interpretations such that $v_{1}[p_{i}]=v_{2}[p_{i}]$ for $i=1,\ldots,m-1$, and $v_{1}[p_{m}]=\neg p_{m}$ and $v_{2}[p_{m}]=\neg\neg p_{m}$, so that

$v[p_{1}],\ldots,v[p_{{m-1}}],\neg p_{m}\vdash\neg\neg A\qquad\mbox{and}\qquad v% [p_{1}],\ldots,v[p_{{m-1}}],\neg\neg p_{m}\vdash\neg\neg A.$

By applying the deduction theorem twice to each of the above deductive relations, we get

$v[p_{1}],\ldots,v[p_{{m-1}}],\neg A\vdash\neg\neg p_{m}\qquad\mbox{and}\qquad v% [p_{1}],\ldots,v[p_{{m-1}}],\neg A\vdash\neg\neg\neg p_{m}.$

Apply schema 2 to the second deductive relation above, we get

$v[p_{1}],\ldots,v[p_{{m-1}}],\neg A\vdash\neg p_{m}.$

By the deduction theorem once more, we have

$v[p_{1}],\ldots,v[p_{{m-1}}]\vdash\neg A\to\neg\neg p_{m}\qquad\mbox{and}% \qquad v[p_{1}],\ldots,v[p_{{m-1}}]\vdash\neg A\to\neg p_{m}.$

With the axiom instance $(\neg A\to\neg p_{m})\to((\neg A\to\neg\neg p_{m})\to\neg\neg A)$, apply modus ponens to each of the last two deductive relations, we get

$v[p_{1}],\ldots,v[p_{{m-1}}]\vdash\neg\neg A,$

so that $v[p_{m}]$ is removed from the original deductive relation. Continue this process until all of the $v[p_{i}]$ are removed on the left, and we get

$\vdash\neg\neg A.$

∎

We record to immediate corollaries:

###### Corollary 1.

If $\neg A$ is a tautology of $V_{n}$, then $\vdash\neg A$.

###### Proof.

By the theorem, $\vdash\neg\neg\neg A$. But $\vdash\neg\neg\neg A\to\neg A$, $\vdash\neg A$ by modus ponens. ∎

In the next corollary, we use $\vdash_{c}A$ and $\vdash_{i}$ to distinguish that $A$ is a theorem of classical and intuitionistic propositional logic respectively.

###### Corollary 2.

(Glivenko’s Theorem) $\vdash_{c}A$ iff $\vdash_{i}\neg\neg A$.

###### Proof.

If $\vdash_{c}A$, then by the soundness theorem of classical propositional logic, $A$ is a tautology of truth-value semantics, which is just $V_{2}$, and therefore by the theorem above, $\vdash_{i}\neg\neg A$.

Conversely, if $\vdash_{i}\neg\neg A$, then certainly $\vdash_{c}\neg\neg A$, as PL${}_{i}$ is a subsystem of PL${}_{c}$. Since $\neg\neg A\to A$ is a theorem of PL${}_{c}$, we get $\vdash_{c}A$ by modus ponens. ∎

In particular, $\vdash_{c}\perp$ iff $\vdash_{i}\perp$, since $\vdash_{i}\neg\neg\perp\leftrightarrow\perp$. In other words, PL${}_{c}$ is consistent iff PL${}_{i}$ is.

Major Section:
Reference
Type of Math Object:
Result

## Mathematics Subject Classification

03B20 Subsystems of classical logic (including intuitionistic logic)

## Recent Activity

May 17
new image: sinx_approx.png by jeremyboden
new image: approximation_to_sinx by jeremyboden
new image: approximation_to_sinx by jeremyboden
new question: Solving the word problem for isomorphic groups by mairiwalker
new image: LineDiagrams.jpg by m759
new image: ProjPoints.jpg by m759
new image: AbstrExample3.jpg by m759
new image: four-diamond_figure.jpg by m759
May 16
new problem: Curve fitting using the Exchange Algorithm. by jeremyboden
new question: Undirected graphs and their Chromatic Number by Serchinnho

## Info

Owner: CWoo
Added: 2012-06-24 - 02:57
Author(s): CWoo

## Versions

(v16) by CWoo 2013-03-22
Powered By: = + + ♡
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 185, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "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": false}, "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.8800755739212036, "perplexity_flag": "head"}