Completeness Theorems. Model Theory. Mathematical Logic. Part 4.

model theory, interpretation, completeness theorem, logic, calculus, intuitionistic, constructive, Kripke semantics, Kripke model, semantics, Kripke structure, scenario, model, completeness, Kripke, sequent

Back to title page

Left

Adjust your browser window
In this book, constructive logic is used as a synonym of intuitionistic logic!

Right

4.4. Constructive Propositional Logic - Kripke Semantics

Saul Aaron Kripke (1940). See also portraits in the gallery http://www.consciencia.org/imagens/banco.

"American logician and philosopher Saul Kripke is one of today's leading thinkers on thought and its manifold relations to the world. His name is attached to objects in several fields of logic from Kripke-Platek axioms in higher recursion theory to the "Brouwer-Kripke scheme" in intuitionistic mathematics. Kripke models for modal logic, a discovery he made in his teen-age years, became part of the standard vocabulary of mathematical logicians after his first article appeared in 1963, when he was just 23 years old. Kripke models and the results that depend upon them are cited today not only in philosophy and logic, but also in linguistics and computer science..." (The Gazette. The newspaper of the John Hopkins University, May 12, 1997, Vol.26, N 34)

S. Kripke (1963). Semantical Considerations on Modal Logic, Acta Philosophica Fennica 16: 83-94.

S. Kripke (1963). Semantical analysis of modal logic. I. Normal modal propositional calculi. Z. Math. Logik Grundl. Math., 9:67-96, 1963.

S. Kripke (1965). Semantical analysis of intuitionistic logic. In: J. N. Crossley, M. A. E. Dummet (eds.), Formal systems and recursive functions. Amsterdam, North Holland, 1965, pp.92-129.

As usual, let us assume, the formula F has been built of "atomic" formulas B₁, B₂, ..., B_n by using propositional connectives only. Instead of simply computing truth values of F from truth values of B₁, B₂, ..., B_n, Kripke proposed to consider the behavior of F when the truth values of B₁, B₂, ..., B_n are changing gradually from false to true according to some "scenario".

Thus, Kripke proposed to replace the classical semantics (interpretation) of the propositional connectives (defined by the classical truth tables) by a more complicated "dynamic" samantics.

Instead of simply saying that ~F is true, iff F is false, let us say that, at some point in a scenario, ~F is true, iff, at this point, F is false and remains false, when truth values of B₁, B₂, ..., B_n are changing according to the scenario.

Let o stand for implication, conjunction or disjunction. Instead of simply saying that FoG is true, iff, FoG is true according to the classical truth tables, let us say that, at some point in a scenario, FoG is true, iff, at this point, it is true and remains true, when truth values of B₁, B₂, ..., B_n are changing according to the scenario.

Example 4.4.1. Let us consider the behavior of the classical axiom L₁₁: Bv~B in the scenario, where, at first, B is false, and at the next step it becomes true:

0 -------------- 1

At the starting point, B is false, ~B also is false (here, for ~B to be true, B must remain false at the next step, but it doesn't). This means that, at the starting point, Bv~B is false. At the next step: B is true, hence, ~B is false, but, of course, Bv~B is true. Thus, in Kripke scenarios, Bv~B is not always true. Surprisingly, some time later (Lemma 4.4.3), we will derive from this simple fact that Bv~B cannot be proved in the constructive logic (we already know this from Section 2.8).

Example 4.4.2. Let us consider the behavior of the classically provable half of the First de Morgan Law: ~(A&B)->~Av~B in the scenario, where, at first A and B are both false, and at the next step, two branches appear in the scenario: in the first branch: A remains false, and B becomes true, in the second branch: A becomes true, and B remains false:

|---01
00--|----------
|---10

At the starting point: A is false, ~A - also is false (for ~A to be true, A must remain false at the next step, but in the second branch it doesn't). Similarly, at the starting point: B is false, ~B - also false (for ~B to be true, B must remain false at the next step, but in the first branch it doesn't). This means that, at the starting point, ~(A&B) is true (because A&B is false, and it remains false in both branches), and ~Av~B is false, hence, ~(A&B)->~Av~B is false. Thus, in Kripke scenarios, ~(A&B)->~Av~B is not always true. Surprisingly, some time later (Lemma 4.4.3), we will derive from this simple fact that the this half of the First de Morgan Law cannot be proved in the constructive logic. We failed to do this in Section 2.8!

Exercise 4.4.1. Investigate, in appropriate scenarios, the behavior of the following classically provable formulas:

~(A&B) -> ~A v ~B,
~~(AvB) -> ~~A v ~~B,
(A->B)->((~A->B)->B),
(A->B)v(B->A),

and verify that, in Kripke scenarios, these formulas are not always true. Some time later (Lemma 4.4.3), we will derive from this simple fact that these formulas cannot be proved in the constructive logic. We failed to do this in Section 2.8! (Hint: try the most simple scenarios first: 00--01, 00-10, 00-11, etc.)

More precisely, the definition of the Kripke semantics for the propositional logic is as follows. Assume, the formula F has been built of "atomic" formulas B₁, B₂, ..., B_n by using propositional connectives only. Instead of considering truth values of F for all the possible tuples of truth values of B₁, B₂, ..., B_n, let us consider the behavior of F in all the possible Kripke scenarios, defined as follows.

Definition of Kripke scenarios. Each scenario s is a triple (b, <=, t) of the following objects. First, b is a finite set of objects called nodes (or, states).

The second member <= is a partial ordering relationship between the nodes, i.e. for all x, y, z in b: x<=y & y<=z -> x<=z (transitivity).

The third member t of the tripple is a function (t means "true"). It associates with each node x a "growing" set t(x) of "atomic" formulas, i.e. a subset of {B₁, B₂, ..., B_n} in such a way that for all x, y in b: x<=y -> t(x)<=t(y), where <= means "is subset of".

Note. In some other textbooks, Kripke scenarios are called Kripke models, or Kripke structures.

Let us say that B_i is true at the node x, iff B_i is in the set t(x). We will denote this fact by x |= B_i ("at x, B_i is true", or "x forces B_i"). Since t is monotonic, if x |= B_i , then y |= B_i for all y after x, i.e. for all y in b such that y>=x. I.e. if B_i is true at some node x, then B_i remains true at all nodes after x.

Let us define x |= F ("F is true at x", or "x forces F") for any formula F that has been built of "atomic" formulas B₁, B₂, ..., B_n by using propositional connectives only.

1. Negation. Suppose, the truth value of x |= F is already defined for all x in b. Then x |= ~F is defined to be true, iff, for all y>=x in b, y |= F is false (i.e. ~(y |= F) is true according to the classical truth table of the negation connective).

2. Implication, conjunction or disjunction. Suppose, the truth values of x |= F and x |= G are already defined for all x in b. Then x |= FoG is defined to be true, iff, for all y>=x in b, (y |= F)o(y |= G) is true according to the classical truth table of the implication, conjunction or disjunction connective respectively.

Lemma 4.4.1. For any formula F, any Kripke scenario (b, <=, t), and any node x in b: if x |= F, then y |= F for all y in b such that y>=x. I.e. if, in a Kripke scenario, a formula becomes true at some node, then it remains true forever after this node.

Proof. By induction.

Induction base. See above: if x |= B_i , then y |= B_i for all y after x, i.e. for all y in b such that y>=x.

Induction step.

1. Negation. Assume, x |= ~F, i.e., according to the classical truth table, not y |= F for all y>=x in b. If y>=x, then is y |= ~F true or false? By definition, y |= ~F would be true, iff not z |= F for all z>=y in b. By transitivity of <=, if z>=y and y>=x, then z>=x. Thus, by our assumption, if z>=y, then not z |= F. Hence, y |= ~F. Q.E.D.

Exercise 4.4.2. Verify that if x is a maximal node in a scenario (b, <=, t), then x |= F, iff F is true at x according to the classical truth tables.

Kripke established that a formula is provable in the constructive propositional logic, iff it is true at all nodes in all Kripke scenarios.

Theorem 4.4.2 (S.Kripke, completeness of the constructive propositional logic). A formula F is provable in the constructive propositional logic (i.e. [L₁-L₁₀, MP] |- F), iff F is true at all nodes in all Kripke scenarios.

As usual, the hard part of the proof is establishing that "true is provable", i.e. if F is true at all nodes in all Kripke scenarios, then [L₁-L₁₀, MP] |- F (see Corollary 4.4.7 below). The easy part of the proof is, as usual, the "soundness lemma":

Lemma 4.4.3. If [L₁-L₁₀, MP] |- F, then F is true at all nodes in all Kripke scenarios.

This lemma will follow from

Lemma 4.4.4. If F is any of the constructive axioms L₁-L₁₀, then, for any Kripke scenario (b, <=, t), and any node x in b: x |= F. I.e. the constructive axioms are true at all nodes in all Kripke scenarios.

and

Lemma 4.4.5. If, in a Kripke scenario (b, <=, t), at the node x in b: x |= F and x |= F->G, then x |= G. Hence, if F and F->G are true at all nodes in all Kripke scenarios, then so is G.

Proof of Lemma 4.4.3. Indeed, by Lemma 4.4.4, all the constructive axioms L₁-L₁₀ are true at all nodes in all scenarios, and, by Lemma 4.4.5, the Modus Ponens rule preserves the property of being "true at all nodes in all scenarios". Q.E.D.

Note. Let us return to the above Example 4.4.2 and Exercise 4.4.1. We established that formulas

~(A&B)->~Av~B
~~(AvB)->~~Av~~B
(A->B)->((~A->B)->B)

are not true at all nodes in all scenarios. Hence, by Lemma 4.4.3, these formulas cannot be proved in the constructive logic [L₁-L₁₀, MP]. We failed to prove this in Section 2.8!

Proof of Lemma 4.4.4.

L₁: B->(C->B)

x |= B->(C->B) is true, iff (y |= B)->(y |= C->B) is true for all y>=x.

x |= B->(C->B) is false, iff (y |= B)->(y |= C->B) is false for some y>=x.

How could (y |= B)->(y |= C->B) be false for some y>=x? According to the classical implication truth table, this could be only, iff y |= B is true, and y |= C->B is false.

y |= C->B is true, iff (z |= C)->(z |= B) is true for all z>=y.

y |= C->B is false, iff (z |= C)->(z |= B) is false for some z>=y.

How could (z |= C)->(z |= B) be false for some z>=y? According to the classical implication truth table, this could be only, iff z |= C is true, and z |= B is false.

Summary:

L₁₀: ~B->(B->C)

y |= ~B is true, iff z |=B is false for all z>=y.

Summary:

Hence, if x |= ~B->(B->C) is false, then there is y>=x such that: a) Az>=y (z |=B is false), and b) Ez>=y (z |= B is true). Contradiction. Thus, x |= ~B->(B->C) is true.

L₃: B&C->B

x |= B&C->B is false
-----------------------iff------------------------
Ey>=x (y |=B&C is true & y |= B is false)
---------------------------iff--------------------------------------
-----------------------Az>=y (z |=B is true & z |= C is true)-----------------------------------------------

Hence, there is y such that x<=y and y |= B is false. From Az>=y (z |=B is true) we obtain that y |= B is true. Contradiction. Thus, x |= B&C->C is true.

L₄: B&C->C

Similarly.

L₅: B->(C->B&C)

L₆: B->BvC

Hence, there are y, z such that x<=y<=z, y |= B is true, and z |= B is false. By Lemma 4.4.1, this is a contradiction. Thus, x |= B->BvC is true.

L₇: C->BvC

Similarly.

L₈: (B->D)->((C->D)->(BvC->D))

x |= (B->D)->((C->D)->(BvC->D)) is false
-----------------------iff------------------------
Ey>=x (y |=B->D is true & y |= (C->D)->(BvC->D) is false)
-----------------------------------iff--------
Ez>=y (z |= C->D is true and z |= BvC->D is false)
-----------------------------------iff--------
Eu>=z (u |= BvC is true and u |= D is false)

L₂: (B->(C->D))->((B->C)->(B->D))

x |= (B->(C->D))->((B->C)->(B->D)) is false
-----------------------iff------------------------
Ey>=x (y |= B->(C->D) is true & y |= (B->C)->(B->D) is false)
-----------------------iff-----------------iff---------------------
----------Az>=y ((z |= B)->(z |= C->D))-----Ez>=y (z |= B->C is true & z |= B->D is false)
---------------------------------------------------------iff----------------------iff------
------------------------------------------------Au>=z ((u |= B)->(u |= C))----Eu>=z (u |= B is true & u |= D is false)

L₉: (B->C)->((B->~C)->~B)

x |= (B->C)->((B->~C)->~B) is false
-----------------------iff-----------------------
Ey>=x (y |= B->C is true & y |= (B->~C)->~B is false)
--------iff-------------------------iff----
--------------Az>=y ((z |= B)->(z |= C))-------------Ez>=y (z |= B->~C is true & z |= ~B is false)
------------------------------------------------------------iff-------------------------iff----
-------------------------------------------Au>=z ((u |= B)->(u |= ~C))----------Eu>=z (u |= B is true)

Exercise 4.4.3. Verify that, in the above recursive definition of x |= F, the item

2. Implication, conjunction or disjunction: x |= FoG is defined to be true, iff, according to the classical truth tables, (y |= F)o(y |= G) is true for all y>=x in b.

could be replaced by

2a. Implication ("non-monotonic" connective): x |= F->G is defined to be true, iff, according to the classical truth tables, (y |= F)->(y |= G) is true for all y>=x in b.

2b. Conjunction or disjunction ("monotonic" connectives): x |= FoG is defined to be true, iff, according to the classical truth tables, (x |= F)o(x |= G) is true.

End of Exercise 4.4.3.

The Hard Part of the Proof

Now, let us try proving that, if F is true at all nodes in all Kripke scenarios, then F is provable in the constructive propositional logic). We will follow the paper by

Judith Underwood. A constructive Completeness Proof for Intuitionistic Propositional Calculus. TR-90-1179, December 1990, Department of Computer Science, Cornell University (http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Summarize/cul.cs/TR90-1179).

based on the contructions from

Melvin Fitting. Intuitionistic Logic, Model Theory and Forcing. North-Holland, Amsterdam, 1969

The smart idea is to generalize the problem in the following way. Instead of considering constructive provability of single formulas, let us consider the constructive provability of D₁, D₂, ..., D_m |- C₁vC₂v... vC_n for arbitrary formulas D₁, D₂, ..., D_m, C₁, C₂, ..., C_n, i.e. let us consider ordered pairs of sets ({D₁, D₂, ..., D_m}, {C₁, C₂, ..., C_n}). Let us call such pairs sequents. If S₁, S₂ are sets of formulas (S₁ may be empty), let us call the sequent (S₁, S₂) constructively provable, iff [L₁-L₁₀, MP]: S₁ |- vS₂, where vS₂ denotes the disjunction of formulas contained in S₂. Moreover, let us consider sets of sequents. This will allow to carry out a specific induction argument (considering single formulas or single sequents does not allow such an argument!).

Let us say that a Kripke scenario (b, <=, t) contains a counterexample for a sequent (S₁, S₂), iff the sequent is false at some node in the scenario (or, more precisely, iff there is x in b such that x |= F for all formulas F in S₁ and not x |= G for all formulas G in S₂).

Additionally, let us use Corollary 7.1.2(b) of Theorem 7.1.1 to replace all negations ~F by F->f, where f is an atomic formula, which is "always false", i.e. which, in a sequent (S₁, S₂), never belongs to S₁. Thus, formulas mentioned in the proof of the following Theorem 4.4.6 do not contain negations (but they may contain the specific atomic formula f).

Theorem 4.4.6. For any set S of sequents, either some sequent of S is constructively provable, or there is a Kripke scenario (b, <=, t), which contains counterexamples for each sequent in S.

Proof. Let us start with a proof overview. We will consider the following cases:

Case 1. S contains (S₁, S₂) such that A&B in S₁ and not (A in S₁ and B in S₁). Let us consider the set S' obtained from S by adding the "missing" formulas A, B to S₁, i.e. by replacing (S₁, S₂) by (S₁U{A, B}, S₂). Let us verify that if Theorem is true for S', then it is true for S...

Case 2. S contains (S₁, S₂) such that A&B in S₂ and not (A in S₂ or B in S₂). Let us consider the following two sets: a) S' - obtained from S by adding the formula A to S₂, i.e. by replacing (S₁, S₂) by (S₁, S₂U{A}). b) S'' - obtained from S by adding the formula B to S₂, i.e. by replacing (S₁, S₂) by (S₁, S₂U{B}). Let us verify that if Theorem is true for S' and S'', then it is true for S...

Case 3. S contains (S₁, S₂) such that AvB in S₁ and not (A in S₁ or B in S₁). Let us consider the following two sets: a) S' - obtained from S by adding the formula A to S₁, i.e. by replacing (S₁, S₂) by (S₁U{A}, S₂). b) S'' - obtained from S by adding the formula B to S₁, i.e. by replacing (S₁, S₂) by (S₁U{B}, S₂). Let us verify that if Theorem is true for S' and S'', then it is true for S...

Case 4. S contains (S₁, S₂) such that AvB in S₂ and not (A in S₂ and B in S₂). Let us consider the set S' obtained from S by adding the "missing" formulas A, B to S₂, i.e. by replacing (S₁, S₂) by (S₁, S₂U{A, B}). Let us verify that if Theorem is true for S', then it is true for S...

Case 5. S contains (S₁, S₂) such that A->B in S₁ and not (A in S₂ or B in S₁). Let us consider the following two sets: a) S' - obtained from S by adding the formula A to S₂, i.e. by replacing (S₁, S₂) by (S₁, S₂U{A}). b) S'' - obtained from S by adding the formula B to S₁, i.e. by replacing (S₁, S₂) by (S₁U{B}, S₂). Let us verify that if Theorem is true for S' and S'', then it is true for S...

Case 6. S contains (S₁, S₂) such that A->B in S₂ and for every sequent (T₁, T₂) in S, not (S₁<=T₁ and A in T₁ and B in T₂). Let us consider the set S' obtained from S by adding the sequent (S₁U{A}, B) to it. Let us verify that if Theorem is true for S', then it is true for S...

Case 7. None of the above cases hold for S. Theorem is true for S - easy to verify...

The first six cases represent the induction argument: proving of Theorem for a sequent set S is reduced to proving it for some other sets - S' and S". By iterating this reduction, we always arrive happily to the Case 7, where Theorem is easy to verify.

Indeed, let us denote by universe(S₁, S₂) the set of all formulas and sub-formulas (of the formulas) contained in S₁US₂. Let us denote by universe(S) the union of the universes of sequents from S.

Exercise 4.4.4. Verify that:

a) When, in the Cases 1-5, the sequent (S₁, S₂) is replaced by some other sequent (T₁, T₂), then universe(T₁, T₂) <= universe(S₁, S₂).

b) When, in the Case 6, because of the sequent (S₁, S₂), the sequent (S₁U{A}, B) is added to S, then universe(S₁U{A}, B) <= universe(S₁, S₂).

c) For a given universe(S), there exist no more than N = 2^{|universe(S)|+1} different sequents (S₁, S₂) such that universe(S₁, S₂) <= universe(S). And, no more than 2^N different sets of sequents.

Thus, any chain of iterated Cases 1-6 cannot be longer than 2^N+1 - either we will arrive at a set of sequents already built at a previous step, or we will arrive at the Case 7.

Now - the proof as it should be.

Let us verify that if Theorem is true for S', then it is true for S.

Assume, some sequent of S' is constructively provable, then it is (S₁U{A, B}, S₂) or some other sequent. If it is some other sequent, then it belongs to S, i.e. some sequent of S is constructively provable. If (S₁U{A, B}, S₂) is constructively provable, then so is (S₁, S₂). Indeed, if S₁U{A, B}|- vS₂ is constructively provable, how to prove S₁ |- vS₂? Since S₁ contains A&B, by axioms L₃ and L₃ we can derive A and B. After this, we can apply the proof of S₁U{A, B}|- vS₂. Hence, S₁ |- vS₂ is constructively provable.

On the other side, if there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S', then it contains also a counterexample for each sequent in S. Indeed, a sequent in S is either (S₁, S₂), or some other sequent. If it is some other sequent, then it belongs to S', i.e. (b, <=, t) contains a counterexample for it. Does (b, <=, t) contain a counterexample also for (S₁, S₂)? We know that it contains a counterexample for (S₁U{A, B}, S₂), i.e. for some x in b, x |= F for all formulas F in S₁U{A, B}and not x |= G for all formulas G in S₂. Hence, (b, <=, t) contains a counterexample also for (S₁, S₂). Q.E.D.

Case 2. S contains (S₁, S₂) such that A&B in S₂ and not (A in S₂ or B in S₂). Let us consider the following two sets:

a) S' - obtained from S by adding the formula A to S₂, i.e. by replacing (S₁, S₂) by (S₁, S₂U{A}).

b) S'' - obtained from S by adding the formula B to S₂, i.e. by replacing (S₁, S₂) by (S₁, S₂U{B}).

Let us verify that if Theorem is true for S' and S'', then it is true for S.

Assume, some sequent of S' and some sequent of S'' is constructively provable. The sequent of S' is (S₁, S₂U{A}) or some other sequent. If it is some other sequent, then it belongs to S, i.e. some sequent of S is constructively provable. The sequent of S'' is (S₁, S₂U{B}) or some other sequent. If it is some other sequent, then it belongs to S, i.e. some sequent of S is constructively provable. So, let us consider the situation, when (S₁, S₂U{A}) and (S₁, S₂U{B}) both are constructively provable.

If S₁ |- AvS₂ and S₁ |- BvS₂ both are constructively provable, how to prove S₁ |- vS₂ (we know that S₂ contains A&B)?

By Theorem 2.3.1, conjunction is distributive to disjunction: [L₁-L₈, MP]: |- (A&B)vC<=->(AvC)&(BvC). Hence, [L₁-L₈, MP]: (AvS₂)&(BvS₂)->(A&B)vS₂. So, let us merge the proofs of S₁ |- AvS₂ and S₁ |- BvS₂, and let us append the proof of Theorem 2.3.1. Thus, we have obtained a proof of S₁ |- (A&B)vS₂.

From Section 2.3 we know that in [L₁-L₈, MP] disjunction is associative, commutative and idempotent. And, by Replacement Lemma 1(e): [L₁-L₈, MP] A<=->B |- AvC<=->BvC. Since S₂ contains A&B, these facts allow, from a proof of S₁ |- (A&B)vS₂, to derive a proof of S₁ |- vS₂.

On the other side, if there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S', then it contains also a counterexample for each sequent in S. Indeed, a sequent in S is either (S₁, S₂), or some other sequent. If it is some other sequent, then it belongs to S', i.e. (b, <=, t) contains a counterexample for it. Does (b, <=, t) contain a counterexample also for (S₁, S₂)? We know that it contains a counterexample for (S₁, S₂U{A}), i.e. for some x in b, x |= F for all formulas F in S₁ and not x |= G for all formulas G in S₂U{A}. Hence, (b, <=, t) contains a counterexample also for (S₁, S₂). Q.E.D.

If there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S'', then it contains also a counterexample for each sequent in S. The argument is similar to the above.

Case 3. S contains (S₁, S₂) such that AvB in S₁ and not (A in S₁ or B in S₁). Let us consider the following two sets:

a) S' - obtained from S by adding the formula A to S₁, i.e. by replacing (S₁, S₂) by (S₁U{A}, S₂).

b) S'' - obtained from S by adding the formula B to S₁, i.e. by replacing (S₁, S₂) by (S₁U{B}, S₂).

Let us verify that if Theorem is true for S' and S'', then it is true for S.

Assume, some sequent of S' and some sequent of S'' is constructively provable. The sequent of S' is (S₁U{A}, S₂) or some other sequent. If it is some other sequent, then it belongs to S, i.e. some sequent of S is constructively provable. The sequent of S'' is (S₁U{B}, S₂) or some other sequent. If it is some other sequent, then it belongs to S, i.e. some sequent of S is constructively provable. So, let us consider the situation, when (S₁U{A}, S₂) and (S₁U{B}, S₂) both are constructively provable.

Let us recall the Exercise 2.3.2 [L₁, L₂, L₈, MP]: if A₁, A₂, ..., A_n, B |- D, and A₁, A₂, ..., A_n, C |- D, then A₁, A₂, ..., A_n , BvC |- D. Thus, if S₁U{A}|- vS₂ and S₁U{B}|- vS₂both are constructively provable, then (since S₁ contains AvB) so is S₁U{B}|- vS₂.

On the other side, if there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S', then it contains also a counterexample for each sequent in S. Indeed, a sequent in S is either (S₁, S₂), or some other sequent. If it is some other sequent, then it belongs to S', i.e. (b, <=, t) contains a counterexample for it. Does (b, <=, t) contain a counterexample also for (S₁, S₂)? We know that it is contains counterexample for (S₁U{A}, S₂), i.e. for some x in b, x |= F for all formulas F in S₁U{A}and not x |= G for all formulas G in S₂. Hence, (b, <=, t) contains a counterexample also for (S₁, S₂). Q.E.D.

If there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S'', then it is also contains counterexample for each sequents in S. The argument is similar to the above.

Let us verify that if Theorem is true for S', then it is true for S.

Assume, some sequent of S' is constructively provable, then it is (S₁, S₂U{A, B}) or some other sequent. If it is some other sequent, then it belongs to S, i.e. some sequent of S is constructively provable. If (S₁, S₂U{A, B}) is constructively provable, then so is (S₁, S₂). Indeed, if S₁|-(AvB) vS₂ is constructively provable, how to prove S₁ |- vS₂ (where S₂ contains AvB)?

From Section 2.3 we know that in [L₁-L₈, MP] disjunction is associative, commutative and idempotent. And, by Replacement Lemma 1(e): [L₁-L₈, MP] A<=->B |- AvC<=->BvC. Since that S₂ contains AvB, these facts allow, from a proof of S₁ |- (AvB)vS₂, to derive a proof of S₁ |- vS₂.

On the other side, if there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S', then it contains also a counterexample for each sequent in S. Indeed, a sequent in S is either (S₁, S₂), or some other sequent. If it is some other sequent, then it belongs to S', i.e. (b, <=, t) contains a counterexample for it. Does (b, <=, t) contain a counterexample also for (S₁, S₂)? We know that it contains a counterexample for (S₁, S₂U{A, B}), i.e. for some x in b, x |= F for all formulas F in S₁ and not x |= G for all formulas G in S₂U{A, B}. Hence, (b, <=, t) contains a counterexample also for (S₁, S₂). Q.E.D.

If there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S'', then it contains also a counterexample for each sequent in S. The argument is similar to the above.

Case 5. S contains (S₁, S₂) such that A->B in S₁ and not (A in S₂ or B in S₁). Let us consider the following two sets:

a) S' - obtained from S by adding the formula A to S₂, i.e. by replacing (S₁, S₂) by (S₁, S₂U{A}).

b) S'' - obtained from S by adding the formula B to S₁, i.e. by replacing (S₁, S₂) by (S₁U{B}, S₂).

Let us verify that if Theorem is true for S' and S'', then it is true for S.

Assume, some sequent of S' and some sequent of S'' is constructively provable. The sequent of S' is (S₁, S₂U{A}) or some other sequent. If it is some other sequent, then it belongs to S, i.e. some sequent of S is constructively provable. The sequent of S'' is (S₁U{B}, S₂) or some other sequent. If it is some other sequent, then it belongs to S, i.e. some sequent of S is constructively provable. So, let us consider the situation, when (S₁, S₂U{A}) and (S₁U{B}, S₂) both are constructively provable.

We have two proofs: S₁ |- AvS₂ and S₁, B |- vS₂, and we know that S₁ contains A->B. How to derive a proof of S₁ |- vS₂?

On the other side, if there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S', then it contains also a counterexample for each sequent in S. Indeed, a sequent in S is either (S₁, S₂), or some other sequent. If it is some other sequent, then it belongs to S', i.e. (b, <=, t) contains a counterexample for it. Does (b, <=, t) contain a counterexample also for (S₁, S₂)? We know that it contains a counterexample for (S₁, S₂U{A}), i.e. for some x in b, x |= F for all formulas F in S₁ and not x |= G for all formulas G in S₂U{A}. Hence, (b, <=, t) contains a counterexample also for (S₁, S₂). Q.E.D.

If there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S'', then it contains also a counterexample for each sequent in S. The argument is similar to the above.

Case 6. S contains (S₁, S₂) such that A->B in S₂ and for every sequent (T₁, T₂) in S, not (S_1<=T₁ and A in T₁ and B in T₂). Let us consider the set S' obtained from S by adding the sequent (S₁U{A}, B) to it.

Let us verify that if Theorem is true for S', then it is true for S.

Assume, some sequent of S' is constructively provable, then it is (S₁U{A}, B) or some other sequent. If it is some other sequent, then it belongs to S, i.e. some sequent of S is constructively provable. If (S₁U{A}, B) is constructively provable, then so is (S₁, S₂). Indeed, if S₁, A |- B is constructively provable, then, by Deduction Theorem 1, S₁ |- A->B, and S₁ |- vS₂ (since S₂ contains A->B).

On the other side, if there is a Kripke scenario (b, <=, t), which contains a counterexample for each sequent in S', then, since S is a subset of S', this scenario contains also a counterexample for each sequent in S.

Case 7. None of the above cases hold for S. Hence, for every sequent (S₁, S₂) in S the following hold:

1) If A&B in S₁, then A in S₁ and B in S₁,

2) If A&B in S₂, then A in S₂ or B in S₂,

3) If AvB in S₁, then A in S₁ or B in S₁,

4) If AvB in S₂, then A in S₂ and B in S₂,

5) If A->B in S₁, then A in S₂ or B in S₁,

6) If A->B in S₂, then there is (T₁, T₂) in S such that S_1<=T₁ and A in T₁ and B in T₂.

For this kind of sequent sets we have a very simple situation:

a) If, in some sequent (S₁, S₂) in S the sets S₁, S₂ contain the same formula A, then from L₆: A->AvB we can derive easily that [L₁-L₈, MP]: S₁ |- vS₂.

b) If the sets S₁, S₂ are disjoint for all sequents (S₁, S₂) in S, then we must (and will) build a scenario, containing a counterexample for each sequent in S.

So, let us suppose that the sets S₁, S₂ are disjoint for all sequents (S₁, S₂) in S, and let us define the following Kripke scenario (b, <=, t):

b = S,

x<=y must be defined for every two members x, y of b, i.e. for every two sequents (S₁, S₂) and (T₁, T₂) in S. Let us define (S₁, S₂) <= (T₁, T₂), iff S₁ <= T₁. Of course, <= is a partial ordering of b.

t must be a monotonic mapping from members of b to sets of atomic formulas. Let us define t(S₁, S₂) as the set of all atomic formulas in S₁. Of course, t is monotonic for <=. (And, of course, f - our atomic "false", never belongs to t(S₁, S₂)).

Thus, (b, <=, t) is a Kripke scenario. Let us prove that it contains a counterexample for each sequent in S. In fact, we will prove that for each sequent (S₁, S₂) in S, and each formula F:

If F in S₁, then (S₁, S₂) |= F.

If F in S₂, then not (S₁, S₂) |= F.

This will mean that, (S₁, S₂) represents a counterexample for (S₁, S₂).

Of course, our proof will be by induction along the structure of the formula F.

a) F is an atomic formula.

If F in S₁, then F in t(T₁, T₂) for every (T₁, T₂) in S such that (S₁, S₂)<=(T₁, T₂). Hence, (S₁, S₂) |= F.

If F in S₂, then, since S₁ and S₂ are disjoint sets, F not in S₁, and F not in t(S₁, S₂), i.e. not (S₁, S₂) |= F.

b) F is A&B.

If F in S₁, then, by (1), A in S₁ and B in S₁. Hence, by induction assumption, (S₁, S₂) |= A and (S₁, S₂) |= B, i.e., by Exercise 4.4.3, (S₁, S₂) |= A&B.

If F in S₂, then, by (2), A in S₂ or B in S₂. If A in S₂, then, by induction assumption, not (S₁, S₂) |= A, i.e., by Exercise 4.4.3, not (S₁, S₂) |= A&B. If B in S₂ - the argument is similar.

c) F is AvB.

If F in S₁, then, by (3), A in S₁ or B in S₁. If A in S₁, then, by induction assumption, (S₁, S₂) |= A, i.e., by Exercise 4.4.3, (S₁, S₂) |= AvB. If B in S₁ - the argument is similar.

If F in S₂, then, by (4), A in S₂ and B in S₂. By induction assumption, not (S₁, S₂) |= A and not (S₁, S₂) |= B, i.e., by Exercise 4.4.3, not (S₁, S₂) |= AvB.

d) F is A->B.

d1) F in S₁. We must prove that (S₁, S₂) |= A->B, i.e. that (T₁, T₂) |= A->B for each (T₁, T₂) in S such that (S₁, S₂)<=(T₁, T₂). So, let us assume that not (T₁, T₂) |= A->B, i.e. that (U₁, U₂) |= A and not (U₁, U₂) |= B for some (U₁, U₂) in S such that (T₁, T₂)<= (U₁, U₂).

Since A->B in S1, A->B also in U₁, and, by (5), A in U₂ or B in U₁. By induction assumption, this means that (not (U₁, U₂) |= A or (U₁, U₂) |= B. Contradiction, hence, (S₁, S₂) |= A->B.

d2) F in S₂. We must prove that not (S₁, S₂) |= A->B, i.e. that there is (T₁, T₂) in S such that (S₁, S₂)<=(T₁, T₂) and (T₁, T₂) |= A and not (T₁, T₂) |= B.

Since A->B in S₂, by (6), there is (T₁, T₂) in S such that (S₁, S₂)<=(T₁, T₂) and A in T₁ and B in T₂. By induction assumption, this means that (T₁, T₂) |= A and not (T₁, T₂) |= B. Q.E.D.

This completes the proof of Theorem 4.4.6.

Note. The above proof contains an algorithm allowing to find, for each set S of sequents, either a constructive proof of some sequent of S, or a Kripke scenario containing counterexamples for each sequent of S.

Corollary 4.4.7. If a formula F is true at all nodes in all scenarios, then [L₁-L₁₀, MP] |- F (i.e. F is provable in the constructive propositional logic).

Indeed, let us consider the set of sequents {(0, {F})} consisting of a single sequent (0, {F}), where 0 is empty set. By Theorem 4.4.6, either the sequent (0, {F}) is constructively provable, or there is a Kripke scenario (b, <=, t), which contains a counterexample for (0, {F}). Since F is true at all nodes in all Kripke scenarios, it cannot have counterexamples; hence, the sequent (0, {F}) (i.e. the formula F) is constructively provable.

Together with Lemma 4.4.3 this Corollary implies the above Theorem 4.4.2 - Kripke's theorem on the completeness of the constructive propositional logic: a formula F is true at all nodes in all Kripke scenarios, iff F is provable in the constructive propositional logic.

Corollary 4.4.8 (S.C.Kleene(?), decidability of the constructive propositional logic). There is an algorithm allowing to determine for any formula F, is this formula provable in the constructive propositional logic [L₁-L₁₀, MP], or not.

Corollary 4.4.9. If FvG is true at all nodes in all scenarios, then F is true at all nodes in all scenarios, or G is true at all nodes in all scenarios.

Proof. Assume, there is a scenario (b₁, <=₁, t₁) such that x₁ |= F is false for some x₁ in b₁, and a scenario (b₂, <=₂, t₂) such that x₂ |= G is false for some x₂ in b₂. We may assume that the (node) sets b₁ and b₂ do not intersect. Let us merge these scenarios by adding a new common starting node x₀, where all B_i are false. Then, x₀ |= F is false (Lemma 4.4.1), and x₀ |= G is false (similarly). Hence, according to the classical disjunction truth table, x₀ |= FvG is false. But, x |= FvG is always true. Hence, x |= F is always true, or x |= G is always true. Q.E.D.

Theorem 4.4.10. (Goedel [1932]). If [L₁-L₁₀, MP]: |- BvC, then [L₁-L₁₀, MP]: |- B or [L₁-L₁₀, MP]: |- C. (If the disjunction BvC is constructively provable, then one of the formulas B, C also is constructively provable.)

Proof. If [L₁-L₁₀, MP]: |- BvC, then, by Kripke's Completeness Theorem 4.4.2, BvC is true at all nodes in all scenarios. Then, by Corollary 4.4.9, so is B or so is C. By Kripke's Completeness Theorem 4.4.2, this means that one of the formulas B, C is constructively provable. Q.E.D.

Let us recall the constructive interpretation of disjunction from Section 1.3:

- To prove BvC constructively, you must prove B, or prove C. To prove BvC classically, you may assume BvC as a hypothesis, and derive a contradiction. Having only such a "negative" proof, you may be unable to determine, which part of the disjunction BvC is true - B, or C, or both.

According to Theorem 4.4.10, the constructive propositional logic [L₁-L₁₀, MP] supports the constructive interpretation of disjunction.

K.Goedel established this fact in 1932:

K.Goedel. Zum intuitionistischen Aussagenkalkuel. Akademie der Wissenschaften in Wien, Mathematisch- naturwissenschaftliche Klasse, Anzeiger, 1932, Vol.69, pp.65-66.

Exercise 4.4.5. (For smart students). By adding the schema (B->C)v(C->B) to the axioms of the constructive logic, we obtain the so-called Goedel-Dummett logic. Verify, that a propositional formula F is provable in Goedel-Dummett logic, iff F is true at all nodes in all linear Kripke scenarios (i.e. in the scenarious that do not allow branching). See also Intuitionistic Logic by Joan Moschovakis in Stanford Encyclopedia of Philosophy, and Michael Dummett in The Internet Encyclopedia of Philosophy.

Back to title page