From: Frederick Williams on
Charlie-Boo wrote:
>
> ... I was
> going to figure out the exact relationship between that approach and
> mine.

Go on then.

--
I can't go on, I'll go on.
From: Frederick Williams on
Charlie-Boo wrote:

> get. (This is something the authors of ZFC axioms' representations do
> not realize when they choose FOL as the language of choice.)

That'd be Skolem.

> And we can generate an extremely wide array of possibilities of other
> very interesting questions regarding formal systems: Is P equivalent
> to |-|-P? |-P and ~|-~|-P?

See L\"ob 'Solution of a Problem of Leon Henkin' JSL, 1955; or, if you
read German, Hilbert & Bernays. Oh, and Jeroslow, 'Redundancies...' JSL,
1973.

--
I can't go on, I'll go on.
From: Frederick Williams on
Charlie-Boo wrote:

>
> Well, let's see. I call this system ABC because I represent wffs
> using letters where
>
> A = |-
> B = ~
> C = (all X)
>
> Notice that P is actually free. The empty string [] represents P. So
> we have e.g.
>
> A = |-P
> B = ~P
> C = (allX)P(X)
> AA = |- |- P
> AB = |- ~P
> AC = |- (allX)P(X)
> BA = ~|-P
> BB = ~~P
> BC = ~(allX)P(X)
> CA = (aA)|-P(A)
> CB = (aA)~P(A)
> CC = (allX)(allY)P(X,Y)
> etc.

Is this alphabet soup of interest to anyone other than you?

--
I can't go on, I'll go on.
From: Frederick Williams on
Charlie-Boo wrote:
>
> On Jul 3, 5:30 am, Frederick Williams <frederick.willia...(a)tesco.net>
> wrote:
> > Charlie-Boo wrote:
> >
> > > Well, let's see. I call this system ABC because I represent wffs
> > > using letters where
> >
> > > A = |-
> > > B = ~
> > > C = (all X)
> >
> > > Notice that P is actually free. The empty string [] represents P. So
> > > we have e.g.
> >
> > > A = |-P
> > > B = ~P
> > > C = (allX)P(X)
> > > AA = |- |- P
> > > AB = |- ~P
> > > AC = |- (allX)P(X)
> > > BA = ~|-P
> > > BB = ~~P
> > > BC = ~(allX)P(X)
> > > CA = (aA)|-P(A)
> > > CB = (aA)~P(A)
> > > CC = (allX)(allY)P(X,Y)
> > > etc.
> >
> > Is this alphabet soup of interest to anyone other than you?
>
> Are you saying that you don't understand it? Do you know what I'm
> doing? I'm listing the first few wffs. Their representation is any
> string of alphabet {A,B,C} so it's real easy to list wffs. Then the
> idea is to see how each would be represented using the provability
> predicate, to compare the two approaches.
>
> Does that help?

Does your ABC system have any theorems? If so, do they have any proofs?

--
I can't go on, I'll go on.