Re: Simple yet Profound Metatheorem

On 19 Dec 2005 07:31:22 -0800, "Charlie-Boo" <chvol@xxxxxxx> wrote:

I don't know whether you've noticed this, but others
have: You complain that I'm just quibbling about syntax,
and at the same time you ignore most of my comments
about the substance of your 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 [].

Yes, we can take [] to represent various things, including
provability. What's your point? Did I say we couldn't do
that? (Was I supposed to know somehow that that's what you
meant by the [] below?)

>> >> 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.

Oh for heaven's sake. How was I supposed to know that that two
[]'s meant entirely different things? Yes, if that's the case
then it's extremely bad notation.

_Incredibly_ bad notation, actually. It's been pointed out
that when you use |- to mean two different things that
makes things impossible to parse. You decide to introduce
a new symbol for |-. Instead of taking advantage of the
new symbol by letting it denote one thing and letting |-
denote the other thing you decide that the new symbol
should _also_ mean two things.

Good idea.

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

Do they use one symbol two mean two different things in the
same expression? I doubt it.

>> >( 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.)

This is gibberish. |-Q is not a wff, it has no free variables.
It is an assertion about a wff.

>> "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 haven't said you couldn't use any particular notation.
I _said_ all you had to do was explain what the notation
meant. But one thing you _cannot_ do is use one notation
to mean two different things. Complaining about that is
not complaining that you're not using the right symbols
for concepts, it's complaining that you're insisting
on using an _ambiguous_ syntax.

This is really a pretty feeble response to my explanations
of why, once we sort out what you mean, the things you've
been saying are nonsense.

>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.

Huh? I didn't say that it is never the case that P==Q is
provable. I said that this does not follow from the assumption
that neither P nor Q is provable.

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


************************

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: About those parenthesis....
    ... > So a better notation than fis quite simply f. ... > I have programmed with Lisp-like semantics using the fsyntax. ... > Even when the first symbol /is/ an operator, ... that this is not a valid reason for making it look like one of the ...
    (comp.lang.lisp)