CHAPTER 12

Gentzen Proof System for Intuitionistic Logic

In 1935 G.Gentzen formulated a first syntactically decidable formalization for

classical and intuitionistic logic and proved its equivalence with the Heyting’s
original Hilbert style formalization (the famous Gentzen’s Hauptsatz). We
present here the original version of his work and discuss his original proof of the
Hauptsatz Theorem. We deal here, as it has happened historically, with proof
theoretical formalizations of the intuitionistic logic only. It means we present
here the intuitionistic logic as a proof system only, as it was done in the original
papers and leave the model theoretic investigations for later.

1 LI - The Gentzen Sequent Calculus

The proof system LI was published by Gentzen in 1935 as a particular case of

his proof system LK for the classical logic. We have already discussed a version
of the original Gentzen’s system LK in the previous chapter ??, so we present
here the proof system LI first and then we show how it can be extended to the
original Gentzen system LK.

Language of LI

Let SEQ = { Γ −→ ∆ : Γ, ∆ ∈ F ∗ } be the set of all Gentzen sequents built

out of the formulas of the language

L = L{∪,∩,⇒,¬}

and the additional symbol −→.

In the intuitionistic logic we deal only with sequents of the form Γ −→ ∆,

where ∆ consists of at most one formula. I.e. we assume that all sequents are
elements of a following subset IS of the set SEQ of all sequents.

IS = {Γ −→ ∆ : ∆ consists of at most one f ormula}. (1)

The set IS is called the set of all intuitionistic sequents.

Axioms of LI

As the axioms of LI we adopt any sequent from the set IS defined by ( 1),
which contains a formula that appears on both sides of the sequent arrow −→,

1
i.e any sequent of the form

Γ1 , A, Γ2 −→ A, (2)

for any formula A ∈ F and any sequences Γ1 , Γ2 ∈ F ∗ .

Inference rules of LI

The set inference rules is divided into two groups: the structural rules and the
logical rules. They are defined as follows.

Structural Rules of LI

Weakening

Γ −→
(→ weak) .
Γ −→ A

A is called the weakening formula.

Contraction

A, A, Γ −→ ∆
(contr →) ,
A, Γ −→ ∆
A is called the contraction formula , ∆ contains at most one formula.

Exchange

Γ1 , A, B, Γ2 −→ ∆
(exchange →) ,
Γ1 , B, A, Γ2 −→ ∆

∆ contains at most one formula.

Logical Rules of LI

Conjunction rules

A, B, Γ −→ ∆ Γ −→ A ; Γ −→ B
(∩ →) , (→ ∩) ,
(A ∩ B), Γ −→ ∆ Γ −→ (A ∩ B)

∆ contains at most one formula.

Disjunction rules

Γ −→ A Γ −→ B
(→ ∪)1 , (→ ∪)2 ,
Γ −→ (A ∪ B) Γ −→ (A ∪ B)

2
 A, Γ −→ ∆ ; B, Γ −→ ∆
(∪ →) ,
(A ∪ B), Γ −→ ∆

∆ contains at most one formula.

Implication rules

A, Γ −→ B Γ −→ A ; B, Γ −→ ∆
(→⇒) , (⇒→) ,
Γ −→ (A ⇒ B) (A ⇒ B), Γ −→ ∆

∆ contains at most one formula.

Negation rules

Γ −→ A A, Γ −→
(¬ →) , (→ ¬) .
¬A, Γ −→ Γ −→ ¬A

Formally we define:

LI = (L, IS, AX, Structural rules, Logical rules}),

where IS is defined by (1), Structural rules and Logical rules are the inference
rules defined above, and AX is the axiom of the system defined by the schema
(2).

We write
`LI Γ −→ ∆
to denote that the sequent Γ −→ ∆ has a proof in LI.

We say that a formula A ∈ F has a proof in LI and write it as

`LI A

when the sequent −→ A has a proof in LI, i.e.

`LI A if and only if `LI −→ A.

2 Decomposition Trees in LI

Search for proofs in LI is a much more complicated process then the one in
classical logic systems RS or GL.

3
Here, as in any other Gentzen style proof system, proof search procedure consists
of building the decomposition trees.

In RS the decomposition tree TA of any formula A, and hence of any sequence

Γ is always unique.

In GL the ”blind search” defines, for any formula A a finite number of decom-
position trees, but it can be proved that the search can be reduced to examining
only one of them, due to the absence of structural rules.

In LI the structural rules play a vital role in the proof construction and hence,
in the proof search. We consider here a number of examples to show the com-
plexity of the problem of examining possible decomposition trees for a given
formula A. We are going to see that the fact that a given decomposition tree
ends with an axiom leaf does not always imply that the proof does not exist.
It might only imply that our search strategy was not good. Hence the problem
of deciding whether a given formula A does, or does not have a proof in LI
becomes more complex then in the case of Gentzen system for classical logic.

Before we define a heuristic method of searching for proof and deciding whether
such a proof exists or not in LI we make some observations.

Observation 1: the logical rules of LI are similar to those in Gentzen type

classical formalizations we examined in previous chapters in a sense that
each of them introduces a logical connective.
Observation 2: The process of searching for a proof is, as before a decompo-
sition process in which we use the inverse of logical and structural rules
as decomposition rules.
For example the implication rule:

A, Γ −→ B
(→⇒)
Γ −→ (A ⇒ B)

becomes an implication decomposition rule (we use the same name

(→⇒) in both cases)

Γ −→ (A ⇒ B)
(→⇒) .
A, Γ −→ B

Observation 3: we write our proofs in as trees, instead of sequences of expres-

sions, so the proof search process is a process of building a decomposition
tree. To facilitate the process we write, as before, the decomposition rules,
structural rules included in a ”tree ” form.

For example the the above implication decomposition rule is written as follows.

4
 Γ −→ (A ⇒ B)

| (→⇒)
A, Γ −→ B

The two premisses implication rule (⇒→) written as the tree decomposition
rule becomes

(A ⇒ B), Γ −→
^
(⇒→)
Γ −→ A B, Γ −→

For example the structural weakening rule is written as the decomposition rule
is written as

Γ −→ A
(→ weak)
Γ −→

We write it in a tree form as follows.

Γ −→ A

| (→ weak)
Γ −→

We define, as before the notion of decomposable and indecomposable formulas

and sequents as follows.

Decomposable formula is any formula of the degree ≥ 1.

Decomposable sequent is any sequent that contains a decomposable for-
mula.
Indecomposable formula is any formula of the degree 0, i.e. any proposi-
tional variable.
Indecomposable sequent is a sequent formed from indecomposable formulas
only.

5
Decomposition tree construction (1): given a formula A ∈ we construct
its decomposition tree TA as follows.
Root of the tree is the sequent −→ A.
Given a node n of the tree we identify a decomposition rule applicable at this
node and write its premisses as the leaves of the node n.
We stop the decomposition process when we obtain an axiom or all leaves of
the tree are indecomposable.
Observation 4: the decomposition tree TA obtained by the construction (1)
most often is not unique.
Observation 5: the fact that we find a decomposition tree TA with non-axiom
leaf does not mean that 6 `LI A. This is due to the role of structural rules
in LI and will be discussed later in the chapter.
We illustrate the problems arising with proof search procedures, i.e. de-
composition trees construction in the next section 3 and give a heuristic
proof searching procedure in the section 4.

3 Proof Search Examples

We perform proof search and decide the existence of proofs in LI for a given
formula A ∈ F by constructing its decomposition trees TA . We examine here
some examples to show the complexity of the problem.

Example 1

Determine whether `LI −→ A for A = ((¬A ∩ ¬B) ⇒ ¬(A ∪ B)).

This means that we have to construct some, or all decomposition trees of

−→ ((¬A ∩ ¬B) ⇒ ¬(A ∪ B)).

If we find a decomposition tree such that all its leaves are axiom, we have a
proof.

If all possible decomposition trees have a non-axiom leaf, proof of A in LI does

not exist.

Consider the following decomposition tree of −→ A.

T1A

−→ ((¬A ∩ ¬B) ⇒ (¬(A ∪ B))

6
 | (−→⇒)
(¬A ∩ ¬B) −→ ¬(A ∪ B)
| (−→ ¬)
(A ∪ B), (¬A ∩ ¬B) −→
| (exch −→)
(¬A ∩ ¬B), (A ∪ B) −→
| (∩ −→)
¬A, ¬B, (A ∪ B) −→
| (¬ −→)
¬B, (A ∪ B) −→ A
| (−→ weak)
¬B, (A ∪ B) −→
| (¬ −→)
(A ∪ B) −→ B
^
(∪ −→)

A −→ B B −→ B

non − axiom axiom

The tree T1A has a non-axiom leaf, so it does not constitute a proof in LI. But
this fact does not yet prove that proof doesn’t exist, as the decomposition tree
in LI is not always unique.

Let’s consider now the following tree.

T2A

−→ ((¬A ∩ ¬B) ⇒ (¬(A ∪ B))

| (−→⇒)
(¬A ∩ ¬B) −→ ¬(A ∪ B)
| (−→ ¬)
(A ∪ B), (¬A ∩ ¬B) −→
| (exch −→)

7
 (¬A ∩ ¬B), (A ∪ B) −→
| (∩ −→)
¬A, ¬B, (A ∪ B) −→
| (exch −→)
¬A, (A ∪ B), ¬B −→
| (exch −→)
(A ∪ B), ¬A, ¬B −→
^
(∪ −→)

A, ¬A, ¬B −→ B, ¬A, ¬B −→

| (exch −→) | (exch −→)

¬A, A, ¬B −→ B, ¬B, ¬A −→
| (¬ −→) | (exch −→)
A, ¬B −→ A ¬B, B, ¬A −→
axiom | (¬ −→)
B, ¬A −→ B
axiom

All leaves of T2A are axioms, what proves that T2A is a proof of A and hence
we proved that
`LI ((¬A ∩ ¬B) ⇒ ¬(A ∪ B)).

Example 2

Part 1: Prove that

`LI −→ (A ⇒ ¬¬A),

Part 2: Prove that

6 `LI −→ (¬¬A ⇒ A).

Solution of Part 1
To prove that
`LI −→ (A ⇒ ¬¬A)
we have to construct some, or all decomposition trees of

−→ (A ⇒ ¬¬A).

8
The tree that ends with all axioms leaves is a proof of (A ⇒ ¬¬A) in LI.

Consider the following decomposition tree of −→ A, for A = (¬¬A ⇒ A)..

TA

−→ (A ⇒ ¬¬A).

| (−→⇒)
A −→ ¬¬A
| (−→ ¬)
¬A, A −→
| (¬ −→)
A −→ A
axiom

All leaves of TA are axioms what proves that TA is a proof of −→ (A ⇒ ¬¬A)

and we don’t need to construct other decomposition trees.

Solution of Part 2
To prove that
6 `LI −→ (¬¬A ⇒ A)
we have to construct all decomposition trees of (A ⇒ ¬¬A) and show that each
of them has an non-axiom leaf.

Consider the first decomposition tree defined as follows.

T1A

−→ (¬¬A ⇒ A)

f irst of 2 choices : (→⇒), (→ weak)

| (→⇒)
¬¬A −→ A
f irst of 2 choices : (→ weak), (contr →)

9
 | (→ weak)
¬¬A −→
f irst of 2 choices : (¬ →), (contr →)
| (¬ →)
−→ ¬A
f irst of 2 choices : (¬ →), (→ weak)
| (→ ¬)
A −→
indecomposable
non − axiom

We use the first tree created to define all other possible decomposition trees by
exploring the alternative search paths as indicated at the nodes of the tree.

T1A

−→ (¬¬A ⇒ A)

| (−→⇒)
one of 2 choices
¬¬A −→ A
]

| (contr −→)

second of 2 choices
¬¬A, ¬¬A −→ A
| (−→ weak)
f irst of 2 choices
¬¬A, ¬¬A −→
| (¬ −→)
f irst of 2 choices
¬¬A −→ ¬A
| (−→ ¬)

10
 the only choice
A, ¬¬A −→
| (exch −→)
the only choice
¬¬A, A −→
| (−→ ¬)
the only choice
A −→ ¬A
| (−→ ¬)
f irst of 2 choices
A, A −→
indecomposable
non − axiom

We can see from the above decomposition trees that the ”blind” construction
of all possible trees only leads to more complicated trees, due to the presence of
structural rules. Observe that the ”blind” application of (contr −→) gives an
infinite number of decomposition trees. To decide that none of them will produce
a proof we need some extra knowledge about patterns of their construction, or
just simply about the number useful of application of structural rules within
the proofs.

In this case we can just make an ”external” observation that the our first tree
T1A is in a sense a minimal one; that all other trees would only complicate
this one in an inessential way, i.e. we will never produce a tree with all axioms
leaves.

One can formulate a deterministic procedure giving a finite number of trees,

but the proof of its correctness require some extra knowledge. We are going to
discuss a motivation and an heuristics for the proof search in the next section.

Within the scope of this book we accept the ”external” explanation for the
heuristics we use as a sufficient solution.

As we can see from the above examples structural rules and especially the
(contr →) rule complicates the proof searching task. Both Gentzen type proof
systems RS and GL from the previous chapter don’t contain the structural
rules and are complete with respect to classical semantics, as is the original
Gentzen system LK, which does contain the structural rules. As (via Com-
pleteness Theorem) all three classical proof system RS, GL, LK are equivalent
we can say that the structural rules can be eliminated from the system LK.

11
A natural question of elimination of structural rules from the intutionistic
Gentzen system LI arizes.

The following example illustrates the negative answer.

Example 3

We know, by the theorem about the connection between classical and intuition-
istic logic (theorem ??) and corresponding Completeness Theorems that for any
formula A ∈ F,
|= A if and only if `I ¬¬A,
where |= A means that A is a classical tautology, `I means that A is intutionis-
tically provable, i.e. is provable in any intuitionistically complete proof system.
The system LI is intuitionistically complete, so we have that for any formula A,

|= A if and only if `LI ¬¬A.

We have just proved that 6 `LI (¬¬A ⇒ A). Obviously |= (¬¬A ⇒ A), so we
know that ¬¬(¬¬A ⇒ A) must have a proof in LI.

We are going to prove that

`LI ¬¬(¬¬A ⇒ A)

and that the structural rule (contr −→) is essential to the existence of its proof,
i.e. that without it the formula ¬¬(¬¬A ⇒ A) is not provable in LI.

The following decomposition tree TA is a proof of A = ¬¬(¬¬A ⇒ A) in LI.

TA

−→ ¬¬(¬¬A ⇒ A)

f irst of 2 choices : (→ ¬), (→ weak)

| (−→ ¬)
¬(¬¬A ⇒ A) −→
f irst of 2 choices : (contr −→), (¬ −→)
| (contr −→)
¬(¬¬A ⇒ A), ¬(¬¬A ⇒ A) −→
one of 2 choices
| (¬ −→)

12
 ¬(¬¬A ⇒ A) −→ (¬¬A ⇒ A)
one of 3 choices
| (−→⇒)
¬(¬¬A ⇒ A), ¬¬A −→ A
one of 2 choices
| (−→ weak)
¬(¬¬A ⇒ A), ¬¬A −→
one of 3 choices
| (exch −→)
¬¬A, ¬(¬¬A ⇒ A) −→
one of 3 choices
| (¬ −→)
¬(¬¬A ⇒ A) −→ ¬A
one of 3 choices
| (−→ ¬)
A, ¬(¬¬A ⇒ A) −→
one of 2 choices
| (exch −→)
¬(¬¬A ⇒ A), A −→
one of 3 choices
| (¬ −→)
A −→ (¬¬A ⇒ A)
one of 3 choices
| (−→⇒)
¬¬A, A −→ A
axiom

Assume now that the rule (contr −→) is not available. The decomposition
possible decomposition trees are as follows.

T1A

13
−→ ¬¬(¬¬A ⇒ A)

| (−→ ¬)
one of 2 choices
¬(¬¬A ⇒ A) −→
| (¬ −→)
only one choice
−→ (¬¬A ⇒ A)
| (−→⇒)
one of 2 choices
¬¬A −→ A
| (−→ weak)
only one choice
¬¬A −→
| (¬ −→)
only one choice
−→ ¬A
| (−→ ¬)
one of 2 choices
A −→
non − axiom

T2A

−→ ¬¬(¬¬A ⇒ A)

| (−→ weak)
second of 2 choices
−→
non − axiom

14
 T3A

−→ ¬¬(¬¬A ⇒ A)
| (−→ ¬)
¬(¬¬A ⇒ A) −→
| (¬ −→)
−→ (¬¬A ⇒ A)
| (−→ weak)
second of 2 choices
−→
non − axiom

T4A

−→ ¬¬(¬¬A ⇒ A)
| (−→ ¬)
¬(¬¬A ⇒ A) −→
| (¬ −→)
−→ (¬¬A ⇒ A)
| (−→⇒)
]
¬¬A −→ A
| (−→ weak)
only one choice
¬¬A −→
| (¬ −→)
only one choice
−→ ¬A
| (−→ weak)
second of 2 choices
−→
non − axiom

This proves that the formula ¬¬(¬¬A ⇒ A) is not provable in LI without

(contr −→) rule, i.e. that this rule can’t be eliminated.

15
4 Proof Search Heuristic Method

Before we define a heuristic method of searching for proof in LI let’s make some
additional observations to the observations 1-5 from section 2.

Observation 6: Our goal while constructing the decomposition tree is to ob-

tain axiom or indecomposable leaves. With respect to this goal the use
logical decomposition rules has a priority over the use of the structural
rules and we use this information while describing the proof search heuris-
tic.
Observation 7: all logical decomposition rules (◦ →), where ◦ denotes any
connective, must have a formula we want to decompose as the first formula
at the decomposition node, i.e. if we want to decompose a formula ◦A,
the node must have a form ◦A, Γ −→ ∆. Sometimes it is necessary to
decompose a formula within the sequence Γ first in order to find a proof.

For example, consider two nodes

n1 = ¬¬A, (A ∩ B) −→ B
and
n2 = (A ∩ B), ¬¬A −→ B.
We are going to see that the results of decomposing n1 and n2 differ dramatically.

Let’s decompose the node n1 . Observe that the only way to be able to de-
compose the formula ¬¬A is to use the rule (→ weak) first. The two possible
decomposition trees that starts at the node n1 are as follows.

T1n1

¬¬A, (A ∩ B) −→ B
| (→ weak)
¬¬A, (A ∩ B) −→
| (¬ →)
(A ∩ B) −→ ¬A
| (∩ →)
A, B −→ ¬A
| (→ ¬)
A, A, B −→
non − axiom

16
 T2n1

¬¬A, (A ∩ B) −→ B

| (→ weak)
¬¬A, (A ∩ B) −→
| (¬ →)
(A ∩ B) −→ ¬A
| (→ ¬)
A, (A ∩ B) −→
| (∩ →)
A, A, B −→
non − axiom

Let’s now decompose the node n2 . Observe that following our Observation 6
we start by decomposing the formula (A ∩ B) by the use of the rule (∩ →) first.
A decomposition tree that starts at the node n2 is as follows.

Tn2

(A ∩ B), ¬¬A −→ B

| (∩ →)
A, B, ¬¬A −→ B
axiom

This proves that the node n2 is provable in LI, i.e.

`LI (A ∩ B), ¬¬A −→ B.

Of course, we have also that the node n1 is also provable in LI, as one can
obtain the node n2 from it by the use of the rule (exch →).

17
Observation 8: the use of structural rules are important and necessary while
we search for proofs. Nevertheless we have to use them on the ”must”
basis and set up some guidelines and priorities for their use.

For example, use of weakening rule discharges the weakening formula, and
hence an information that may be essential to the proof. We should use
it only when it is absolutely necessary for the next decomposition steps.
Hence, the use of weakening rule (→ weak) can, and should be restricted
to the cases when it leads to possibility of the use of the negation rule
(¬ →). This was the case of the decomposition tree T1n1 . We used it
as an necessary step, but still it discharged too much information and we
didn’t get a proof, when proof of the node existed.
In this case the first rule in our search should have been the exchange
rule, followed by the conjunction rule (no information discharge) not the
weakening (discharge of information) followed by negation rule. The full
proof of the node n1 is the following.

T3n1

¬¬A, (A ∩ B) −→ B

| (exch −→)
(A ∩ B), ¬¬A −→ B
| (∩ →)
A, B, ¬¬A −→ B
axiom

As a result of the observations 1- 5 from section 2 and observations 6 - 8

above we adopt the following.

Heuristic Procedure for Proof Search in LI.

For any A ∈ F we construct the decomposition trees T→A following the rules
below.

Decomposition Tree Generation rules.

1. Use first logical rules where applicable.

18
2. Use (exch →) rule to decompose, via logical rules, as many formulas on the
left side of −→ as possible.

3. Use (→ weak) only on a ”must” basis in connection with (¬ →) rule.

4. Use (contr →) rule as the last recourse and only to formulas that contain ¬
or ⇒ as connectives.
5. Let’s call a formula A to which we apply (contr →) rule a contraction
formula.
6. The only contraction formulas are formulas containing ¬ or ⇒ between theirs
logical connectives.
7. Within the process of construction of all possible trees use (contr →) rule
only to contraction formulas.
8. Let C be a contraction formula appearing on the node n of the decomposi-
tion tree of T→A . For any contraction formula C, any node n, we apply
(contr →) rule the the formula C at most as many times as the number
of sub-formulas of C.

If we find a tree with all axiom leaves we have a proof, i.e. `LI A and if all (finite
number) trees have a non-axiom leaf we have proved that proof of A does not
exist, i.e. 6 `LI A.

5 LK - Original Gentzen system for the classical

logic

In the original Gentzen work the intuitionistic logic is obtained as a particular

case of his system LK for classical logic. We deal here with a propositional part
of the original formalization.

The differences are as follows.

Language of LK

In classical case we adopt the whole set

SEQ = {Γ −→ ∆ : Γ, ∆ ∈ F ∗ (3)

instead of its subset IS defined by ( 1), i.e. as follows.

IS = {Γ −→ ∆ : ∆ consists of at most one f ormula}

adopted for the intuitionistic logic.

19
Axioms of LK

We adopt the set of axioms, relevant to the difference of the language. I.e. in
the classical case we have as an axiom any sequent of the form

Γ1 , A, Γ2 −→ Γ3 , A, Γ4 (4)

while it becomes
Γ1 , A, Γ2 −→ A
in the case of the intuitionistic logic.

Rules of inference of LK

The changes are as follows.

1. There two more structural rules in the system LK. One more contraction
rule:

Γ −→ ∆, A, A,
(→ contr) ,
Γ −→ ∆, A

and one more exchange rule:

∆ −→ Γ1 , A, B, Γ2
(→ exchange) .
∆ −→ Γ1 , B, A, Γ2

Observe that they both become obsolete in the language of the intuitionistic
logic.

2. In all inference rules we drop the intuitionistic restriction that the sequence
∆ in the succedant of the sequence is empty.

3. In particular, we add the sequence ∆ to all succedants which were empty or

one formula in all of the rules of LI.

The rules of inference of LK are hence as follows.

Structural Rules of LK

Weakening

Γ −→ ∆ Γ −→ ∆
(weakening →) , (→ weakening) .
A, Γ −→ ∆ Γ −→ ∆, A

A is called the weakening formula.

Contraction

20
 A, A, Γ −→ ∆ Γ −→ ∆, A, A,
(contr →) , (→ contr) ,
A, Γ −→ ∆ Γ −→ ∆, A
A is called the contraction formula.

Exchange

Γ1 , A, B, Γ2 −→ ∆ ∆ −→ Γ1 , A, B, Γ2
(exchange →) , (→ exchange) .
Γ1 , B, A, Γ2 −→ ∆ ∆ −→ Γ1 , B, A, Γ2

Logical Rules of LK

Conjunction rules

A, B, Γ −→ ∆ Γ −→ ∆, A ; Γ −→ ∆, B∆
(∩ →) , (→ ∩) .
(A ∩ B), Γ −→ ∆ Γ −→ ∆, (A ∩ B)

Disjunction rules

Γ −→ ∆, A, B A, Γ −→ ∆ ; B, Γ −→ ∆
(→ ∪) , (∪ →) .
Γ −→ ∆, (A ∪ B) (A ∪ B), Γ −→ ∆

Implication rules

A, Γ −→ ∆, B Γ −→ ∆, A ; B, Γ −→ ∆
(→⇒) , (⇒→) .
Γ −→ ∆, (A ⇒ B) (A ⇒ B), Γ −→ ∆

Negation rules

Γ −→ ∆, A A, Γ −→ ∆
(¬ →) , (→ ¬) .
¬A, Γ −→ ∆ Γ −→ ∆, ¬A

Formally we define:

LK = (SEQ, AX, Structural rules of LK, Logical rules of LK}),

where SEQ is defined by (1), Structural rules of LK , Logical rules of

LK are the inference rules defined above, and AX is the axiom of the system
defined by the schema ( 4).

21
5.1 Exercises and Homework

1. Give a formal proof LI axioms A1 - A11 and all examples of intuitionistic

tautologies from Chapter 10.

2. Show that none of the formulas from chapter 10 that are classical and not
intuitionistic tautologies is provable in LI.

3. Find the formal proofs in LI of double negation of all of formulas from

chapter 10 that are classical and not intuitionistic tautologies.

4. Give the proof of the Glivenko theorem, i.e. prove that any formula A ∈ F,
A is a classically provable if and only if ¬¬A is an intuitionistically provable.

5. Give examples of formulas illustrating that the following theorems hold.

Theorem 5.1 (Gödel) For any A, B ∈ F, a formula (A ⇒ ¬B) is a classically

provable if and only if it is an intuitionistically provable.

Theorem 5.2 (Gödel) If a formula A contains no connectives except ∩ and ¬,

then A is a classically provable if and only if it is an intuitionistically provable.

6. Give LK proofs of all formulas from chapter 10 that are not provable in LI.

22