I see now that my sketch proof of "completeness" for Rob 
Arthan's proposed new "new_specification" cannot be turned 
into a rigorous proof.

When withness are obtained using the choice function, they 
may fail the fourth of his specified constraints on the 
witnesses.  They will do so in just the kinds of case which 
Rob was particularly interested in, viz. those in which the 
constants are characterised through some universal property.
If the extension is conservative then there must be values 
for all the constants in every model of the theory being 
extended, but possibly there might not be terms which denote 
those values.

Whether the new "new_specification" is or is not "complete" 
(in the sense which I identified) is now (once again) unclear 
to me.  My purported "obvious proof" of completeness is 
fallacious, but its failure does not yield a proof of 
incompleteness.

Roger Jones

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to