[FOM] Cylindric Algebra and Consistency
Vaughan Pratt
pratt at cs.stanford.edu
Sat May 28 05:32:06 EDT 2011
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
More information about the FOM
mailing list