# PHIL30043 Power and Limits of Logic

##### von Brendan Hill 06/07/2017

## PHIL30043 Power and Limits of Logic

von Brendan Hill## 1. Godel's Incompleteness

### 1.1. Godel numbering

1.1.1. Definition

1.1.1.1. A relationship between natural numbers and statements such that

1.1.1.1.1. 1) Every statement has a unique number

1.1.1.1.2. 2) The Godel number of any statement is calculable

1.1.1.1.3. 3) It is decidable as to whether a number the Godel number of some statement (and if so what statement)

1.1.1.2. Denote ^A^ the Godel number of the expression A

### 1.2. Diagonalisation

1.2.1. Diagonalisation of a formula

1.2.1.1. Definition

1.2.1.1.1. Is sort of a function from the set of formulas to the set of formulas

1.2.1.1.2. Given a formula A (in particular with free variable x), its diagonalisation is (exists x) (x = ^A^ and A(x))

1.2.1.1.3. Equivalently, "A(^A^) is true"

1.2.1.1.4. Equivalently, "A holds true of its own Godel numer"

1.2.1.1.5. Note: The diagonalisation of a formula simply yields another formula, it is not asserting the truth of that formula!

1.2.1.2. Examples

1.2.1.2.1. Diagonalisation of "x is even"

1.2.1.2.2. Diagonalisation of "x + 0 = x"

1.2.1.2.3. Diagonalisation of "x = x+1"

1.2.2. The diagonalisation function diag(n)

1.2.2.1. Definition

1.2.2.1.1. diag(n) a function from N => N

1.2.2.1.2. If n is NOT the Godel number of some formula, just return 0

1.2.2.1.3. Otherwise, return the Godel number of the diagonalisation of that formula

1.2.2.1.4. So diag(^A(x)^) = ^"(exists x) (x=^A(x)^ and A(x)"^

1.2.2.1.5. Equivalently, diag(^A(x)^) = ^"A(^A^) is true"^

1.2.2.1.6. Equivalently, diag(^A(x)^) = ^"A holds true of its own Godel number"^

1.2.2.2. Examples

1.2.2.2.1. if n=1234 (not the Godel number of any formula)

1.2.2.2.2. if n=^"x is even"^

1.2.2.2.3. if n=^"x+0=x"^

1.2.2.3. diag(n) is recursive

1.2.2.3.1. So it is represented in Q

1.2.3. Diagonalisation Lemma

1.2.3.1. Definition

1.2.3.1.1. If diag(n) is represented in some theory T...

1.2.3.1.2. ...then for any formula B(y)...

1.2.3.1.3. ...there exists some sentence G...

1.2.3.1.4. ...such that T |- G == B(^G^)

1.2.3.2. Proof

1.2.3.2.1. Representation of diag(n) in the theory

1.2.3.2.2. Consider F, G

1.2.3.2.3. So if T represents diag(n), then for any formulat B(n), there is some statement G such that T |- G == B(^G^)

1.2.3.3. In other words....

1.2.3.3.1. If a theory represents diag(n), then for every predicate, there exists some sentence which is logically equivalent to the predicate of the Godel number of that sentence!

1.2.3.3.2. This is a bit like a "fixed point" for the predicate (although we are not asserting that this is the only fixed point)

1.2.3.3.3. Each predicate magically has some (at least one) related sentence which is logically equivalent to that predicate, fed the Godel number of that sentence, which is WEIRD

### 1.3. Definability

1.3.1. Definition

1.3.1.1. A set of numbers N is definable by a formula B(n) in theory T iff...

1.3.1.1.1. ... T |- B(n) iff n in N

1.3.1.1.2. ... T |- ~B(n) iff n not in N

1.3.2. Implications

1.3.2.1. If T is a consistent theory at least as strong as Q, then the set of theorems in T is not definable in T

1.3.2.2. Proof

1.3.2.2.1. Let T be a consistent theory at least as strong as Q

1.3.2.2.2. Denote C(y)

1.3.2.2.3. Question: does T |- G or not?

1.3.2.2.4. Either way, contradiction. Hence, C does not exist, so the set of theorems of T is not definable in T.

### 1.4. Examples of applications of Incompleteness

1.4.1. Any consistent, deductively defined extension of Q is incomplete

1.4.1.1. Since T extends Q, it does not represent its own theorems

1.4.1.2. Since T extends Q, it represents all recursive sets

1.4.1.3. So the set of theorems of T is not a recursive set

1.4.1.4. So T is not decidable

1.4.1.5. If it were complete, then it would be decidable (since consistent and DDT)

1.4.1.6. So it isn't complete!

1.4.2. Set of theorems of predicate logic is undecidable

1.4.2.1. Suppose the theorems of predicate logic were undecidable

1.4.2.2. Then, any statement of Q could be proven from axioms, simply (Q1 & Q2 & ...) => S

1.4.2.3. But Q isn't decidable!

1.4.2.4. So, predicate logic is undecidable

1.4.2.5. (eg. "Problem reduction")

1.4.3. True Arithmetic is undecidable

1.4.3.1. Since TA has a model (by definition, the standard model of arithmetic), it is consistent

1.4.3.2. Since TA is the set of all things true of the model, it is complete

1.4.3.3. Because consistent and complete, it is not DDT

1.4.3.4. Because extension of Q, it is not decidable

1.4.4. Summary

1.4.4.1. Consistent, Q-extension ==>

1.4.4.1.1. ~DefinesOwnSetOfTheorems (1)

1.4.4.1.2. DefinesAllRecursiveSets (2)

1.4.4.1.3. So ~HasRecursiveSetOfTheorems (3)

1.4.4.2. Consistent, Complete, DDT ==> HasRecursiveSetOfTheorems (4)

1.4.4.2.1. So, Consistent, DDT, Q-extension ==> Incomplete (5)

1.4.4.3. PL

1.4.4.3.1. If PL decidable then Q decidable (6)

1.4.4.3.2. But Q not decidable

1.4.4.3.3. So PL undecidable (7)

1.4.4.4. TA

1.4.4.4.1. Consistent, Complete, Q-extension

1.4.4.4.2. So DefinesAllRecursiveSets (from 2)

1.4.4.4.3. So ~DefinesOwnSetOfTheorems (from 1)

1.4.4.4.4. So ~HasRecursiveSetOfTheorems (from 3)

1.4.4.4.5. So ~DDT (from 5) (8)

1.4.4.5. So Truth in standard model of arithmetic is not recursive, and not recursively enumerable

### 1.5. Lobs theorem

1.5.1. Provability predicate

1.5.1.1. Definition

1.5.1.1.1. A predicate B in theory T such that

1.5.1.2. If T is DDT, then it the following statement is recursive:

1.5.1.2.1. "x is the Godel number of a T-proof of the statement with Godel number y"

1.5.1.3. So B(y) = (exists x)P(x,y) says that there exists a proof of y

1.5.2. Implications

1.5.2.1. If T proves that a proof of A implies A... then T proves A

1.5.2.1.1. If diagonalisation lemma holds for T, and there is a provability predicate B for T...

1.5.2.1.2. ...then...

1.5.2.1.3. ... T |- B(^y^) => y implies that T |- y

1.5.2.2. Godels Second Incompleteness Theorem

1.5.2.2.1. if B is a provability predicate for T

1.5.2.2.2. And diagonalisation lemma holds for T

1.5.2.2.3. And T is consistent

1.5.2.2.4. Then T does not prove that ~B(^1=0^)

1.5.2.2.5. Ie. T cannot prove its own consistency

1.5.3. Proof

1.5.3.1. Too complicated lol

## 2. Computability

### 2.1. Definition

2.1.1. (This wasn't really presented as a theorem in lecture notes)

2.1.2. The set of recursive functions is exactly the set of functions computable by register machines

2.1.3. Equivalently, for Turing-machines, and other formulations

### 2.2. Proof

2.2.1. ==> Any recursive function can be implemented as a register machine

2.2.1.1. Zero: has a simple register machine with a single instruction

2.2.1.2. Succ: has a simple register machine with a single instruction

2.2.1.3. Identity: has a simple register machine with a few instructions

2.2.1.4. Cn[]: just chain the relevant register machines together

2.2.1.5. Pr[]: simple put in a bigger register machine which decrements counter and repeats etc

2.2.1.6. Mn[]: simply put in a bigger register machine which increments counter, checks condition and halts

2.2.2. <== Any register machine can be represented as a recursive function

2.2.2.1. Represent the state of the register machine as a number

2.2.2.1.1. Prime number theorem: STATE(S,A,B,C....) === 2^S * 3^A * 5^B * 7^C etc

2.2.2.1.2. The machine has halted when S=0, so when STATE is odd

2.2.2.2. Produce primitive recursive function which calculates the state of the register machine at step number N

2.2.2.2.1. Function accepting x1,x2,....xm,n

2.2.2.2.2. Pr(takestep, n)

2.2.2.2.3. takestep defined by conditions where coefficients are 0 if case does not match instruction, 1 if case does match instruction

2.2.2.2.4. Each instruction in the register machine is simply multiplication, exponentiation, etc!

2.2.2.3. Produce minimisation function to calculate the step number at which it halts (if any)

2.2.2.3.1. Given the STATE value, return s (extracted from p0^s)

2.2.2.3.2. When s=0, RM has halted, and minimisation has terminated

2.2.2.3.3. If s never is 0, the RM never halts, and the minimisation is undefined

2.2.2.4. Produce primitive function to extract the output number from the state at the final step

2.2.2.4.1. Given the minimisation function finding the value of y such that the RM halts

2.2.2.4.2. Call the Pr(takestep,y) function, divide repeated by 3, the number of times we divide by 3 is the final output.

2.2.3. What it means

2.2.3.1. Register machines and recursive functions pick out exactly the same set of calculations/computations

2.2.3.2. Fun fact: any recursive function can be rewritten to use only a single minimisation function!

### 2.3. Incomputability Incalculability

2.3.1. Definition

2.3.1.1. There are functions which are incomputable/incalculable

2.3.2. Proof: direct appeal to cardinalities

2.3.2.1. There are countably many recursive functions/register-machines/turing-machines/pick your favourite

2.3.2.2. However there are uncountably many functions

2.3.2.2.1. Eg. consider that each function has a "characteristic bitstream", and every bitstream characterizes some function

2.3.2.2.2. There are uncountably many bitstreams

2.3.2.2.3. So there are uncountably many functions

2.3.2.3. Therefore the are functions which are non-recursive/not-register-machine-computable/not-turing-machine-computable/etc

2.3.3. Examples

2.3.3.1. Diagonalisation of total recursive functions

2.3.3.1.1. Idea: within the set of total functions, any enumeration of total recursive functions will miss some total functions

2.3.3.1.2. Define f*

2.3.3.1.3. Suppose f* was recursive

2.3.3.1.4. Therefore f* is non-recursive

2.3.3.2. Halting problem

2.3.3.2.1. The Idea: If we assume that the halting problem is Turing-computable, then we can derive a contradiction. Hence, the halting problem is not Turing-computable.

2.3.3.2.2. Proof

2.3.3.3. Busy Beaver function

2.3.3.3.1. The Idea

2.3.3.3.2. Proof

## 3. Compactness

### 3.1. Definition

3.1.1. Positive formulation

3.1.1.1. X has a model <=> Every finite subset X' has a model

3.1.1.2. Equivalently: X is satisfiable if and only iff every finite subset X' is satisfiable

3.1.2. Negative formulation

3.1.2.1. X doesn't have a model <=> Some finite subset X' doesn't have a model

3.1.2.2. Equivalently: X is unsatisfiable if and only if some finite subset X' is unsatisfiable

3.1.3. Due to equivalent between |= and |- (soundness and completeness) we can say the same for trees

### 3.2. Proof

3.2.1. X is consistent => [All] X' is consistent

3.2.1.1. Clearly, if X has a model M, then every finite subset X' has a model - obviously M, if nothing else.

3.2.1.2. Equivalently, if [Exists] X' inconsistent => X is inconsistent

3.2.2. [All] X' are consistent ==> X is consistent

3.2.2.1. Instead show the contrapositive: that X is inconsistent ==> Some finite X' is inconsistent

3.2.2.2. Instead, show this contrapositive using trees, given the equivalence between |= and |-,

3.2.2.2.1. If "X |-" (ie. the tree starting with X closes), then the closed tree is finite, and every branch is closed in finite number of steps.

3.2.2.2.2. Only a finite number of statements , X', were used to produce the tree closure

3.2.2.2.3. That finite set of statements, X', is inconsistent

3.2.2.2.4. Hence there exists a finite subset X' of X, which is inconsistent

3.2.2.3. So if X is inconsistent, then some finite subset X' is inconsistent

3.2.2.4. So if all finite subsets X' are consistent, then X is consistent

3.2.2.5. True with respect to models as well as proofs, since |- <==> |=

### 3.3. Applications/consequences

3.3.1. Generally, able to show satisfiability of X without producing a complete model (just produce model for every subset)

3.3.2. Inexpressibility of finitude in FOPL

3.3.2.1. "There is no way to say that there are only finitely many things"

3.3.2.2. Sentences: X

3.3.2.2.1. "There are only finitely many things"

3.3.2.2.2. "It is not the case that there exist exactly 1 things"

3.3.2.2.3. "It is not the case that there exist exactly 2 things"

3.3.2.2.4. "It is not the case that there exist exactly 3 things"

3.3.2.2.5. etc

3.3.2.3. However any finite X' of X is satisfiable/consistent, since the first n are true of any model with n+ objects..

3.3.2.4. By compactness theorem, X is consistent, ie. satisfiable, ie. has a model

3.3.2.5. But that means it is true in some infinite models! This is a contradiction

3.3.2.6. Hence, "There are only finitely many things" cannot be expressed in FOPL

3.3.3. The consistency of infinitesimals with the reals

3.3.3.1. Statement S: There exists c such that c < 1/n for all n

3.3.3.2. Sets defined

3.3.3.2.1. Let X1 be the set of statements already true

3.3.3.2.2. Let X2 be the set of statements 0 < c < 1/1, 1/2, 1/3, ......

3.3.3.2.3. Let X be X1 + X2

3.3.3.2.4. Let X' be any finite subset of X

3.3.3.3. The statement above is true for any finite X' subset X, since we find the X2 statement with largest denominator 1/n and set x = 1/(n+1)

3.3.3.4. Since S is consistent why any finite X' subset of X, by the compactness theory, X is consistent

3.3.3.5. Hence, infinitesimals defined in this way are consistent with the reals (aka. hyperreals)

3.3.3.6. So given the standard model of the reals M, we can create a non-standard model including hyperreals, which makes the same things true!

3.3.4. Countable model theorem

3.3.4.1. Definition

3.3.4.1.1. If (finite or countably infinite) set X can be satisfied, then it can be satisfied by some finite or countably infinite domain

3.3.4.2. Proof

3.3.4.2.1. Suppose X is finite/countably-infinite set of statements which is satisfiable

3.3.4.2.2. So a branch of the tree starting with X remains open

3.3.4.2.3. This branch uses finite/countably-infinite number of names

3.3.4.2.4. So a model with finite/countably-infinite number of objects in its domain can be constructed

3.3.4.2.5. So X can be satisfied by a finite/countably-infinite model

## 4. Completeness

### 4.1. Definition

4.1.1. Positive formulation

4.1.1.1. The completeness theorem states that if an argument is valid according to models, then is valid according to the proof method.

4.1.1.2. Equivalently, if there exists no model for {X, ~A} (ie. unsatisfiable), then the argument "X |- A" is valid (according to the proof method).

4.1.1.3. Equivalently, validity in terms of models (ie. no countermodel) implies validity in terms of proof methods (ie. tree closes)

4.1.1.4. Equivalently, "|=" ==> "|-"

4.1.2. Contrapositive formulation

4.1.2.1. Equivalently, if there the proof method states that an argment is invalid, then, there exists a countermodel

4.1.2.2. Equivalently, invalidity in terms of methods (ie. existence of countermodel) implies invalidity in terms of proof methods (ie. tree remains open)

4.1.2.3. The tableaux method for PL is complete: if there is no model in which {X,~A}, then the tree starting with {X, ~A} will close.

4.1.2.4. Equivalently, "|/-" ==> "|/="

### 4.2. Examples

4.2.1. The tableaux method for FOPL is complete

## 5. Soundness

### 5.1. Definition

5.1.1. Positive formulation

5.1.1.1. The soundness property states that if an argument is valid according to a proof method, then there exists no countermodel to the argument

5.1.1.2. Equivalently, validity in terms of proof methods (ie. tree closes) implies validity in terms of models (ie. no countermodel exists)

5.1.1.3. Equivalently, "|-" ==> "|="

5.1.2. Contrapositive formulation

5.1.2.1. Equivalently, if a countermodel for the argument exists, then the proof method will show that the argument is invalid.

5.1.2.2. Equivalently, invalidity in terms of models (ie. existence of countermodel) implies invalidity in terms of proof methods (ie. tree remains open)

5.1.2.3. Equivalently, "|/=" ==> "|/-"

### 5.2. Examples

5.2.1. The tableaux proof method for PL or FOPL is sound: if a tree starting with {X, ~A} closes (Ie. X |- A), then there exists no model for {X, ~A}. Ie. validity in terms of the proof method implies validity in terms of models

## 6. Basic concepts

### 6.1. Language

6.1.1. A definition of allowable sentences?

### 6.2. Sentence

6.2.1. Properties

6.2.1.1. True or false (given a model)

6.2.1.2. Tautological

6.2.1.3. Contradictory

6.2.2. Relationships

6.2.2.1. Equivalence

6.2.2.1.1. Embeds

6.2.2.1.2. Transitive

6.2.2.1.3. Symmetric

6.2.2.1.4. Reflexive

6.2.2.2. Entailment / Implication / Consequence

6.2.2.2.1. A -> B A entails B A implies B B is a consequence of A

6.2.2.2.2. Transitive

6.2.2.2.3. Not symmetric

6.2.2.2.4. Reflexive

6.2.3. Set of sentences

6.2.3.1. Properties

6.2.3.1.1. Satisfiable / unsatisfiable

### 6.3. Argument

6.3.1. Definition

6.3.1.1. A set of premises and a conclusion

6.3.2. Properties

6.3.2.1. Valid / Invalid

6.3.2.1.1. Validity according to models

6.3.2.1.2. Validity according to proof methods

### 6.4. Model

6.4.1. An interpretation (true/false) of all atomic sentences / literals

6.4.2. Defines truth for a language

6.4.3. Cannot contain contradiction

6.4.3.1. Since interpretation function is a *function*, it returns exactly one output for each input

### 6.5. Proof method

6.5.1. Properties

6.5.1.1. Sound / unsound

6.5.1.2. Complete / incomplete

6.5.1.3. Decidability

## 7. Advanced concepts

### 7.1. Set

7.1.1. Definition

7.1.1.1. Unordered (possibility infinite) collection of distinct elements

7.1.2. Properties

7.1.2.1. Empty / Non-empty

7.1.2.2. Cardinality

7.1.2.2.1. Finite

7.1.2.2.2. Infinite

7.1.2.3. Can't contain themselves (for this course at least)

7.1.2.3.1. Must only contain "earlier defined" sets

7.1.3. Special examples

7.1.3.1. The Empty Set

7.1.3.2. Omega

7.1.3.2.1. Same cardinality as the set of natural numbers

7.1.3.2.2. Same cardinality as any countably infinite set

7.1.3.3. Set of all bitstreams

7.1.3.3.1. Uncountably infinite!

7.1.4. Recursivity of sets

7.1.4.1. Recursive set

7.1.4.1.1. Characteristic function (of a set)

7.1.4.1.2. Definition

7.1.4.2. Recursively enumerable set

7.1.4.2.1. A set such that some recursive total function e, e(0), e(1), e(2), .... enumerates the members of the set

7.1.4.2.2. (NOTE: Says nothing about non-membership of the set, in finite time... could wait forever!)

7.1.4.3. Relationships

7.1.4.3.1. A recursive set is recursively enumerable.

7.1.4.3.2. But a recursively enumerable set is not necessarily a recursive set

7.1.5. Theory

7.1.5.1. Definition

7.1.5.1.1. A set of statements closed under logical consequence

7.1.5.1.2. If T |- A, then A in T

7.1.5.2. Qualities of theories

7.1.5.2.1. Properties

7.1.5.2.2. Relationships

7.1.5.3. Ways of defining theories

7.1.5.3.1. Deductively defined theory

7.1.5.4. Examples

7.1.5.4.1. Robinson's Arithmetic (Q)

7.1.5.4.2. Peano Arithmetic (PA)

7.1.5.4.3. Truth Arithmetic

### 7.2. Function

7.2.1. Definition

7.2.1.1. A function has a domain, a range, and a mapping

7.2.1.2. Each object in the domain is mapped to exactly one object in the range

7.2.1.3. Total function

7.2.1.3.1. Definition

7.2.1.4. Partial function

7.2.1.4.1. Definition

7.2.2. Notation

7.2.2.1. Mathematical notation

7.2.2.2. Lambda notation

7.2.3. Recursive functions

7.2.3.1. Definition

7.2.3.1.1. Functions made up of specific building blocks

7.2.3.1.2. Recursive functions are either the basic functions, or functions built up via composite functions from recursive functions, and nothing else

### 7.3. Register Machine

7.3.1. Definition

7.3.1.1. Finite number of buckets

7.3.1.2. Unending supply of marbles

7.3.1.3. Instruction sets

7.3.1.3.1. [#, +/- Bucket, Next, -Next]

7.3.1.4. Input in buckets, output in first bucket (by convention)

7.3.2. Relationship to functions

7.3.2.1. A RM "computes the partial function" f if and only if; a) for every input x for which f(x) is defined, the RM outputs f(x) on that input; and b) for every input x for which f(x) is undefined, the RM never halts

7.3.2.2. Ie. it computs the partial function if it produces the correct outputs, and always halts for undefined values

### 7.4. Diagonalisation

7.4.1. Any set which is uncoutnably infinite can be diagonalised: any enumeration will miss out some members (actually, the vast majority of members)

7.4.2. Examples

7.4.2.1. Any enumeration of bitstreams which miss out the bistream with bits flipped along the diagonal

7.4.2.2. Any enumeration of real numbers will miss out the real number with digits incremented along the diagonal

7.4.2.3. Any enumeration of the characteristic bistreams of functions will miss out the characteristic bitstream of the functions which are flipped

7.4.2.4. Any enumeration of Turing machines will miss out [ TODO ]

7.4.2.5. Any enumeration of recursive functions will miss out on f*(n)=f_n(n)+1

7.4.2.5.1. If f* was in the enumeration then it is at index m

7.4.2.5.2. So f*(m)=f_m(m)+1=f*(m)+1 - contradiction!

## 8. Logics taxonomy

### 8.1. Propositional logic

8.1.1. Language

8.1.1.1. Literals

8.1.1.2. Connectives

8.1.1.2.1. And, Or, Imply, Negate

8.1.1.3. Sentences built up from these (using brackets)

8.1.2. Models

8.1.2.1. Made up of true/false values for each proposition

8.1.3. Normal forms

8.1.3.1. Disjunctive normal form

8.1.3.1.1. Not unique

8.1.3.1.2. Every statement is equivalent to something in DNF

8.1.3.1.3. Process

8.1.3.2. Conjunctive normal form / Clausal form

8.1.3.3. XOR conjunctive normal form

8.1.4. Proof methods

8.1.4.1. Tableaux

8.1.4.1.1. Process

8.1.4.1.2. Soundness of Tableaux method for FOPL

8.1.4.1.3. Completeness of Tableaux method for FOPL

8.1.4.1.4. Decidability of Tableaux method for FOPL

### 8.2. First order predicate logic

8.2.1. Language

8.2.1.1. Predicate literals Px

8.2.1.2. Connectives

8.2.1.2.1. And, Or, Imply, Negate

8.2.1.3. Quantifiers

8.2.1.3.1. Universal, existential

8.2.1.4. Sentences built up from these (using brackets)

8.2.2. Models

8.2.2.1. Non-empty domain

8.2.2.2. Interpretation (true/false) of all P(x1,x2..xn)

8.2.2.3. Interpretation of all names (from domain objects)

8.2.2.4. NOTE: "standard name" - natural, canonical name for domain objects

8.2.3. Normal forms

8.2.3.1. Prenex normal form

8.2.3.1.1. Quantifiers followed by DNF

8.2.3.1.2. Every statement in FOPL equivalent to something in Prenex

8.2.3.1.3. Process

8.2.4. Proof methods

8.2.4.1. Tableaux with quantifiers

8.2.4.1.1. ??

8.2.4.2. Hilbert proofs

8.2.4.2.1. Language

8.2.4.2.2. Process

8.2.4.2.3. Conditional proofs

8.2.4.2.4. Soundness of Hilbert proof method for FOPL

8.2.4.2.5. Completeness of Hilbert proof method for FOPL

8.2.4.2.6. Hilbert Inconsistency Definition

8.2.4.2.7. Decidability of Hilbert proof method for FOPL