Microsoft Word - Complexity_Considerations_FOL2.doc
Radosław Hofman, cSAT problem lower bound, 2007  
Abstract—This article deals with the lower bound that 
is considered as the worst case minimal amount of time 
required to calculate a problem result for cSAT (counted 
Boolean satisfiability problem). It uses the observation 
that Boolean algebra is a complete first-order theory 
where every sentence is decidable. Lower bound of this 
decidability is defined and shown. 
The article shows that deterministic calculation model 
made up of finite number of machines (algorithms), 
oracles, axioms, or predicates is incapable of solving 
considered NP-complete problem when its instance 
grows to infinity. This is a direct proof of the fact that P 
and NP complexity classes differ and oracle capable of 
solving NP-complete problems in polynomial time must 
consist of infinite number of objects (i.e., must be 
nondeterministic). 
Corollary of this article clears complexity hierarchy: 
P < NP 
Index terms—complexity class, P vs NP, Boolean 
algebra, first order theory, first order predicate calculus. 
I. INTRODUCTION 
Unknown relation between P and NP  [5] complexity 
classes remains one of the significant unsolved problems in 
complexity theory. P complexity class consists of problems 
solvable by deterministic Turing machine (DTM) in 
polynomially bounded time, while NP complexity class 
consists of problem solvable by nondeterministic Turing 
machine (NDTM) in polynomially bounded time. This means 
that DTM can verify the solution of every NP problem in 
polynomially bounded time, even if polynomial algorithm for 
finding this solution is unknown  [13]. 
All known attempts to prove whether these classes are or 
are not equal could not convince the community that 
arguments used there are final. Problem with attempts 
showing that P=NP is mainly with counter examples 
provided for methods described by solvers (see for example: 
 [6],  [9]), especially for large instances. Problem with proof 
attempts that P≠NP touches mainly the difference between a 
problem and an algorithm. Proving the inequality of these 
classes is equivalent to proving that “there is no such 
algorithm that solves a particular NP problem in 
polynomially bounded time.” Algorithm is an immaterial 
object, so proving that it does not exist is rather difficult. 
Can then the inequality of complexity classes be proved? 
One of the possible ways is to use the properties of first-order 
theory. Useful properties include every sentence ϕ in theory 
T is provable if there exists a set of axioms a, b, c, … such 
that ϕ can be obtained using these axioms and the inference 
Manuscript created December 29, 2006. Author is Ph. D. student of 
Department of Information Systems at The Poznan University of 
Economics, http://www.kie.ae.poznan.pl, email: radekh@teycom.pl. 
rules “modus ponens” and “universal generalization” (a ∧ b ∧ 
c… → ϕ)  [2]. 
II. BACKGROUND 
This section presents some background for the first-order 
theory and other rules used in the article. 
A. First-Order Theories 
First-order theory is a given set of axioms in some 
language. Language consists of logical symbols and set 
constants, functions, and relation symbols (predicates). 
Terms and formulas are built from language and give rise to 
sentences, which are formulas with no free variables in body. 
Theory is then a set of sentences which may be closed if it 
contains all consequences of its elements. Theory can be also 
complete (i.e. every sentence can be proved or disproved), 
consistent (not every sentence is provable), or decidable 
(every sentence can be proved or disproved and there exists a 
computational path (algorithm) showing which sentences are 
provable). 
An example of first-order theory that is complete and 
decidable is Boolean algebra  [16] or Zermelo–Frænkel set 
theory. 
B. First-Order Logic 
First-order logic, also called first-order predicate calculus 
(FOPC), is a system of deductions extending propositional 
logic. Atomic sentences of first-order logic are called 
predicates and are written usually in the form P(t1, t2, …,tn). 
An important ingredient of the first-order logic not found in 
propositional logic is quantification. 
In 1929, Gödel  [8] proved that every valid logical formula 
is valid in first-order logic. In other words, it is proved that 
for complete first-order theory, inference rules of FOPC are 
sufficient to prove any valid formula. 
First-order predicate calculus language consists of 
predicates, constants, functions, variables, logical operators 
(NOT, OR, AND), quantifiers, parentheses, and some types 
of equality symbol. There is also a set of rules for recognition 
of terms and well-formed formulas (wffs). 
There are four axioms for quantification: 
1) PRED-1: (∀ x Z(x)) → Z(t) 
2) PRED-2: Z(t) → (∃ x Z(x)) 
3) PRED-3: (∀ x (W → Z(x))) → (W → ∀ x Z(x)) 
4) PRED-4: (∀ x (Z(x) → W)) → (∃ x Z(x) → W) 
An important theorem for first-order logic is the outcome 
from Herbrand’s work (known as Herbrand’s theorem). It 
states that in predicate logic without equality, a formula A in 
prenex form (all quantifiers at the front) is provable if and 
only if a sequent S comprising substitution instances of the 
quantifier-free subformula of A is propositionally derivable, 
and A can be obtained from S by structural rules and 
quantifier rules only. In other words, it states that the formula 
cSAT problem lower bound 
Radosław Hofman, cSAT problem lower bound, 2007  
is provable, if, and only if we can rewrite it without quantifier 
substituting values and obtain provable formula. For 
example: 
∀ x Z(x) = Z(0) ∧ Z(1) 
∃ x Z(x) = Z(0) ∨ Z(1) 
C. Boolean Algebra 
Boolean algebra (also called Boolean lattice) is an 
algebraic structure containing objects and operations upon 
them and set of axioms (see Section D). It consists of one 
unary operation ¬ (not) and two binary operations ∧ (and), ∨ 
(or) also with two distinct elements 0 (constant representing 
false), 1 (constant representing true). Language of Boolean 
algebra considered as language for first order logic also 
contains symbols: = (equality), ⇒ (implication), parentheses 
and quantifiers, ∀ (universal), and ∃ (existential). 
Boolean algebra has the essentials of logic properties as 
well as all set operations (union, intersection, complement). 
D. Axioms of Boolean Algebra 
Given below is a complete list of Boolean algebra axioms. 
This set is not a minimal set of axioms (especially staring 
from  Ax13)) – some axioms can be derived from others, but it 
does not change the reasoning used in this article (the list is 
larger only for clearness and ensuring that it is complete): 
Ax1) a = b can be written as (a ∧ b) ∨ (¬a ∧ ¬b) 
Ax2) a ⇒ b = ¬a ∨ (a ∧ b) 
Ax3) a ∨ (b ∨ c) = a ∨ b ∨ c = (a ∨ b) ∨ c 
Ax4) a ∧ (b ∧ c) = a ∧ b ∧ c = (a ∧ b) ∧ c 
Ax5) a ∨ b = b ∨ a 
Ax6) a ∧ b = b ∧ a 
Ax7) a ∨ (a ∧ b) = a 
Ax8) a ∧ (a ∨ b) = a 
Ax9) a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c) 
Ax10) a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c) 
Ax11) a ∨ ¬a = 1 
Ax12) a ∧ ¬a = 0 
Ax13) a ∨ a = a 
Ax14) a ∧ a = a 
Ax15) a ∨ 0 = a 
Ax16) a ∧ 1 = a 
Ax17) a ∨ 1 = 1 
Ax18) a ∧ 0 = 0 
Ax19) ¬0 = 1 
Ax20) ¬1 = 0 
Ax21) ¬(a ∨ b) = ¬a ∧ ¬b 
Ax22) ¬(a ∧ b) = ¬a ∨ ¬b 
Ax23) ¬¬a=a 
Using universal generalization, one may add in every 
axiom definition, the universal quantifier stating “for all x 
axiom body” (). 
E. Computational Tree 
Corollary of the considerations stated earlier establishes 
that every formula in Boolean algebra is decidable. It is said 
to be proved (or called “tautology”) if there exists a 
transformation path from a set of axioms to a sentence that we 
are trying to prove. Until the authors are discussing FOPC, 
one may say that every sentence is provable, if, and only if we 
can start with axiom and repeatedly apply “modus ponens” or 
“universal generalization” and obtain this sentence  [2]. 
One may then consider every possible (provable) sentence 
to be deducible from axioms, which may be presented as the 
graph shown in Fig.  1. 
Axiom 1 Axiom 2 Axiom 3
Axiom n
Sentence 1.1 Sentence 1.2 Sentence 1.3 Sentence 1.m...
Modus ponens
General universalization
  Figure 1 Example of deducible tree 
Axioms may also be the result of computations, especially 
when they are not independent (e.g., ZF axioms) or when 
computations fall in a cycle. Usually, during computation one 
would skip deduction to already proven sentences because it 
does not introduce any new information, so deductions to 
axioms would have been omitted. 
F. Inference Rules and Deduction 
Modus ponens is an inference rule using the reasoning: if a 
and a → b are both proved, then b is also proved. 
Universal generalization is an inference rule using the 
reasoning: if P(a) is proved, and a is a free variable, then ∀ a 
P(a) is also proved. 
Deduction theorem (in fact deduction meta-theorem) states 
that if formula F can be deduced from E, then the implication 
P → Q can be directly shown to be deducible from the empty 
set. Using symbol “├” for deducible, one may write: if P ├ Q 
then ├ P → Q. One may generalize it to a finite sequence of 
assumption formulas P1, P2, P3, …, Pn ├ Q: 
P1, P2, P3… Pn-1 ├ Pn → Q and repeat it until we obtain the 
empty set on the left-hand side: ├ (P1 → (…(Pn-1 → (Pn → 
Q))…). 
Deduction follows three kinds of steps: setting up a set of 
assumptions (hypothesis), reiteration - calling hypothesis 
made previously to make it recent, and deduction, which is 
removing recent hypothesis. If one wants to convert proof 
done using deduction meta-theorem to axiomatic proof, then 
usually the following axioms would have been involved: 
1) P → (Q → P) 
2) (P → (Q → R)) → ((P → Q) → (P → R)) 
3) Modus ponens: (P ∧ (P → Q)) → Q 
G. Corollaries 
Theorem 1––If formula expressible in FOPC language is 
deducible, then every possible transformation of this formula 
obtained by usage inference rules and axioms is also 
deducible, and can be expressed in the same language. 
Theorem 2––If every transformation of formula is 
Radosław Hofman, cSAT problem lower bound, 2007  
expressible in FOPC, then the optimal for certain resource for 
chosen computational model is also expressible in the same 
language. 
Proofs of these theorems are provided in the appendix 
( VI.A and  VI.B). 
One needs to focus on Theorem 1 and have good 
understanding of significance of Gödels work. Let there be 
considered some formula ϕ which is intended to be proven or 
disproved. Assuming that there exists some deterministic 
transformation T1 which transform formula ϕ to ϕ1: 
ϕ1=T1(ϕ), there can also exist another transformation T2 
taking ϕ1 as input and returning ϕ2 as output: 
ϕ2=T2(ϕ1)=T2(T1(ϕ)). Continuing this idea of 
transformations one reaches ϕTRUE or ϕFALSE formula 
allowing to prove or disprove ϕ. 
Theorem 1 is in fact summary of Gödels Theorem  [8], 
stating that ϕ, ϕ1, ϕ2… ϕx can all be expressed in FOPC 
language. 
Above in fact causes statement of Theorem 2: if every 
possible transformation / reformulation of formula is 
expressible in FOPC language, then (by power of every 
quantification) also optimal transformation is expressible in 
FOPC language. It does not matter what is nature of this 
transformations. If they are deterministic (for certain input 
always returns same output in finite number of steps). 
Optimal way to solve the problem (decide on formula) can be 
then written as: ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) 
III. CSAT LOWER BOUND 
A. Problem Definition 
In this work, the authors consider  a problem called “Count 
of Satisfaction of Boolean Expression for formula ϕ.” This 
problem is almost the same as the classical SAT problem, but 
instead of the question “Is there an assignment to variables 
such that formula ϕ is satisfied?”, they ask the question “Are 
there at least L assignments such that formula ϕ is satisfied?”. 
L in problem instance is written unary, and the remaining 
part of the instance is exactly the same as in SAT problem 
(the authors assume that it is in conjunctive normal form 
(CNF)). 
It is easy to show that the problem is in NP – Guess & 
Check algorithm, for NDTM requires O(L*n) steps to check 
(certificate size is L*v where v is the number of Boolean 
variables used). 
It is also easy to show that the problem is NP-complete. 
One can show it using reduction from SAT problem and ask 
the question “Is there at least L=1 assignment such that 
formula ϕ is satisfied?” 
B. Measurable Predicate 
Problem question is easy to understand by a human, but it 
certainly extends to FOPC language defined in Section  II. To 
express it in a defined language, one  needs to define 
predicate “µ” – measure. This predicate is a representation of 
sigma-additive (countably additive) measurable function 
known as “set cardinality.” Definition of this predicate 
requires one constant variable n – number of different 
Boolean variables used. Predicate “µ” will measure number 
of assignments satisfying formula ϕ. 
1: µ(∅) :- 0 
2: µ(TRUE) :- 2n 
3: µ(FALSE) :- 0 
4: µ(¬ϕ1) :- 2n-µ(ϕ1) 
5: µ(a1) :- 2n-1 
6: µ(a1∧a2…∧ak) 
 ∃ ai, aj: i≠j ∧ ai=¬aj :- µ(FALSE) 
 ∃ ai, aj: i≠j ∧ ai=aj :- µ(a1∧a2…aj-1∧aj+1...∧ak) 
  :- 2n-k 
µ(ϕ1∨ϕ2) :- µ(ϕ1)+µ(ϕ2)−µ(ϕ1∧ϕ2) 
One may think of adding some more conditions to this 
predicate, but the list given earlier is sufficient to calculate 
measure for every formula for a defined language (growth of 
number of axioms and definitions is discussed in Section  H). 
It is also compliant with sigma-measurable function 
definition. 
One may also observe that usage of measure leads to 
exponential number of calculations required for CNF. This is 
a consequence of sigma-additivity property: for any sets a 
and b: µ(a∪b)=µ(a)+µ(b)−µ(a∩b). If one considers m sets, 
then this function transforms to: 
⋅−=
})..({
aaPS Sa
aa IU µµ , where 
P({a1..am}) is power set over m sets, which means that it has 
2m objects in it. If one is able to calculate the measure of a set 
or intersection of sets, then the calculation of union of m sets 
requires Ω(2m) intersections to be measured. 
Problem question using predicate “µ” is then: “µ(ϕ)≥L?”. 
Direct calculation may not  be the only possible way for 
solving problems, and the authors now analyze the definition 
of lower bound, deterministic and nondeterministic 
computation models. 
C. Lower Bound Definition 
Lower bound in Big-O notation is denoted as Ω(g(n)), and 
for its use in this article, one may assume that it is used to 
express problem lower bound. Interpretation of lower bound 
is “minimum value of function in the worst case,” and is 
defined as f(n) ∈ Ω(g(n)) ⇔ 0
inflim >
∞→ ng
In most of the complexity considerations, two types of 
resources are used in the expressions of problem lower 
bounds or algorithm upper bounds. These resources are time 
(number of steps required) and space (number of 
symbols/tape cells required). 
Theorem 3––Time complexity of problem/algorithm is 
always greater than or equal to space complexity. This 
theorem is proved in Section  VI.C. 
Theorem 4––Minimal number of symbols required for 
unambiguous description of object is Ω(log(N)), where N 
represents the number of possible objects to be stored. In 
other words, this means that if one has N different objects that 
may occur in computations at a certain step and would want 
to store information on which one occurred, then Ω(log(N)) 
Radosław Hofman, cSAT problem lower bound, 2007  
symbols are required. This theorem is proved in Section 
 VI.D. 
In this work, the authors mainly  consider time complexity 
using observation from Theorems 3 and 4. 
Theorem 5––Lower bound calculated to express a specific 
resource (time or space) usage for deciding formula 
expressed in FOPC for a chosen computational model is 
equal to the minimal usage of this resource for the best 
possible transformation of formula in this language. This 
theorem is proved in Section  VI.E. 
Theorem 5 is consequence of Theorem 2. If one had set of 
deterministic transformations expressing optimal way to 
solve the problem:  
ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) then by power of 
definitions it can be shown that lower bound for problem 
solution is exactly equal to time required by this optimal 
solution. This is consequence of lower bound definition – it is 
asymptotically minimal amount of resource required to solve 
the problem. Repeating most important observations till this 
point: 
a) formula ϕ can be expressed in FOPC language (from 
Gödels Theorem  [8]) 
b) any possible transformation of formula can be 
expressed in FOPC language ϕ1=T1(ϕ) (Theorem 1) 
c) if every deterministic transformation can be expressed 
in FOPC language then also optimal deterministic 
transformation can be expressed in FOPC language   
(Theorem 2)  
ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) 
d) resource cost of optimal transformation of formula is 
equal to deterministic lower bound of the problem 
Roughly speaking, lower bound should be considered as 
the minimal amount of resource used for computation for the 
worst case. In case of time, it is the minimal number of 
operations to perform. It is even intuitive to see that if one 
could express calculation in some “steps,” then lower bound 
is equivalent to minimal number of “steps” required in the 
worst case. 
D. Nondeterministic Calculation Model 
Nondeterministic calculation model may be considered as 
the “luckiest possible guesser.” Such an approach expresses 
that the role of NDTM to answer a problem question is to 
guess the certificate and check it. If the check can be 
performed in O(nc) for some constant c, then one considers 
the problem as part of NP complexity class. 
One has to remember that DTM is a “special case” of 
NDTM where from every machine state, only one possibility 
to choose the next state exists, regardless of the symbol in the 
cell where the tape read/write head is positioned. This means 
that every problem solvable by DTM in O(nc) steps is 
solvable also on NDTM in at most same number of steps (or 
may be less). 
A good example expressing the differences between DTM 
and NDTM is the 2SAT problem (classic satisfaction of 
Boolean expression in CNF problem, but where in each 
clause there are at most two literals). This problem is solvable 
by DTM in O(n3) steps, but NDTM may guess the correct 
assignment and verify it in O(n). 
In terms of first-order logic and Herbrand’s theorem, one 
can see that NDTM is a verifier of Herbrand’s subformulas. 
When the formula is expressed using existential quantifier:  
∃ <a: assignment> F(a), then, according to Herbrand’s 
theorem, it is equivalent to: F(a1) ∨ F(a2)… ∨ F(ak). NDTM 
is able to check each of F(ai) simultaneously, even if the 
number of possible assignments is exponential, excepting 
when at least one of the computation paths led to an accepting 
state. 
One can see that for a nondeterministic calculation model 
problem, the number of steps of lower bound is equal to the 
minimal number of steps required to check the certificate. 
For example, for 2SAT problems one can have different 
approaches. 
Number of possible 
Herbrand’s 
subformulas 
Minimal number 
of steps to check 
each subformula 
Total 
calculatio
n cost 
1 2n N n 
(guessing only p 
variables) 
n*p3 N*p3 
(without splitting) 
3 n3 
 Table 1  Different approaches for nondeterministic 
calculation 
Table 1 presents different approaches differing mainly in 
the number of “guesses.” Calculation of problem lower 
bound for nondeterministic model of calculation returns the 
minimal number of steps required to check subformula. 
The last row presents the approach where the problem is 
not split, so it is calculated as in the deterministic model of 
calculations. 
E. Deterministic Calculation Model 
As mentioned in  Section D, deterministic model of 
calculations follows a single computation path. It is obvious 
that despite direct calculations, DTM can also perform Guess 
& Check algorithm (simulating NDTM). This time, the 
authors do not assume that DTM is the “luckiest possible 
guesser” and for lower bound complexity calculation of this 
approach, they have to assume that DTM is the “worst 
possible guesser.” This is also a consequence of the slight 
change in computation goal - NDTM has to “accept” when 
there is computational path leading to accepting state, while 
DTM has to “decide” on input, which means that the answer 
“NO” can be produced only when there is no possible way of 
reaching the accepting state (NDTM can be defined without 
rejecting state). 
Additionally, DTM requires an iterator (space on tape 
where number of current “guess” can be stored), which 
according to Theorem 4 requires Ω(log(H)), where H 
represents the possible number of “guesses.” 
Table 2 shows what time complexity would look like. 
Radosław Hofman, cSAT problem lower bound, 2007  
Number of 
possible 
Herbrand’s 
subformulas 
Minimal 
number of 
steps to 
check each 
subformula 
Total calculation 
cost 
1 2n N 2n*n+log(2n) 
2 2p n*p3 2n*n*p3+log(2p) 
K 1 n3 n3 
 Table 2 Different approaches for deterministic calculation 
In this table, the last row represents the minimal possible 
number of steps to calculate result. It is easy to show that for 
DTM, this row also presents deterministic problem lower 
bound because if any of the “guessing” approaches had been 
better, then it would have been used to present minimal 
deterministic calculation cost (we assume that values in the 
table are “best possible” not “best known” - see Theorem 5). 
F. cSAT Nondeterministic Algorithm Upper Bound 
Upper bound for algorithm solving cSAT problem is 
polynomial. It is a consequence of Herbrand’s theorem and 
ability of NDTM to: 
generate all possible subformulas in O(nc) 
verify each of them in O(nc) 
NDTM algorithm can be described using the following 
steps: 
1) Guess sets of measure L consisting of assignments of 
variables (time O(L*v)) 
2) Verify guessed set (time O(L*v)) 
This procedure leads to accepting the state (if at least one 
computation path is accepting) in at most O(L*v) steps and 
because instance size n∈Ω(L+v), the solution is provided in 
O(n2). 
G. cSAT Deterministic Lower Bound 
Now, using the observations described in the earlier 
sections, the authors calculate deterministic lower bound of 
cSAT problem (it is known that its nondeterministic upper 
bound is O(L*v)). 
First, one needs to write the problem in the FOPC 
language. One  uses the predicate µ: µ(ϕ)≥L. 
This problem may be considered to be harder than the 
classic SAT problem. If one tries to guess all possible 
subsets, then we would have Ω(
v22 ) subsets, so according to 
Theorem 4, it would require Ω(2v) symbols to store 
information about the considered subset, which, according to 
Theorem 3, leads to the conclusion that such a calculation 
requires at least Ω(2v) steps. “Guessing” only subsets of size 
L leads to Ω(2v) different subsets, so that it can be calculated 
by NDTM in polynomial time (Ω(v*L) steps), but requires 
Ω(2v*v*L) steps to calculate on DTM. 
In fact, following the assumption that DTM is the worst 
possible guesser, one may see that the number of hypotheses 
(“guesses”) used during computation can lead to an 
exponential usage of time if “depth” of hypothesis path is 
longer than O(log(n)) or any of the hypotheses has more than 
polynomial number of possible values. For example, if one 
states hypothesis A with possibilities, it is true or false 
(constant number of possibilities) and it is followed by 
hypothesis B (true or false), etc.; we need O(n) hypotheses 
before we can decide on formula, then in the worst case we 
require Ω(2n) steps to give the answer “NO.” 
Leaving then all Guess & Check approaches, the authors 
try to determine the minimal possible number of steps for 
DTM to decide on problem input. According to Theorem 5 
and considerations from the earlier sections, the authors 
conclude that the shortest possible path consists of steps 
transforming input formula to axioms of theory. If one can 
show that every transformation requires exponential number 
of steps or usage of object using exponential number of 
symbols to store, then it will be direct proof that lower bound 
of cSAT problem is over-polynomial. 
When will one be able to observe exponential growth of 
minimum number of required steps? If after using an axiom 
or predicate, one will obtain a formula of multiplicative 
length by a factor greater than 1. For example, if for formula 
of size n1 (considered to be in CNF), the authors use  Ax9) for 
one parenthesis, they obtain new formula in the format 
v1∧(n2,1)∨v2∧(n2,2)∨…∨vm∧(n2,m). In each of the m parts, 
one can use a variable from the beginning to remove all its 
negations from body, so |n2,*|<|n1|−m, but for very large n1, 
these parts of formula will still require further 
transformations, which if done only with  Ax9) would lead to 
exponential growth. Concluding this paragraph, one may say 
that if transformation reduces size of formula substring by 
O(nc) and multiplies this shorter string in formula making 
string grow to n2, where n2∈Ω(n1*c), then this path leads to 
exponential growth of formula and thus its lower bound is 
Ω(2n). 
In Table 3, the authors present the effect obtained by usage 
of every possible transformation, but before this the authors 
define polynomial purifying function for formula. This 
function will use axioms  Ax7),  Ax8),  Ax11),  Ax12),  Ax13), 
 Ax14),  Ax15),  Ax16),  Ax17),  Ax18),  Ax19),  Ax20),  Ax23), 
and two observations: 
µ(ϕ1)=µ(ϕ1∧(TRUE))=µ(ϕ1∧(v1∨v2∨…∨TRUE)); 
µ(v1∧ϕ1)=µ(ϕ2) where ϕ2 is obtained by replacing every 
occurrence of v1 in ϕ1 with constant TRUE. 
Roughly speaking, this function  looks for variables that 
can be cleared out from formula and prepare it for the next 
step of calculation. The authors assume that at every step of 
calculation, formula is in a form not allowing the use of any 
of the above axioms or rules. It is also important to remember 
that the number of transformation rules does not matter - refer 
to Section  H. 
Transfor
mation 
used 
Length 
string 
used 
Result 
string 
length 
Lower 
bound for 
path 
Remarks for “worst 
case” 
 Ax1)    
 Ax2)    
These axioms cannot be 
used since input never 
contains these symbols 
 Ax3) n1 n1 Ω(cSAT) 
 Ax4) n1 n1 Ω(cSAT) 
These axioms do not 
change formula length 
Radosław Hofman, cSAT problem lower bound, 2007  
Transfor
mation 
used 
Length 
string 
used 
Result 
string 
length 
Lower 
bound for 
path 
Remarks for “worst 
case” 
 Ax5) n1 n1 Ω(cSAT) 
 Ax6) n1 n1 Ω(cSAT) 
 Ax7)    
 Ax8)    
These axioms cannot be 
used because formula is 
transformed by purifying
function 
 Ax9) 
m1+m2+
2*m1*
m2+nr-
 Ax10) 
m1+m2+
2*m1*
m2+nr-
Used on two parenthesis 
replaces them with string 
of size 2*m1*m2, after 
using these axioms 
purifying function will 
reduce size but in the 
worst case only by 2 
symbols 
 Ax11), 
 Ax12), 
 Ax13), 
 Ax14), 
 Ax15), 
 Ax16), 
 Ax17), 
 Ax18), 
 Ax19), 
 Ax20) 
These axioms cannot be 
used because formula is 
transformed by purifying
function 
 Ax21) n1 n1 Ω(cSAT) 
 Ax22) n1 n1 Ω(cSAT) 
These axioms do not 
change formula length 
 Ax23)    As  Ax20) above 
µ1    
µ2    
µ3    
These rules cannot be 
used because formula is 
transformed by purifying
function 
µ4 n1 n1 Ω(cSAT) 
Can be used with  Ax21), 
 Ax22) or  Ax23), but 
does not change length 
of formula 
µ5    As µ3 above 
µ6 m1+m2 
m1*m2 
n  Treating formula as 
consisting of two parts 
 Table 3 Lower bounds for every possible transformation 
of cSAT formula 
The variables used in Table 3 are the following: 
n1 – Length of the formula 
nr – Length of the remaining part of the formula 
m1 – Length of first part/parenthesis of the formula 
m2 – Length of second part/parenthesis of the formula 
p1 – Number of parentheses in the formula 
 – The authors consider asymptotic behavior of the 
function, so one may use kind of “mean” m1 – representing 
Ω(m1). 
It is clear that in the worst case,  Ax9),  Ax10), or µ6 have to 
be used several times before purifying function would make 
significant reduction of length. Lower bound is considered as 
the minimal worst case, so from this table it is clear that in the 
worst case it is Ω(mp)=Ω(2p*log(m)) and because p and m are 
both O(n), the whole lower bound is Ω(2n). 
H. More Conditions and More Axioms 
The above considerations prove clearly that deterministic 
lower bound for cSAT problem considered with FOPC 
language defined is exponential. But one needs to answer one 
additional question – Is it the result of too poor FOPC axioms 
set definition? Or are too few predicates defined? 
In  [1] Baker–Gill–Solovay theorem, authors have shown 
that problem “Is P equal to NP?” can be relativized using 
oracles. Oracle is a machine (black box) that gives answers to 
certain type of problems in one step. One can then imagine 
that there are a very large number of oracles which can solve 
certain types of instances. DTM task is to pick up one of them 
(or use them sequentially because if the number of oracles is 
an attribute of the machine, then even if we have used 
millions of them, the complexity in terms of relation to 
instance size is O(1)). 
The authors presume then, that for cSAT problem, there 
exists some deterministic algorithm calculating answer in 
O(nc) steps. Following lower bound calculation, one knows 
that this algorithm calculates a result requiring Ω(2n) 
transformations. Reminding optimal transformation as 
described above: ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) 
and x∈Ω(2n). 
The presumption made here can be presented as existence 
of some transformation TA≡Tx-k(Tx-k-1(…(Tx-k-m(   ))…)), 
where m is exponential (TA is equivalent to exponential 
number of transformations in FOPC language, on optimal 
transformation path). The authors also assume that TA is 
deterministic, as deterministic lower bound is discussed in 
this section, and computable in polynomial number of steps. 
Now, one need to look on transformation path as on 
decision process, where at each step there is a decision to be 
made (decision which transformation is to be used). Each 
decision takes Ω(1) space to be stored. If m was dynamic and 
asymptotically equal to 2n, and also computable in 
polynomial number of steps then this would be equal to O(2n) 
decisions in O(nc) time what contradicts Theorem 3. 
Considering constant m (invented by algorithm designer) 
one may ask what is common in a large number of Turing 
machines (in the sense of defined algorithms), large number 
of axioms, large number of predicates, large number of 
oracles, or large m in above transformation TA? Their number 
is always a constant, even if very large. If then anyone defines 
multiple TMs, adds multiple axioms, predicates, defines 
large number of oracles, or finds one transformation TA 
equivalent to exponential number of other transformation, 
then in fact after defining them, one may have constant 
number of machines, axioms, predicates, transformations, 
and oracles. 
The authors then assume that there exists a machine 
denoted by LDTM in which implements are equivalent to 
large number of TMs, large number of axioms, predicates, 
implements TA and are connected to multitude of oracles. 
Such a defined machine is (by power of assumption) capable 
Radosław Hofman, cSAT problem lower bound, 2007  
of answering cSAT questions for a finite number of differing 
input types (number of types is a consequence of maximal 
input size). 
In other words, the authors assume that there exists a 
machine LDTM able to answer cSAT questions for instance 
size less than or equal to nl. They may consider having 
( )lncO  different input types, and each type is covered at least 
by one combination of axioms, predicates, or oracles 
allowing LDTM to give answer in O(n) steps. One may 
assume that there are gl such combinations. Denoting |gi(nl)| 
number of instances solved by ith combination of axioms and 
oracles for instance nl symbols long, the authors have 
assumed that: |||)(|
cng ≥∑
, where ( ) ||||
cng <∀
Now the authors determine the ability of this machine to 
answer cSAT question where n=nl*y. Number of 
combinations of axioms and oracles remain constant (gl), but 
they assume that each combination covers more instances 
(considered to be “same type”) gl(n)=gl(nl*y)≤gl(nl)
y. The 
number of possible types grows from ( )lncO  to 
( ) ( )( )ynyn ll cOcO =* . 
Calculating instances covered by gl definitions, we have: 
ngyng
|)(||)*(| . 
If one proves that for y growing to infinity 
lcng |||)(|
, it will be proof that not all instances of 
size O(nl*y) are solvable using LDTM definitions, so these 
large instances will require calculations using deterministic 
lower bound discussed in Section  G. Proof is presented in 
 VI.F, so corollary about impossibility to answer cSAT 
problems in polynomial time by LDTM holds. 
IV. COROLLARIES 
To summarize this article, the authors repeat the deduction 
path: 
a) formula ϕ can be expressed in FOPC language (from 
Gödels Theorem  [8]) 
b) any possible transformation of formula can be 
expressed in FOPC language ϕ1=T1(ϕ) (Theorem 1) 
c) if every deterministic transformation can be expressed 
in FOPC language then also optimal deterministic 
transformation can be expressed in FOPC language   
(Theorem 2)  
ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) 
d) resource cost of optimal transformation of formula is 
equal to deterministic lower bound of the problem 
e) TA equivalent to exponential number of 
transformations computable in polynomial time 
contradicts Theorem 3 
f) large number of defined constant set of 
transformations, oracles, algorithms, machines ect. 
cannot cover all possible inputs for growing instance 
size (Theorem 6) 
g) optimal solution of problem requires Ω(2n) 
transformations 
h) deterministic lower bound for cSAT problem is then 
Ω(2n), then cSAT∉P (Theorem 5) 
i) NDTM solves cSAT in polynomial time, so 
cSAT∈NP 
j) this means that P≠NP 
If above considerations are correct then checking problem 
known to be in P has to show that it is in P using the same 
reasoning. Such check for 2SAT problem if presented in 
Section  VI.G - lower bound for this problem is Ω(nc). 
In  [1], there was presented an oracle A for which PA=NPA. 
Proof presented in Section  VI.F and problem lower bound 
lead to corollary, and if A is able to solve cSAT in 
polynomial time, then A has to be nondeterministic - it has to 
consist of infinite number of objects: deterministic oracles, 
algorithms, DTMs, axioms, rules etc. (the authors also 
consider NDTM as an infinite set of DTM duplicates - each 
for one computational branch). 
This work discusses problem P=NP, as described in  [5]. It 
may be said to relativize (see  [1]) to deterministic model of 
computation showing that deterministic calculation model 
made up of finite number of machines (algorithms), oracles, 
axioms, or predicates is incapable of solving the considered 
problem when its instance grows to infinity. 
On the other hand, one may conclude that if restrictions on 
maximum input length problem are set, then the problem can 
be proved to be in P using a large number of machines, 
axioms, algorithms, predicates, or oracles. 
For deterministic model of computation, one  knows then 
that P≠NP. 
Using Theorem 13 from  [12], the authors also know that 
NP-complete≠(NP-P). In this theorem, the authors have 
proved that: if P≠NP and U is some NP-complete language 
then U=A∪B where neither A nor B language is 
NP-complete (at least one of them is also not equal to P: A≠P 
∨ B≠P). Complexity classes can be put in a picture (Fig. 2): 
Figure 2 Relation between P, NP, and NP-complete classes 
V. REFERENCES 
[1] Baker T. P., Gill J., Solovay R., “Relativizations of the P 
=? NP question”, SIAM Journal on Computing, vol. 4, 
no. 4, 1975, pp. 431-442. 
[2] Barwise J., Etchemendy J., “Language Proof and Logic”, 
Seven Bridges Press, CSLI (University of Chicago 
Press) and New York, 2000. 
[3] Chandra A. K., Kozen D. C., Stockmeyer L. J., 
“Alternation”, Journal of the ACM, vol. 28, no. 1, 1981. 
[4] Cook S. A., “The complexity of theorem-proving 
procedures”, Proceedings of the Third Annual ACM 
Symposium on Theory of Computing, 1971, pp. 
151-158. 
Radosław Hofman, cSAT problem lower bound, 2007  
[5] Cook S. A., “P versus NP problem”, unpublished. 
Available at: 
http://www.claymath.org/millennium/P_vs_NP/Official
_Problem_Description.pdf 
[6] Diaby M., “P = NP: Linear programming formulation of 
the traveling salesman problem”, 2006, unpublished. 
Available at: http://arxiv.org/abs/cs.CC/0609005 
[7] Gallier J. H., "Logic for Computer Science: Foundations 
of Automatic Theorem Proving", Harper & Row 
Publishers, 1986. 
[8] Gödel K., "Über formal unentscheidbare Sätze der 
Principia Mathematica und verwandter Systeme", I. 
Monatshefte für Mathematik und Physik, vol. 38, 1931, 
pp. 173-198. 
[9] Hofman R., “Report on article: P=NP linear 
programming formulation of the traveling salesman 
problem”, 2006, unpublished. Available at: 
http://arxiv.org/abs/cs.CC/0610125 
[10] Jech T., “Set Theory: The Third Millennium Edition, 
Revised and Expanded”, ISBN 3-540-44085-2, 2003. 
[11] Karp R. M., “Reducibility among combinatorial 
problems”, In Complexity of Computer Computations, 
Proceedings of the Symposium of IBM Thomas J. 
Watson Research Center, Yorktown Heights, NY. 
Plenum, New York, 1972, pp. 85-103. 
[12] Landweber, Lipton, Robertson, “On the structure of sets 
in NP and other complexity classes”, Theoretical 
Computer Science, vol. 15, 1981, pp. 181-200. 
[13] Papadimitriou C.H., Steiglitz K., “Combinatorial 
Optimization: Algorithms and Complexity”, 
Prentice-Hall, Englewood Cliffs, 1982. 
[14] Razborov A., Rudich S., “Natural proofs”, Journal of 
Computer and System Sciences, vol. 55, no. 1, 1997, pp. 
24-35. 
[15] Savitch W. J., “Relationships between nondeterministic 
and deterministic tape complexities”, Journal of 
Computation and System Science, vol. 4, 1970, pp. 
177-192. 
[16] Tarski A., Givant S., “A Formalization of Set Theory 
Without Variables”, American Mathematical Society, 
Providence, RI, 1987. 
VI. APPENDIX 
A. Proof 1 - Proof of Theorem 1 
Theorem 1 - If formula expressible in FOPC language is 
deducible, then every possible transformation of this formula 
obtained by usage inference rules and axioms is also 
deducible and can be expressed in the same language. 
This theorem is a direct consequence of FOPC definitions. 
If ϕ is deducible, then: 
• ϕ ∧ axiom 
• ϕ → axiom 
• ∀ x ϕ 
are also deducible. 
B. Proof 2 - Proof of Theorem 2 
Theorem 2 - If every transformation of formula is 
expressible in FOPC, then the optimal for certain resource for 
chosen computational model is also expressible in the same 
language. 
This theorem is a consequence of Theorem 1 and FOPC 
definitions. If the goal of calculation is to decide on formula 
based on theory axioms, then it is required to obtain formula 
as a consequence of axioms (with empty left-hand side):  
├ (P1 → (…(Pn-1 → (Pn → Q))…). 
The authors said that every possible transformation of 
formula is expressible in FOPC and this directly means that 
the optimal in the aspect of a certain resource (time or space) 
path is also expressible in FOPC. 
C. Proof 3 - Proof of Theorem 3 
Theorem 3 - Time complexity of problem/algorithm is 
always greater than or equal to space complexity. 
This theorem is a consequence of Turing machine 
definition, which states that in one step, a machine can read or 
write one (or in general constant) number of symbols. If then 
f(n) symbols were written, then machine had used at least f(n) 
steps to write them. 
D. Proof 4 - Proof of Theorem 4 
Theorem 4 - Minimal number of symbols required for 
unambiguous description of object is Ω(log(N)), where N 
represents the number of possible objects to be stored. 
In this section, the function log is considered to have ∑ in 
root, where ∑ represents the number of the symbols in the 
alphabet: log(∑)=1. 
The authors prove the theorem using contradiction. 
Suppose that one knows “compression” algorithm allowing 
to write each of N symbols using log(N)−f(N) symbols, where 
f(N) is a function such that: ∀ N: 0<f(N)<log(N). 
On log(N)−f(N),one can write at most ∑log(N)-f(N) different 
strings. 
)log(
)log(
)log(
)()log(
NfNfNf
NfN NN
Now the authors check whether this number is greater than 
the number of objects to be identified by checking limens: 
lim  
It is easy to see that if f(N)=0, then limens is equal to zero 
(which means that exactly N different objects can be 
described using a string of desired length), but when f(N)>1 
(it is the smallest value making difference in the number of 
symbols used), it is negative which means that less than N 
objects can be represented using a string of this length. 
E. Proof 5 - Proof of Theorem 5 
Theorem 5 - Lower bound calculated to express specific 
resource (time or space) usage for deciding formula 
expressed in FOPC for a chosen computational model is 
equal to the minimal usage of this resource for best possible 
transformation of formula in this language. 
Proof of this theorem is in fact a direct corollary of 
Radosław Hofman, cSAT problem lower bound, 2007  
Theorems 1 and 2. If any transformation of formula is 
expressible in FOPC language, then the optimal in terms of 
chosen resource is also expressible in FOPC language and 
when the authors calculate lower bound for this resource for 
the whole transformation path (from input string to decidable 
form (to axioms)), then they obtain the value of lower bound 
for the considered problem. 
F. Proof 6 - Proof of Not Covering by Constant Set of 
Definitions All Possible Large Instances by LDTM 
Assumptions: ( ) ||||
cng <∀
 and |||)(|
cng ≥∑
. Also 
gi(n) function operates on natural numbers and returns natural 
numbers, so ( ) |1|||
cng . 
One want to solve yn
lcng |||)(|
 for y growing to 
infinity. 
First one may observe that: ∑∑
|1||)(|  if 
one can solve inequality yn
yn ll cc |||1|
, then it will be 
equivalent to prove that the proof is correct. 
The  new equality presented by the authors is free from i 
variables, so it can be rewritten as: ynyn ll ccl |||1|* <− . 
Now the authors take logarithm on both sides to the base l: 
( ) ( )
( ) ( ) ( )
( ) ( )
( ) ( )||log|1|log1
||log*|1|log*1
||log|1|loglog
||log|1|*log
At this point, it is obvious that this inequality holds - 1/y 
when y grows to infinity may be omitted and one has 
inequality of two logarithms where this one on the left-hand 
side is the logarithm of lower value. 
More formally, one may calculate limens: 
( ) ( )
1loglim
loglim
||log|1|log
lim  
Proof is then correct. 
G. Proof 7 - Lower Bound for 2SAT Problem 
2SAT problem is a special case of cSAT problem. Its 
special factors are: 
• L = 1 (problem question is “µ(ϕ)>=1” or 
“µ(ϕ)>0”) 
m1=m2=…=mp=2 
The authors assume that the input string is in CNF and 
purifying function (defined in Section  III.G) cannot be 
applied. 
They use  Ax9) on parenthesis to select next parenthesis 
such that: 
• parenthesis has not been used yet 
• parenthesis contains negation of variable used in 
a previous step 
Every time the usage of  Ax9) will be followed by purifying 
function usage. 
For example:  
(a∨b)1∧(a∨¬c)2∧(c∨d)3∧(¬b∨¬c)4∧(¬b∨¬a)5∧(¬d∨¬a)
6∧(e∨f)7 the authors would have used  Ax9) for parenthesis: 1 
and 6 (last variable is: ¬d), then 3 (lv: c), then 4 (lv: ¬b), then 
1 (second time, lv: a), then 5 (lv: ¬b), then 1 (third time, lv: 
a), then 6 (second time, lv: ¬d), then 3 (second time, lv: c), 
and finally 2. Every parenthesis will be used at most on every 
path from any pair of parentheses. 
At every stage, calculation formula will contain at most 
p+1 conjunctions (where p is the number of parenthesis 
processed) and each conjunction will contain at most every 
variable once. Every parenthesis will be used at most p2 
times, which means that at every stage of computation, 
formula length is O(p3). 
This may not be a time optimal solution. According to 
Theorem 2, optimal transformation path is expressible using 
axioms and predicates defined for FOPC, but to show that the 
problem is in P, one does not need to look for optimal 
transformation path - the authors have shown that there exists 
at least one transformation path polynomially bounded to 
instance size, and even if it is not the optimal one, it shows 
that 2SAT problem is in P.

  This article discusses completeness of Boolean Algebra as First Order Theory
in Goedel's meaning. If Theory is complete then any possible transformation is
equivalent to some transformation using axioms, predicates etc. defined for
this theory. If formula is to be proved (or disproved) then it has to be
reduced to axioms. If every transformation is deducible then also optimal
transformation is deducible. If every transformation is exponential then
optimal one is too, what allows to define lower bound for discussed problem to
be exponential (outside P). Then we show algorithm for NDTM solving the same
problem in O(n^c) (so problem is in NP), what proves that P \neq NP.
  Article proves also that result of relativisation of P=NP question and oracle
shown by Baker-Gill-Solovay distinguish between deterministic and
non-deterministic calculation models. If there exists oracle A for which
P^A=NP^A then A consists of infinite number of algorithms, DTMs, axioms and
predicates, or like NDTM infinite number of simultaneous states.

Microsoft Word - Complexity_Considerations_FOL2.doc
Radosław Hofman, cSAT problem lower bound, 2007  
Abstract—This article deals with the lower bound that 
is considered as the worst case minimal amount of time 
required to calculate a problem result for cSAT (counted 
Boolean satisfiability problem). It uses the observation 
that Boolean algebra is a complete first-order theory 
where every sentence is decidable. Lower bound of this 
decidability is defined and shown. 
The article shows that deterministic calculation model 
made up of finite number of machines (algorithms), 
oracles, axioms, or predicates is incapable of solving 
considered NP-complete problem when its instance 
grows to infinity. This is a direct proof of the fact that P 
and NP complexity classes differ and oracle capable of 
solving NP-complete problems in polynomial time must 
consist of infinite number of objects (i.e., must be 
nondeterministic). 
Corollary of this article clears complexity hierarchy: 
P < NP 
Index terms—complexity class, P vs NP, Boolean 
algebra, first order theory, first order predicate calculus. 
I. INTRODUCTION 
Unknown relation between P and NP  [5] complexity 
classes remains one of the significant unsolved problems in 
complexity theory. P complexity class consists of problems 
solvable by deterministic Turing machine (DTM) in 
polynomially bounded time, while NP complexity class 
consists of problem solvable by nondeterministic Turing 
machine (NDTM) in polynomially bounded time. This means 
that DTM can verify the solution of every NP problem in 
polynomially bounded time, even if polynomial algorithm for 
finding this solution is unknown  [13]. 
All known attempts to prove whether these classes are or 
are not equal could not convince the community that 
arguments used there are final. Problem with attempts 
showing that P=NP is mainly with counter examples 
provided for methods described by solvers (see for example: 
 [6],  [9]), especially for large instances. Problem with proof 
attempts that P≠NP touches mainly the difference between a 
problem and an algorithm. Proving the inequality of these 
classes is equivalent to proving that “there is no such 
algorithm that solves a particular NP problem in 
polynomially bounded time.” Algorithm is an immaterial 
object, so proving that it does not exist is rather difficult. 
Can then the inequality of complexity classes be proved? 
One of the possible ways is to use the properties of first-order 
theory. Useful properties include every sentence ϕ in theory 
T is provable if there exists a set of axioms a, b, c, … such 
that ϕ can be obtained using these axioms and the inference 
Manuscript created December 29, 2006. Author is Ph. D. student of 
Department of Information Systems at The Poznan University of 
Economics, http://www.kie.ae.poznan.pl, email: radekh@teycom.pl. 
rules “modus ponens” and “universal generalization” (a ∧ b ∧ 
c… → ϕ)  [2]. 
II. BACKGROUND 
This section presents some background for the first-order 
theory and other rules used in the article. 
A. First-Order Theories 
First-order theory is a given set of axioms in some 
language. Language consists of logical symbols and set 
constants, functions, and relation symbols (predicates). 
Terms and formulas are built from language and give rise to 
sentences, which are formulas with no free variables in body. 
Theory is then a set of sentences which may be closed if it 
contains all consequences of its elements. Theory can be also 
complete (i.e. every sentence can be proved or disproved), 
consistent (not every sentence is provable), or decidable 
(every sentence can be proved or disproved and there exists a 
computational path (algorithm) showing which sentences are 
provable). 
An example of first-order theory that is complete and 
decidable is Boolean algebra  [16] or Zermelo–Frænkel set 
theory. 
B. First-Order Logic 
First-order logic, also called first-order predicate calculus 
(FOPC), is a system of deductions extending propositional 
logic. Atomic sentences of first-order logic are called 
predicates and are written usually in the form P(t1, t2, …,tn). 
An important ingredient of the first-order logic not found in 
propositional logic is quantification. 
In 1929, Gödel  [8] proved that every valid logical formula 
is valid in first-order logic. In other words, it is proved that 
for complete first-order theory, inference rules of FOPC are 
sufficient to prove any valid formula. 
First-order predicate calculus language consists of 
predicates, constants, functions, variables, logical operators 
(NOT, OR, AND), quantifiers, parentheses, and some types 
of equality symbol. There is also a set of rules for recognition 
of terms and well-formed formulas (wffs). 
There are four axioms for quantification: 
1) PRED-1: (∀ x Z(x)) → Z(t) 
2) PRED-2: Z(t) → (∃ x Z(x)) 
3) PRED-3: (∀ x (W → Z(x))) → (W → ∀ x Z(x)) 
4) PRED-4: (∀ x (Z(x) → W)) → (∃ x Z(x) → W) 
An important theorem for first-order logic is the outcome 
from Herbrand’s work (known as Herbrand’s theorem). It 
states that in predicate logic without equality, a formula A in 
prenex form (all quantifiers at the front) is provable if and 
only if a sequent S comprising substitution instances of the 
quantifier-free subformula of A is propositionally derivable, 
and A can be obtained from S by structural rules and 
quantifier rules only. In other words, it states that the formula 
cSAT problem lower bound 
Radosław Hofman, cSAT problem lower bound, 2007  
is provable, if, and only if we can rewrite it without quantifier 
substituting values and obtain provable formula. For 
example: 
∀ x Z(x) = Z(0) ∧ Z(1) 
∃ x Z(x) = Z(0) ∨ Z(1) 
C. Boolean Algebra 
Boolean algebra (also called Boolean lattice) is an 
algebraic structure containing objects and operations upon 
them and set of axioms (see Section D). It consists of one 
unary operation ¬ (not) and two binary operations ∧ (and), ∨ 
(or) also with two distinct elements 0 (constant representing 
false), 1 (constant representing true). Language of Boolean 
algebra considered as language for first order logic also 
contains symbols: = (equality), ⇒ (implication), parentheses 
and quantifiers, ∀ (universal), and ∃ (existential). 
Boolean algebra has the essentials of logic properties as 
well as all set operations (union, intersection, complement). 
D. Axioms of Boolean Algebra 
Given below is a complete list of Boolean algebra axioms. 
This set is not a minimal set of axioms (especially staring 
from  Ax13)) – some axioms can be derived from others, but it 
does not change the reasoning used in this article (the list is 
larger only for clearness and ensuring that it is complete): 
Ax1) a = b can be written as (a ∧ b) ∨ (¬a ∧ ¬b) 
Ax2) a ⇒ b = ¬a ∨ (a ∧ b) 
Ax3) a ∨ (b ∨ c) = a ∨ b ∨ c = (a ∨ b) ∨ c 
Ax4) a ∧ (b ∧ c) = a ∧ b ∧ c = (a ∧ b) ∧ c 
Ax5) a ∨ b = b ∨ a 
Ax6) a ∧ b = b ∧ a 
Ax7) a ∨ (a ∧ b) = a 
Ax8) a ∧ (a ∨ b) = a 
Ax9) a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c) 
Ax10) a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c) 
Ax11) a ∨ ¬a = 1 
Ax12) a ∧ ¬a = 0 
Ax13) a ∨ a = a 
Ax14) a ∧ a = a 
Ax15) a ∨ 0 = a 
Ax16) a ∧ 1 = a 
Ax17) a ∨ 1 = 1 
Ax18) a ∧ 0 = 0 
Ax19) ¬0 = 1 
Ax20) ¬1 = 0 
Ax21) ¬(a ∨ b) = ¬a ∧ ¬b 
Ax22) ¬(a ∧ b) = ¬a ∨ ¬b 
Ax23) ¬¬a=a 
Using universal generalization, one may add in every 
axiom definition, the universal quantifier stating “for all x 
axiom body” (). 
E. Computational Tree 
Corollary of the considerations stated earlier establishes 
that every formula in Boolean algebra is decidable. It is said 
to be proved (or called “tautology”) if there exists a 
transformation path from a set of axioms to a sentence that we 
are trying to prove. Until the authors are discussing FOPC, 
one may say that every sentence is provable, if, and only if we 
can start with axiom and repeatedly apply “modus ponens” or 
“universal generalization” and obtain this sentence  [2]. 
One may then consider every possible (provable) sentence 
to be deducible from axioms, which may be presented as the 
graph shown in Fig.  1. 
Axiom 1 Axiom 2 Axiom 3
Axiom n
Sentence 1.1 Sentence 1.2 Sentence 1.3 Sentence 1.m...
Modus ponens
General universalization
  Figure 1 Example of deducible tree 
Axioms may also be the result of computations, especially 
when they are not independent (e.g., ZF axioms) or when 
computations fall in a cycle. Usually, during computation one 
would skip deduction to already proven sentences because it 
does not introduce any new information, so deductions to 
axioms would have been omitted. 
F. Inference Rules and Deduction 
Modus ponens is an inference rule using the reasoning: if a 
and a → b are both proved, then b is also proved. 
Universal generalization is an inference rule using the 
reasoning: if P(a) is proved, and a is a free variable, then ∀ a 
P(a) is also proved. 
Deduction theorem (in fact deduction meta-theorem) states 
that if formula F can be deduced from E, then the implication 
P → Q can be directly shown to be deducible from the empty 
set. Using symbol “├” for deducible, one may write: if P ├ Q 
then ├ P → Q. One may generalize it to a finite sequence of 
assumption formulas P1, P2, P3, …, Pn ├ Q: 
P1, P2, P3… Pn-1 ├ Pn → Q and repeat it until we obtain the 
empty set on the left-hand side: ├ (P1 → (…(Pn-1 → (Pn → 
Q))…). 
Deduction follows three kinds of steps: setting up a set of 
assumptions (hypothesis), reiteration - calling hypothesis 
made previously to make it recent, and deduction, which is 
removing recent hypothesis. If one wants to convert proof 
done using deduction meta-theorem to axiomatic proof, then 
usually the following axioms would have been involved: 
1) P → (Q → P) 
2) (P → (Q → R)) → ((P → Q) → (P → R)) 
3) Modus ponens: (P ∧ (P → Q)) → Q 
G. Corollaries 
Theorem 1––If formula expressible in FOPC language is 
deducible, then every possible transformation of this formula 
obtained by usage inference rules and axioms is also 
deducible, and can be expressed in the same language. 
Theorem 2––If every transformation of formula is 
Radosław Hofman, cSAT problem lower bound, 2007  
expressible in FOPC, then the optimal for certain resource for 
chosen computational model is also expressible in the same 
language. 
Proofs of these theorems are provided in the appendix 
( VI.A and  VI.B). 
One needs to focus on Theorem 1 and have good 
understanding of significance of Gödels work. Let there be 
considered some formula ϕ which is intended to be proven or 
disproved. Assuming that there exists some deterministic 
transformation T1 which transform formula ϕ to ϕ1: 
ϕ1=T1(ϕ), there can also exist another transformation T2 
taking ϕ1 as input and returning ϕ2 as output: 
ϕ2=T2(ϕ1)=T2(T1(ϕ)). Continuing this idea of 
transformations one reaches ϕTRUE or ϕFALSE formula 
allowing to prove or disprove ϕ. 
Theorem 1 is in fact summary of Gödels Theorem  [8], 
stating that ϕ, ϕ1, ϕ2… ϕx can all be expressed in FOPC 
language. 
Above in fact causes statement of Theorem 2: if every 
possible transformation / reformulation of formula is 
expressible in FOPC language, then (by power of every 
quantification) also optimal transformation is expressible in 
FOPC language. It does not matter what is nature of this 
transformations. If they are deterministic (for certain input 
always returns same output in finite number of steps). 
Optimal way to solve the problem (decide on formula) can be 
then written as: ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) 
III. CSAT LOWER BOUND 
A. Problem Definition 
In this work, the authors consider  a problem called “Count 
of Satisfaction of Boolean Expression for formula ϕ.” This 
problem is almost the same as the classical SAT problem, but 
instead of the question “Is there an assignment to variables 
such that formula ϕ is satisfied?”, they ask the question “Are 
there at least L assignments such that formula ϕ is satisfied?”. 
L in problem instance is written unary, and the remaining 
part of the instance is exactly the same as in SAT problem 
(the authors assume that it is in conjunctive normal form 
(CNF)). 
It is easy to show that the problem is in NP – Guess & 
Check algorithm, for NDTM requires O(L*n) steps to check 
(certificate size is L*v where v is the number of Boolean 
variables used). 
It is also easy to show that the problem is NP-complete. 
One can show it using reduction from SAT problem and ask 
the question “Is there at least L=1 assignment such that 
formula ϕ is satisfied?” 
B. Measurable Predicate 
Problem question is easy to understand by a human, but it 
certainly extends to FOPC language defined in Section  II. To 
express it in a defined language, one  needs to define 
predicate “µ” – measure. This predicate is a representation of 
sigma-additive (countably additive) measurable function 
known as “set cardinality.” Definition of this predicate 
requires one constant variable n – number of different 
Boolean variables used. Predicate “µ” will measure number 
of assignments satisfying formula ϕ. 
1: µ(∅) :- 0 
2: µ(TRUE) :- 2n 
3: µ(FALSE) :- 0 
4: µ(¬ϕ1) :- 2n-µ(ϕ1) 
5: µ(a1) :- 2n-1 
6: µ(a1∧a2…∧ak) 
 ∃ ai, aj: i≠j ∧ ai=¬aj :- µ(FALSE) 
 ∃ ai, aj: i≠j ∧ ai=aj :- µ(a1∧a2…aj-1∧aj+1...∧ak) 
  :- 2n-k 
µ(ϕ1∨ϕ2) :- µ(ϕ1)+µ(ϕ2)−µ(ϕ1∧ϕ2) 
One may think of adding some more conditions to this 
predicate, but the list given earlier is sufficient to calculate 
measure for every formula for a defined language (growth of 
number of axioms and definitions is discussed in Section  H). 
It is also compliant with sigma-measurable function 
definition. 
One may also observe that usage of measure leads to 
exponential number of calculations required for CNF. This is 
a consequence of sigma-additivity property: for any sets a 
and b: µ(a∪b)=µ(a)+µ(b)−µ(a∩b). If one considers m sets, 
then this function transforms to: 
⋅−=
})..({
aaPS Sa
aa IU µµ , where 
P({a1..am}) is power set over m sets, which means that it has 
2m objects in it. If one is able to calculate the measure of a set 
or intersection of sets, then the calculation of union of m sets 
requires Ω(2m) intersections to be measured. 
Problem question using predicate “µ” is then: “µ(ϕ)≥L?”. 
Direct calculation may not  be the only possible way for 
solving problems, and the authors now analyze the definition 
of lower bound, deterministic and nondeterministic 
computation models. 
C. Lower Bound Definition 
Lower bound in Big-O notation is denoted as Ω(g(n)), and 
for its use in this article, one may assume that it is used to 
express problem lower bound. Interpretation of lower bound 
is “minimum value of function in the worst case,” and is 
defined as f(n) ∈ Ω(g(n)) ⇔ 0
inflim >
∞→ ng
In most of the complexity considerations, two types of 
resources are used in the expressions of problem lower 
bounds or algorithm upper bounds. These resources are time 
(number of steps required) and space (number of 
symbols/tape cells required). 
Theorem 3––Time complexity of problem/algorithm is 
always greater than or equal to space complexity. This 
theorem is proved in Section  VI.C. 
Theorem 4––Minimal number of symbols required for 
unambiguous description of object is Ω(log(N)), where N 
represents the number of possible objects to be stored. In 
other words, this means that if one has N different objects that 
may occur in computations at a certain step and would want 
to store information on which one occurred, then Ω(log(N)) 
Radosław Hofman, cSAT problem lower bound, 2007  
symbols are required. This theorem is proved in Section 
 VI.D. 
In this work, the authors mainly  consider time complexity 
using observation from Theorems 3 and 4. 
Theorem 5––Lower bound calculated to express a specific 
resource (time or space) usage for deciding formula 
expressed in FOPC for a chosen computational model is 
equal to the minimal usage of this resource for the best 
possible transformation of formula in this language. This 
theorem is proved in Section  VI.E. 
Theorem 5 is consequence of Theorem 2. If one had set of 
deterministic transformations expressing optimal way to 
solve the problem:  
ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) then by power of 
definitions it can be shown that lower bound for problem 
solution is exactly equal to time required by this optimal 
solution. This is consequence of lower bound definition – it is 
asymptotically minimal amount of resource required to solve 
the problem. Repeating most important observations till this 
point: 
a) formula ϕ can be expressed in FOPC language (from 
Gödels Theorem  [8]) 
b) any possible transformation of formula can be 
expressed in FOPC language ϕ1=T1(ϕ) (Theorem 1) 
c) if every deterministic transformation can be expressed 
in FOPC language then also optimal deterministic 
transformation can be expressed in FOPC language   
(Theorem 2)  
ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) 
d) resource cost of optimal transformation of formula is 
equal to deterministic lower bound of the problem 
Roughly speaking, lower bound should be considered as 
the minimal amount of resource used for computation for the 
worst case. In case of time, it is the minimal number of 
operations to perform. It is even intuitive to see that if one 
could express calculation in some “steps,” then lower bound 
is equivalent to minimal number of “steps” required in the 
worst case. 
D. Nondeterministic Calculation Model 
Nondeterministic calculation model may be considered as 
the “luckiest possible guesser.” Such an approach expresses 
that the role of NDTM to answer a problem question is to 
guess the certificate and check it. If the check can be 
performed in O(nc) for some constant c, then one considers 
the problem as part of NP complexity class. 
One has to remember that DTM is a “special case” of 
NDTM where from every machine state, only one possibility 
to choose the next state exists, regardless of the symbol in the 
cell where the tape read/write head is positioned. This means 
that every problem solvable by DTM in O(nc) steps is 
solvable also on NDTM in at most same number of steps (or 
may be less). 
A good example expressing the differences between DTM 
and NDTM is the 2SAT problem (classic satisfaction of 
Boolean expression in CNF problem, but where in each 
clause there are at most two literals). This problem is solvable 
by DTM in O(n3) steps, but NDTM may guess the correct 
assignment and verify it in O(n). 
In terms of first-order logic and Herbrand’s theorem, one 
can see that NDTM is a verifier of Herbrand’s subformulas. 
When the formula is expressed using existential quantifier:  
∃ <a: assignment> F(a), then, according to Herbrand’s 
theorem, it is equivalent to: F(a1) ∨ F(a2)… ∨ F(ak). NDTM 
is able to check each of F(ai) simultaneously, even if the 
number of possible assignments is exponential, excepting 
when at least one of the computation paths led to an accepting 
state. 
One can see that for a nondeterministic calculation model 
problem, the number of steps of lower bound is equal to the 
minimal number of steps required to check the certificate. 
For example, for 2SAT problems one can have different 
approaches. 
Number of possible 
Herbrand’s 
subformulas 
Minimal number 
of steps to check 
each subformula 
Total 
calculatio
n cost 
1 2n N n 
(guessing only p 
variables) 
n*p3 N*p3 
(without splitting) 
3 n3 
 Table 1  Different approaches for nondeterministic 
calculation 
Table 1 presents different approaches differing mainly in 
the number of “guesses.” Calculation of problem lower 
bound for nondeterministic model of calculation returns the 
minimal number of steps required to check subformula. 
The last row presents the approach where the problem is 
not split, so it is calculated as in the deterministic model of 
calculations. 
E. Deterministic Calculation Model 
As mentioned in  Section D, deterministic model of 
calculations follows a single computation path. It is obvious 
that despite direct calculations, DTM can also perform Guess 
& Check algorithm (simulating NDTM). This time, the 
authors do not assume that DTM is the “luckiest possible 
guesser” and for lower bound complexity calculation of this 
approach, they have to assume that DTM is the “worst 
possible guesser.” This is also a consequence of the slight 
change in computation goal - NDTM has to “accept” when 
there is computational path leading to accepting state, while 
DTM has to “decide” on input, which means that the answer 
“NO” can be produced only when there is no possible way of 
reaching the accepting state (NDTM can be defined without 
rejecting state). 
Additionally, DTM requires an iterator (space on tape 
where number of current “guess” can be stored), which 
according to Theorem 4 requires Ω(log(H)), where H 
represents the possible number of “guesses.” 
Table 2 shows what time complexity would look like. 
Radosław Hofman, cSAT problem lower bound, 2007  
Number of 
possible 
Herbrand’s 
subformulas 
Minimal 
number of 
steps to 
check each 
subformula 
Total calculation 
cost 
1 2n N 2n*n+log(2n) 
2 2p n*p3 2n*n*p3+log(2p) 
K 1 n3 n3 
 Table 2 Different approaches for deterministic calculation 
In this table, the last row represents the minimal possible 
number of steps to calculate result. It is easy to show that for 
DTM, this row also presents deterministic problem lower 
bound because if any of the “guessing” approaches had been 
better, then it would have been used to present minimal 
deterministic calculation cost (we assume that values in the 
table are “best possible” not “best known” - see Theorem 5). 
F. cSAT Nondeterministic Algorithm Upper Bound 
Upper bound for algorithm solving cSAT problem is 
polynomial. It is a consequence of Herbrand’s theorem and 
ability of NDTM to: 
generate all possible subformulas in O(nc) 
verify each of them in O(nc) 
NDTM algorithm can be described using the following 
steps: 
1) Guess sets of measure L consisting of assignments of 
variables (time O(L*v)) 
2) Verify guessed set (time O(L*v)) 
This procedure leads to accepting the state (if at least one 
computation path is accepting) in at most O(L*v) steps and 
because instance size n∈Ω(L+v), the solution is provided in 
O(n2). 
G. cSAT Deterministic Lower Bound 
Now, using the observations described in the earlier 
sections, the authors calculate deterministic lower bound of 
cSAT problem (it is known that its nondeterministic upper 
bound is O(L*v)). 
First, one needs to write the problem in the FOPC 
language. One  uses the predicate µ: µ(ϕ)≥L. 
This problem may be considered to be harder than the 
classic SAT problem. If one tries to guess all possible 
subsets, then we would have Ω(
v22 ) subsets, so according to 
Theorem 4, it would require Ω(2v) symbols to store 
information about the considered subset, which, according to 
Theorem 3, leads to the conclusion that such a calculation 
requires at least Ω(2v) steps. “Guessing” only subsets of size 
L leads to Ω(2v) different subsets, so that it can be calculated 
by NDTM in polynomial time (Ω(v*L) steps), but requires 
Ω(2v*v*L) steps to calculate on DTM. 
In fact, following the assumption that DTM is the worst 
possible guesser, one may see that the number of hypotheses 
(“guesses”) used during computation can lead to an 
exponential usage of time if “depth” of hypothesis path is 
longer than O(log(n)) or any of the hypotheses has more than 
polynomial number of possible values. For example, if one 
states hypothesis A with possibilities, it is true or false 
(constant number of possibilities) and it is followed by 
hypothesis B (true or false), etc.; we need O(n) hypotheses 
before we can decide on formula, then in the worst case we 
require Ω(2n) steps to give the answer “NO.” 
Leaving then all Guess & Check approaches, the authors 
try to determine the minimal possible number of steps for 
DTM to decide on problem input. According to Theorem 5 
and considerations from the earlier sections, the authors 
conclude that the shortest possible path consists of steps 
transforming input formula to axioms of theory. If one can 
show that every transformation requires exponential number 
of steps or usage of object using exponential number of 
symbols to store, then it will be direct proof that lower bound 
of cSAT problem is over-polynomial. 
When will one be able to observe exponential growth of 
minimum number of required steps? If after using an axiom 
or predicate, one will obtain a formula of multiplicative 
length by a factor greater than 1. For example, if for formula 
of size n1 (considered to be in CNF), the authors use  Ax9) for 
one parenthesis, they obtain new formula in the format 
v1∧(n2,1)∨v2∧(n2,2)∨…∨vm∧(n2,m). In each of the m parts, 
one can use a variable from the beginning to remove all its 
negations from body, so |n2,*|<|n1|−m, but for very large n1, 
these parts of formula will still require further 
transformations, which if done only with  Ax9) would lead to 
exponential growth. Concluding this paragraph, one may say 
that if transformation reduces size of formula substring by 
O(nc) and multiplies this shorter string in formula making 
string grow to n2, where n2∈Ω(n1*c), then this path leads to 
exponential growth of formula and thus its lower bound is 
Ω(2n). 
In Table 3, the authors present the effect obtained by usage 
of every possible transformation, but before this the authors 
define polynomial purifying function for formula. This 
function will use axioms  Ax7),  Ax8),  Ax11),  Ax12),  Ax13), 
 Ax14),  Ax15),  Ax16),  Ax17),  Ax18),  Ax19),  Ax20),  Ax23), 
and two observations: 
µ(ϕ1)=µ(ϕ1∧(TRUE))=µ(ϕ1∧(v1∨v2∨…∨TRUE)); 
µ(v1∧ϕ1)=µ(ϕ2) where ϕ2 is obtained by replacing every 
occurrence of v1 in ϕ1 with constant TRUE. 
Roughly speaking, this function  looks for variables that 
can be cleared out from formula and prepare it for the next 
step of calculation. The authors assume that at every step of 
calculation, formula is in a form not allowing the use of any 
of the above axioms or rules. It is also important to remember 
that the number of transformation rules does not matter - refer 
to Section  H. 
Transfor
mation 
used 
Length 
string 
used 
Result 
string 
length 
Lower 
bound for 
path 
Remarks for “worst 
case” 
 Ax1)    
 Ax2)    
These axioms cannot be 
used since input never 
contains these symbols 
 Ax3) n1 n1 Ω(cSAT) 
 Ax4) n1 n1 Ω(cSAT) 
These axioms do not 
change formula length 
Radosław Hofman, cSAT problem lower bound, 2007  
Transfor
mation 
used 
Length 
string 
used 
Result 
string 
length 
Lower 
bound for 
path 
Remarks for “worst 
case” 
 Ax5) n1 n1 Ω(cSAT) 
 Ax6) n1 n1 Ω(cSAT) 
 Ax7)    
 Ax8)    
These axioms cannot be 
used because formula is 
transformed by purifying
function 
 Ax9) 
m1+m2+
2*m1*
m2+nr-
 Ax10) 
m1+m2+
2*m1*
m2+nr-
Used on two parenthesis 
replaces them with string 
of size 2*m1*m2, after 
using these axioms 
purifying function will 
reduce size but in the 
worst case only by 2 
symbols 
 Ax11), 
 Ax12), 
 Ax13), 
 Ax14), 
 Ax15), 
 Ax16), 
 Ax17), 
 Ax18), 
 Ax19), 
 Ax20) 
These axioms cannot be 
used because formula is 
transformed by purifying
function 
 Ax21) n1 n1 Ω(cSAT) 
 Ax22) n1 n1 Ω(cSAT) 
These axioms do not 
change formula length 
 Ax23)    As  Ax20) above 
µ1    
µ2    
µ3    
These rules cannot be 
used because formula is 
transformed by purifying
function 
µ4 n1 n1 Ω(cSAT) 
Can be used with  Ax21), 
 Ax22) or  Ax23), but 
does not change length 
of formula 
µ5    As µ3 above 
µ6 m1+m2 
m1*m2 
n  Treating formula as 
consisting of two parts 
 Table 3 Lower bounds for every possible transformation 
of cSAT formula 
The variables used in Table 3 are the following: 
n1 – Length of the formula 
nr – Length of the remaining part of the formula 
m1 – Length of first part/parenthesis of the formula 
m2 – Length of second part/parenthesis of the formula 
p1 – Number of parentheses in the formula 
 – The authors consider asymptotic behavior of the 
function, so one may use kind of “mean” m1 – representing 
Ω(m1). 
It is clear that in the worst case,  Ax9),  Ax10), or µ6 have to 
be used several times before purifying function would make 
significant reduction of length. Lower bound is considered as 
the minimal worst case, so from this table it is clear that in the 
worst case it is Ω(mp)=Ω(2p*log(m)) and because p and m are 
both O(n), the whole lower bound is Ω(2n). 
H. More Conditions and More Axioms 
The above considerations prove clearly that deterministic 
lower bound for cSAT problem considered with FOPC 
language defined is exponential. But one needs to answer one 
additional question – Is it the result of too poor FOPC axioms 
set definition? Or are too few predicates defined? 
In  [1] Baker–Gill–Solovay theorem, authors have shown 
that problem “Is P equal to NP?” can be relativized using 
oracles. Oracle is a machine (black box) that gives answers to 
certain type of problems in one step. One can then imagine 
that there are a very large number of oracles which can solve 
certain types of instances. DTM task is to pick up one of them 
(or use them sequentially because if the number of oracles is 
an attribute of the machine, then even if we have used 
millions of them, the complexity in terms of relation to 
instance size is O(1)). 
The authors presume then, that for cSAT problem, there 
exists some deterministic algorithm calculating answer in 
O(nc) steps. Following lower bound calculation, one knows 
that this algorithm calculates a result requiring Ω(2n) 
transformations. Reminding optimal transformation as 
described above: ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) 
and x∈Ω(2n). 
The presumption made here can be presented as existence 
of some transformation TA≡Tx-k(Tx-k-1(…(Tx-k-m(   ))…)), 
where m is exponential (TA is equivalent to exponential 
number of transformations in FOPC language, on optimal 
transformation path). The authors also assume that TA is 
deterministic, as deterministic lower bound is discussed in 
this section, and computable in polynomial number of steps. 
Now, one need to look on transformation path as on 
decision process, where at each step there is a decision to be 
made (decision which transformation is to be used). Each 
decision takes Ω(1) space to be stored. If m was dynamic and 
asymptotically equal to 2n, and also computable in 
polynomial number of steps then this would be equal to O(2n) 
decisions in O(nc) time what contradicts Theorem 3. 
Considering constant m (invented by algorithm designer) 
one may ask what is common in a large number of Turing 
machines (in the sense of defined algorithms), large number 
of axioms, large number of predicates, large number of 
oracles, or large m in above transformation TA? Their number 
is always a constant, even if very large. If then anyone defines 
multiple TMs, adds multiple axioms, predicates, defines 
large number of oracles, or finds one transformation TA 
equivalent to exponential number of other transformation, 
then in fact after defining them, one may have constant 
number of machines, axioms, predicates, transformations, 
and oracles. 
The authors then assume that there exists a machine 
denoted by LDTM in which implements are equivalent to 
large number of TMs, large number of axioms, predicates, 
implements TA and are connected to multitude of oracles. 
Such a defined machine is (by power of assumption) capable 
Radosław Hofman, cSAT problem lower bound, 2007  
of answering cSAT questions for a finite number of differing 
input types (number of types is a consequence of maximal 
input size). 
In other words, the authors assume that there exists a 
machine LDTM able to answer cSAT questions for instance 
size less than or equal to nl. They may consider having 
( )lncO  different input types, and each type is covered at least 
by one combination of axioms, predicates, or oracles 
allowing LDTM to give answer in O(n) steps. One may 
assume that there are gl such combinations. Denoting |gi(nl)| 
number of instances solved by ith combination of axioms and 
oracles for instance nl symbols long, the authors have 
assumed that: |||)(|
cng ≥∑
, where ( ) ||||
cng <∀
Now the authors determine the ability of this machine to 
answer cSAT question where n=nl*y. Number of 
combinations of axioms and oracles remain constant (gl), but 
they assume that each combination covers more instances 
(considered to be “same type”) gl(n)=gl(nl*y)≤gl(nl)
y. The 
number of possible types grows from ( )lncO  to 
( ) ( )( )ynyn ll cOcO =* . 
Calculating instances covered by gl definitions, we have: 
ngyng
|)(||)*(| . 
If one proves that for y growing to infinity 
lcng |||)(|
, it will be proof that not all instances of 
size O(nl*y) are solvable using LDTM definitions, so these 
large instances will require calculations using deterministic 
lower bound discussed in Section  G. Proof is presented in 
 VI.F, so corollary about impossibility to answer cSAT 
problems in polynomial time by LDTM holds. 
IV. COROLLARIES 
To summarize this article, the authors repeat the deduction 
path: 
a) formula ϕ can be expressed in FOPC language (from 
Gödels Theorem  [8]) 
b) any possible transformation of formula can be 
expressed in FOPC language ϕ1=T1(ϕ) (Theorem 1) 
c) if every deterministic transformation can be expressed 
in FOPC language then also optimal deterministic 
transformation can be expressed in FOPC language   
(Theorem 2)  
ϕTRUE/FALSE=Tx(Tx-1(Tx-1(…(T2(T1(ϕ)))…)) 
d) resource cost of optimal transformation of formula is 
equal to deterministic lower bound of the problem 
e) TA equivalent to exponential number of 
transformations computable in polynomial time 
contradicts Theorem 3 
f) large number of defined constant set of 
transformations, oracles, algorithms, machines ect. 
cannot cover all possible inputs for growing instance 
size (Theorem 6) 
g) optimal solution of problem requires Ω(2n) 
transformations 
h) deterministic lower bound for cSAT problem is then 
Ω(2n), then cSAT∉P (Theorem 5) 
i) NDTM solves cSAT in polynomial time, so 
cSAT∈NP 
j) this means that P≠NP 
If above considerations are correct then checking problem 
known to be in P has to show that it is in P using the same 
reasoning. Such check for 2SAT problem if presented in 
Section  VI.G - lower bound for this problem is Ω(nc). 
In  [1], there was presented an oracle A for which PA=NPA. 
Proof presented in Section  VI.F and problem lower bound 
lead to corollary, and if A is able to solve cSAT in 
polynomial time, then A has to be nondeterministic - it has to 
consist of infinite number of objects: deterministic oracles, 
algorithms, DTMs, axioms, rules etc. (the authors also 
consider NDTM as an infinite set of DTM duplicates - each 
for one computational branch). 
This work discusses problem P=NP, as described in  [5]. It 
may be said to relativize (see  [1]) to deterministic model of 
computation showing that deterministic calculation model 
made up of finite number of machines (algorithms), oracles, 
axioms, or predicates is incapable of solving the considered 
problem when its instance grows to infinity. 
On the other hand, one may conclude that if restrictions on 
maximum input length problem are set, then the problem can 
be proved to be in P using a large number of machines, 
axioms, algorithms, predicates, or oracles. 
For deterministic model of computation, one  knows then 
that P≠NP. 
Using Theorem 13 from  [12], the authors also know that 
NP-complete≠(NP-P). In this theorem, the authors have 
proved that: if P≠NP and U is some NP-complete language 
then U=A∪B where neither A nor B language is 
NP-complete (at least one of them is also not equal to P: A≠P 
∨ B≠P). Complexity classes can be put in a picture (Fig. 2): 
Figure 2 Relation between P, NP, and NP-complete classes 
V. REFERENCES 
[1] Baker T. P., Gill J., Solovay R., “Relativizations of the P 
=? NP question”, SIAM Journal on Computing, vol. 4, 
no. 4, 1975, pp. 431-442. 
[2] Barwise J., Etchemendy J., “Language Proof and Logic”, 
Seven Bridges Press, CSLI (University of Chicago 
Press) and New York, 2000. 
[3] Chandra A. K., Kozen D. C., Stockmeyer L. J., 
“Alternation”, Journal of the ACM, vol. 28, no. 1, 1981. 
[4] Cook S. A., “The complexity of theorem-proving 
procedures”, Proceedings of the Third Annual ACM 
Symposium on Theory of Computing, 1971, pp. 
151-158. 
Radosław Hofman, cSAT problem lower bound, 2007  
[5] Cook S. A., “P versus NP problem”, unpublished. 
Available at: 
http://www.claymath.org/millennium/P_vs_NP/Official
_Problem_Description.pdf 
[6] Diaby M., “P = NP: Linear programming formulation of 
the traveling salesman problem”, 2006, unpublished. 
Available at: http://arxiv.org/abs/cs.CC/0609005 
[7] Gallier J. H., "Logic for Computer Science: Foundations 
of Automatic Theorem Proving", Harper & Row 
Publishers, 1986. 
[8] Gödel K., "Über formal unentscheidbare Sätze der 
Principia Mathematica und verwandter Systeme", I. 
Monatshefte für Mathematik und Physik, vol. 38, 1931, 
pp. 173-198. 
[9] Hofman R., “Report on article: P=NP linear 
programming formulation of the traveling salesman 
problem”, 2006, unpublished. Available at: 
http://arxiv.org/abs/cs.CC/0610125 
[10] Jech T., “Set Theory: The Third Millennium Edition, 
Revised and Expanded”, ISBN 3-540-44085-2, 2003. 
[11] Karp R. M., “Reducibility among combinatorial 
problems”, In Complexity of Computer Computations, 
Proceedings of the Symposium of IBM Thomas J. 
Watson Research Center, Yorktown Heights, NY. 
Plenum, New York, 1972, pp. 85-103. 
[12] Landweber, Lipton, Robertson, “On the structure of sets 
in NP and other complexity classes”, Theoretical 
Computer Science, vol. 15, 1981, pp. 181-200. 
[13] Papadimitriou C.H., Steiglitz K., “Combinatorial 
Optimization: Algorithms and Complexity”, 
Prentice-Hall, Englewood Cliffs, 1982. 
[14] Razborov A., Rudich S., “Natural proofs”, Journal of 
Computer and System Sciences, vol. 55, no. 1, 1997, pp. 
24-35. 
[15] Savitch W. J., “Relationships between nondeterministic 
and deterministic tape complexities”, Journal of 
Computation and System Science, vol. 4, 1970, pp. 
177-192. 
[16] Tarski A., Givant S., “A Formalization of Set Theory 
Without Variables”, American Mathematical Society, 
Providence, RI, 1987. 
VI. APPENDIX 
A. Proof 1 - Proof of Theorem 1 
Theorem 1 - If formula expressible in FOPC language is 
deducible, then every possible transformation of this formula 
obtained by usage inference rules and axioms is also 
deducible and can be expressed in the same language. 
This theorem is a direct consequence of FOPC definitions. 
If ϕ is deducible, then: 
• ϕ ∧ axiom 
• ϕ → axiom 
• ∀ x ϕ 
are also deducible. 
B. Proof 2 - Proof of Theorem 2 
Theorem 2 - If every transformation of formula is 
expressible in FOPC, then the optimal for certain resource for 
chosen computational model is also expressible in the same 
language. 
This theorem is a consequence of Theorem 1 and FOPC 
definitions. If the goal of calculation is to decide on formula 
based on theory axioms, then it is required to obtain formula 
as a consequence of axioms (with empty left-hand side):  
├ (P1 → (…(Pn-1 → (Pn → Q))…). 
The authors said that every possible transformation of 
formula is expressible in FOPC and this directly means that 
the optimal in the aspect of a certain resource (time or space) 
path is also expressible in FOPC. 
C. Proof 3 - Proof of Theorem 3 
Theorem 3 - Time complexity of problem/algorithm is 
always greater than or equal to space complexity. 
This theorem is a consequence of Turing machine 
definition, which states that in one step, a machine can read or 
write one (or in general constant) number of symbols. If then 
f(n) symbols were written, then machine had used at least f(n) 
steps to write them. 
D. Proof 4 - Proof of Theorem 4 
Theorem 4 - Minimal number of symbols required for 
unambiguous description of object is Ω(log(N)), where N 
represents the number of possible objects to be stored. 
In this section, the function log is considered to have ∑ in 
root, where ∑ represents the number of the symbols in the 
alphabet: log(∑)=1. 
The authors prove the theorem using contradiction. 
Suppose that one knows “compression” algorithm allowing 
to write each of N symbols using log(N)−f(N) symbols, where 
f(N) is a function such that: ∀ N: 0<f(N)<log(N). 
On log(N)−f(N),one can write at most ∑log(N)-f(N) different 
strings. 
)log(
)log(
)log(
)()log(
NfNfNf
NfN NN
Now the authors check whether this number is greater than 
the number of objects to be identified by checking limens: 
lim  
It is easy to see that if f(N)=0, then limens is equal to zero 
(which means that exactly N different objects can be 
described using a string of desired length), but when f(N)>1 
(it is the smallest value making difference in the number of 
symbols used), it is negative which means that less than N 
objects can be represented using a string of this length. 
E. Proof 5 - Proof of Theorem 5 
Theorem 5 - Lower bound calculated to express specific 
resource (time or space) usage for deciding formula 
expressed in FOPC for a chosen computational model is 
equal to the minimal usage of this resource for best possible 
transformation of formula in this language. 
Proof of this theorem is in fact a direct corollary of 
Radosław Hofman, cSAT problem lower bound, 2007  
Theorems 1 and 2. If any transformation of formula is 
expressible in FOPC language, then the optimal in terms of 
chosen resource is also expressible in FOPC language and 
when the authors calculate lower bound for this resource for 
the whole transformation path (from input string to decidable 
form (to axioms)), then they obtain the value of lower bound 
for the considered problem. 
F. Proof 6 - Proof of Not Covering by Constant Set of 
Definitions All Possible Large Instances by LDTM 
Assumptions: ( ) ||||
cng <∀
 and |||)(|
cng ≥∑
. Also 
gi(n) function operates on natural numbers and returns natural 
numbers, so ( ) |1|||
cng . 
One want to solve yn
lcng |||)(|
 for y growing to 
infinity. 
First one may observe that: ∑∑
|1||)(|  if 
one can solve inequality yn
yn ll cc |||1|
, then it will be 
equivalent to prove that the proof is correct. 
The  new equality presented by the authors is free from i 
variables, so it can be rewritten as: ynyn ll ccl |||1|* <− . 
Now the authors take logarithm on both sides to the base l: 
( ) ( )
( ) ( ) ( )
( ) ( )
( ) ( )||log|1|log1
||log*|1|log*1
||log|1|loglog
||log|1|*log
At this point, it is obvious that this inequality holds - 1/y 
when y grows to infinity may be omitted and one has 
inequality of two logarithms where this one on the left-hand 
side is the logarithm of lower value. 
More formally, one may calculate limens: 
( ) ( )
1loglim
loglim
||log|1|log
lim  
Proof is then correct. 
G. Proof 7 - Lower Bound for 2SAT Problem 
2SAT problem is a special case of cSAT problem. Its 
special factors are: 
• L = 1 (problem question is “µ(ϕ)>=1” or 
“µ(ϕ)>0”) 
m1=m2=…=mp=2 
The authors assume that the input string is in CNF and 
purifying function (defined in Section  III.G) cannot be 
applied. 
They use  Ax9) on parenthesis to select next parenthesis 
such that: 
• parenthesis has not been used yet 
• parenthesis contains negation of variable used in 
a previous step 
Every time the usage of  Ax9) will be followed by purifying 
function usage. 
For example:  
(a∨b)1∧(a∨¬c)2∧(c∨d)3∧(¬b∨¬c)4∧(¬b∨¬a)5∧(¬d∨¬a)
6∧(e∨f)7 the authors would have used  Ax9) for parenthesis: 1 
and 6 (last variable is: ¬d), then 3 (lv: c), then 4 (lv: ¬b), then 
1 (second time, lv: a), then 5 (lv: ¬b), then 1 (third time, lv: 
a), then 6 (second time, lv: ¬d), then 3 (second time, lv: c), 
and finally 2. Every parenthesis will be used at most on every 
path from any pair of parentheses. 
At every stage, calculation formula will contain at most 
p+1 conjunctions (where p is the number of parenthesis 
processed) and each conjunction will contain at most every 
variable once. Every parenthesis will be used at most p2 
times, which means that at every stage of computation, 
formula length is O(p3). 
This may not be a time optimal solution. According to 
Theorem 2, optimal transformation path is expressible using 
axioms and predicates defined for FOPC, but to show that the 
problem is in P, one does not need to look for optimal 
transformation path - the authors have shown that there exists 
at least one transformation path polynomially bounded to 
instance size, and even if it is not the optimal one, it shows 
that 2SAT problem is in P.
