[FOM] Cylindric Algebra and Consistency

[Vaughan Pratt]

On 5/27/2011 3:14 PM, Dana Scott wrote:
> Starting with the last variable, xn, we can choose
> either to COMPLEMENT the variety (as a subset of
> a higher dimension), or to PROJECT the subset down
> to the next lower dimension.  We can notate such
> a sequence of operations by symbolic combinations
> such as
>
> 	CPPCPPPCPCP...CPCP(V)
>
> with at most n P's. (We work here from the inside out
> projecting and complementing as directed, treating
> the variables in the order xn, x(n-1),...,x2,x1.)

My understanding was that varieties are closed with respect to the 
Zariski topology (as generated by the complements of the algebraic 
sets).  Hence I don't see how this can work for more than the 
sublanguage of PA consisting of those formulas whose matrix (assuming 
prenex normal form) consists of atomic formulas all of the same sign; 
equivalently a possibly negated monotone combination of atoms.  Since no 
nontrivial induction hypothesis φ(x) ⊃ φ(x+1) can have this form, it's 
not clear to me how this sublanguage could bear on Con(PA).

Modulo that detail, Dana makes essentially the same point I made on 
Wednesday at http://www.cs.nyu.edu/pipermail/fom/2011-May/015509.html in 
reply to Tim Chow:

> From a naive set theoretic standpoint the "properties of N" form the
> power set of N (or of N^k when there are k free variables in the formula
> at hand). The meaning of a formula in prenex normal form is obtained by
> starting from the predicate defined by the matrix and alternately
> complementing and projecting out dimensions as you work up the stack of
> quantifiers. It is an article of faith of naive set theory that the
> results of these operations are well-defined, ostensibly justifying your
> claim that "a first-order formula defines a precise property of N."

(If one needs a finite code for the predicate denoted by the 
quantifier-free matrix, the matrix itself can presumably serve that 
purpose, and I don't see a better code offhand for an arbitrary Boolean 
combination of the denotations of the atoms.)

However I then made the point that this line of reasoning is 
set-theoretic.  Without further qualification beyond the remark that 
Replacement doesn't seem to be needed, it would appear to assume Con(Z).

Intuitively the reasoning is simple enough that it ought not to need the 
whole of Con(Z).  And in fact we have a proof of this, in the form of 
Genzen's proof of Con(PA).

Perhaps there is some other way besides Gentzen's proof of seeing that 
not all of Con(Z) is needed in this denotational-semantics proof of 
Con(PA), but so far no one seems to have offered one.

Vaughan Pratt