1 GL - A Gent Zen Sequent Calculus for Classical Propositional Logic

We present here a proof system GL for the classical Propositional logic that is a version of the original Gent Zen systems LK.

We give a constructive of the completeness theorem for the system GL. The proof is very similar to the proof of the completeness theorem for the system RS.

The axioms, the rules of inference of the system GL operate, as in the original system LK, on expressions called by Gent Zen sequents, hence the name Gent Zen sequent calculus.

Language of GL

We adopt a Propositional language L = L_{{È,
Ç, Þ , ¬ }} with the set of formulas denoted by F and we add a new symbol

¾®

called a Gent Zen arrow, to it. As the next step we build expressions called sequents. The sequents are built out of finite sequences (empty included) of formulas, i.e. elements of F^*, and the additional sign ¾® .

We denote , as in the RS system, the finite sequences of formulas by Greek capital letters G , D , S , with indices if necessary. We define a sequent as follows.

Sequent

For any G , D Î F^*, the expression

G ¾® D

is called a sequent. G is called the antecedent of the sequent, D is called the succedent, and each formula in G and D is called a sequent-formula.

We denote the sequents by the letter S, with or without subscripts.

Meaning of sequents

Intuitively, a sequent A₁ ,..., A_n ¾® B₁ ,..., B_m (where n,m ³ 1) means: if A₁ Ç ... Ç A_n then B₁ È ... È B_m .

The sequent A₁ ,..., A_n ¾® (where n ³ 1) means that A₁ Ç ... Ç A_n yields a contradiction.

The sequent ¾® B₁ ,..., B_m (where m ³ 1) means that B₁ È ... È B_m holds.

The empty sequent ¾® means that there is a contradiction.

Given non empty sequences G, D, we denote by

any conjunction of all formulas of G, and by

any disjunction of all formulas of D .

The intuitive meaning of a sequent G ¾® D (where G, D are nonempty) is hence that, whatever is the semantics, it is logically equivalent to the formula (s _G Þ d _D) , i.e.

G ¾® D º (s

Þ d

Formal semantics for sequents

Formally, let v: VAR ¾® {T, F } be a Boolean truth assignment, v^* its extension to the set of formulas F. We extend v^* to the set SEQ = { G ¾® D : G , D Î F^* } of all sequents as follows: for any sequent G ¾® D Î SEQ,

(G ¾® D ) = v

) Þ v

) .

In the case when G = Ø or D = Ø we define:

( ¾® D ) = T Þ v

) ,

( G ¾® ) = v

) Þ F.

Model

The sequent G ¾® D is satisfiable if there is a truth assignment v: VAR ¾® {T, F } such that v^*(G ¾® D )= T. Such a truth assignment is called a model for G ¾® D . We write

v |= G ¾® D

to denote that v is a model for G ¾® D .

Counter- model

The sequent G ¾® D is falsifiable if there is a truth assignment v, such that v^*(G ¾® D )= F. In this case v is called a counter-model for G ¾® D and we write it as

v ¬ |= G ¾® D .

Tautology

The sequent G ¾® D is a tautology if v^*(G ¾® D )= T for all truth assignments v: VAR ¾® {T, F } and we write

|= G ¾® D

to denote that G ¾® D is a tautology.

example

Let G ¾® D be a sequent

a, (b Ç a) ¾® ¬ b, (b Þ a) .

The truth assignment v for which v(a) = T and v(b) = T is a model for G ¾® D , as shows the following computation.

v^*( a, (b Ç a) ¾® ¬ b, (b Þ a) ) = v^*(s _{{a, (b Ç a)}} ) Þ v^*(d _{{¬ b, (b Þ a)}} ) = v(a) Ç ( v(b) Ç v(a) ) Þ ¬ v(b) È (v(b) Þ v(a)) = T Ç T cap T Þ ¬ T È (T Þ T ) = T Þ (F È T) = T Þ T = T.

Observe that the only v for which v^*(G) = v^*( a, (b Ç a) = T is the above v(a) = T and v(b) = T that is a model for G ¾® D . Hence it is impossible to find v which would falsify it, what proves that G ¾® D is a tautology, i.e.

|= a, (b Ç a) ¾® ¬ b, (b Þ a) .

The Proof System GL

The rules of inference of GL are of the form:

S₁

S₁ ; S₂

where S₁ , S₂ and S are sequents. S₁ , S₂ are called premises and S is called the conclusion of the rule of inference.

Each rule of inference introduces a new logical connective to the antecedent or to the succedent of the conclusion sequent. We denote the rule that introduces the logical connective ° to the antecedent of the conclusion sequent S by ( ° ®). The notation ( ® ° ) means that the logical connective is introduced to the succedent of the conclusion sequent S.

As our language contains the connectives: Ç , È, Þ and ¬ , we are going to adopt the following inference rules: (Ç ® ) and (® Ç ), (È ® ) and (® È ), (Þ ® ) and (® Þ ), and finally, (¬ ® ) and (® ¬ ).

Axioms of GL

As the axioms of GL we adopt any sequent which contains a formula that appears on both sides of the sequent arrow ¾® , i.e. any sequent of the form

G₁, A, G₂ ¾® D₁, A, D₂ , (1)

for any formula A Î F and any sequences G₁,G₂, D₁, D₂ Î F^*.

Inference rules of GL

We denote by G ^', D ^' finite sequences formed out of literals i.e. out of Propositional variables or negations of Propositional variables. G , D denote any finite sequences of formulas.

The inference rules of GL are defined as follows.

Conjunction rules

(Ç ® )

G ^', A, B, G ¾® D ^'

G ^', (A Ç B ), G ¾® D ^'

, ( ® Ç)

G ¾® D , A,D ^' ; G ¾® D , B,D ^'

G ¾® D , (A Ç B ), D ^'

Disjunction rules

(® È)

G ¾® D , A, B, D ^'

G ¾® D , (A È B), D ^'

, ( È ® )

G ^', A, G ¾® D ^' ; G ^', B, G ¾® D ^'

G ^', (A È B), G ¾® D ^'

Implication rules

(® Þ)

G ^' , A, G ¾® D , B, D ^'

G ^' , G ¾® D , (A Þ B), D ^'

, ( Þ ® )

G ^', G ¾® D , A, D ^' ; G ^', B, G ¾® D , D ^'

G ^', (A Þ B), G ¾® D , D ^'

Negation rules

(¬ ® )

G ^', G ¾® D , A, D ^'

G ^', ¬ A, G ¾® D ,D ^'

, ( ® ¬)

G ^' , A, G ¾® D ,D ^'

G ^' , G ¾® D ,¬ A , D ^'

Formally we define:

GL = ( SEQ, AX , (È ), (¬ È ), (Ç ), (¬ Ç ), (Þ ), (¬ Þ ),(¬ ¬ ))

where SEQ = { G ¾® D : G , D Î F^* } , (È ), (¬ È ), (Ç ), (¬ Ç ), (Þ ), (¬ Þ ),(¬ ¬ ) are the inference rules defined above and AX is the axiom of the system defined by the schema X.

We define the notion of a formal proof in GL as in any proof system, i.e., by a formal proof of a sequent G ¾® D in the proof system GL we understand any sequence

G₁ ¾® D ₁ , G₂ ¾® D ₂ , .... , G_n ¾® D _n

of sequents of formulas (elements of SEQ, such that G₁ ¾® D ₁ Î AX, G_n ¾® D _n = G ¾® D , and for all i (1 <i £ n) G_i ¾® D _i Î AX, or G_i¾® D _i is a conclusion of one of the inference rules of GL with all its premises placed in the sequence G₁ ¾® D ₁ , .... G_i-1 ¾® D_i-1 .

We write, as usual,

G ¾® D

to denote that G ¾® D has a formal proof in GL, or we write simply

|- G ¾® D

when the system GL is fixed.

We say that a formula A Î F, has a proof in GL and denote it by |-_GL A if the sequent ¾® A has a proof in GL, i.e. we define:

A iff ¾® A . (2)

We write, however, the formal proofs in GL in a form of proof trees rather then in a form of sequences.

Proof trees

A proof tree, or GL-proof of G ¾® D is a tree T_{G ¾® D} of sequents satisfying the following conditions:

1. The topmost sequent, i.e. the root of T_{G ¾® D} is G ¾® D ,

2. the leafs are axioms,

3. the nodes are sequents such that each sequent on the tree follows from the ones immediately preceding it by one of the rules.

We picture, and write our proof-trees with the node on the top, and leafs on the very bottom, instead of more common way, where the leafs are on the top and root is on the bottom of the tree.

In particular cases we will write our proof- trees indicating additionally the name of the inference rule used at each step of the proof.

For example, the tree-proof (in GL) of the de Morgan law ( ¬ ( a Ç b) Þ (¬ a È ¬ b )) is the following.

¾® (¬ (a Ç b ) Þ (¬ a È ¬ b ))

| (¾® Þ )

¬ (a Ç b) ¾® (¬ a È ¬ b )

| (¾® È )

¬ (a Ç b) ¾® ¬ a , ¬ b

| (¾® ¬ )

b, ¬ (a Ç b) ¾® ¬ a

| (¾® ¬ )

b, a, ¬ (a Ç b) ¾®

| (¬ ¾® )

b, a ¾® (a Ç b)

Ù ( ¾® Ç )

b, a ¾® a b, a ¾® b

Soundness of GL

It is an easy exercise to verify that the axiom and the rules of inference of GL are sound, i.e. that the following theorem holds.

Theorem 1.1 [Soundness of GL] For any sequent G ¾® D Î SEQ,

if |-

G ¾® D then |= G ¾® D .

In particular, following the definition X we get the following.

Theorem 1.2 [Formula Soundness of GL] For any formula A Î F,

if |-

A then |= A.

Completeness of GL

There are the following two completeness theorems for GL. The second, called formula completeness theorem is a particular case of the first theorem.

Theorem 1.3 [Completeness Theorem] For any sequent G ¾® D Î SEQ,

G ¾® D iff |= G ¾® D .

Following the definition X we get, as a particular case of the above the following theorem.

Theorem 1.4 [Formula Completeness Theorem] For any formula A Î F,

A iff |= A.

The proof of the Completeness Theorem is similar to the proof for the RS system and can be assigned as an exercise.

This document was translated from L^AT_EX by H^EV^EA.