[FOM] Meta-logic

Sat Aug 19 18:10:01 EDT 2006

Dear Allen,

Quoting "A.P. Hazen" <a.hazen at philosophy.unimelb.edu.au> Wed, 16 Aug 2006:

>    Vladimir Sazonov says that he has shown that "in a  weak
> framework," the completeness theorem is provable iff NP=coNP.

Sorry, I want to retract this statement (for the predicate logic) and 
leave it as an open question. (But the "if" case is of course true 
under appropriate formulation.) Note that in my paper [2] which I 
referred to there was actually no such statement.

Can
> you tell  us,  Vladimir, how your "weak framework" compares to the
> systems in Simpson's book?

I will better give a positive description of the system and the 
formulation of the result (with some *corrections* to [2]). The problem 
is that the completeness theorem for FOL cannot be formulated 
straightforwardly in this weak framework. I rather mean appropriate 
"deterministic" or "constructive" (see below) approximation to its 
usual formulation. So, it is necessary to define everything almost from 
scratch.

Let P={p_0,p_1,...} be the sequence of all polynomial time computable 
operations and predicates

* over finite binary strings {0,1}* (variables x,y,z,...),

* over unary strings (1}* (called also natural numbers with the empty 
string representing 0 ? zero; variables i,j,k,...), and

* over infinite binary strings {0,1}^\infty (variables alpha,beta,...; 
alpha(i) denotes i-th bit in the string alpha).

The allowed values of operations from P are finite (unary or binary) 
strings or just truth values.

Computability is understood as usually in terms of Turing Machines - 
with oracles for infinite binary strings.

T2K denotes a second-order theory with the above three sorts.

Its primitive non-logical operations and predicates are

p_1,p_2,...

Note that the application alpha(i) to a unary string is actually among 
the above operations.

NON-LOGICAL AXIOMS of T2K are:

Ax1: All (universal closures of) bounded formulas (i.e. with 
quantifiers only of the form forall x < term and exists x < term where 
x does not occur free in the term and < means lexicographical ordering 
on the (finite) binary strings) true in the standard model with three 
sorts M = <{1}*, {0,1}*, {0,1}^\infty; p_1,p_2,...>.

In particular, Ax1 implies the bounded induction axiom (as well as 
sharply bounded one - with bounded quantifiers over unary strings). 
Analogously, the closure under composition for infinite string 
arguments also follows from Ax1.

Ax2: Extensionality for infinite binary strings,

Ax3: Separation for infinite strings and bounded formulas B:

          exists alpha forall i (alpha(i)<=> B(i)),

Ax4: Konig?s axiom (Lemma) for the binary trees given by any bounded 
formula B(x).

Now, before formulating the main result on T2K some preliminary 
considerations are necessary.

Note that T2K does not prove that the exponential (exp) is total function.

In particular, it is the open question in T2K whether some polynomial 
time computable enumeration x_i (with i unary) of ALL finite binary 
strings does exist (and is consistent with the assertion that exp is 
not total function).

However there exists a good candidate \xi_i (polynomial time computable 
polynomial optimal sequence of binary strings - in fact, the fastest, 
up to a polynomial, sequence of binary strings; it can be explicitly 
defined in terms of the Universal TM; see [1]).

Assuming that exp is total, \xi_i can be easily shown to enumerate all 
finite binary strings. Otherwise it is an open question in general. In 
any case, the set of so called *deterministic* or *constructive(ble)* 
finite binary strings

{\xi_i : i is unary string}

is closed (provably in T2K) under polynomial time computable 
operations. (Note that unary strings are evidently constructive.) So, 
this set serves as a *constructive* approximation to the set of ALL 
(from the point of view of T2K) finite binary strings. Non-constructive 
finite binary strings are called *random*. (They do not exist if exp is 
the total function.)

That exp is not provably total in T2K is the key point in the further 
considerations. You know that completeness proof of propositional logic 
(PL) requires (the total) exp (at least it is unknown whether it can be 
done better). Therefore the more general case of first order logic 
(FOL) also requires exp.

Now, the question is what is the meaning of one of the known proofs of 
completeness of FOL *in the framework where exp is not provably total*, 
whether it can be imitated. Thus, our attention to such a theory as T2K.

Note that (some of) finite binary strings can evidently serve as (codes 
of) first-order formulas. (This is decidable in PTIME.)

Trying to imitate in T2K the well-known proof of completeness of FOL 
based on Konig Lemma, we can define a polynomial time computable 
sequence F_i^alpha (relative to alpha) of +/- signed formulas with 
F_0^alpha = +F a given formula F with the sign + meaning that we 
evaluate it as true; see [2] for the details and appropriate comments 
below (on the participating sequence \xi_i). By construction, this 
sequence F_i^alpha satisfies (provably in T2K) some natural closure 
properties (for example, if +(A&B) appears then both +A and +B appear 
too, and analogously for negated and quantified formulas).  Moreover, 
*in the traditional framework* (say, in ZFC)

Th: A sentence F is satisfiable in some model iff

(*) for some alpha there are no such (unary) i and j that both 
F_i^alpha = +G and F_j^alpha = -G hold.

(Otherwise neg(F) is called a tautology.)

Then using Konig Lemma would eventually give the evident enumeration 
procedure or the proof system for all first-order tautologies leading 
to a form of completeness theorem.

BUT this theorem cannot be imitated straightforwardly and fully in T2K, 
because exp is not provably total and we cannot guarantee that 
F_i^alpha  evaluates (by +/-) ALL possible first-order sentences. But 
we can adapt the construction of this sequence by appropriate 
incorporating in its definition/computation the above sequence \xi_i of 
constructive finite binary strings; see [2] for the details. This will 
guarantee that the polynomial time computable sequence F_i^alpha will 
consist of ALL (+/- signed) FOL sentences represented by finite 
*constructive* binary strings, (assuming that the initial formula F is 
such).

This leads to the following theorem

T2K |- forall constructively presented F:
F is a FOL-tautology
[i.e. its negation is not not satisfieble in the sense of (*)] iff
exists n forall x(|x|=n => CLOSED(neg(F),x))

where CLOSED(G,x) abbreviates exist i,j<|x|(G_i^x=-G_j^x) with the 
finite string x in the superscript considered as representing the 
infinite string x000... .

Note that the statement forall x(|x|=n => CLOSED(neg(F),x))
can be reduced to an equivalent propositional tautology (represented by 
constructive binary string). It follows

MAIN RESULT:
Provability in T2K of existence of a proof system (in the sense of Cook 
and Reckhow) for propositional tautologies will give rise to a proof 
system for FOL-tautologies, and vice versa. [IMPORTANT: Here we tacitly 
assume ONLY those candidates for tautologies representable by 
***constructive*** binary strings.]

Thus, in the absence of the (provably) total exp function we can only 
prove (in T2K) that the *existence* of complete calculi for 
propositional and predicate logic (only for the tautologies represented 
by constructive binary strings) are equivalent. So, in principle it is 
possible that only for constructively presented tautologies we have 
proof system in the framework of T2K.)

Of course, T2K + the totality of exp proves the completeness both of 
propositional and predicate logic (in the traditional sense, as all 
finite binary strings are constructive in this case).

It is evident that CoNP=NP would imply the provability in T2K of 
existence of proof systems both for (full, not only constructively 
presented) propositional and hence for (constructively presented) 
predicate logic.

For the full language of predicate logic we even do not have the 
reasonable concept of tautology (or satisfiability in a model) in the 
absence of the total exp.

FINAL NOTE: Presentation Ax1 in T2K in terms of a set of all TRUE 
bounded formulas in the standard model is not an essential point. We 
could restrict the language of T2K to a finite basis and Ax1 to several 
quantifier-free axioms (with free variables) describing these 
operations plus the schema of Bounded Induction. Then formulation of 
some results would be only slightly changed, if necessary.

Refereces:

[1] V.Sazonov, A logical approach to the problem "P=?NP", in: MFCS'80, 
Lecture Notes in Computer Science, N88, Springer, New York, 1980, 
P.562--575. (An important correction to this paper is given in [2, 
Page.490.]) http://www.csc.liv.ac.uk/~sazonov/papers.html

[2] V.Sazonov, On existence of complete predicate calculus in 
metamathematics without exponentiation, MFCS'81, Lecture Notes in 
Computer Science, N118, Springer, New York, 1981, P.483--490. 
(Available by request)

Best wishes,

Vladimir Sazonov

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.