1 Proof Systems - Introduction

Proof systems are built to prove theorems. They can be thought as an inference machine with theorems being its final products and a starting point called axioms of the system, called also logical axioms. The inference machine is defined by a finite set of rules, called inference rules. They describe the way we are allowed to transform the information within the system. The process of building theorems can be depicted as follows:

AXIOMS

¯ ¯ ¯

RULES applied to AXIOMS

¯ ¯ ¯

THEOREMS

¯ ¯ ¯

RULES applied to all what is above

¯ ¯ ¯

NEW THEOREMS

¯ ¯ ¯

. . etc. .

We give here a general definition of a proof system and discuss its most important properties.

2 Basic Definitions

When defining a proof system S we specify, as the first step, the language L we work with. It can be a Propositional language, but it can be any other formal language.

Language L of S: Usually, as in the Propositional case, the language L consists of its alphabet A and a set of expressions, denoted here by F , i.e.
L = ( A , F ).
We assume that the both sets A and F are enumerable, i.e. we will deal here with enumerable languages only.

The set F usually denotes the set of well formed formulas, of the language L , but it denotes sometimes a set of all finite sequences of formulas, or sets of formulas, or other expressions, called Gentzen sequent, or sets of clauses in the case of the resolution based systems. This is the reason to call F the set of expressions rather then the set of formulas.

Expressions F: We assume, besides that F is enumerable, that it primitively recursive i.e. that there is an effective procedure to determine whether a given expression is in F .

The proof system acts as an inference machine, with theorems being its final products. This inference machine is defined by first setting, as a starting point a certain non-empty, proper subset AX of F , called a set of axioms of the system S.

Axioms AX of S: We assume that the axioms AX of S form a proper, non-empty subset of the set F of expressions of our language. Moreover, the set AX is primitively recursive i.e. there is an effective procedure to determine whether a given expression A Î F is in AX or not.

The production of theorems is to be done by the means of inference rules. The inference rules transform an expression, or finite string of expressions, called premises, into another expression, called conclusion. At this stage the rules don't carry any meaning - they define only how to transform strings of symbols of our language into another string of symbols. This is a reason why the proof system investigations are often called syntactic methods as opposed to semantic methods, which deal with the meaning of the language.

Rules of inference R: We assume that a proof system contains only a finite number of inference rules. The set of rules of inference is denoted by R. Additionally, we assume that each rule has a finite number of premises and one conclusion, i.e. is defined by a certain relation, which assigns a single expression, called conclusion, to a finite string of expressions, called its premises. Moreover, we also assume that one can effectively decide, for any rule, whether a given string of expressions form its premises and conclusion or not, i.e. that all relations r Î R are primitively recursive.

Formally, we assume that for each r Î R, there is a number m, called the number of premises of r, such that r is a relation defined in F^m with values in F, i.e.

r Í F^m × F

and all r Î R are primitively recursive relations.

If r Í F^m × F and (P₁ , ..., P_m , A) Î r, then P₁ , ..., P_m will be called the premises of r and A its conclusion.

We usually write the inference rules in a following convenient way. If r is a one premises rule then we write it as

(r)

where A is a premise, and B is a conclusion of r.

If r is a two premises rule, then we write it as

(r)

P₁ ; P₂

where P₁ , P₂ are the premises of r and A is its conclusion. P₁ is called a left premise of r and P₂ is called a right premise.

If r is a three premises rule, then we write it accordingly as

(r)

P₁ ; P₂ ; P₃

where P₁ , P₂, P₃ are the premises of r and A is its conclusion.

In general, if r is an m- premises rule, then we will write it as

(r)

P₁ ; P₂ ; .... ; P_m

where P₁ , P₂, ..., P_m are the premises of r and A is its conclusion.

Now we are ready to define formally a proof system.

Proof system S: By a proof system we understand a triple
S = ( L , AX, R ),
where

L = { A , F } is a formal language, called the language of S.

AX is called a set of axioms of the system. It is a non-empty, proper, primitively recursive subset of the set of expressions F .

R is a finite set of rules of inference and all r Î R are primitively recursive relations.

The theorems of the system are the final product of single or multiple use of the inference rules, with axioms taken as a starting point. A single use of an inference rule is called a direct consequence, a multiple application of rules of inference i.e. a process of constructing a theorem is called a proof. We hence introduce the following notions.

Direct consequence: A conclusion of a rule of inference is called a direct consequence of its premises. I.e. for any rule of inference r, if P₁ ,... P_n and A are in the relation described by r, then the expression A is called a direct consequence of the expressions P₁ ,... P_n by virtue of r.
Proof of A in S: A proof of an expression A in a proof system S is a sequence
A₁ ,... A_n
of expressions, such that, A_n is A and for each i, 1 £ i £ n , either A_i is an axiom of the system or A_i is a direct consequence of some of the preceding expressions by virtue of one of the rules of inference.

We write

|- _S A

to denote that A has a proof in S. When the proof system S is fixed we often write simply

|- A .

Theorem of S

Any expression A such that A has o proof in S, i.e.

is called a theorem of S.

The set of all theorems of S is denoted by Th_S, i.e.

Th_S = { A Î F : |- _S A } .

In order to prove theorems, we often use some extra information available, besides the axioms of the proof system. To describe formally this process we introduce the notions of a proof from a given set of expressions.

Proof of A from G in S: Given a set G of expressions of a proof system, by a proof of A from G we will understand a proof where the expressions from G are added to the set AX of the axioms of the system.

Formally, a proof of A from G is a sequence

A₁ ,... A_n

of expressions, such that A_n is A and for each i, 1 £ i £ n , either A_i is an axiom of the system, or A_i is in G , or A_i is a direct consequence of some of the preceding expressions by virtue of one of the rules of inference. We write

G |- _S A

to denote that A has a proof from G in S and

G |- A ,

when the system S is fixed.

Specific axioms

If G |- _S A then the expressions of G are called specific axioms or hypotheses of the proof of A from G .

Finite G

If G is a finite set and G = { B₁ , B₂ , ... , B_n }, then we write

B₁ , B₂ , ... , B_n |-

instead of { B₁ , B₂ , ... , B_n } |- _S A .

Empty G

The case of G = Ø is a special one. By the definition of a proof of A from G , Ø |- A means that in the proof of A only axioms AX of S were used. We hence write

|- _S A

to denote that A has a proof from empty G .

Consequence of G: If G |- _S A then A is called a consequence of G in S.

The above notion that A is a consequence of G determines a consequence operation Cn_S which to every set G Ì F , assigns a set of all its consequences. I.e. for any G Ì F we define its set of all consequences Cn _S(G ) as follows.

Cn _S(G ) = { A Î F : G |- _S A }.

Formally, we define the consequence operation as follows.

Consequence operation in S

Given a proof system S = ( L , AX, R). A function

_S : 2

¾® 2

such that for every G Î 2^F

Cn _S(G ) = { A Î F : G |- _S A }

is called the consequence operation in S. We remind that 2^F denotes a set of all subsets of F.

The consequence operation Cn _S has the following properties.

Monotonicity: For any sets G , D of expressions of S,

if G Ì D then Cn _S(G ) Ì Cn _S(D ).

The monotonicity is often expressed as a fact that adding new information (specific axioms) to the system do not invalidate old theorems.

Transitivity: For any sets G ₁ , G ₂ ,G ₃ of expressions of S,

if G ₁ Ì Cn _S(G ₂ ) and G ₂ Ì Cn _S(G ₃ ), then G ₁ Ì Cn _S(G ₃ ).

The transitivity property is often stated in the following way: if A is a consequence of a set D , such that all elements of D are consequences of G , then A is also a consequence of G .

Finiteness: For any expression A Î F and any set G Ì F,

A Î Cn _S(G ) if and only if there is a finite subset G ₀ of G such that A Î Cn _S(G ₀ ).

The proofs are included in the Problems section.

Formalized theory S(G ): A system
S(G ) = ( L , AX, G , R )
is called a formalized theory based on a proof system S = ( L , AX, R ), with the set of specific axioms G and the set of logical axioms AX.
Theorems of S(G ): Given a formalized theory S(G ), any A such that G |- _S A is called a theorem of S(G ) .

The set of all theorems of S(G ) is denoted by Th_S(G ). By definition, Th_S(G ) = Cn_S(G ). In particular,

Th_S = Th_S(Ø ) = Cn_S(Ø )

and for any set G Ì F,

Th_S Ì Th_S(G ) .

Even if the set of axioms and the inference rules of the proof system are primitively recursive it doesn't mean that the notion of "theorem" is also primitively recursive, i.e. that there always will be an effective, mechanical method (effective procedure) for determining, given any expression A of the system, whether there is a proof of A.

Decidable system: A proof system, for which there is a mechanical method for determining, given any expression A of the system, whether there is a proof of A, is called decidable; otherwise it is undecidable.

A decidable proof system is, roughly speaking, one for which a machine can be advised to test its expressions for theoremhood, whereas, in an undecidable theory, ingenuity is required to determine whether the expressions are theorems.

Observe that the above notion of decidability of the system does not require to find a proof, it requires only a mechanical procedure of deciding whether there is a proof of any expression of the system.

The proof system such that a mechanical procedure of finding proofs for its expressions will be called syntactically decidable, i.e. we introduce the following notion.

Syntactically decidable system: A proof system, for which there is a mechanical method for determining, given any expression A of the system, not only whether there is a proof of A, but also of finding such a proof, is called syntactically decidable; otherwise it is syntactically undecidable.

A Hilbert style proof system for classical Propositional logic is an example of a decidable, but not syntactically decidable proof system.

The Gentzen and Resolution style proof systems for classical Propositional logic are the examples of both decidable and syntactically decidable proof systems.

2.1 Proof systems and formal proofs - Definitions

We will define now formally the notions introduced intuitively in the previous sections and establish notations to be used later in the book.

Definition 2.1 [Proof System]

By a proof system we will understand a triple

S = ( L , AX , R)

where

Language: L is called a language of the system. It consists of an alphabet A and a set F of expressions formed out of elements of A . Both sets are non-empty and enumerable. Moreover, we assume that the both sets A and F are primitively recursive.
Axioms: AX is called a set of axioms of the system. It is a non-empty, proper subset of the set of expressions F . We also assume that AX is primitively recursive, i. e. we can always decide whether a given expression is in AX or not.
Rules: R is a finite set of rules of inference. We assume that for each r Î R, there is a number m, called the number of premises of r, such that r is a relation defined in F^m with values in F.

If r Í F^m × F and (P₁ , ..., P_m , A) Î r, then P₁ , ..., P_m will be called the premises of r and A its conclusion.

A will be also called a direct consequence of P₁ ,... P_m by virtue of r.

We assume additionally that all r Î R are primitively recursive relations.

The proof systems are design to prove theorems. Proving theorems means generating their proofs. We will define now a formal notion of a proof.

Formal proof of A in S

Given a proof system S = ( L , AX, R). By a formal proof of an expression A of the language L in S we will understand any sequence

A₁ , .... , A_n

of expressions of L such that

A₁ Î AX,
A_n = A ,
and for all i, 1 < i £ n, either A_i Î AX, or A_i is a direct consequence of some of the preceding expressions by virtue of one of the rules of inference.

If for an expression A of L there is a formal proof in a proof system S = ( L , AX , R), then it will be denoted by

When the proof system S is fixed, we will write simply

|- A

to denote that A has a proof (is provable) in a given system.

Theorem of S

Any A such that

will be called a theorem of S .

Set of theorems of S

The set of all theorems of the system S will be denoted by Th_S , i.e.

= { A: |-

A }.

Given a proof system S = ( L , AX , R), we will write the inference rules in a more convenient way, namely if r is a one premise rule i.e. r Í F × F, then we will write it as

(r)

where A is a premise, and B is a conclusion of r.

If r is a two premises rule i.e. r Í F² × F, then we will write it as

(r)

P₁ ; P₂

where P₁ , P₂ are the premises of r and A is its conclusion. P₁ is called a left premise of r and P₂ is called a right premise.

If r is a three premises rule i.e. r Í F³ × F, then we will write it as

(r)

P₁ ; P₂ ; P₃

where P₁ , P₂, P₃ are the premises of r and A is its conclusion.

In general, if r is an m- premises rule i.e. r Í F^m × F, then we will write it as

(r)

P₁ ; P₂ ; .... ; P_m

where P₁ , P₂, ..., P_m are the premises of r and A is its conclusion.

2.2 Some examples

As we have mentioned in the introduction, at this stage we haven't assigned yet any meaning to the axioms and inference rules of the proof systems. The rules of inference in proof systems define only how to transform strings of symbols of our language into another string of symbols. The definition of a formal proof says that in order to prove a theorem of a system one has to construct of s sequence of proper transformations, defined by the rules of inference.

The meaning of this process will be given by a semantics for the system. In the next section we will describe this process and and then we will discuss what kind of properties we want the proof system to have to assure that for example all we prove is true, or that we can always prove all we know to be true.

Example 2.1 (System S₁)

Let S₁ be the following proof system:

S₁ = ( L

{ P, Þ }

, (A Þ A ), (r)

where A, B are any formulas of the Propositional language L _{{ P, Þ }}.

Observe that even the system S₁ has only one axiom, it represents an infinite number of formulas. We call such an axiom axiom schema.

The following system S₂, even if it looks very much alike the system S₁, will produce, as we will see, a different set of theorems.

Example 2.2 (System S₂)

Let S₂ be the following proof system:

S₂ = ( L

{ P, Þ }

, (a Þ a ), (r)

where a Î VAR and B is any formulas of the Propositional language L _{{ P, Þ
}}.

Observe that for example a formula (( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))) is of the form A Þ A for A being (Pa Þ ( b Þ c)), and hence is an axiom of S₁, but is not an axiom of the system S₂, as this systems permits axioms of the form: (a Þ a ) for a being a Propositional variable.

Here are some examples of theorems and formal proofs in both systems.

Of course,

S₁

( ( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c)))

and the axiom

(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c)))

forms a formal proof of itself in S₁.

The formulas P(a Þ a), and PP(a Þ a) are theorems of both, S₁ and S₂, i.e.
|- P(a Þ a),

|- PP(a Þ a

for S₁ and S₂.

The formal proofs in both systems of above formulas are identical and are as follows.

The formal proof of P(a Þ a) in S₁ and S₂ is:

(a Þ a),	P(a Þ a).
axiom	rule application
	for B=(a Þ a)

The formal proof of PP(a Þ a) in S₁ and S₂ is:

(a Þ a),	P(a Þ a),	PP(a Þ a).
axiom	rule application	rule application
	for B=(a Þ a)	for B=P(a Þ a)

3. The formula PP(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))) is a theorem of S₁ i.e.

S₁

PPP(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))),

but it is not a theorem of S₂, i.e.

¬ |-

S₁

PPP(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))).

The formal proof of PPP(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))) in S₁ is:

(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))),	P(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))) ,
axiom	rule r application

PP(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))),	PPP(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))).
rule r application	rule r application

Let's now search for a proof of our formula in S₂. If it had the proof, the only last step in this proof would be the application of the rule r to the formula PP(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))) . This formula, in turn, if it had the proof, the only last step in its proof would be the application of the rule r to the formula P(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))) . And again, this one could be obtained only from the formula (( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))) by the virtue of the rule r. Here the search process stops; the rule r puts P in front of the formulas, hence couldn't be applied here. The formula (( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))) isn't an axiom of S₂, what means that the only possible way of finding the proof has failed, i.e. we have proved that ¬ |-_S₁ PPP(( Pa Þ ( b Þ c)) Þ (Pa Þ ( b Þ c))).

The above procedure is an effective, automatic procedure of searching for a proof of our formula in both our proof systems. If the search ends with an axiom, we have a proof, if it doesn't end with an axiom it means that the proof does not exist. We have described it, as an example, for one particular formula. It can be easely extended to any formula A of L _{{
P, Þ }} by the re-iteration of the following steps. Check the main connective of A. If it is P, it means that A was obtained by the rule r, so we erase the main connective P. If the main connective is Þ , it means that there were no applications of r, so we have a proof if A is an axiom, and the proof does not exist, otherwise. This proves the following.

Fact 2.1 Proof systems S₁ and S₂ are syntactically decidable.

Observe also, that the systems S₁ and S₂ are such that we can easely describe the general form of their theorems, namely we have the following.

S₁

= { Pⁿ(A Þ A ): n Î N, A Î F },

S₂

= { Pⁿ(a Þ a ): n Î N, a Î VAR },

where Pⁿ denotes n-iteration of P.

Obviously we have that Th_S₁¹ Th_S₂, and Th_S₂Ì Th_S₁.

The proof systems S₁ and S₂ are very simple, indeed. Here is an example of another two, slightly more complex proof systems.

Example 2.3 (Systems S₃ and S₄) Consider two proof systems S₃ and S₄ of the language L _{{ È , ¬ }} with the set F of all formulas, defined as follows;

S₃ = ( L

{ È , ¬ }

, (A È ¬ A) ,

B È (A È ¬ A)

, for any A, B Î F)

S₄ = ( L

{ È , ¬ }

, (A È ¬ A) ,

(A È ¬ A)

B È (A È ¬ A)

, for any A, B Î F).

Describe the sets of theorems of S₃ and S₄.

Do they produce the same sets of theorems? I.e. is it true/ false that

{ A: |-

S₃

A } = { A: |-

S₄

A }?

If yes, prove it, if not give a formula which is a theorem of one system and is not a theorem of other system.

Are the systems S₃ and S₄ syntactically decidable?

Let's first describe the set of theorems of both systems.

System S₃

Obviously, |- _S₃ (A È ¬ A). One application of the inference rule gives us the proof of ((A È ¬ A) È (A È ¬ A)). The next application of the rule (to the already produced formula) will give us the proof of (((A È ¬ A) È (A È ¬ A)) È (A È ¬ A)). It is easy to see that all theorems of S₃ will be of the form af the disjunction of the axiom of S₃, what we denote as follows:

S₃

= { È _n (A È ¬ A)ⁿ: n Î N, A Î F },

where È _n(A È ¬ A)ⁿ denotes a disjunction of n formulas of the form (A È ¬ A).

System S₄

Obviously, as before, |- _S₄ (A È ¬ A). One application of the inference rule gives us the proof of (B È (A È ¬ A)), where B is a certain formula from F. The rule can't be, by its definition, applied to already produced theorem (except for a theorem which is the axiom), so the multiple application of the rule means application to the axiom and producing all possible formulas of the form (B È (A È ¬ A)), where B's are different for different applications. Hence

S₄

={ (B È (A È ¬ A)): A, B Î F } È { (A È ¬ A): A Î F }.

Theorems of S₃ and S₄

Obviously, Th_S₃ Í Th_S₄, as we have, by definition, that È _n (A È ¬ A)ⁿ = È _n-1(A È ¬ A)^n-1 È (A È ¬ A) and È _n-1 (A È ¬ A)^n-1 is a formula of L _{{ È
, ¬ }} . We can denote it by B. I.e. we have proved that any theorem of S₃ is an axiom or has a form (B È (A È ¬ A)) for a certain B Î F.

The formula ((a È ¬ b) È (a È ¬ a)) has a proof in S₄, i.e.

S₄

((a È ¬ b) È (a È ¬ a)),

but obviously

¬ |-

S₃

((a È ¬ b) È (a È ¬ a)).

The above proves that

S₃

Í Th

S₄

and Th

S₃

¹ Th

S₄

Syntactically decidable

It follows immediately form the form of the sets Th_S₃ and Th_S₄ that both systems are syntactically decidable. The design of the proper proof searching procedure is left to the reader as an exercise.

The following natural questions arise.

Q1: Are all proof systems syntactically decidable ?
Q2: Can we give an example of a simple proof system which would not be syntactically decidable, but would be decidable? (Where "simple " means for example, a system with only one rule of inference, and say, one or two axiom).

The answers are straightforward: no, not all the systems are syntactically decidable, moreover, as we will see, the most "natural" and historically first developed proof systems for classical logic were not syntactically decidable. They are however, in a case of Propositional logic, decidable, but the proof of their decidability, as we will see later, is neither obvious nor straightforward.

Hilbert Systems These system contain a Modus Ponens rule as a rule of inference, and are usually called Hilbert style formalizations. We will call them here Hilbert style proof systems, or Hilbert systems, for short.

Modus Ponens is probably the oldest of all known rules of inference as it was already known to the Stoics (3rd century B.C.). It is also considered as the most "natural" to our intuitive thinking and historically the proof systems containing it as the inference rule play a special role in logic. Their emphasis is on logical axioms, keeping the rules of inference to minimum, often admitting only Modus Ponens, as the sole inference rule.

Here is an example of a simple proof system based on a language with implication as the only connective, with two axioms (axiom schemas) which characterize the implication, and with Modus Ponens as a sole rule of inference.

Example 2.4 (Hilbert System H₁)

Let H₁ be the following proof system:

H₁ = ( L

{ Þ }

, A1, A2, MP )

where A1, A2 are axioms of the system, MP is its rule of inference, called Modus Ponens, defined as follows:

A1

(A Þ ( B Þ A)),

A2

((A Þ ( B Þ C )) Þ ((A Þ B) Þ (A Þ C ))),

MP

(MP)

A ; (A Þ B)

and A, B, C are any formulas of the Propositional language L _{{ Þ }}.

Finding formal proofs in this system requires some ingenuity. Let's construct, as an example, the formal proof of such a simple formula as aÞ a.

The formal proof of (a Þ a) in H₁ is a sequence

B₁ , B₂ , B₂ , B₂ , B₅

as defined below.

B₁ = ((a Þ ( a Þ a)) Þ ((a Þ (a Þ a) ) Þ (a Þ a)))),	B₂ = (aÞ ( a Þ a)),
axiom A2 for A=a, B= (a Þ a), and C=a	axiom A1 for A=a, B=a

B₃ = ((a Þ ( a Þ a) ) Þ (a Þ a))),	B₄ = (aÞ ( a Þ a)),
MP application to B₁ and B₂	axiom A1 for A=a, B=a

B₅ = (a Þ a)

MP application to B₃ and B₄

If we replace a variable a by an arbitrary formula A Î F in the above formal proof, we will obtain the formal proof of (A Þ A) , for an arbitrary A Î F, i.e.

H₁

(A Þ A)

for any A Î F.

It is easy to see that the above proof wasn't construct automatically. The main step in its construction was the choice of a proper form (substitution) of logical axioms to start with. This choice is far from obvious for un-experienced prover.

Generate proof from axioms: If we wanted to find a procedure which would generate automatically a proof for a given formula from the axioms of the system, we would have to consider, in the first step an infinite number of all possible formulas of the form of the axioms A₁ and A₂ to start with and hence this method would be far from being decidable.

Observe that our all previous systems S₁ - S₄ were syntactically decidable for one simple reason. Their inference rules were such that it was possible to "reverse" them; to use them in the reverse manner in order to search proofs, and to be able to do so in a blind, fully automatic way. I.e. we were able to conduct an argument of the type: "if this formula has a proof that the only way to construct it was from such and such formula by the means of our inference rule, and that formula is given automatically."

We will see now, that one can't apply the the above argument to the proof systems which contain Modus Ponens as an inference rule.

Search for proof by the means of MP: Let's now see how it would be possible to search for a proof of a given formula B backward. It means let's assume that B is a conclusion of the inference rule, find its premises. If they are axioms, the proof is found. If at least one is not axiom, it would mean that it is in turn, a conclusion of the rule, so we find its premises and continue this process as long as the formal proof, it means we stop on axioms everywhere, is found. Our inference rule is the Modus Ponens. The rule says: given two formulas A and (A Þ B) we can write then down a formula B.

Assume now that we have a formula B and want to find its proof. If it is an axiom, we have the proof- the formula itself. If it is not an axiom, it had to be obtained by the application of the Modus Ponens rule, to certain two formulas A and (A Þ B). But there is infinitely many of those formulas - all we know about them, that to find a proof of B, or they both have to be axioms (it means have a form of the axioms A1 or A2) or, if not, they had to be obtained, in their turn, from the application of Modus Ponens to some pairs of formulas C, ( C Þ A) and D, ( D Þ (A Þ B)), respectively. Here again, there is infinite (enumerably infinite) number of such formulas. We continue until the proof is found, i.e. until all formulas found have the form of axioms A₁ or A₂.

Obviously, this procedure is also far from being automatically decidable and hence we have the following.

Fact 2.2 The proof system H₁ is not syntactically decidable.

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