- (s)(P(s) → R(s))
I find the following way of securing self-reference easier to understand. Start with a language that has nestable quotation marks, which I'll represent with ‘...’, and some string manipulation tools. I'll use straight double quotation marks for meta-language quotation. Add to the language a new symbol "@" which is ungrammatical (i.e., no well-formed formula may contain it). For any sequence of symbols s, we define two new sequences of symbols N(s) and Q(s) by the following rules. If s contains no quoted expressions or contains imbalanced opening and closing quotation marks, N(s) and Q(s) are just "@". If s contains a quoted expression, Q(s) is the first quoted expression, without its outermost quotation marks (but with any nested quotations being included), and N(s) is the result of taking s and replacing that first quoted occurrence of Q(s), as well as its surrounding single quotation marks, with "@". Thus:
- Q("abc‘def‘ghi’’+jkl")="def‘ghi’"
- N("abc‘def‘ghi’’+jkl")="abc@+jkl".
- (s)(‘(s)(@=M(s) → R(s))’=M(s) → R(s)).
One can also adapt this to work with Goedel numbers and hence presumably for use in proving incompleteness.
[Removed a nasty typo.]
3 comments:
So, if valid argument, FOL shows it valid. Thus FOL's complete
Ergo you're discussing undecidability--which as the halting problem shows, are a very few self-referential statements (ie, the procedure will show invalidity...approx. 99% of the time....) How many undecidable arguments are there? Well if only a very few, and they are all self-refential (ie something like for all x, X loves All--> X loves herself), then you write an app to get rid of those very few glitches, and bada bing....the system's near perfect .
in short thats what programmers have done. Were undecidability a real issue, your OS would not work, nor would massive servers/DBs crunching numbers (say for mission critical stuff).
Ergo, the Paradox fetish is overrated (and...Goedel himself not the final word--his numbering system very obscure).
Those who assign Godel's incompleteness theorem an incidental purpose, because math can go on very well thank you ... miss the point. Godel showed math wasn't a perfectly lawful game, as Hilbert believed. It depends on natural numbers (which most kids figure out, when they learn algebra.) Concepts make laws, but it's nice to examine them first. Trouble is, there's nothing to examine with natural numbers - they just are. It's fine to program away. But what about AI? It's been almost here since the 80s, but seems farther off now. Trust 'mission-critical stuff'? One mission critical mess-up and we're toast. Numbers are the basis of programs. How many programmers think it doesn't matter whether numbers are science, a lawful game, or a social contract?
Post a Comment