ファイル置き場 Sendai Logic Homepage speaker10

Some conservative extension results of classical

logic over intuitionistic logic

Hajime Ishihara

School of Information Science

Japan Advanced Institute of Science and Technology Nomi, Ishikawa 923-1292, Japan

Workshop on Proof Theory and Computability Theory 2012 March 20 – 23, 2012

Contents

◮ Minimal, intuitionistic and classical logics

◮ _{The G¨}odel-Gentzen negative translation

◮ The conservative extension result with respect to negative formulas

◮ Leivant’s conservative extension result

◮ A variant of the G¨odel-Gentzen translation

◮ Another conservative extension result

◮ Intuitionistic and classical sequent calculi

◮ Some conservative extension results based on the sequent calculi

◮ Concluding remarks (Orevkov’s result)

Language

◮ We use the standard language of (many-sorted) first-order predicate logic based on

◮ (individual) variables v0, v1, . . .;

◮ n-ary predicate (relation) symbols R₀ⁿ, R₁ⁿ, . . .;

◮ n-ary function symbols f₀ⁿ, f₁ⁿ, . . .;

◮ (individual) constants c0, c1, . . .;

◮ primitive logical operators ∧, ∨, →, ⊥, ∀, ∃.

◮ We introduce the abbreviations ¬A ≡ A → ⊥ and A ↔ B ≡ (A → B) ∧ (B → A).

◮ Terms and formulas are defined as usual.

◮ The set of free variables in a formula A is denoted by FV(A).

Minimal logic

The deduction

A

has the assumption A and the conclusion A. D1

A ^DB² A ∧ B ^∧I

A ∧ BD A ^∧Er

A ∧ BD B ^∧El DA

A ∨ B ^∨Ir DB A ∨ B ^∨Il

D1

A ∨ B [A] D2

C [B] D3

C

C ^∨E

[A] DB A → B ^→I

D1

A → B ^DA²

B ^→E

Minimal logic

DA

∀yA[x/y ] ^∀I

∀xAD A[x/t] ^∀E A[x/t]D

∃xA ^∃I

D1

∃yA[x/y ] [A] D2

C

C ^∃E

◮ In ∀E and ∃I, t must be free for x in A.

◮ In ∀I, D must not contain assumptions containing x free, and y ≡ x or y 6∈ FV(A).

◮ _{In ∃E, D2} must not contain assumptions containing x free except A, x 6∈ FV(C ), and y ≡ x or y 6∈ FV(A).

Minimal logic

We denote by

Γ ⊢_mA

that there is a deduction in minimal logic with the conclusion A and the assumptions in Γ.

Example (minimal logic)

[¬¬(A → B)]

[¬¬A] [¬B]

[A → B] [A]

B ^→E

⊥ ^→E

¬A ^→I

⊥ ^→E

¬(A → B) ^→I

⊥ ^→E

¬¬B ^→I

¬¬A → ¬¬B ^→I

¬¬(A → B) → (¬¬A → ¬¬B) ^→I

Intuitionistc logic

Intuitionistic logic is obtained from minimal logic by adding the intuitionistic absurdity rule:

D⊥ A ^⊥i We denote by

Γ ⊢_i A

that there is a deduction in intuitionistic logic with the conclusion A and the assumptions in Γ.

Note that

Γ ⊢_mA ⇒ Γ ⊢_i A.

Example (intuitionistic logic)

[¬¬A → ¬¬B]

[¬(A → B)]

[¬A] [A]

⊥ B ^⊥i A → B

⊥

¬¬A

¬¬B

[¬(A → B)]

[B] A → B

⊥

¬B

⊥

¬¬(A → B)

(¬¬A → ¬¬B) → ¬¬(A → B)

Classical logic

Classical logic is obtained from intuitionistic logic by strengthening the absurdity rule to theclassical absurdity rule:

[¬A] D⊥

A ^⊥c We denote by

Γ ⊢_c A

that there is a deduction in classical logic with the conclusion A and the assumptions in Γ.

Note that

Γ ⊢_i A ⇒ Γ ⊢_c A.

Examples (classical logic)

[¬¬A] [¬A]

⊥ ^→E

A ^⊥c

¬¬A → A ^→I

[¬(A ∨ ¬A)]

[¬(A ∨ ¬A)]

[A] A ∨ ¬A ^∨Ir

⊥ ^→E

¬A ^→I A ∨ ¬A ^∨Il

⊥ ^→E

A ∨ ¬A ^⊥c

The G¨odel-Gentzen negative translation

Definition

The G¨odel-Gentzen negative translation (·)^g on the formulas of predicate logic is defined inductively by

◮ _⊥^g _{≡ ⊥;}

◮ _P^g ≡ ¬¬P for P atomic;

◮ _{(A ∧ B)}^g _{≡ A}^g _{∧ B}^g_;

◮ _{(A ∨ B)}^g _{≡ ¬(¬A}^g _{∧ ¬B}^g_);

◮ _{(A → B)}^g _{≡ A}^g _{→ B}^g_;

◮ _(∀xA)^g _{≡ ∀xA}^g_;

◮ _(∃xA)^g _{≡ ¬∀x¬A}^g_.

The G¨odel-Gentzen negative translation

Lemma

⊢mA^g ↔ ¬¬A^g. Proof.

By induction on the complexity of A. Proposition

If Γ ⊢_c A, then Γ^g ⊢m ^{Ag, where Γg = {Bg} | B ∈ Γ}. Proof.

By induction on the height of deduction tree.

The G¨odel-Gentzen negative translation

.... A ∨ B

[A].. C..

[B].. C..

C ^∨E

is translated into

....

¬¬C^g → C^g

.... (A ∨ B)^g

[¬C^g] [A^g]

.... C^g

⊥

¬A^g

[¬C^g] [B^g]

.... C^g

⊥

¬B^g

¬A^g ∧ ¬B^{g ∧I}

⊥

¬¬C^g C^g

The G¨odel-Gentzen negative translation

[¬A]..

⊥.. A ^⊥c is translated into

....

¬¬A^g → A^g

[¬A^g] ....

⊥

¬¬A^{g →I}

A^{g →E}

Negative formulas

Definition

We define the class N of negative formulas as follows. Let P range over atomic formulas distinct from ⊥, and N and N^′ over N . Then N is inductively generated by the clause

⊥, ¬P, N ∧ N^′, ∀xN, N → N^′∈ N .

Lemma

If N ∈ N , then ⊢mN ↔ N^g. Proof.

By induction on the definition of N .

The conservative extension result

Theorem

If Γ ⊆ N and A ∈ N , then Γ ⊢_c A implies Γ ⊢_m A. Proof.

Suppose that Γ ⊆ N and A ∈ N . Then Γ ⊢_m B^g for each B ∈ Γ and A^g ⊢mA by Lemma. Therefore, if Γ ⊢_c A, then Γ^g ⊢m^Ag,

and so Γ ⊢m A.

Leivant’s conservative extension result

Definition

We define simultaneously classes S (spreading), W (wiping) and I (isolating) of formulas as follows. Let P range over atomic

formulas distinct from ⊥, S and S^′ over S, W and W^′ over W, and I and I^′ over I. Then S, W and I are inductively generated by the clauses

◮ ⊥, P, S ∧ S^′, S ∨ S^′, ∀xS, ∃xS, I → S ∈ S;

◮ _{⊥, W ∧ W}′, ∀xW , S → W ∈ W;

◮ P, W , I ∧ I^′, I ∨ I^′, ∃xI , S → I ∈ I. Note that

N ⊆ S ∩ W ∩ I.

Leivant’s conservative extension result

Proposition

◮ If A ∈ S, then ⊢_i A → A^g;

◮ If A ∈ W, then ⊢i A^g → A;

◮ If A ∈ I, then ⊢i A^g → ¬¬A. Proof.

By simultaneous induction on the definition of S, W and I.

Leivant’s conservative extension result

Theorem (Leivant 1985)

If Γ ⊆ S and A ∈ W, then Γ ⊢c A implies Γ ⊢i A. Proof.

Suppose that Γ ⊆ S and A ∈ W. Then Γ ⊢i B^g for each B ∈ Γ and A^g ⊢i A by Proposition. Therefore, if Γ ⊢c A, then Γ^g ⊢mA^g, and so Γ ⊢_i A.

A variant of the G¨odel-Gentzen translation

We introduce

◮ the symbol “∗” as a special proposition letter (a place holder);

◮ an abbreviation ¬_∗A ≡ A → ∗. Definition

The ∗-negative translation (·)^∗ on the formulas of predicate logic is defined by A^∗≡ A^g[⊥/∗], that is,

◮ _⊥∗ _{≡ ∗;}

◮ _P∗ _{≡ ¬}

∗^¬∗P for P atomic;

◮ _{(A ∧ B)}∗ _{≡ A}∗_{∧ B}∗_;

◮ _{(A ∨ B)}∗ _{≡ ¬}

∗^(¬∗^{A∗∧ ¬}∗^B∗);

◮ _{(A → B)}∗_{≡ A}∗_{→ B}∗_;

◮ _(∀xA)∗_{≡ ∀xA}∗_;

◮ _(∃xA)∗_{≡ ¬}

∗^∀x¬∗^A∗.

A variant of the G¨odel-Gentzen translation

Lemma

⊢m^A∗↔ ¬_∗¬_∗A^∗. Proof.

Note that ⊥ is treated as an arbitrary proposition letter in minimal logic and A^∗↔ ¬_∗¬_∗A^∗ ≡ (A^g ↔ ¬¬A^g)[⊥/∗]. Since

⊢mA^g ↔ ¬¬A^g, we have ⊢m A^∗↔ ¬_∗¬_∗A^∗. Proposition

If Γ ⊢c A, then Γ^∗ ⊢mA^∗, where Γ^∗ = {B^∗ | B ∈ Γ}. Proof.

Since Γ^∗≡ Γ^g[⊥/∗] and A^∗ ≡ A^g[⊥/∗], if Γ ⊢c A, then Γ^g ⊢mA^g, and hence Γ^∗⊢m A^∗.

Another conservative extension result

Definition

We define simultaneously classes Q, R, J and K of formulas as follows. Let P range over atomic formulas distinct from ⊥, Q and Q^′ over Q, R and R^′ over R, J and J^′ over J , and K and K^′ over K. Then Q, R, J and K are inductively generated by the clauses

◮ ⊥, P, Q ∧ Q^′, Q ∨ Q^′, ∀xQ, ∃xQ, J → Q ∈ Q;

◮ _{⊥, R ∧ R}′_{, R ∨ R}′, ∀xR, J → R ∈ R;

◮ ⊥, P, J ∧ J^′, J ∨ J^′, ∃xJ, R → J ∈ J ;

◮ _{J, K ∧ K}′, ∀xK , Q → K ∈ K.

Another conservative extension result

Proposition

◮ If A ∈ Q, then ⊢_i A → A^∗;

◮ If A ∈ R, then ⊢i ¬_∗¬A → A^∗;

◮ If A ∈ J , then ⊢i A^∗→ ¬_∗¬_∗A. Proof.

By simultaneous induction on the definition of Q, R and J .

Another conservative extension result

A set Γ of formulas is closed under (·)^∗ if Γ ⊢_i A^∗[∗/C ] for each A ∈ Γ and C being free for ∗ in A^∗.

Theorem (I 2000)

If Γ is a set of formulas closed under (·)^∗ and A ∈ K, then Γ ⊢_c A implies Γ ⊢_i A.

Proof.

By induction on the definition of K. Suppose that Γ ⊢_c A and A ∈ J . Then Γ^∗ ⊢mA^∗, and hence Γ^∗⊢i ¬_∗¬_∗A. Therefore Γ^∗[∗/A] ⊢i (¬_∗¬_∗A)[∗/A] ≡ (A → A) → A, and, since Γ is closed under (·)^∗, we have Γ ⊢_i A.

Corollary

If Γ ⊆ Q and A ∈ K, then Γ ⊢_c A implies Γ ⊢_i A.

Application (Barr’s theorem)

Definition

We define classes G and G_I of geometric formulas and geometiric implications, respectively, as follows. Let P range over atomic formulas distinct from ⊥, G and G^′ over G and GI over GI. Then G and GI are inductively generated by the clauses

◮ ⊥, ⊤, P, G ∧ G^′, G ∨ G^′, ∃xG ∈ G;

◮ _{G → G}′_{, ∀xG} I ∈ GI, where ⊤ ≡ ⊥ → ⊥.

Theorem (Barr’s thoerem)

If Γ ⊆ GI and A ∈ GI, then Γ ⊢c A implies Γ ⊢i A. Proof.

Note that G ⊆ Q ∩ J , and hence G_I ⊆ Q ∩ K.

Application (first-order arithmetic)

Theorem

If A ∈ K, then PA ⊢ A implies HA ⊢ A. Proof.

The axioms and the axiom schema of the first-order arithmetic are closed under (·)^∗.

Corollary

PAis conservative over HA with respect to Π⁰₂ formulas, and, moreover, the following form of formulas.

∀x[∀u1∃v1. . . ∀un∃vn(s(~u, ~v , x) = 0) → ∃y (t(x, y ) = 0)].

Proof.

Π⁰₂ formulas and the formulas of the above form are in K.

Application (first-order arithmetic)

Moreover, we can extend the class R (and hence the classes J , Q and K) by the clause

⊥,P, R ∧ R^′, R ∨ R^′, ∀xR, J → R ∈ R, because, for atomic P, since HA ⊢ P ∨ ¬P, we have HA_{⊢ ¬}

∗^{¬P → P∗}, and the following proposition holds for the extended classes in HA.

Proposition

◮ If A ∈ Q, then HA ⊢ A → A^∗;

◮ If A ∈ R, then HA ⊢ ¬_∗¬A → A^∗;

◮ If A ∈ J , then HA ⊢ A^∗→ ¬_∗¬_∗A.

Schwichtenberg’s question

Helmut Schwichtenberg has asked about a possibility of extending the classes R and J , defined by the clauses

◮ _{⊥, R ∧ R}′_{, R ∨ R}′, ∀xR, J → R ∈ R;

◮ ⊥, P, J ∧ J^′, J ∨ J^′, ∃xJ, R → J ∈ J ,

by introducing ∃ and ∀ in the clauses, respectively, to the classes R0 and J0, defined by

◮ _{⊥, R ∧ R}′_{, R ∨ R}′_{, ∀xR,∃xR}, J → R ∈ R0;

◮ ⊥, P, J ∧ J^′, J ∨ J^′,∀xJ, ∃xJ, R → J ∈ J₀.

Intuitionistic sequent calculus G3i

P, Γ ⇒ P ^Ax ⊥, Γ ⇒ A L⊥

A, B, Γ ⇒ C A ∧ B, Γ ⇒ C ^L∧

Γ ⇒ A Γ ⇒ B Γ ⇒ A ∧ B ^R∧ A, Γ ⇒ C B, Γ ⇒ C

A ∨ B, Γ ⇒ C ^L∨

Γ ⇒ A

Γ ⇒ A ∨ B ^R∨1

Γ ⇒ B

Γ ⇒ A ∨ B ^R∨2 A → B, Γ ⇒ A B, Γ ⇒ C

A → B, Γ ⇒ C ^L→

A, Γ ⇒ B Γ ⇒ A → B ^R→ where in Ax, P is atomic.

Intuitionistic sequent calculus G3i

∀xA, A[x/t], Γ ⇒ C

∀xA, Γ ⇒ C ^L∀

Γ ⇒ A[x/y ] Γ ⇒ ∀xA ^R∀ A[x/y ], Γ ⇒ C

∃xA, Γ ⇒ C ^L∃

Γ ⇒ A[x/t] Γ ⇒ ∃xA ^R∃ where in R∀, y 6∈ FV(Γ), y ≡ x or y 6∈ FV(A), and in L∃, y 6∈ FV(Γ, C ), y ≡ x or y 6∈ FV(A).

We denote by

⊢i ^{Γ ⇒ A}

that there is a deduction of the sequent Γ ⇒ A in G3i. Note that

⊢i Γ ⇒ A if and only if Γ ⊢_i A.

Classical sequent calculus G3c

P, Γ ⇒ ∆, P ^Ax ⊥, Γ ⇒ ∆ L⊥

A, B, Γ ⇒ ∆ A ∧ B, Γ ⇒ ∆ ^L∧

Γ ⇒ ∆, A Γ ⇒ ∆, B Γ ⇒ ∆, A ∧ B ^R∧ A, Γ ⇒ ∆ B, Γ ⇒ ∆

A ∨ B, Γ ⇒ ∆ ^L∨

Γ ⇒ ∆, A, B Γ ⇒ ∆, A ∨ B ^R∨ Γ ⇒ ∆, A B, Γ ⇒ ∆

A → B, Γ ⇒ ∆ ^L→

A, Γ ⇒ ∆, B Γ ⇒ ∆, A → B ^R→ where in Ax, P is atomic.

Classical sequent calculus G3c

∀xA, A[x/t], Γ ⇒ ∆

∀xA, Γ ⇒ ∆ ^L∀

Γ ⇒ ∆, A[x/y ] Γ ⇒ ∆, ∀xA ^R∀ A[x/y ], Γ ⇒ ∆

∃xA, Γ ⇒ ∆ ^L∃

Γ ⇒ ∆, A[x/t], ∃xA Γ ⇒ ∆, ∃xA ^R∃ where in R∀ and L∃, y 6∈ FV(Γ, ∆), y ≡ x or y 6∈ FV(A). We denote by

⊢c ^{Γ ⇒ ∆}

that there is a deduction of the sequent Γ ⇒ ∆ in G3c. Note that

⊢c Γ ⇒ A if and only if Γ ⊢c A.

Positive and negative occurrences

◮ C occurs positively in C ;

◮ if C occurs positively and negatively in A or in B, then C occurs positively and negatively, respectively, in A ∧ B and in A ∨ B;

◮ if C occurs negatively in A or positively in B, and positively in A or negatively in B, then C occurs positively, and negatively, respectively, in A → B;

◮ if C occurs positively and negatively in A, then C occurs positively and negatively, respectively, in ∀xA and in ∃xA.

Strictly positive occurrences

◮ C occurs strict positively in C ;

◮ if C occurs strict positively in A or in B, then C occurs strict positively in A ∧ B and in A ∨ B;

◮ if C occurs strict positively in B, then C occurs strict positively in A → B;

◮ if C occurs strict positively in A, then C occurs strict positively in ∀xA and in ∃xA.

Some conservative extension results

Lemma

If ⊢i ∗ⁿ, Γ, ¬_∗∆ ⇒ A, where ∗ⁿstands for n copies of ∗, and ∗ does not occur in Γ negatively nor positively in A, then ⊢_i Γ ⇒ A. Proof.

By induction on the depth of a deduction of

⊢i ∗ⁿ, Γ, ¬_∗∆ ⇒ A. Lemma

If ⊢_i Γ, ¬_∗A[x/y ], ¬_∗∆ ⇒ ∗, where ∗ does not occur in the antecedent negatively, there is no strictly positive occurrence of ∀ in Γ, and y 6∈ FV(Γ), y ≡ x or y 6∈ FV(A), then

⊢i ^{Γ, ¬}∗^{∀xA, ¬}∗^{∆ ⇒ ∗.}

Proof.

By induction on the depth of a deduction of

⊢i ^{Γ, ¬}∗^{A[x/y ], ¬}∗^{∆ ⇒ ∗.}

Some conservative extension results

Lemma

If ⊢_i Γ, ¬_∗A, ¬_∗∆ ⇒ ∗, where ∗ does not occur in the antecedent negatively, and there is no strictly positive occurrence of ∨ in Γ, then either ⊢_i Γ ⇒ A, or ⊢_i Γ, ¬_∗∆ ⇒ ∗.

Proof.

By induction on the depth of a deduction of

⊢i ^{Γ, ¬}∗^{A, ¬}∗^{∆ ⇒ ∗.}

Corollary

If ⊢_i Γ, ¬_∗A[x/y ], ¬_∗∆ ⇒ ∗, where ∗ does not occur in the antecedent negatively, there is no strictly positive occurrence of ∨ in Γ, and y 6∈ FV(Γ), y ≡ x or y 6∈ FV(A), then

⊢i ^{Γ, ¬}∗^{∀xA, ¬}∗^{∆ ⇒ ∗.}

Some conservative extension results

Definition

We define simultaneously classes R₀, J₀, Q_m and K_m (m = 1, 2) of formulas as follows. Let P range over atomic formulas distinct from ⊥ and ∗, R and R^′ over R0, J and J^′ over J0, Qm and Q_m^′ over Q_m, and K_m and K_m^′ over K_m (m = 1, 2). Then R0, J0, Q_m and Km (m = 1, 2) are inductively generated by the clauses

◮ _{⊥, R ∧ R}′_{, R ∨ R}′, ∀xR, ∃xR, J → R ∈ R₀;

◮ ⊥, P, J ∧ J^′, J ∨ J^′, ∀xJ, ∃xJ, R → J ∈ J0;

◮ _{P, R, Q1∧ Q}′

1^{, Q1∨ Q}1^{′, ∃xQ1, J → Q1∈ Q1;}

◮ _{P, R, Q2∧ Q}′

2^{, ∀xQ2, ∃xQ2, J → Q2 ∈ Q2;}

◮ _{J, Km∧ K}′

m^{, ∀xKm, Qm→ Km ∈ Km} (m = 1, 2).

Some conservative extension results

Proposition

If either Γ ⊆ Q1 or Γ ⊆ Q2, ∆ ⊆ R0 and Σ ⊆ J0, then

⊢cΓ, ∆ ⇒ Σ implies ⊢_i Γ, ¬_∗¬∆, ¬_∗Σ ⇒ ∗. Proof.

By induction on the depth of a deduction of ⊢_c Γ, ∆ ⇒ Σ.

Some conservative extension results

Theorem (I 2011)

For each m = 1, 2, if Γ ⊆ Q_m and A ∈ K_m, then ⊢_c Γ ⇒ A implies

⊢i Γ ⇒ A. Proof.

By induction on the definition of K_m.

Suppose that A ∈ J0 and ⊢c Γ ⇒ A. Then ⊢i Γ, ¬_∗A ⇒ ∗, by Proposition. Therefore, since A is free for ∗ in Γ, ¬_∗A, ∗, we have

⊢i Γ, A → A ⇒ A, and so ⊢i Γ ⇒ A.

Concluding remarks (Orevkov’s result)

Theorem (Orevkov 1968)

If Γ ⊆ O_k⁻and A ∈ O_k⁺ (k = 1, . . . , 7), then Γ ⊢_c A implies Γ ⊢_i A.

Concluding remarks (Orevkov’s result)

We define classes O⁻_k and O_k⁺ (k = 1, . . . , 7) of formulas as follows. Let P range over atomic formulas distinct from ⊥, X_k and X_k^′ over O⁻_k and Y_k and Y_k^′ over O⁺_k (k = 1, . . . , 7). Then O_k⁻ and O⁺_k are inductively generated by the clauses

1. {→⁺, ¬⁺, ∀⁺}.

◮ _{⊥, P, X}

1∧ X₁^′, X1∨ X₁^′, ∀xX1, ∃xX1, Y1→ X1∈ O⁻₁ ⊆ Q;

◮ _{⊥, P, Y}

1∧ Y₁^′, Y1∨ Y₁^′, ∃xY1∈ O⁺₁ ⊆ J ⊆ K. 2. {→⁺, ¬⁺, ∨⁻}.

◮ _{⊥, P, X}

2^{∧ X}2^{′, ∀xX}2, ∃xX2, Y2^{→ X}2^{∈ O−}₂ ^{⊆ Q}2;

◮ _{⊥, P, Y}

2^{∧ Y}2^{′, Y}2^{∨ Y}2^{′, ∀xY}2, ∃xY2^{∈ O+}2 ^{⊆ J}0^{⊆ K}2. 3. {→⁺, ¬⁺, ∀⁻}.

◮ _{⊥, P, X}

3∧ X₃^′, X3∨ X₃^′, ∃xX3, Y3→ X3∈ O⁻₃ ⊆ Q1;

◮ _{⊥, P, Y}

3∧ Y₃^′, Y3∨ Y₃^′, ∀xY3, ∃xY3∈ O⁺₃ ⊆ J0⊆ K1.

Concluding remarks (Orevkov’s result)

4. {→⁻, ¬⁻, ∨⁺, ∃⁺}.

◮ _{⊥, P, X}

4∧ X₄^′, X4∨ X₄^′, ∀xX4, ∃xX4∈ O⁻₄ ⊆ Q;

◮ _{⊥, P, Y}

4∧ Y₄^′, ∀xY4, X4→ Y4∈ O₄⁺⊆ K. 5. {→⁻, ¬⁻, ∨⁺, →⁺, ∀⁺}.

◮ _{⊥, P, X}

5∧ X₅^′, X5∨ X₅^′, ∀xX5, ∃xX5∈ O⁻₅;

◮ _{⊥, P, Y}

5∧ Y₅^′, ∃xY5, ¬X5∈ O₅⁺. 6. {→⁻, ¬⁻, ∨⁺, →⁺, ∨⁻}.

◮ _{⊥, P, X}

6∧ X₆^′, ∀xX6, ∃xX6∈ O₆⁻;

◮ _{⊥, P, Y}

6∧ Y₆^′, ∀xY6, ∃xY6, ¬X6∈ O⁺₆. 7. {→⁻, ¬⁻, ∨⁺, →⁺, ∀⁻}.

◮ _{⊥, P, X}

7^{∧ X}7^{′, X}7^{∨ X}7^{′, ∃xX}7^{∈ O−}₇;

◮ _{⊥, P, Y}

7^{∧ Y}7^{′, ∀xY}7, ∃xY7, ¬X7^{∈ O+}₇.