Re: Simple yet Profound Metatheorem

David C. Ullrich wrote:
> On 16 Dec 2005 11:07:53 -0800, "Charlie-Boo" wrote:

> All you have to do is explain what your notation means.

[] means necessity. |- means provability. Since "There is an
overwhelming diversity of systems of modal propositional logic. Their
accounts of theorem differ from one another. [We can] take the box of
modal logic to mean 'it is provable' rather than 'it is
necessary'.'" (The Unprovability of Consistency, George Boolos)
but |- always means provable, I use |- for provable rather than [].

> >> Or, in extremely bad notation: |- (|-Q == Q)
> >> (bad notation because the first |- means |-, while
> >> the second |- refers to some encoding of provability)

> >And [] ( []Q == Q ) ?

> Is it extemely bad notation? No.

Don't you see the parallel? If |- (|-Q == Q) is extremely bad
notation because the first |- means |- while the second |- refers to
some encoding of provability, then [] ( []Q == Q ) is extremely bad
notation because the first [] means |- while the second [] refers to
some encoding of provability.

I'll have to break the bad news to Boolos, Kripke, Solovay et, al.

> >( P = |- Q) => ( P = |-P) because P must be r.e.

> Uh, this is gibberish. A set of natural numbers is or is not
> r.e. What the hell does it mean to say that a wff is r.e.?

Since the relation (over its free variables) |-Q is recursively
enumerable for any Q, and P = |-Q, then relation P is recursively
enumerable. (Wffs express relations.)

> "red herrings about syntax". Right.

There's nothing more trivial than a purported syntax error, yet you
use it to trump all other considerations and proof that the author
doesn't know anything about the subject. And when you consider the
fact that there is so little formal standardization in logic (there is
no ANSI for mathematicians), it's silly to even claim that a certain
syntax can't be used because it is not "standard".

I once surveyed about 20 proofs of the Recursion Theorem to determine
the most common syntax used to express it. I couldn't. Every proof
used a different syntax. Try it and you'll see. Even referring to
"Godel's 1st. Incompleteness Theorem" is wrong, because there are
two 1st. theorems in Godel's 1931 paper - based on soundness and
based on w-consistency. (Someone once published a survey of syntaxes
used in logic and the variations were enormous. Also note the Boolos
quote above.)

A more productive attitude is "Let's represent . . . with the
syntax . . . as that is probably more commonly used. Then . . ."

> > Thm. ((|- P) = (|- Q)) => |- (P=Q)

> This is obviously false.
> If neither P nor Q is provable (so that
> ((|- P) = (|- Q)) is true) it certainly
> does not follow that P==Q _is_ provable.

Let's suppose that P is "1>2" and Q is "2>3". Then P==Q is
(1>2)==(2>3) which IS provable.

> ************************
>
> David C. Ullrich

.

Relevant Pages

  • Re: Program compression
    ... means using tools (such as parse-tree rewrite rules or syntax ... enough keyword and/or syntax to trigger expansion back to the full ... let's say you have a text string which contains the notation ... favorite notation for nested lists is, ...
    (comp.programming)
  • Re: PHP global namespace clogged up
    ... >> the OO side of PHP for many months after I first started learning it. ... >> notation may strenghten one of PHP's weaknesses, ... > to climb - one for the procedural syntax and one for the OO syntax. ...
    (comp.lang.php)
  • Re: First class types and their representation
    ... It makes sense to use a common representation ... now, the notation is a little hairy, but it is possible to map much of a C ... however "i" is regarded as a single element terminating after the the ... types, but thus far this has not been needed (if I were to add a syntax, I ...
    (comp.lang.misc)
  • Re: modifying array access syntax
    ... What I had in mind is something that resembles standard notation for the field in question, ... Recall that for beginners in mathematics, the notations typically used in mathematics are by far not obvious. ... So I think the basic tradeoff is as follows: If your interest is to develop the code for your own experiments, it's probably more effective to invest some time into learning the Lisp syntax in order to forget about syntactic issues altogether in the long run. ...
    (comp.lang.lisp)
  • Re: PHP global namespace clogged up
    ... > success is based on it's easy accessibility. ... > notation may strenghten one of PHP's weaknesses, ... > compulsory OO notation will undermine it's fundamental strength of easy ... to climb - one for the procedural syntax and one for the OO syntax. ...
    (comp.lang.php)