Heyting's intuitionistic propositional calculus

Heyting's axiomatization (1930) of IL

edit
number axiom
I  
II  
III  
IV  
V  
VI  
VII  
VIII  
IX  
X  
XI  

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   Hypothesis
2   Hypothesis
3   Axiom V
4   MP 2, 3
5   Axiom III
6   MP 4, 5
7   Axiom I
8   MP 1, 7
9   MP 8, 6
10   Axiom II
11   MP 9, 10
12   Summary 1, 2; 11

The Deduction Theorem (DT) has not been proven yet so it cannot be used yet. The sequent   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   Axiom V
2   Axiom III
3   MP 1, 2
4   Hypothesis
5   Axiom II
6   MP 4, 5
7   MP 6, 3
8   Axiom II
9   MP 7, 8
10   Axiom VI
11   MP 9, 10
12   Summary 4; 11

The sequent   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

edit

Sketch of proof: Look at Axiom IV; it states

 

Let   so that the consequent is the goal,  . Then the antecedent becomes

 

If   is replaced by  , then the second conjunct becomes

 

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

 

If   is let to become   then this first conjunct will become True. Why?

 

is an instance of Axiom V, and

 

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

 

because (in general)

 

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

Looking at the following sequence of implications

 

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

 

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   Axiom I
2   Axiom V
3   Axiom III
4   MP 2, 3
5   Axiom II
6   Axiom V
7   Axiom III
8   MP 6, 7
9   ANDi (IR) 1, 4
10   Axiom IV
10.1   MP 9, 10
11   ANDi (IR) 10.1, 5
12   Axiom IV
13   MP 11, 12
14   ANDi (IR) 13, 8
15   Axiom IV
16   MP 14, 15
17   Axiom VI
18   ANDi (IR) 16, 17
19   Axiom IV
20   MP 18, 19

Cosliced MP Theorem

edit

The Modus Ponens inference rule states that

 

Now "coslice" the above with an antecedent  :

 

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

 ;

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   Hypothesis
2   Axiom III
3   MP 1, 2
4   Axiom I
5   Axiom IV
6   ANDi (IR) 4, 3
7   MP 6, 5
8   Summary 1; 7


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

 

Here is a proof sketch for it:

 

is assumed as hypothesis. Use Axiom III to derive

 

and continue rightwards:

 
index formula justification
1   Hypothesis
2   Axiom III
3   MP 1, 2
4   Axiom II
5   ANDi (IR) 3, 4
6   Axiom IV
7   MP 5, 6
8   Axiom VI
9   ANDi (IR) 7, 8
10   Axiom IV
11   MP 9, 10
12   Summary 1; 11


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

  
  
 
index formula justification
1   Hypothesis
2   Fold The Telescope Theorem (IR) 1
3   Hypothesis
4   Theorem, on 3
5   Axiom II
6   ANDi (IR) 4, 5
7   Axiom IV
8   MP 6, 7
9   ANDi (IR) 8, 2
10   Axiom IV
11   MP 9, 10
12   Summary 1, 3; 11

Deduction Theorem (DT)

edit

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

 

Given the proof

 

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

 ,

where   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   is an axiom or hypothesis or theorem in the original proof, then

index formula justification
1   Axiom or Hypothesis or Theorem
2   Axiom V
3   MP 1, 2

so   in the derived proof is just as true as the original  .

Now suppose that   is derived by MP from two prior alphas:   and  , and assume as inductive step that both   and   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

 

which in the derived proof becomes

 

From   derive   through the THEN Distribution theorem (proved earlier).

Then

 

is true by Modus Ponens. Then the step

 

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

 

is valid then

 

is also valid.

OK, from the above considerations, given only   as premises (i.e., hypotheses), what can be derived? From these premises may be derived   using Axiom V. Moreover,   may be appended to the list because it is a proven theorem (Reflexivity of Implication). Then, according to the coslice sequent,   may be deduced. To summarize,

 .

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

 .

A special case of this for   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.

 
 
 

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

 
 
 

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

 
 

An example of quoting a three-premise sequent:

index formula justification
1   Original
2   DT on 1
3   DT on 2
4   DT on 3
5   FT on 4
6   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   Hypothesis
2   ANDeL
3   ANDeR
4   MP 1, 2
5   MP 1, 3
6   ANDeL
7   ANDeR
8   MP 5, 6
9   MP 5, 7
10   ANDi
11   MP 4, 10
12   MP 8, 11
13   ANDi
14   MP 12, 13
15   MP 9, 14
16   Summary 1;15
17   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   Hypothesis
2   ANDeL (IR) 1
3   ANDeR (IR) 1
4   ANDeL (IR) 3
5   ANDeR (IR) 3
6   ANDi (IR) 2, 4
7   ANDi (IR) 6, 5
8   Summary 1; 7
9   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   Hypothesis
2   Axiom II
3   MP 1, 2
4   ANDeR
5   MP 3, 4
6   Summary 1; 5
7   DT 6

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


index formula justification
1   Hypothesis
2   ANDeL (IR) 1
3   ANDeR (IR) 1
4   ANDeL (IR) 2
5   ANDeR (IR) 2
6   ANDi (IR) 5, 3
7   ANDi (IR) 4, 6
8   Summary 1; 7
9   DT 8

Since   and  , then the two ways of ANDing twice yield logically equivalent results:

 

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,

 

may be quoted by a single formula:

 .

Remaining axioms

edit

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

 
 .


index formula justification
1   Axiom VII
2   Axiom II
3   ANDi (IR) 1, 2
4   Axiom IV
5   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):

 
 

Axiom V is Axiom THEN introduction Consequent (THENiC):

 

Axiom X is Axiom THEN introduction Antecedent (THENiA):

 

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   THENiC
THEN-2   THENdist
AND-1   ANDeL
AND-2   ANDeR
AND-3   ANDi
OR-1   ORiL
OR-2   ORiR
OR-3   ORiA
NOT-1   THENiA, NOTe
NOT-2   NOTi

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

Now proving in the other direction

edit

Axiom I

edit
index formula justification
1   ANDi
1.1   THENdist
2   MP 1, 1.1
3   Theorem: THEN Reflexive
4   MP 3, 2


Theorem: THEN Reflexive Proof sketch: Use THENdist:

 

and let  :

 

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

 
 

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

index formula justification
1   THENiC
2   THENiC
3   THENdist
4   MP 1, 3
5   MP 2, 4

Axiom II

edit
index formula justification
1   Hypothesis
2   ANDeL
3   ANDeR
4   MP 1, 2
5   MP 1, 3
6   ANDi
7   MP 5, 6
8   MP 4, 7
9   Summary 1; 8
10   DT 9

Axiom III

edit
index formula justification
1   Hypothesis
2   Hypothesis
3   ANDeL
4   ANDeR
5   MP 2, 3
6   MP 2, 4
7   MP 5, 1
8   ANDi
9   MP 7, 8
10   MP 6, 9
11   Summary 1, 2; 10
12   DT 11
13   DT 12

Axiom IV

edit
index formula justification
1   Hypothesis
2   ANDeL
3   ANDeR
4   MP 1, 2
5   MP 1, 3
6   Hypothesis
7   MP 6, 4
8   MP 7, 5
9   Summary 1, 6; 8
10   DT 9
11   DT 10

Axiom V

edit
 

is Axiom THENiC


Axiom VI

edit
index formula justification
1   Hypothesis
2   ANDeL
3   ANDeR
4   MP 1, 2
5   MP 1, 3
6   MP 4, 5
7   Summary 1; 6
8   DT 7

Axiom VII

edit
 

is Axiom ORiL


Axiom VIII

edit
index formula justification
1   ORiR
2   ORiL
3   ORiA
4   MP 1, 3
5   MP 2, 4

Axiom IX

edit
index formula justification
1   Hypothesis
2   ANDeL
3   ANDeR
4   MP 1, 2
5   MP 1, 3
6   ORiA
7   MP 4, 6
8   MP 5, 7
9   Summary 1; 8
10   DT 9

Axiom X

edit
 

is Axiom THENiA

Axiom XI

edit
index formula justification
1   Hypothesis
2   ANDeL
3   ANDeR
4   MP 1, 2
5   MP 1, 3
6   NOTi
7   MP 4, 6
8   MP 5, 7
9   Summary 1; 8
10   DT 9

Conclusion

edit

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:

 .

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:

 .

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

edit