Prev: proof of existing quine
Next: i will play the part of Androcles.
From: zuhair on 13 May 2010 23:59
On May 10, 10:13 am, Marshall <marshall.spi...(a)gmail.com> wrote:
> On May 7, 2:20 pm, zuhair <zaljo...(a)gmail.com> wrote:
>
> > On May 7, 8:18 am, Marshall <marshall.spi...(a)gmail.com> wrote:
>

>
> I regret I don't have time to respond to all of your detailed
> comments.
> Let me just explain the bit about substitution. (It's a consideration
> that's
> important to me and my applications; it may have no relevance to
> you at all.)
>
> Consider the subset of first order logic in which quantifiers are
> limited
> to a single level of universal quantification.

Marshall wrote:

Quote---------------------------------------------------------------------------------------------
This is related to
> equational logic. In such cases we can omit the quantifiers entirely;
every unbound variable is implicitly universally quantified. This
allows us to write the associative property like this:

    x ^ (y ^ z) = (x ^ y) ^ z

Quite terse and easy to understand, imho.
-------------------------------------------------------------------
Quote finished.

Well, I don't see were this system fail your desired
properties.

the above can be simply be written using this system as:


x. y z = x y. z

I know you are using variables.

However suppose we are using formulas Q,P,R

then we can have the following:

Q. P R :<> Q P. R

Zuhair


>
> In such a system, every variable in any true formula can be
> replaced with any expression, and it will yield a true formula.
> (Modulo issues of name capture.) The replacement, or
> substitution, can be simple textual substitution.
>
> This is an important property, and one which I don't think
> you're supporting. But it may not matter to your particular
> application.
>
> Also, and I wish I had thought of this sooner, but here's a
> paper that you really ought to read:
>
> from Boolean Algebra to Unified Algebra
> Eric C. R. Hehner
>
> http://www.cs.toronto.edu/~hehner/BAUA.pdf
>
> I was quite taken by this paper. I really didn't think
> there was much useful to say about syntax, and this
> paper demonstrates otherwise.
>
> In looking it up, I discover that he also has some new
> papers on similar topic; I can't vouch for them, but I
> will certainly read them. Who knows, he may have something
> awesome or he may have gone off the deep end. :-)
>
> Oh, another tiny comment: the "rationale" as it were for
> ^ and v being used for AND and OR comes from lattice
> theory. Boolean algebra is a kind of lattice algebra, and
> those symbols make exquisite sense in the context of
> lattices.
>
> Marshall

First  |  Prev  | 
Pages: 1 2 3 4
Prev: proof of existing quine
Next: i will play the part of Androcles.