Heyting's intuitionistic propositional calculus

Heyting's axiomatization (1930) of IL

number	axiom
I	$p\to p\wedge p$
II	$p\wedge q\to q\wedge p$
III	$(p\to q)\to (p\wedge r\to q\wedge r)$
IV	$((p\to q)\wedge (q\to r))\to (p\to r)$
V	$q\to (p\to q)$
VI	$p\wedge (p\to q)\to q$
VII	$p\to p\vee q$
VIII	$p\vee q\to q\vee p$
IX	$((p\to r)\wedge (q\to r))\to ((p\vee q)\to r)$
X	$\mathrm{\neg }p\to (p\to q)$
XI	$((p\to q)\wedge (p\to \mathrm{\neg }q))\to \mathrm{\neg }p$

The above axiomatization does not have the expected rules of AND introduction and elimination, which are very convenient to work with, so derive those first.

index	formula	justification
1	$p$	Hypothesis
2	$q$	Hypothesis
3	$q\to (p\to q)$	Axiom V
4	$p\to q$	MP 2, 3
5	$(p\to q)\to (p\wedge p\to q\wedge p)$	Axiom III
6	$p\wedge p\to q\wedge p$	MP 4, 5
7	$p\to p\wedge p$	Axiom I
8	$p\wedge p$	MP 1, 7
9	$q\wedge p$	MP 8, 6
10	$q\wedge p\to p\wedge q$	Axiom II
11	$p\wedge q$	MP 9, 10
12	$p,q⊢p\wedge q$	Summary 1, 2; 11

The Deduction Theorem (DT) has not been proven yet so it cannot be used yet. The sequent $p,q⊢p\wedge q$ may be applied like an inference rule, which may be called "ANDi (IR)", which is short for "AND introduction (Inference Rule)". The turnstile symbol, $⊢$, may be read as "proves" or "therefore".

index	formula	justification
1	$q\to (p\to q)$	Axiom V
2	$[q\to (p\to q)]\to [q\wedge p\to (p\to q)\wedge p]$	Axiom III
3	$q\wedge p\to (p\to q)\wedge p$	MP 1, 2
4	$p\wedge q$	Hypothesis
5	$p\wedge q\to q\wedge p$	Axiom II
6	$q\wedge p$	MP 4, 5
7	$(p\to q)\wedge p$	MP 6, 3
8	$(p\to q)\wedge p\to p\wedge (p\to q)$	Axiom II
9	$p\wedge (p\to q)$	MP 7, 8
10	$(p\wedge (p\to q))\to q$	Axiom VI
11	$q$	MP 9, 10
12	$p\wedge q⊢q$	Summary 4; 11

The sequent $p\wedge q⊢q$ may be applied like an inference rule, which may be called "ANDeR (IR)", which is short for "AND elimination Right (Inference Rule)".

Reflexivity of Implication

Sketch of proof: Look at Axiom IV; it states

$((p\to q)\wedge (q\to r))\to (p\to r)$

Let $r=p$ so that the consequent is the goal, $p\to p$. Then the antecedent becomes

$(p\to q)\wedge (q\to p)$

If $q$ is replaced by $q\wedge (q\to p)$, then the second conjunct becomes

$[q\wedge (q\to p)\to p]$

which is Axiom VI and therefore True. Note that $q$ may still be replaced by any formula and this second conjunct will remain True. Now looking at the first conjunct, it is

$p\to [q\wedge (q\to p)]$

If $q$ is let to become $p\to p$ then this first conjunct will become True. Why?

$p\to (p\to p)$

is an instance of Axiom V, and

$p\to ((p\to p)\to p)$

is also an instance of Axiom V. These two instances together should imply that

$p\to ((p\to p)\wedge ((p\to p)\to p))$

because (in general)

$\alpha \to \beta ,\alpha \to \gamma {⊢}_{IL}\alpha \to \beta \wedge \gamma$

although this has to be proven (either separately or somehow included as part of the proof).

Looking at the following sequence of implications

$p\underset{I}{\overset{}{\to }}(p\wedge p)\underset{V,III}{\overset{}{\to }}((q\to p)\wedge p)\underset{II}{\overset{}{\to }}(p\wedge (q\to p))\underset{V,III}{\overset{}{\to }}((p\to p)\wedge (q\to p))$

where $\alpha \to \beta \to \gamma$ is interpreted neither as $\alpha \to (\beta \to \gamma )$ nor as $(\alpha \to \beta )\to \gamma$ but as a separate pair of implications: $\alpha \to \beta$ and $\beta \to \gamma$ from which shall be derived $\alpha \to \gamma$ (by "THEN Composition" so to say, which is actually Transitivity of Implication, Axiom IV). The sequence of THEN Compositions shall yield

$p\to [(p\to p)\wedge (q\to p)]$

which is the subgoal which makes the first conjunct True. Having proven both conjuncts True, use ANDi as an inference rule to introduce their conjunction. Then invoke Axiom IV.

index	formula	justification
1	$p\to p\wedge p$	Axiom I
2	$p\to ((p\to p)\to p)$	Axiom V
3	$[p\to ((p\to p)\to p)]\to [p\wedge p\to ((p\to p)\to p)\wedge p]$	Axiom III
4	$p\wedge p\to ((p\to p)\to p)\wedge p$	MP 2, 3
5	$((p\to p)\to p)\wedge p\to p\wedge ((p\to p)\to p)$	Axiom II
6	$p\to (p\to p)$	Axiom V
7	$[p\to (p\to p)]\to [p\wedge ((p\to p)\to p)\to (p\to p)\wedge ((p\to p)\to p)]$	Axiom III
8	$p\wedge ((p\to p)\to p)\to (p\to p)\wedge ((p\to p)\to p)$	MP 6, 7
9	$[p\to p\wedge p]\wedge [p\wedge p\to ((p\to p)\to p)\wedge p]$	ANDi (IR) 1, 4
10	$[p\to p\wedge p]\wedge [p\wedge p\to ((p\to p)\to p)\wedge p]\to [p\to ((p\to p)\to p)\wedge p]$	Axiom IV
10.1	$p\to ((p\to p)\to p)\wedge p$	MP 9, 10
11	$[p\to ((p\to p)\to p)\wedge p]\wedge [((p\to p)\to p)\wedge p\to p\wedge ((p\to p)\to p)]$	ANDi (IR) 10.1, 5
12	$[p\to ((p\to p)\to p)\wedge p]\wedge [((p\to p)\to p)\wedge p\to p\wedge ((p\to p)\to p)]\to [p\to p\wedge ((p\to p)\to p)]$	Axiom IV
13	$p\to p\wedge ((p\to p)\to p)$	MP 11, 12
14	$[p\to p\wedge ((p\to p)\to p)]\wedge [p\wedge ((p\to p)\to p)\to \{(p\to p)\wedge ((p\to p)\to p)\}]$	ANDi (IR) 13, 8
15	$[p\to p\wedge ((p\to p)\to p)]\wedge [p\wedge ((p\to p)\to p)\to (p\to p)\wedge ((p\to p)\to p)]\to [p\to (p\to p)\wedge ((p\to p)\to p)]$	Axiom IV
16	$p\to \{(p\to p)\wedge ((p\to p)\to p)\}$	MP 14, 15
17	$(p\to p)\wedge ((p\to p)\to p)\to p$	Axiom VI
18	$[p\to \{(p\to p)\wedge ((p\to p)\to p)\}]\wedge [\{(p\to p)\wedge ((p\to p)\to p)\}\to p]$	ANDi (IR) 16, 17
19	$[p\to \{(p\to p)\wedge ((p\to p)\to p)\}]\wedge [\{(p\to p)\wedge ((p\to p)\to p)\}\to p]\to (p\to p)$	Axiom IV
20	$p\to p$	MP 18, 19

Cosliced MP Theorem

The Modus Ponens inference rule states that

$q,q\to r⊢r$

Now "coslice" the above with an antecedent $p$:

$p\to (q\to r),p\to q⊢p\to r$

where "coslice" comes from an analogy with category theory. Applying DT twice to this would yield the Axiom of THEN Self-Distribution:

$(p\to (q\to r))\to ((p\to q)\to (p\to r))$;

however, we do not have DT available yet. In fact, the Cosliced MP Theorem is a lemma that is necessary for proving DT.

Here is a preliminary lemma:

index	formula	justification
1	$p\to q$	Hypothesis
2	$(p\to q)\to (p\wedge p\to q\wedge p)$	Axiom III
3	$p\wedge p\to q\wedge p$	MP 1, 2
4	$p\to p\wedge p$	Axiom I
5	$(p\to p\wedge p)\wedge (p\wedge p\to q\wedge p)\to (p\to q\wedge p)$	Axiom IV
6	$(p\to p\wedge p)\wedge (p\wedge p\to q\wedge p)$	ANDi (IR) 4, 3
7	$p\to q\wedge p$	MP 6, 5
8	$p\to q⊢p\to q\wedge p$	Summary 1; 7

Another lemma, which might be called the "Fold The Telescope" Theorem:

$p\to (q\to r)⊢p\wedge q\to r$

Here is a proof sketch for it:

$p\to (q\to r)$

is assumed as hypothesis. Use Axiom III to derive

$p\wedge q\to (q\to r)\wedge q$

and continue rightwards:

$p\wedge q\to (q\to r)\wedge q\underset{II}{\overset{}{\to }}q\wedge (q\to r)\underset{VI}{\overset{}{\to }}r$

index	formula	justification
1	$p\to (q\to r)$	Hypothesis
2	$[p\to (q\to r)]\to [p\wedge q\to (q\to r)\wedge q]$	Axiom III
3	$p\wedge q\to (q\to r)\wedge q$	MP 1, 2
4	$(q\to r)\wedge q\to q\wedge (q\to r)$	Axiom II
5	$[p\wedge q\to (q\to r)\wedge q]\wedge [(q\to r)\wedge q\to q\wedge (q\to r)]$	ANDi (IR) 3, 4
6	$[p\wedge q\to (q\to r)\wedge q]\wedge [(q\to r)\wedge q\to q\wedge (q\to r)]\to [p\wedge q\to q\wedge (q\to r)]$	Axiom IV
7	$p\wedge q\to q\wedge (q\to r)$	MP 5, 6
8	$(q\wedge (q\to r))\to r$	Axiom VI
9	$[p\wedge q\to q\wedge (q\to r)]\wedge [(q\wedge (q\to r))\to r]$	ANDi (IR) 7, 8
10	$[p\wedge q\to q\wedge (q\to r)]\wedge [(q\wedge (q\to r))\to r]\to [p\wedge q\to r]$	Axiom IV
11	$p\wedge q\to r$	MP 9, 10
12	$p\to (q\to r)⊢p\wedge q\to r$	Summary 1; 11

Now for the Cosliced MP. Brief sketch of the proof:

$p\to (q\to r)$ ∴ $p\wedge q\to r$

$p\to q$ ∴ $p\to q\wedge p$

$p\to q\wedge p\underset{II}{\overset{}{\to }}p\wedge q\to r$

index	formula	justification
1	$p\to (q\to r)$	Hypothesis
2	$p\wedge q\to r$	Fold The Telescope Theorem (IR) 1
3	$p\to q$	Hypothesis
4	$p\to q\wedge p$	Theorem, on 3
5	$q\wedge p\to p\wedge q$	Axiom II
6	$[p\to q\wedge p]\wedge [q\wedge p\to p\wedge q]$	ANDi (IR) 4, 5
7	$[p\to q\wedge p]\wedge [q\wedge p\to p\wedge q]\to [p\to p\wedge q]$	Axiom IV
8	$p\to p\wedge q$	MP 6, 7
9	$(p\to p\wedge q)\wedge (p\wedge q\to r)$	ANDi (IR) 8, 2
10	$(p\to p\wedge q)\wedge (p\wedge q\to r)\to (p\to r)$	Axiom IV
11	$p\to r$	MP 9, 10
12	$p\to (q\to r),p\to q⊢p\to r$	Summary 1, 3; 11

Deduction Theorem (DT)

The Deduction Theorem is a metatheorem, which may be applied as an inference rule, is analogous to currying, and may be stated thus:

$\frac{{\gamma }_1,{\gamma }_2,...,{\gamma }_m⊢\beta }{{\gamma }_1,{\gamma }_2,...,{\gamma }_{m-1}⊢{\gamma }_m\to \beta }$

Given the proof

${\alpha }_1,{\alpha }_2,...,{\alpha }_{n-1},{\alpha }_n=\beta$

where each ${\alpha }_i$ is either a hypothesis, or an axiom, or a theorem (proved elsewhere), or is proved by MP from two previous ${\alpha }_j$'s —but $\beta$ is required to be proved by MP from two previous $\alpha$'s— the following modification of it may be deduced:

${\alpha }_k\to {\alpha }_1,{\alpha }_k\to {\alpha }_2,...,{\alpha }_k\to {\alpha }_k,...,{\alpha }_k\to {\alpha }_n$,

where ${\alpha }_k$ is the last hypothesis in the sequence.

This modification might be here called "coslicing" of a proof (by way of analogy with coslice categories).

(By the way, what is the difference between a sequent and a proof? A sequent is a sort of abstracted summary of a proof, which includes only hypotheses to the left of the turnstile and a conclusion to the right of it. It does not include the intermediate steps of the proof; the proof includes hypotheses, the conclusion, but also any axioms and theorems and intermediate derived formulas.)

How to prove that the derived proof is as valid as the original? If ${\alpha }_i$ is an axiom or hypothesis or theorem in the original proof, then

index	formula	justification
1	${\alpha }_i$	Axiom or Hypothesis or Theorem
2	${\alpha }_i\to ({\alpha }_k\to {\alpha }_i)$	Axiom V
3	∴ ${\alpha }_n\to {\alpha }_i$	MP 1, 2

so ${\alpha }_k\to {\alpha }_i$ in the derived proof is just as true as the original ${\alpha }_i$.

Now suppose that ${\alpha }_j$ is derived by MP from two prior alphas: ${\alpha }_i$ and ${\alpha }_i\to {\alpha }_j$, and assume as inductive step that both ${\alpha }_i$ and ${\alpha }_i\to {\alpha }_j$ have been shown to be true already. (Axioms and theorems are valid —necessarily true, so to say— and hypotheses are assumed to be true.) Then

${\alpha }_i,{\alpha }_i\to {\alpha }_j⊢{\alpha }_j$

which in the derived proof becomes

${\alpha }_k\to {\alpha }_i,{\alpha }_k\to ({\alpha }_i\to {\alpha }_j)\stackrel{?}{⊢}{\alpha }_k\to {\alpha }_j$

From ${\alpha }_k\to ({\alpha }_i\to {\alpha }_j)$ derive $({\alpha }_k\to {\alpha }_i)\to ({\alpha }_k\to {\alpha }_j)$ through the THEN Distribution theorem (proved earlier).

Then

${\alpha }_k\to {\alpha }_i,({\alpha }_k\to {\alpha }_i)\to ({\alpha }_k\to {\alpha }_j)⊢{\alpha }_k\to {\alpha }_j$

is true by Modus Ponens. Then the step

${\alpha }_k\to {\alpha }_i,{\alpha }_k\to ({\alpha }_i\to {\alpha }_j)\stackrel{\sqrt{}}{⊢}{\alpha }_k\to {\alpha }_j$

in the derived proof is valid.

Thus, the cosliced proof remains as valid as the original proof. By abstracting/summarizing proofs into sequents, a similar result holds for sequents: i.e., if a sequent is valid then the coslice of that sequent is valid; i.e., if

${\gamma }_1,{\gamma }_2,...,{\gamma }_m⊢\beta$

is valid then

${\gamma }_m\to {\gamma }_1,{\gamma }_m\to {\gamma }_2,...,{\gamma }_m\to {\gamma }_m⊢{\gamma }_m\to \beta$

is also valid.

OK, from the above considerations, given only ${\gamma }_1{\gamma }_2,...,{\gamma }_{m-1}$ as premises (i.e., hypotheses), what can be derived? From these premises may be derived ${\gamma }_m\to {\gamma }_1,{\gamma }_m\to {\gamma }_2,...,{\gamma }_m\to {\gamma }_{m-1}$ using Axiom V. Moreover, ${\gamma }_m\to {\gamma }_m$ may be appended to the list because it is a proven theorem (Reflexivity of Implication). Then, according to the coslice sequent, ${\gamma }_m\to \beta$ may be deduced. To summarize,

${\gamma }_1,{\gamma }_2,...,{\gamma }_{m-1}⊢{\gamma }_m\to \beta$.

A formula which may be derived by "quoting" DT is

$(({\gamma }_1\wedge {\gamma }_2\wedge ...\wedge {\gamma }_m)\to \beta )\to (({\gamma }_1\wedge {\gamma }_2\wedge ...\wedge {\gamma }_{m-1})\to ({\gamma }_m\to \beta ))$.

A special case of this for $m=2$ is the Unfold The Telescope Theorem.

"Quoting" involves changing each comma before the turnstile of a sequent to an AND, and the turnstile itself to THEN (→). Intuitionistic sequents have only one formula after the turnstile. Axiom VI is the "quoted" form of Modus Ponens.

The reverse process might be called "unquoting"; DT may be run in reverse. (The proof of this is a lot easier; just apply MP one time.) As an analogy, actors "unquote" a written play (or screenplay) when they act it out. A stenographer "quotes" the proceedings in a courtroom. What DT does is help to quote. The Fold/Unfold Telescope theorems help with quoting as well.

Applying DT twice to the Cosliced MP rule yields the Axiom of THEN Self-Distribution.

$p\to (q\to r),p\to q⊢p\to r$

$p\to (q\to r)⊢(p\to q)\to (p\to r)$

$⊢(p\to (q\to r))\to ((p\to q)\to (p\to r))$

Applying DT twice to ANDi (IR) yields Axiom ANDi:

$p,q⊢p\wedge q$

$p⊢q\to p\wedge q$

$⊢p\to (q\to p\wedge q)$

Also, applying DT to the ANDeR (IR) yields Axiom ANDeR:

$p\wedge q⊢q$

$⊢p\wedge q\to q$

An example of quoting a three-premise sequent:

index	formula	justification
1	$\alpha ,\beta ,\gamma ⊢\delta$	Original
2	$\alpha ,\beta ⊢\gamma \to \delta$	DT on 1
3	$\alpha ⊢\beta \to (\gamma \to \delta )$	DT on 2
4	$⊢\alpha \to (\beta \to (\gamma \to \delta ))$	DT on 3
5	$⊢\alpha \wedge \beta \to (\gamma \to \delta )$	FT on 4
6	$⊢(\alpha \wedge \beta )\wedge \gamma \to \delta$	FT on 5

FT is shorthand for "Fold the Telescope". Now prove that AND is associative in order to be able to remove the parentheses around the conjunction of alpha and beta.

index	formula	justification
1	$\alpha \wedge (\beta \wedge \gamma )$	Hypothesis
2	$\alpha \wedge (\beta \wedge \gamma )\to \alpha$	ANDeL
3	$\alpha \wedge (\beta \wedge \gamma )\to (\beta \wedge \gamma )$	ANDeR
4	$\alpha$	MP 1, 2
5	$\beta \wedge \gamma$	MP 1, 3
6	$\beta \wedge \gamma \to \beta$	ANDeL
7	$\beta \wedge \gamma \to \gamma$	ANDeR
8	$\beta$	MP 5, 6
9	$\gamma$	MP 5, 7
10	$\alpha \to (\beta \to \alpha \wedge \beta )$	ANDi
11	$\beta \to (\alpha \wedge \beta )$	MP 4, 10
12	$\alpha \wedge \beta$	MP 8, 11
13	$\alpha \wedge \beta \to (\gamma \to (\alpha \wedge \beta )\wedge \gamma )$	ANDi
14	$\gamma \to (\alpha \wedge \beta )\wedge \gamma$	MP 12, 13
15	$(\alpha \wedge \beta )\wedge \gamma$	MP 9, 14
16	$\alpha \wedge (\beta \wedge \gamma )⊢(\alpha \wedge \beta )\wedge \gamma$	Summary 1;15
17	$⊢\alpha \wedge (\beta \wedge \gamma )\to (\alpha \wedge \beta )\wedge \gamma$	DT 16

Now prove the same thing but using the Inference Rule versions of ANDeL and ANDeR, in order to compare the two proofs.

index	formula	justification
1	$\alpha \wedge (\beta \wedge \gamma )$	Hypothesis
2	$\alpha$	ANDeL (IR) 1
3	$\beta \wedge \gamma$	ANDeR (IR) 1
4	$\beta$	ANDeL (IR) 3
5	$\gamma$	ANDeR (IR) 3
6	$\alpha \wedge \beta$	ANDi (IR) 2, 4
7	$(\alpha \wedge \beta )\wedge \gamma$	ANDi (IR) 6, 5
8	$\alpha \wedge (\beta \wedge \gamma )⊢(\alpha \wedge \beta )\wedge \gamma$	Summary 1; 7
9	$⊢\alpha \wedge (\beta \wedge \gamma )\to (\alpha \wedge \beta )\wedge \gamma$	DT 8

Using ANDeL (IR) and ANDeR (IR) inference rules alongside MP helps save almost half of the steps. This latter proof is more Natural Deduction-like. ANDeL has not been proven yet, though.

index	formula	justification
1	$p\wedge q$	Hypothesis
2	$p\wedge q\to q\wedge p$	Axiom II
3	$q\wedge p$	MP 1, 2
4	$q\wedge p\to p$	ANDeR
5	$p$	MP 3, 4
6	$p\wedge q⊢p$	Summary 1; 5
7	$⊢p\wedge q\to p$	DT 6

The sequent in line 6 gives the inference rule form of the theorem.

index	formula	justification
1	$(\alpha \wedge \beta )\wedge \gamma$	Hypothesis
2	$\alpha \wedge \beta$	ANDeL (IR) 1
3	$\gamma$	ANDeR (IR) 1
4	$\alpha$	ANDeL (IR) 2
5	$\beta$	ANDeR (IR) 2
6	$\beta \wedge \gamma$	ANDi (IR) 5, 3
7	$\alpha \wedge (\beta \wedge \gamma )$	ANDi (IR) 4, 6
8	$(\alpha \wedge \beta )\wedge \gamma ⊢\alpha \wedge (\beta \wedge \gamma )$	Summary 1; 7
9	$⊢(\alpha \wedge \beta )\wedge \gamma \to \alpha \wedge (\beta \wedge \gamma )$	DT 8

Since $\alpha \wedge (\beta \wedge \gamma )\to (\alpha \wedge \beta )\wedge \gamma$ and $(\alpha \wedge \beta )\wedge \gamma \to \alpha \wedge (\beta \wedge \gamma )$, then the two ways of ANDing twice yield logically equivalent results:

$\alpha \wedge (\beta \wedge \gamma )\leftrightarrow (\alpha \wedge \beta )\wedge \gamma$

so that the parentheses may be removed altogether; the three conjuncts form an "AND association", so to say, where all associates treat each other equally.

Then, the sequent containing four formulas,

$\alpha ,\beta ,\gamma ⊢\delta$

may be quoted by a single formula:

$\alpha \wedge \beta \wedge \gamma \to \delta$.

Remaining axioms

Applying the Unfold The Telescope theorem to Axiom IX yields Axiom OR introduction Antecedent (ORiA):

$((p\to r)\wedge (q\to r))\to ((p\vee q)\to r)$

∴ $(p\to r)\to ((q\to r)\to (p\vee q\to r))$.

index	formula	justification
1	$q\to q\vee p$	Axiom VII
2	$q\vee p\to p\vee q$	Axiom II
3	$(q\to q\vee p)\wedge (q\vee p\to p\vee q)$	ANDi (IR) 1, 2
4	$((q\to q\vee p)\wedge (q\vee p\to p\vee q))\to (q\to p\vee q)$	Axiom IV
5	$q\to p\vee q$	MP 3, 4

This is Axiom OR introduction Right (ORiR).

Applying the Unfold The Telescope theorem to Axiom XI yields Axiom NOT introduction (or Reductio Ad Absurdum):

$((p\to q)\wedge (p\to \mathrm{\neg }q))\to \mathrm{\neg }p$

∴ $(p\to q)\to ((p\to \mathrm{\neg }q)\to \mathrm{\neg }p)$

Axiom V is Axiom THEN introduction Consequent (THENiC):

$p\to (q\to p)$

Axiom X is Axiom THEN introduction Antecedent (THENiA):

$\mathrm{\neg }p\to (p\to q)$

That proves all of the axioms of Intuitionistic Propositional Calculus mentioned in Wikipedia's Propositional calculus article (abbreviate it as just IPC):

label	axiom	alternative label
THEN-1	$p\to (q\to p)$	THENiC
THEN-2	$(p\to (q\to r))\to ((p\to q)\to (p\to r))$	THENdist
AND-1	$p\wedge q\to p$	ANDeL
AND-2	$p\wedge q\to q$	ANDeR
AND-3	$p\to (q\to p\wedge q)$	ANDi
OR-1	$p\to p\vee q$	ORiL
OR-2	$q\to p\vee q$	ORiR
OR-3	$(p\to r)\to ((q\to r)\to (p\vee q\to r))$	ORiA
NOT-1	$\mathrm{\neg }p\to (p\to q)$	THENiA, NOTe
NOT-2	$(p\to q)\to ((p\to \mathrm{\neg }q)\to \mathrm{\neg }p)$	NOTi

This means that Heyting's IPC contains Wikipedia's IPC.

Now proving in the other direction

Axiom I

index	formula	justification
1	$p\to (p\to p\wedge p)$	ANDi
1.1	$[p\to (p\to p\wedge p)]\to [(p\to p)\to (p\to p\wedge p)]$	THENdist
2	$(p\to p)\to (p\to p\wedge p)$	MP 1, 1.1
3	$p\to p$	Theorem: THEN Reflexive
4	$p\to (p\wedge p)$	MP 3, 2

Theorem: THEN Reflexive Proof sketch: Use THENdist:

$(p\to (q\to r))\to ((p\to q)\to (p\to r))$

and let $r=p$:

$(p\to (q\to p))\to ((p\to q)\to (p\to p))$

This should yield the desired conclusion if the two antecedents are satisfied:

$p\to (q\to p)$

$p\to q$

The first antecedent is Axiom THENiC so it will be true for any formula that is substituted for $q$. The second antecedent will become true if $q$ gets replaced by $p\to p$ (although $q\to p$ could also work), in which case the second antecedent will also be an instance of Axiom THENiC.

index	formula	justification
1	$p\to ((p\to p)\to p)$	THENiC
2	$p\to (p\to p)$	THENiC
3	$[p\to ((p\to p)\to p)]\to [p\to (p\to p)]\to (p\to p)$	THENdist
4	$(p\to (p\to p))\to (p\to p)$	MP 1, 3
5	$p\to p$	MP 2, 4

Axiom II

index	formula	justification
1	$p\wedge q$	Hypothesis
2	$p\wedge q\to p$	ANDeL
3	$p\wedge q\to q$	ANDeR
4	$p$	MP 1, 2
5	$q$	MP 1, 3
6	$q\to (p\to q\wedge p)$	ANDi
7	$p\to q\wedge p$	MP 5, 6
8	$q\wedge p$	MP 4, 7
9	$p\wedge q⊢q\wedge p$	Summary 1; 8
10	$⊢p\wedge q\to q\wedge p$	DT 9

Axiom III

index	formula	justification
1	$p\to q$	Hypothesis
2	$p\wedge r$	Hypothesis
3	$p\wedge r\to p$	ANDeL
4	$p\wedge r\to r$	ANDeR
5	$p$	MP 2, 3
6	$r$	MP 2, 4
7	$q$	MP 5, 1
8	$q\to (r\to q\wedge r)$	ANDi
9	$r\to q\wedge r$	MP 7, 8
10	$q\wedge r$	MP 6, 9
11	$p\to q,p\wedge r⊢q\wedge r$	Summary 1, 2; 10
12	$p\to q⊢p\wedge r\to q\wedge r$	DT 11
13	$⊢(p\to q)\to (p\wedge r\to q\wedge r)$	DT 12

Axiom IV

index	formula	justification
1	$(p\to q)\wedge (q\to r)$	Hypothesis
2	$((p\to q)\wedge (q\to r))\to (p\to q)$	ANDeL
3	$((p\to q)\wedge (q\to r))\to (q\to r)$	ANDeR
4	$p\to q$	MP 1, 2
5	$q\to r$	MP 1, 3
6	$p$	Hypothesis
7	$q$	MP 6, 4
8	$r$	MP 7, 5
9	$(p\to q)\wedge (q\to r),p⊢r$	Summary 1, 6; 8
10	$(p\to q)\wedge (q\to r)⊢p\to r$	DT 9
11	$⊢((p\to q)\wedge (q\to r))\to (p\to r)$	DT 10

Axiom V

$q\to (p\to q)$

is Axiom THENiC

Axiom VI

index	formula	justification
1	$p\wedge (p\to q)$	Hypothesis
2	$p\wedge (p\to q)\to p$	ANDeL
3	$p\wedge (p\to q)\to (p\to q)$	ANDeR
4	$p$	MP 1, 2
5	$p\to q$	MP 1, 3
6	$q$	MP 4, 5
7	$p\wedge (p\to q)⊢q$	Summary 1; 6
8	$⊢(p\wedge (p\to q))\to q$	DT 7

Axiom VII

$p\to p\vee q$

is Axiom ORiL

Axiom VIII

index	formula	justification
1	$p\to q\vee p$	ORiR
2	$q\to q\vee p$	ORiL
3	$(p\to q\vee p)\to ((q\to q\vee p)\to (p\vee q\to q\vee p))$	ORiA
4	$(q\to q\vee p)\to (p\vee q\to q\vee p)$	MP 1, 3
5	$p\vee q\to q\vee p$	MP 2, 4

Axiom IX

index	formula	justification
1	$(p\to r)\wedge (q\to r)$	Hypothesis
2	$((p\to r)\wedge (q\to r))\to (p\to r)$	ANDeL
3	$((p\to r)\wedge (q\to r))\to (q\to r)$	ANDeR
4	$p\to r$	MP 1, 2
5	$q\to r$	MP 1, 3
6	$(p\to r)\to ((q\to r)\to (p\vee q\to r))$	ORiA
7	$(q\to r)\to (p\vee q\to r)$	MP 4, 6
8	$p\vee q\to r$	MP 5, 7
9	$(p\to r)\wedge (q\to r)⊢(p\vee q)\to r$	Summary 1; 8
10	$⊢((p\to r)\wedge (q\to r))\to (p\vee q\to r)$	DT 9

Axiom X

$\mathrm{\neg }p\to (p\to q)$

is Axiom THENiA

Axiom XI

index	formula	justification
1	$(p\to q)\wedge (p\to \mathrm{\neg }q)$	Hypothesis
2	$((p\to q)\wedge (p\to \mathrm{\neg }q))\to (p\to q)$	ANDeL
3	$((p\to q)\wedge (p\to \mathrm{\neg }q))\to (p\to \mathrm{\neg }q)$	ANDeR
4	$p\to q$	MP 1, 2
5	$p\to \mathrm{\neg }q$	MP 1, 3
6	$(p\to q)\to ((p\to \mathrm{\neg }q)\to \mathrm{\neg }p)$	NOTi
7	$(p\to \mathrm{\neg }q)\to \mathrm{\neg }p$	MP 4, 6
8	$\mathrm{\neg }p$	MP 5, 7
9	$(p\to q)\wedge (p\to \mathrm{\neg }q)⊢\mathrm{\neg }p$	Summary 1; 8
10	$⊢((p\to q)\wedge (p\to \mathrm{\neg }q))\to \mathrm{\neg }p$	DT 9

Conclusion

The axioms of HPC (Heyting's propositional calculus) can all be proved using the Hilbert-style axioms IPC (as set out in Wikipedia's propositional calculus article). Then since any formula of HPC can be proved through its axioms, then applying transitivity, any formula of HPC may be proved through IPC; therefore IPC contains HPC:

$IPC\supset HPC$.

Earlier was proved the converse, i.e., that the HPC axioms prove the IPC axioms. So any formula provable through the IPC axioms can be proved through the HPC axioms (due to transitivity of implication, or composition of implication, so to say). Thus, the theory of HPC contains the theory of IPC:

$HPC\supset IPC$.

Since the two theories (sets of theorems) contain each other, then it follows by the Schröder–Bernstein Theorem that the two theories are equal.

References

• Chapter 3 : Algebras for Logic, §3.1.3 by Template:W