If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

[Graham Cooper]

Formal Theory means all sentences in the Theory are systematically
enumerated.

ZFC is NOT a formal Theory!

There is no method given to distinguish between theorems and predicate
calculus formulas.

X=X is a formula.
!(X=X) is a formula.
E(X) !(X=X) is a formula.

XeX is a formula
!(XeX) is a formula
XeY is a formula
XeY <-> !(XeX) is a formula
A(X) XeY <-> !(XeX) is a formula
E(Y)A(X) XeY <-> !(XeX) is a formula

there are many, many wrong formulas in Predicate Calculus.

Predicate Calculus is just the SYNTAX CHECKER.

10 prnt "hello"

SYNTAX ERROR

10 print "hello"
20 goto 10

does not guarantee a WFF. (program)

You have NO WAY of enumerating Theorems!

Herc

[Frederick Williams]

Graham Cooper wrote:
>
> Formal Theory means all sentences in the Theory are systematically
> enumerated.
>
> ZFC is NOT a formal Theory!
>
> There is no method given to distinguish between theorems and predicate
> calculus formulas.
>

> [...]

>
> You have NO WAY of enumerating Theorems!

What is enumerated is G\"odel numbers of theorems. So which theorem
comes first depends on the enumerator and the G\"odel numbering.

--
Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.

[George Greene]

On Oct 5, 3:59 am, Graham Cooper <grahamcoop...@gmail.com> wrote:
> Formal Theory means all sentences in the Theory are systematically enumerated.
>
> ZFC is NOT a formal Theory!

You are Lying.

> There is no method given to distinguish between theorems and predicate calculus formulas.

There is no such thing as a "predicate calculus formula".

It does not matter what you think "formal theory" means or what you
think "predicate calculus formula" means.

The theory we are talking about is first-order ZFC.
It is a theory in standard classical first-order logic.
Like all such formal theories, it is defined as the theory that
follows from ITS AXIOMS.
ZFC "is", first and foremost, A SIMPLE SET OF AXIOMS.
A theory then FOLLOWS from them.


> X=X is a formula.

No, it isn't.
ZFC is a language with ONE binary predicate, set-membersip.
" = " is A DEFINED term. It's a MACRO. It's an ABBREVIATION.
Anything in ZFC that can be said with = can be said WITHOUT it.

> XeX is a formula

Not really. You are using capital letters. That is a mistake.

> there are many, many wrong formulas in Predicate Calculus.

YOU DON'T KNOW what "predicate calculus" MEANS!
What YOU ARE CALLING "predicate calculus" is what the people WHO
ACTUALLY KNOW WHAT THESE TERMS MEAN
are calling a first-order language. In this particular investigation,
THE (there is only one) first-order language involved is a very
simple one: it has ONE binary predicate -- e. It also has one
constant -- O -- and a couple of unary functions that you could
think of as Skolem functions for the axioms that require the Union of
a set (of sets) and the Power set (of a set) to exist.

> Predicate Calculus is just the SYNTAX CHECKER.

There is a syntactic notion of consequence but you are lying about
what predicate calculus IS.
ANY *calculus* is a method FOR CALCULATING something. It is a method
for DERIVING RESULTS
from initially-posed problem-statements. It is the kind of thing that
allows you, when given 34 and 35,
to derive or CALCULATE that their sum is 69. The "syntax-checker" is
just the rules of construction & grammar
for a first-order LANGUAGE. Predicate calculus is the system that
lets you DERIVE LOGICAL CONSEQUENCES OF
sentences in that language.

> You have NO WAY of enumerating Theorems!

You are LYING, Herc.
You DON'T KNOW what a THEOREM *is* !!
A THEOREM is something that GETS PROVED!

First-order logic has bunches of inference rules for INFERRING AND
PROVING things
from PREVIOUSLY accepted statements. OR FROM NOTHING, in the case of
( P V ~P ).
From the first-order viewpoint, any and every 0th-order tautology
really can be inferred from
nothing, if it's in the language. Even if the 0th-order version isn't
in the language, replacing
the propositional letters in a tautology with formulas that ARE in the
language will yield
a first-order validity that is valid for the same reasons that made
the 0th-order version tautologous.

The way in which we enumerate theorems is BY PROVING them.
Every theorem has at least one proof and that suffices to enumerate
all of them
since they all have DIFFERENT proofs.

[George Greene]

On Oct 5, 8:47 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:

> What is enumerated is G\"odel numbers of theorems.  So which theorem
> comes first depends on the enumerator and the G\"odel numbering.

But the point is, you don't even have to go as far as actual numbers,
and you don't (and shouldn't) accept
an ignorant newbie's terminology.
If you take any first-order language at all (over a finite signature),
the theory of its VALIDITIES is recursively enumerable.
You can enumerate the validities just by deriving them. Each PROOF
can BE a number, not merely HAVE a godel number --
there are many different NUMERALS and numeration-systems possible!
You don't NEED to BOTHER with anything as complicated as a godel-
numbering!

You just have to be AWARE that since the DEFINITION of "theorem" is a
sentence THAT GETS PROVED,
the proof itself can BE the number. The proving IS the enumerating.
Most people get this quickly.
The person you are talking to is new and skipped the basic course.

[George Greene]

On Oct 5, 3:59 am, Graham Cooper <grahamcoop...@gmail.com> wrote:
> Formal Theory means

SHUT UP.
You DON'T KNOW.
When WE say "formal theory" -- it's OUR term -- it means
a theory where every sentence in it WAS FORMALLY DERIVED FROM
an initial set OF AXIOMS -- and the initial set was halfway simple and
easy-to-describe.
The usual criterion is that it has to be [totally] recursive.

If the axiom-set was recursive then the formal theory of its
consequences will be recursively enumerable.
In othr words, the "enumerability" HAPPENS AUTOMATICALLY
*in*the*definition* of a formal theory
as being generated using the process of PROOF or derivation or
inference using a system of RULES
of inference, which is also known as a LOGIC. In THIS case, the logic
in question is standard
classical first-order logic. It has some rules of inference which you
could learn if you would ever
take a course. It does NOT NEED ANY logical AXIOMS beyond the 0th-
order tautologies (and
anything 1st-order that matches their structure via substitution of a
1st-order formula for a propositional letter).

[George Greene]

On Oct 5, 3:59 am, Graham Cooper <grahamcoop...@gmail.com> wrote:

> Formal Theory means all sentences in the Theory are systematically
> enumerated.

Tht's Lie #1 . Who are you supposed to be? MItt Romney?

> ZFC is NOT a formal Theory!

That's Lie # 2. It's usually defined as an axiom-set but if you want
to TALK set theory then it is
the formal theory containng all and only the theoerms PROVEN FROM
those axioms.

>
> There is no method given to distinguish between theorems and predicate
> calculus formulas.

This is Lie # 3. It's not immediately rebuttable because you don't
know what "predicate calculus formulas" MEANS, and because we don't
talk that way.

> You have NO WAY of enumerating Theorems!

That's more like Lie # 0. THAT statement was BORN a lie.
Since theorems are BY DEFINITION *proved*, they are BORN "enumerated".
A theorem's proof IS its "number".

[Graham Cooper]

George's idiocy is in full bloom here!

His underlying contradictions and FAILURE TO STATE THEOREM 1 of ZFC
result in this copious false output and misunderstandings of what a
theorem, formula, or theory actually are.

Herc

[Frederick Williams]

Graham Cooper wrote:

>
> George's idiocy is in full bloom here!
>
> His underlying contradictions and FAILURE TO STATE THEOREM 1 of ZFC
> result in this copious false output and misunderstandings of what a
> theorem, formula, or theory actually are.

I don't get it. Which is the first theorem in an enumeration will
depend on how they are enumerated.

[Graham Cooper]

On Oct 6, 8:58 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:

> Graham Cooper wrote:
>
> > George's idiocy is in full bloom here!
>
> > His underlying contradictions and FAILURE TO STATE THEOREM 1 of ZFC
> > result in this copious false output and misunderstandings of what a
> > theorem, formula, or theory actually are.
>
> I don't get it.  Which is the first theorem in an enumeration will
> depend on how they are enumerated.

You said use Godel numbering.

In that case: using an alphabet of

{a, b, c, d, e, f, g, 0, 1, E, A, (, ), ,, {, } +, -, =, >,<, !}

the first theorem of ZFC is

a

George seems to think VALIDATED THEOREMS are numbered as they are
VALIDATED.

Neither of you have an INKLING what the enumeration method is, or even
what parses as a well formed if not validated formula.

Herc

[Mike Delanis]

"Graham Cooper" <graham...@gmail.com> wrote in message
news:f76717da-e106-4b58...@q9g2000pbo.googlegroups.com...



> 20 goto 10

interpreter BASIC ............. you must be 60 years old.

[Curt Welch]

My first access to computers was with an interpreted basic system in the
early 1970's. Odd that when I first read your comment about being 60 it
seemed way too high. But them I remembered I'm 56 soon, so 60 really is
about right. Odd that I don't feel anything like "60". I think that's
because I started to ignore my age once I hit 50 so I still feel like I'm
in my 40's. :)

--
Curt Welch http://CurtWelch.Com/
cu...@kcwc.com http://NewsReader.Com/

[Mike Terry]

"Curt Welch" <cu...@kcwc.com> wrote in message
news:20121005234532.149$l...@newsreader.com...

> "Mike Delanis" <inv...@invalid.com> wrote:
> > "Graham Cooper" <graham...@gmail.com> wrote in message
> > news:f76717da-e106-4b58...@q9g2000pbo.googlegroups.com...
> >
> > > 20 goto 10
> >
> > interpreter BASIC ............. you must be 60 years old.
>
> My first access to computers was with an interpreted basic system in the
> early 1970's. Odd that when I first read your comment about being 60 it
> seemed way too high. But them I remembered I'm 56 soon, so 60 really is
> about right. Odd that I don't feel anything like "60". I think that's
> because I started to ignore my age once I hit 50 so I still feel like I'm
> in my 40's. :)
>

The question shouldn't be "When did you *first* use interpreted basic?". It
should be "When might someone reasonably *last* have used it?" I recall
using line-numbered basic at work in the late 1980s, so 60 is way to high as
you first thought.

Mike.

[Graham Cooper]

On Oct 7, 12:11 am, "Mike Terry"
<news.dead.person.sto...@darjeeling.plus.com> wrote:
> "Curt Welch" <c...@kcwc.com> wrote in message
>
> > "Mike Delanis" <inva...@invalid.com> wrote:
> > > "Graham Cooper" <grahamcoop...@gmail.com> wrote in message

> > >news:f76717da-e106-4b58...@q9g2000pbo.googlegroups.com...
>
> > > > 20 goto 10
>
> > > interpreter BASIC .............  you must be 60 years old.
>
> > My first access to computers was with an interpreted basic system in the
> > early 1970's.  Odd that when I first read your comment about being 60 it
> > seemed way too high.  But them I remembered I'm 56 soon, so 60 really is
> > about right.  Odd that I don't feel anything like "60".  I think that's
> > because I started to ignore my age once I hit 50 so I still feel like I'm
> > in my 40's. :)
>
> The question shouldn't be "When did you *first* use interpreted basic?".  It
> should be "When might someone reasonably *last* have used it?"  I recall
> using line-numbered basic at work in the late 1980s, so 60 is way to high as
> you first thought.
>
> Mike.

A THEORY *should* have line numbers.

A Syntactic Formula Enumeration

F0001 X
F0002 X=X
F0003 E(X) X=X
F0004 A(x) X=X
F0005 X^Y
F0006 X^Y->X

A subset of which is sifted into Theoremhood!


F0001 ------- X
F0002 ------ X=X
F0003 T0001 E(X) X=X
F0004 T0002 A(X) X=X
F0005 ------- X^Y
F0006 ------- X^Y->X
F0007 T0003 A(X) X^Y->X
...

Herc
--
LOGIC
E(Y) Y={x|P(x)} <-> DERIVE( E(Y) Y={x|P(x)} )
DERIVE(T) <-> DERIVE(a) ^ DERIVE(b) ^ (a^b)->T

MATHEMATICS
E(Y) Y={x|P(x)} <-> PRVBLE( E(Y) Y={x|P(x)} )
PRVBLE(T) <-> NOT(DERIVE(NOT(T)))

[George Greene]

On Oct 5, 7:23 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> George seems to think VALIDATED THEOREMS are numbered as they are
> VALIDATED.

DAMN, you're stupid. "Validated theorems" IS REDUNDANT.
It *IS*NOT* a THEOREM, UNLESS AND UNTIL it is "validated",
i.e., unless and until it is PROVED! "Theorem" *MEANS* " *proved*
sentence."
The fact that YOU DIDN'T KNOW THIS *proves*you're*stupid*.

>
> Neither of you have an INKLING what the enumeration method is

Idiot,
the proof IS A FINITE STRING OF SYMBOLS.
YOU CAN ALWAYS attach numbers to those.
Haven't you heard of Ascii ?? You do SEEM to be that OLD.
More to the point, SINCE EVERY PROOF IS DIFFERENT,
it is a trivial matter TO ESTABLISH AN ORDERING on them.
FOR EXAMPLE, you could use the length-lexicographic ordering
(where shorter proofs always have lower numbers and proofs
of equal length get ordered on the basis of an ordering on the
individual characters, at the earliest character at which they
differ).
SO WE DO SO TOO have not only "an inkling", but AN ACTUAL
DEFINITION of an enumeration method.
NOT that we need have BOTHERED.
ANYBODY CAN SEE that the proof is an enumerator.

[George Greene]

On Oct 5, 7:23 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

> > > His underlying contradictions and FAILURE TO STATE THEOREM 1 of ZFC

DAMN, you're stupid.
In the first place, all first-order validities OVER THE LANGUAGE
are theorems of the theory, as well as all individual axioms
themselves.
It hardly even matters HOW you number these; the numbering IS NOT
a feature of ZFC *itself*! ZFC *DOES NOT CARE* how anybody numbers
its theorems!

"It's a lifted tautology" is the proof of one "early" class of
theorems;
"It's an [instance of an] axiom" is the proof of another.
Which one anyone ranks "first" IS NOT important.
My personal preference is to order them in the order of the lengths
of their proofs but all proofs of the form "it's an axiom" are
arguably of
THE SAME length (ZERO), so there, you might have to split to ordering
among the proved sentences themselves.

Another point that makes enumeration irrelevant is that all the new
theorems
that you get from the axioms were in fact already present from the
UNDERLYING VALIDITIES that were provable FROM NO axioms,
because every proved theorem only USES a FINITE number of the axioms.
Thus, if the theorem was "h" and the axioms (or instances of axioms)
used
to prove it were a,b,c,d,f, and g, then
a^b^c^d^f^f->h
WAS ALREADY A THEOREM of *pure* predicate calculus, was ALREADY
a first-order validity. So there really is a sense in which the
axioms merely
highlight a subset of the validities, as opposed to adding new stuff.
The order in which this highlighting occurs IS NOT important.
I'm SORRY FOR YOU, HERC, that the only treatment YOU have seen
HAPPENS to STRESS the "enumeration". You're a victim of a lame
education.
Which would be easily cured if you only had sense enough to read
ANOTHER book.

[George Greene]

On Oct 6, 5:09 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> A THEORY *should* have line numbers.

Should I sponsor a contest for best reaction to this??
"DAMN, you're stupid!" just seems uncouth, overworked,
and cliche'd by now.

[George Greene]

On Oct 5, 7:23 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> the first theorem of ZFC is
>
> a

a *IS* NOT a theorem, DUMBASS -- IT DOESN'T HAVE A PROOF.
IT IS NOT EVEN A WFF in the relevant language!

It is not completely clear what the alphabet of the language is
because
a lot of the axioms are set EXISTENCE axioms and they don't all always
get skolemized.
The usual treatment has the wrong number of axioms anyway.
Both Pairing AND Separation can GO AWAY once you get Replacement.
That's an important aspect of the transition from Z to ZF, but most
people
and treatments KEEP both Pairing and Separation even after adding
Replacement.
Union and Power usually ARE Skolemized.
The { a,b } notation does not LOOK like a Skolem function but it is a
way of taking two arguments and producing one set-constant out of
them, so you could think of it as a fancy Skolemization of the axiom
for Pairing.
There usually IS a constant for the empty set since in ZFC, that is
the
ONLY constant you actually NEED.
If you order the functors so that all the 0-ary ones (all one of them)
come
before all the unary ones (all two of them), and these come before
all
the binary ones (all one of them, the one from Pairing),
then the earliest wff in the language is
OeO, but it is false; so if you make ~ have a low enough number, the
shortest theorem would be
~OeO.
But even that is not really "theorem 1" because you cannot use theorem-
length
alone as an ordering (some short theorems have long proofs). You have
to use proof-length, and it takes a while to prove that the empty set
exists --
You have to use Separation with a contradictory predicate.

[Graham Cooper]

On Oct 8, 6:38 am, George Greene <gree...@email.unc.edu> wrote:
>
> Another point that makes enumeration irrelevant is that all the new
> theorems
> that you get from the axioms were in fact already present from the
> UNDERLYING VALIDITIES that were provable FROM NO axioms,
> because every proved theorem only USES a FINITE number of the axioms.
> Thus, if the theorem was "h" and the axioms (or instances of axioms)
> used
> to prove it were a,b,c,d,f, and g, then
> a^b^c^d^f^f->h
> WAS ALREADY A THEOREM of *pure* predicate calculus, was ALREADY
> a first-order validity.  So there really is a sense in which the
> axioms merely
> highlight a subset of the validities, as opposed to adding new stuff.
> The order in which this highlighting occurs IS NOT important.
> I'm SORRY FOR YOU, HERC, that the only treatment YOU have seen
> HAPPENS to STRESS the "enumeration".  You're a victim of a lame
> education.
> Which would be easily cured if you only had sense enough to read
> ANOTHER book.

You can stick to "ENUMERABLE" if you are too clueless to WORK_OUT the
ENUMERATION.

ATLEAST THAT'S SOMETHING TANGIBLE!

BUT YOU ARE CONTRADICTING YOURSELF ALL OVER THE PLACE.

YOU SAID THE SET OF TRUTHS ARE 'AUTOMATIC' AND NOT POSSIBLE TO DERIVE
FROM AN ALGORITHM.

Herc
--

GEORGE'S SET THEORY!
*****************************

GEORGE'S RELATION ALGEBRA!
aRb

GEORGE'S INFERENCE RULES!
P -> P
~(X -> ~X)
a^b^c^d^f^g->h

GEORGE'S SET AXIOMS!
1. Extensionality:
AxAy [Az (zex <-> zey) -> x=y]
2. Regularity:
Ax [Ea (aex) <-> Ey (yex & ~Ez (zey & zex))]
3. Specification Schema:
AzAw_1...w_nEyAx [xey <-> (xez & phi)]
4. Pairing:
AxAyEz (xez & yez)
5. Union:
AfEaAyAx [(xey & yef) -> xea]
6. Replacement Schema:
AaAw_1...w_n [Ax (xea -> E!y phi) -> EbAx (xea -> Ey (yeb & phi)]
7. Infinity:
Ex [0ex & Ay (yex -> S(y)ex)]
8. Powerset:
AxEyAz [z subset x -> zey]
9. Wellordering:
AxEr (r wellorders x)

GEORGE'S VALIDATED SENTENCES!
THEOREM 1 = ..
THEOREM 2 = ..
THEOREM 3 = !E(R) XeR <-> !(XeX) *TADAAAA*

[Charlie-Boo]

On Oct 5, 8:47 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:

> Graham Cooper wrote:
>
> > Formal Theory means all sentences in the Theory are systematically
> > enumerated.
>
> > ZFC is NOT a formal Theory!
>
> > There is no method given to distinguish between theorems and predicate
> > calculus formulas.
>
> > [...]
>
> > You have NO WAY of enumerating Theorems!
>
> What is enumerated is G\"odel numbers of theorems.  So which theorem
> comes first depends on the enumerator and the G\"odel numbering.

Give them the Godel number consisting of the number of the first
symbol times 100 plus the number of the second symbol etc. so the
order of the numbers and of the wffs coincide. Then the first one is
the theorem that is alphabetically first. Which one is that?

Or better yout, just start enumerating theorems and stop after the
first one and tell us what it is ok?

What is theorem 1? Excellent question. A question that one could
easily answer for any genuine axiomatic system!!!!!

C-B

[George Greene]

On Oct 7, 7:38 pm, Charlie-Boo <shymath...@gmail.com> wrote:
> Or better yout, just start enumerating theorems and stop after the
> first one and tell us what it is ok?

Start enumerating them HOW?
Herc doesn't know. You are probably smarter than Herc but you haven't
said how either.

> What is theorem 1?  Excellent question.

It is NOT an excellent question. ANY theorem can be theorem 1.

>  A question that one could
> easily answer for any genuine axiomatic system!!!!!

ZFC *is* a set of axioms (and the theorems that follow from them).
The LANGUAGE of the theory has the property that some of the Wffs (in
the LANGUAGE)
are VALID -- they are automatically true EVEN WITHOUT any axioms.

Herc doesn't know what "predicate calculus" MEANS.
At the moment he seems to have it confused with "first-order
language",
since he has (falsely) claimed that "predicate calculus is just the
syntax-checker".
"predicate calculus" IS ACTUALLY *just*that* -- a CALCULUS -- for
deriving consequences
from premises, where both of those are sentences from A FIRST-order
language, i.e.,
a language WITH PREDICATES.

[George Greene]

On Oct 7, 5:48 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> YOU SAID THE SET OF TRUTHS
> ARE 'AUTOMATIC' AND NOT POSSIBLE TO DERIVE
> FROM AN ALGORITHM.

I *did*not*say* that, DUMBASS.
I SAID that they were derived from NO AXIOMS at all.
If Chris Menzel had kept his hateful-ass MOUTH shut then you MIGHT
have understood me. UNfortunately he HAD to talk about "logical
axioms"
and thereby keep you confused.
In an attempt TO UNconfuse you, I have REMINDED you that
that the LOGIC is defined by its RULES OF INFERENCE, AS OPPOSED
to any AXIOMS! AXIOMS are for THE OBJECT theory -- they are for the
theory
in and about which you are conducting the investigation. The purpose
of
the LOGIC is to DERIVE THEOREMS FROM the axioms. The LOGIC,
I repeat, is defined by its RULES OF INFERENCE and
OF*FUCKING*COURSE*THERE*IS* an algorithm for using those rules to
produce proofs!

[Graham Cooper]

On Oct 9, 6:54 am, George Greene <gree...@email.unc.edu> wrote:
> On Oct 7, 5:48 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
>
> > YOU SAID THE SET OF TRUTHS
> > ARE 'AUTOMATIC' AND NOT POSSIBLE TO DERIVE
> > FROM AN ALGORITHM.
>
> I *did*not*say* that,  DUMBASS.

------8<-----------------------------


[HERC]
IF FOLtheorem(S) THEN ZFCtheorem(S)
is not algorithmic.


[GEORGE]
> It's MUCH BETTER than algorithmic, dumbass, it's AUTOMATIC.
> It's automatic BECAUSE classical logic IS MONOTONIC.
> It's automatic because (P-->Q) --> ((P&R)-->Q)
> IS A TAUTOLOGY.
> When we SAY that something is a theorem of pure/plain FOL,
> what we MEAN is that we can derive it, using THE INFERENCE RULES

--------------------------8<-------

So where are all these "automatic" theorems coming from
if they are not "algorithmic" in derivation.

Is there a Transitive Closure on Inference for all true Predicates
derived from P. Calculus?

What do you need ZFC for if Predicate Calculus _CALCULATES_

~E(R) XeR <-> ~(XeX)

Axiom Of SEPARATION deals with this already!

Herc

[George Greene]

On Oct 8, 7:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> On Oct 9, 6:54 am, George Greene <gree...@email.unc.edu> wrote:
> > It's MUCH BETTER than algorithmic, dumbass, it's AUTOMATIC.
> > It's automatic BECAUSE classical logic IS MONOTONIC.
> > It's automatic because (P-->Q) --> ((P&R)-->Q)
> > IS A TAUTOLOGY.
> > When we SAY that something is a theorem of pure/plain FOL,
> > what we MEAN is that we can derive it, using THE INFERENCE RULES
>
> --------------------------8<-------
>
> So where are all these "automatic" theorems coming from
> if they are not "algorithmic" in derivation.

I DID NOT SAY that this was NOT algorithmic! I said that it was
BETTER
than algorithmic, and I said that we can derive it USING INFERENCE
RULES!
THAT USE *IS* algorithmic, DUMBASS!

But you have cut too much as usual. YOU were talking about *ZFC*
and what was algorithmic FROM THAT.
*I* was talking about VALID FORMULAS that DO NOT depend on any
axioms of ZFC, OR ON ANY AXIOMS *PERIOD*.

I NEVER SAID THAT ANY proof/derivation/theorem was NOT algorithmic!


HERE is what I said this ABOUT: Some turd that YOU excreted.

YOU said:
[HERC]
IF FOLtheorem(S) THEN ZFCtheorem(S)
is not algorithmic.

And THAT IF-THEN statement REALLY IS NOT algorithmic!
That statement IS NEITHER a theorem of ZFC *nor* a theorem
of predicate calculus! THAT statement is a statement IN NATURAL
language ABOUT two different theories! And THAT statement
REALLY IS *automatically* true! THAT statement is true
BECAUSE CLASSICAL INFERENCE IS MONOTONIC.
THAT statement IS NOT STATED IN *THE*LANGUAGE*OF*
"predicate calculus" OR in the first-order language of ZFC!
THAT statement is just a statement about the consequences
of 2 theories! And since ZFC has MORE AXIOMS than
*pure* FOL (which has/needs NONE -- since first-order logic is
A LOGIC, its inferences are defined by ITS INFERENCE RULES
AND NOT by any axioms), IT REALLY IS AUTOMATIC than ANYthing
that is an "FOLTheorem" (over the same language) IS A THEOREM OF
*ANY*AND*EVERY* first-order theory (again, over the latter theory's
first-
order language).

THAT'S automatic BECAUSE OF THE *META*fact that
CLASSICAL INFERENCE IS MONOTONIC.

THAT'S automatic because
(P->Q)->((P^R)->Q) IS A TAUTOLOGY -- and there are MANY SIMPLE
"algorithms" that PROVE THAT THAT IS A TAUTOLOGY!

[George Greene]

On Oct 8, 7:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> What do you need ZFC for if Predicate Calculus _CALCULATES_
>
> ~E(R) XeR <-> ~(XeX)

You've spelled it wrong. It's
~Er[ xer <--> ~xex ].

And You DON'T need ZFC *For*THAT*, CLEARLY! THAT is just AN INSTANCE
of
~Er[ xRr <--> ~xRx ] -- this is true FOR ANY binary relation, NOT
just one
that happens to be spelled "e".

What you DO need ZFC in order to make "e" MEAN "is a member of the
set".
WITHOUT ZFC, the ~E sentence above means SIMULTANEOUSLY ANYOF
"There is no barber who shaves all&only those barbers who don't shave
themselves",
"There is no wanker who wanks all&only those wankers who don't wank
themselves",
"There is no TM that halts on all&only those TMs that don't halt on
themselves",
"There is no set that contains all&only those sets that don't contain
themselves", AD NAUSEAM.

You need ZFC to tell you what sets DO exist! -- This validity ONLY
tells you that a certain kind of set canNOT exist!

ZFC is not the only axiomatization of set theory. If you are trying
this
at home, trying this on your own, trying to come up with your own
BETTER
axiomatization of set theory, then you MUST BE CAREFUL TO AVOID ALL
inconsistencies, IN PARTICULAR AND ESPECIALLY THIS ONE (Russell's
Paradox), since avoidance of THIS paradox is not even coming from your
theory,
but from logic alone. The way this paradox can thwart your set theory
IS IF
your set theory, in proving that many sets exist, HAPPENS TO STUMBLE
ACROSS
a proof that Er[ xer <--> ~xex ]. IF THAT HAPPENS, THEN YOUR THEORY
IS
INCONSISTENT and SOME part of it MUST be abandoned.
In naive set theory, THIS DOES happen (this set r MUST exist), so
naive set
theory is inconsistent (and therefore worthless).

[George Greene]

On Oct 8, 7:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> What do you need ZFC for if Predicate Calculus _CALCULATES_
>
> ~E(R) XeR <-> ~(XeX)
>
> Axiom Of SEPARATION deals with this already!

Idiot,
in the context of *pure* predicate calculus, you have NO AXIOMS AT
ALL.
YOU HAVE NO "Axiom of Separation" WITH WHICH to "deal with this"!
Versus PURE predicate calculus, ZFC *is*not* "already"!! THE CALCULUS
is "already"! The calculus COMES FIRST!
THEN YOU ADD some axioms AFTERWARD!
If the theory you are trying to build ABOVE AND BEYOND just raw
predicate
calculus, USING predicate calculus as a framework, is a theory THAT
REQUIRES
SOME SETS TO EXIST, then that newer/larger theory you are building IS
A SET theory, and you must be careful that it DOES NOT prove that a
Russell-set must exist, because if it calls a Russell-set into
existence, YOUR THEORY IS INCONSISTENT and therefore worthless.

[Graham Cooper]

[1]

> a proof that Er[ xer <--> ~xex ].  IF THAT HAPPENS, THEN YOUR THEORY
> IS INCONSISTENT and SOME part of it MUST be abandoned.

So the AXIOMS are a *CONSTRAINT* what formula are allowed.


[2]

> (P->Q)->((P^R)->Q)  IS A TAUTOLOGY -- and there are MANY SIMPLE
> "algorithms" that PROVE THAT THAT IS A TAUTOLOGY!

only in FOL.

Axioms (R here) are 2OL or 3OL (Regularity)

so they range over all expressions within their own theory
(including P and Q)
and LIMIT the usage/range of certain symbols.



[3]

>You need ZFC to tell you what sets DO exist! -- This validity ONLY
>tells you that a certain kind of set canNOT exist!

ALL(set) mem e set IFF p(mem,set)
AND EXIST(anotherset) mem e anotherset


This is what ZFC does, limits the relation 'e'.


[4]

> The way this paradox can thwart your set theory
> IS IF your set theory, in proving that many sets exist,
> HAPPENS TO STUMBLE ACROSS
> a proof that Er[ xer <--> ~xex ].
> IF THAT HAPPENS, THEN YOUR THEORY IS
> INCONSISTENT and SOME part of it MUST be abandoned.
> In naive set theory, THIS DOES happen
> (this set r MUST exist), so naive set
> theory is inconsistent (and therefore worthless).

What's the difference between Predicate Calculus
and Naive Set Theory.

They are both ZERO-AXIOM logic systems.

If NST is inconsistent, what rules in Predicate Calculus
are you using to ensure ZFC does not inherit NST inconsistency?


Herc

[George Greene]

On Oct 9, 6:01 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> So the AXIOMS are a *CONSTRAINT* what formula are allowed.

No. *NOTHING* is "allowed". "Allowed" is not a relevant status.
The formulas come from a first-order LANGUAGE with a SIGNATURE.
The signature is a list of predicate- and function- NAMES, each of
which has an -arity (a number of arguments). ALL of the well-formed
formulas in the relevant
first-order LANGUAGE are built out of logical symbols predicates,
applied to arguments that are built out of these functions.

> [2]
>
> > (P->Q)->((P^R)->Q)  IS A TAUTOLOGY -- and there are MANY SIMPLE
> > "algorithms" that PROVE THAT THAT IS A TAUTOLOGY!
>
> only in FOL.

You are LYING. Tautologies are from *0*-OL.

> Axioms (R here) are 2OL or 3OL (Regularity)

NO, you are lying AGAIN. The VERSION of set theory that we are
talking about
here IS *1ST*-order ZFC! The LANGUAGE that all these formulas
(including
all the axioms) come from is a *1ST*-order language! The LOGIC in
which
we are deriving these proofs IS *1ST*-order logic!

> >You need ZFC to tell you what sets DO exist! -- This validity ONLY
> >tells you that a certain kind of set canNOT exist!
>
> ALL(set)  mem e set    IFF  p(mem,set)
>          AND  EXIST(anotherset) mem e anotherset
>
> This is what ZFC does, limits the relation 'e'.

Exactly. It *defines* e.
With no axioms, e wouldn't mean anything at all.
With no axioms, you would HAVE NO WAY OF TELLING whether
the "e" in ~Er[ xer <-> ~xex ] meant
"_ shaves _ " (in which case the sentence would mean "there is no
barber
who shaves all and only those barbers who don't shave themselves") or
"set _ is a member of set _ " (in which case the sentence would mean
there
is no set whose members are all&only those sets that are not members
of themselves).

In all these theories, the axioms constrain the meaning or
interpretation
of the functions and predicates occuring in them.


> [4]

> What's the difference between Predicate Calculus
> and Naive Set Theory.

Predicate calculus is a calculus. It's a logic. It is defined by its
INFERENCE RULES. It's used to prove/derive/infer THEOREMS
*from*prior* assumptions.
SOME theorems (like P V~P) can be inferred or derived (USING THESE
RULES, AND USING THE ALGORITHMS DEFINED for applying these rules) FROM
NO prior assumptions. But the formulas so proved/derived/assumed need
to be in a first-
order LANGUAGE, first.

Naive set theory is a theory. WITH AXIOMS.

> They are both ZERO-AXIOM logic systems.

NO, THEY ARE NOT. Naive Set Theory IS NOT a "logic system".
It's a A THEORY. WITH SOME AXIOMS. ONE OF ITS AXIOMS IS
the NAIVE set-COMPRENSION axiom, ExAy[ yex <-> phi(y) ].
This is an axiom-schema saying that you get an axiomatic automatically
proven-true theorem confirming the existence of a set corresponding
to EVERY predicate phi(.) that is definable in the language.
In particular, it says you get a set when phi(y) means ~yey.
SO THIS THEORY IS INCONSISTENT.
This theory is *IN* predicate calculus. It's UNDER predicate
calculus.
It's worked with USING predicate calculus, IN THE FRAMEWORK of
predicate calculus.

> If NST is inconsistent, what rules in Predicate Calculus
> are you using to ensure ZFC does not inherit NST inconsistency?

We are using THE SAME rules of predicate calculus FOR BOTH
ZFC and NST.
There is NO inheritance because ZFC *replaces* NST's
NAIVE set-COMPREHENSION axiom with the axiom of
SEPARATION.

It is the naive set-comprehension axiom that causes the problem.
That axiom is inconsistent/paradoxical in itself.
It simply CANnot be the case that EVERY predicate defines a set.
You need a more complicated, less naive set of axioms to define sets.
Zermelo gave a first one in 1903.
Frankel filled in an obvious hole later (That is how we got ZF).
The axiom of choice seemed like an obvious hole too, but that
got very complicated for about 30 years from 1936-66.

[Graham Cooper]

So this formula is barred!

ExAy[ yex <-> phi(y) ].

Now you're saying Predicate Calculus (with only infererence rules
over predicates which you wrongly call FOL)

P -> P
~P v P
(P ^ Q) -> P
....
and a few more like that..

et voila!

NOT( EXIST(INFERENCE) INFERENCXE= ExAy[ yex <-> phi(y) ] )


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

OK so you DEFINE THE MEANING OF 'e' purely for use at the AXIOM LEVEL.

and you STILL GET THE PARADOX:

E(rs) A(x) x ee rs <-> !(x ee rs)

in Predicate Calculus.

Predicate Calculus WORKS ALL OF THIS OUT,
it does resolution, consistency checks, et al
(using FOL INFERENCE RULES (ranging over variables))

PC is consistent because it derives
NOT[ EXIST(rs) A(x) x ee rs <-> !(x ee rs) ]

and prevents E(rs) going on the LHS of any further consistent
inferences.

BUT, JUST TO BE DOUBLE SURE...
the SETS REALLY DO EXIST IN THE AXIOMS LEVEL
by BARRING rs from instantiating with 'e' too.

since 'e' is now a reserved letter,
(implicit by being a new symbol in the axioms)

***********

WRONG GEORGE!

You're flicking in and out of
FORMULA SYNTAX CALCULUS
1OL, 2OL, 3OL
INFERENCE vs MODUS PONENS
NAIVE SET THEORY
CONSISTENCY BY VERIFICATION THEORY
CONSISTENCY BY STRATIFICATION THEORY
CONSISTENCY BY FORMULA RESTRICTION
(of the term 'e')

You have no LOGIC THEORY, you have an ORACLE, you have DERIVED SETS
with no RUSSELL SET

for the 20TH TIME HERE:

E(X) NOT(X=X)

is in the language of predicate calculus.

YOU DON"T HAVE A TRANSITIVE CLOSURE OF LOGIC
BASED ON INFERENCE RULES

and if you did THEY CERTAINLY WOULDN'T BE FOL
THEY WOULD NECESSARILY RANGE OVER FORMULAS.

Herc

[George Greene]

On Oct 11, 4:03 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:


> So this formula is barred!
>
>  ExAy[ yex <-> phi(y) ].

No, it's not BARRED. It isn't even a formula.
It's a SCHEMA. It's A WHOLE BUNCH of formulas.
AND ONE of them, the one that you get when phi(y)=~yey,
PRODUCES A CONTRADICTION.
So this canNOT be an AXIOM-SCHEMA. It is barred from THAT role.
But no formula, not even contradictions, is EVER barred just from
BEING a formula
and being IN the language, IF it's well-formed according to the rules
defining the language.
It's just false. Or provably false. But you would not be ABLE to
prove it "false" UNLESS
it first WERE a formula! It is NOT *barred*, just because it is
disproved!

> Now you're saying  Predicate Calculus  (with only infererence rules
> over predicates which you wrongly call FOL)

SHUT UP. I'M the one with two degrees in it.
You do NOT KNOW enough to be telling me that *I* am calling anything
wrongly.
It is long past time you figured out WHO is TEACHING this course and
who is taking it.
You can type
"predicate calculus" "first-order logic" into Google and SEE FOR
YOURSELF what kind of relationship they are generally known to have.

[George Greene]

On Oct 11, 4:03 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> Now you're saying  Predicate Calculus  (with only infererence rules
> over predicates which you wrongly call FOL)
>
> P -> P
> ~P v P
> (P ^ Q) -> P
> ....
> and a few more like that..
>
> et voila!

Why do you keep starting sentences with "you're saying"??
and then following them with stuff *I*NEVER*SAID*???

I certainly never said that anything like what you are posting here is
FOL.
The things you just posted are TAUTOLOGIES FROM *0th*-order logic!

[George Greene]

On Oct 11, 4:03 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

> OK so you DEFINE THE MEANING OF 'e' purely for use at the AXIOM LEVEL.
>
> and you STILL GET THE PARADOX:

NO, DUMBASS, you get the paradox WITHOUT DEFINING ANY meaning for e.
ErAx[xRr <--> ~xrx]
is contradictory FOR ALL binary relations r, REGARDLESS of whether R
is
a, b, c, d, e, f, g, h, i, j, k, u, v, w, or shaves, or contains, or
wanks.

[George Greene]

On Oct 11, 4:03 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> Now you're saying  Predicate Calculus  (with only infererence rules
> over predicates which you wrongly call FOL)

I'm certainly not THE ONLY one calling it that way, DUMBASS.

http://en.wikipedia.org/wiki/First-order_logic

[Graham Cooper]

Hilbert-style systems and natural deduction

A deduction in a Hilbert-style deductive system is a list of formulas,
each of which is a logical axiom, a hypothesis that has been assumed
for the derivation at hand, or follows from previous formulas via a
rule of inference. The logical axioms consist of several axiom schemes
of logically valid formulas; these encompass a significant amount of
propositional logic. The rules of inference enable the manipulation of
quantifiers. Typical Hilbert-style systems have a small number of
rules of inference, along with several infinite schemes of logical
axioms. It is common to have only modus ponens and universal
generalization as rules of inference.

Natural deduction systems resemble Hilbert-style systems in that a
deduction is a finite list of formulas. However, natural deduction
systems have no logical axioms; they compensate by adding additional
rules of inference that can be used to manipulate the logical
connectives in formulas in the proof.

first-order logic is undecidable (although semidecidable), provided
that the language has at least one predicate of arity at least 2
(other than equality). This means that there is no decision procedure
that determines whether arbitrary formulas are logically valid. This
result was established independently by Alonzo Church and Alan Turing
in 1936 and 1937


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

Also, this is what I was calling "AXIOMS" of predicate calculus the
other day.

http://en.wikipedia.org/wiki/First-order_logic#Provable_identities

Herc

[George Greene]

On Oct 12, 3:02 am, Graham Cooper <grahamcoop...@gmail.com> wrote:
> Also, this is what I was calling "AXIOMS" of predicate calculus the
> other day.
>
> http://en.wikipedia.org/wiki/First-order_logic#Provable_identities

Something that is provABLE is BY DEFINITION *not* an AXIOM!
Axioms are what theorems get proven *FROM* --
THE WAY IT WORKS
is that you USE the rules of inference TO PROVE
*theorems*
FROM
the axioms!
So the fact that YOU were referring to something that is "a provable
identity"
as "an axiom" PROVES YOU'RE STUPID.
Or at least under-informed about what is going on around here.
But THAT
is not even the point.
THE POINT is that THERE ARE MANY EQUIVALENT
ways in which to define standard classical first-order logic
and the way I WAS TEACHING YOU *IN*THIS* course
is a way that defines it WITH NO AXIOMS AT ALL, because
it prefers instead to define it via RULES OF INFERENCE.
That would've been helpful FOR YOU because it would have
AVOIDED CONFUSING YOU
between axioms OF THE OBJECT THEORY (set theory
in this case) and axioms of THE LOGIC, which is a separate framework.

[George Greene]

> On Oct 12, 2:06 pm, George Greene <gree...@email.unc.edu> wrote:

> >http://en.wikipedia.org/wiki/First-order_logic

On Oct 12, 3:02 am, Graham Cooper <grahamcoop...@gmail.com> wrote:

> Hilbert-style systems and natural deduction

Why are you bothering to quote a difference between
Hilbert-systems and natural-deduction-systems?

What difference does THAT make?

[Graham Cooper]

deductive system is a list of formulas,
each of which is a logical axiom

there is no decision procedure
that determines whether arbitrary formulas are logically valid

So much for your ALGORITHMIC proof that

~E(r) xer <-> ~xex

is a part of ZFC AUTOMATICALLY.

Herc

[George Greene]

On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> deductive system is a list of formulas,
> each of which is a logical axiom

NO, a deductive system IS NOT a list of formulas.

JEEzus.

> there is no decision procedure
> that determines whether arbitrary formulas are logically valid

THERE IS, however, an algorithm that CONFIRMS that a formula is
logically valid WHEN IT IS.
The consequence relation for standard classical first-order logic IS
SEMI-decidable.
The reason it is not a decision procedure is that there is no
algorithm that can confirm
(in the general case) that a first-order wff is NOT valid when it's
NOT (although that is also
confirmable SOMEtimes -- every confirmation that a wff IS valid is
also a confirmation&proof
that its denial is not).

> So much for your ALGORITHMIC proof that
>
> ~E(r) xer <-> ~xex
>
> is a part of ZFC AUTOMATICALLY.

NO, DUMBASS -- THERE IS a proof -- so, therefore, there is, also, by
definition, AN ALGORITHM that CONFIRMS
the existence of a proof -- that
~Er[ xer <--> ~xex ] is valid.
If you had any sense you would just PRESENT THIS PROOF YOURSELF.

BECAUSE this proof depends ON NO axioms -- LOGICAL OR OTHERWISE --
this sentence is necessarily valid
and necessarily a theorem OF ALL first-order formal theories in which
IT CAN BE STATED AT ALL, i.e., in which
a binary predicate e is in THE FIRST-ORDER LANGUAGE in which the
theory is being phrased.
All those theories "have" or "contain" (a theory is a set of sentences
that is closed under logical consequence)
all the first-order validities PLUS their axioms PLUS the theorems
THAT FOLLOW FROM their axioms.

[camg...@hush.com]

On Oct 13, 9:39 am, George Greene <gree...@email.unc.edu> wrote:
> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
>
> > deductive system is a list of formulas,
> > each of which is a logical axiom
>
> NO, a deductive system IS NOT a list of formulas.
>
> JEEzus.

That's a quote from WIKI

>
> > there is no decision procedure
> > that determines whether arbitrary formulas are logically valid
>
> THERE IS, however, an algorithm that CONFIRMS that a formula is
> logically valid WHEN IT IS.

so why can't you do brute force lexicographically on ALL formulas and
output

VALID
NOT VALID

> The consequence relation for standard classical first-order logic IS
> SEMI-decidable.
> The reason it is not a decision procedure is that there is no
> algorithm that can confirm
> (in the general case) that a first-order wff is NOT valid when it's
> NOT (although that is also
> confirmable SOMEtimes -- every confirmation that a wff IS valid is
> also a confirmation&proof
> that its denial is not).
>
> > So much for your ALGORITHMIC proof that
>
> > ~E(r) xer <-> ~xex
>
> > is a part of ZFC AUTOMATICALLY.
>
> NO, DUMBASS -- THERE IS a proof -- so, therefore, there is, also, by
> definition, AN ALGORITHM that CONFIRMS
> the existence of a proof -- that
> ~Er[ xer <--> ~xex ] is valid.
> If you had any sense you would just PRESENT THIS PROOF YOURSELF.

I don't present proofs.
I enter them into proof software and claim the theorem is true as far
as the axioms and consistency of the proof software is concerned.

>
> BECAUSE this proof depends ON NO axioms -- LOGICAL OR OTHERWISE --
> this sentence is necessarily valid
> and necessarily a theorem OF ALL first-order formal theories in which
> IT CAN BE STATED AT ALL, i.e., in which
> a binary predicate e is in THE FIRST-ORDER LANGUAGE in which the
> theory is being phrased.
> All those theories "have" or "contain" (a theory is a set of sentences
> that is closed under logical consequence)
> all the first-order validities PLUS their axioms PLUS the theorems
> THAT FOLLOW FROM their axioms.

..because you say so.

Where on EARTH have you guys been HIDING this

******************************************************
*PLATONIC WORLD OF ABSOLUTE TRUTHS*
******************************************************

FOR THE LAST 10 YEARS YOU'VE BEEN DENYING

1 SINGLE FORMULA IS BONA FIDE TRUE#.

As far as MATHS AND LOGIC is CONCERNED

#TRUE = W.R.T. STATED AXIOMS

I have not SEEN a FORMAL PROOF BY RESOLUTION ONCE on SCI.LOGIC.

I wan't born with

T |- formula & ~formula
->
! (T |- formula )
&
T |- ~EXIST(formula)

embedded into my AXIOMLESS AUTOMATIC Thought Processes!!

Last chance George, put up THEOREM 1 of your AXIOMLESS LOGIC THEORY or
SHUT UP!

Herc

[Richard Tobin]

In article <458567d7-d298-4c8f...@n16g2000yqi.googlegroups.com>,

<camg...@hush.com> wrote:

>> THERE IS, however, an algorithm that CONFIRMS that a formula is
>> logically valid WHEN IT IS.

>so why can't you do brute force lexicographically on ALL formulas and
>output
>
>VALID
>NOT VALID

Because there isn't an algorithm that confirms that a formula is
invalid when it is.

-- Richard

[camg...@hush.com]

On 13 Oct, 10:45, rich...@cogsci.ed.ac.uk (Richard Tobin) wrote:
> In article <458567d7-d298-4c8f-af7d-36473f1ae...@n16g2000yqi.googlegroups.com>,

>
>  <camgi...@hush.com> wrote:
> >> THERE IS, however, an algorithm that CONFIRMS that a formula is
> >> logically valid WHEN IT IS.
> >so why can't you do brute force lexicographically on ALL formulas and
> >output
>
> >VALID
> >NOT VALID
>

>
> Because there isn't an algorithm that confirms that a formula is
> invalid when it is.
>
> -- Richard

[GG]

THERE IS, however, an algorithm that CONFIRMS that a formula is
logically valid WHEN IT IS.

Use this!

if (valid(formula)) write (formula + " is valid")
else write (formula + " is not valid")


What are you saying, valid() doesn't halt when the formula is invalid?

Herc

[George Greene]

On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> there is no decision procedure
> that determines whether arbitrary formulas are logically valid

This is entirely -- ENTIRELY -- analogous to the case where there is
no TM-that-always-halts
(no decision procedure) that determines whether an arbitrary TM halts
on an arbitrary input-
string: THERE IS, HOWEVER, a TM that CONFIRMS that an arbitrary TM
*does* halt on an
arbitrary input string, WHEN the tm DOES halt on the string.
That's called the universal TM -- it can run ANY tm on ANY string and
just SEE WHAT HAPPENS.
If the TM halts on the string then the universal TM emulating that run
ALSO halts (yes/true/accept).

If a first-order formula is valid (or contradictory) then there IS an
algorithm that CONFIRMS that,
that halts PROVING that the formula is valid (or that its denial is
contradictory).
But it is not a decision-procedure in the general case, because in the
OTHER case,
in the OPPOSITE case, in the case where the formula you throw at this
algorithm
is NEITHER valid nor contradictory, the algorithm may fail to halt or
to give any final answer.
Just as will happen with the universal TM if you give it a TM and a
string on which the TM does NOT halt.

[George Greene]

> > NO, a deductive system IS NOT a list of formulas.
>
> > JEEzus.

On Oct 12, 8:37 pm, camgi...@hush.com wrote:
> That's a quote from WIKI

So FUCKING what??
That's a quote in the context OF THAT treatment. And you should have
NAMED the treatment or article.
Nothing IS EVER "a quote from WIKI". What it IS is "a quote from the
Wikipedia article on <whatever>."
DIFFERENT wikipedia articles are going to treat the SAME topic
DIFFERENTLY!!


Any time anybody is trying to explain anything to you, they may have
to tell you
what THEIR terms mean in the context of THEIR presentation. This does
NOT
obligate OTHER people to use those terms in the same way. FOR
EXAMPLE:
IF YOU GOOGLE (jointly) the pair of terms "Deductive System" and
"Inference Rule",
you will get, FROM THE WIKIPEDIA ARTICLE ON First-Order Logic, (all
that follows is quoted from the article)
>> Deductive systems
A deductive system is used to demonstrate, on a purely syntactic
basis, that one formula is a logical consequence of another formula.
There are many such systems for first-order logic, including Hilbert-
style deductive systems, natural deduction, the sequent calculus, the
tableaux method, and resolution. These share the common property that
a deduction is a finite syntactic object; the format of this object,
and the way it is constructed, vary widely. These finite deductions
themselves are often called derivations in proof theory. They are also
often called proofs, but are completely formalized unlike natural-
language mathematical proofs.

A deductive system is sound if any formula that can be derived in the
system is logically valid. Conversely, a deductive system is complete
if every logically valid formula is derivable. All of the systems
discussed in this article are both sound and complete. They also share
the property that it is possible to effectively verify that a
purportedly valid deduction is actually a deduction; such deduction
systems are called effective.

A key property of deductive systems is that they are purely syntactic,
so that derivations can be verified without considering any
interpretation. Thus a sound argument is correct in every possible
interpretation of the language, regardless whether that interpretation
is about mathematics, economics, or some other area.

In general, logical consequence in first-order logic is only
semidecidable: if a sentence A logically implies a sentence B then
this can be discovered (for example, by searching for a proof until
one is found, using some effective, sound, complete proof system).
However, if A does not logically imply B, this does not mean that A
logically implies the negation of B. There is no effective procedure
that, given formulas A and B, always correctly decides whether A
logically implies B.
Rules of inference
Further information: List of rules of inference

A rule of inference states that, given a particular formula (or set of
formulas) with a certain property as a hypothesis, another specific
formula (or set of formulas) can be derived as a conclusion. The rule
is sound (or truth-preserving) if it preserves validity in the sense
that whenever any interpretation satisfies the hypothesis, that
interpretation also satisfies the conclusion.

For example, one common rule of inference is the rule of substitution.

[George Greene]

On Oct 12, 8:52 pm, camgi...@hush.com wrote:
> Use this!
>
> if (valid(formula))  write (formula + " is valid")
>    else write (formula + " is not valid")
>
> What are you saying, valid() doesn't halt when the formula is invalid?

WELL DONE!
Congratulations!

[Graham Cooper]

On Oct 14, 1:48 am, George Greene <gree...@email.unc.edu> wrote:
> > > NO, a deductive system IS NOT a list of formulas.
>
> > > JEEzus.
>
> On Oct 12, 8:37 pm, camgi...@hush.com wrote:
>
> > That's a quote from WIKI
>
> So FUCKING what??
> That's a quote in the context OF THAT treatment.  And you should have
> NAMED the treatment or article.

You can't follow the context of this quote?


----8<----------------------------

> > >http://en.wikipedia.org/wiki/First-order_logic

> On Oct 12, 3:02 am, Graham Cooper <grahamcoop...@gmail.com> wrote:

> > Hilbert-style systems and natural deduction

> Why are you bothering to quote a difference between
> Hilbert-systems and natural-deduction-systems?
> What difference does THAT make?

deductive system is a list of formulas,
each of which is a logical axiom

(taken from full paragraph in previous post which you didn't read)

---------------------------

Logic axiom being the topic for the last 2 weeks.

Herc

[Graham Cooper]

These are just INFERENCES mind you.

You still owe me some BASE THEOREMS, otherwise all your "proofs" are
Oracular.

I'll print the table here, nice one!

http://en.wikipedia.org/wiki/List_of_rules_of_inference

----------------------------------

RESOLUTION IS STATED AS:

((p v q) ^ (!p v r)) -> (q v r)


So you have to get

xRr <-> !xRr
p = xRr
!p = xRr

???


Mind you, only 1 inference rule is needed, modus ponens and it can
pattern match the rest as axioms, since modus ponens will CREATE A NEW
FORMULA as well as derive it, so there only has to be one inference
rule that instantiates new formula.

But anything in the form LHS -> RHS can be used to instantiate a new
line, fine with me. ;-)

Herc

[George Greene]

> > > > NO, a deductive system IS NOT a list of formulas.
>
> > > > JEEzus.
>

On Oct 13, 3:36 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > >
On Oct 12, 8:37 pm, camgi...@hush.com wrote:
>
> > > That's a quote from WIKI

> You can't follow the context of this quote?

Idiot,
YOU MISQUOTED IT.
IT *DID*NOT*SAY* that "a deductive system is a list of formulas"!
IT SAID,

"A deduction in a Hilbert-style deductive system is a list of
formulas, each of which is a logical axiom, a hypothesis that has been
assumed for the derivation at hand, or follows from previous formulas
via a rule of inference."

It said a DEDUCTION, *NOT* "a deductive system", was a list of
formulas!
DAMN, you're stupid!
And it IS consistent with this for ZERO of them to be logical axioms!
What *IT* means by "logical axiom" CAN VARY from ONE Hilber-style
system TO ANOTHER.
AND THERE ARE SOME WITH *NO* "logical axioms"!

[George Greene]

On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> These are just INFERENCES mind you.
>
> You still owe me some BASE THEOREMS, otherwise all your "proofs" are
> Oracular.

NO, I DON'T.

In the NON-logical context, in the SET THEORY or NUMBER THEORY (Peano
Arithmetic)
or group theory OR ANY OTHER AXIOMATIC THEORY context, in the context
of anything
for which you might actually be USING first-order logic, any
investigation TO WHICH you might
be APPLYING first-order logic, what YOU are calling a "base theorem"
is called AN AXIOM.
That's what axioms ARE FOR. They are true DESPITE not having any
proofs (other than "it's an axiom".)

In the pure-logical context, there is no difference between a logical
axiom and the conclusion of an inference
rule that infers/derives that conclusion FROM AN EMPTY set of
premises.
I'm NOT being ORACULAR when I insist that P V ~ P
is true, withOUT any proof in a FIRST-order system. P V ~P
*is*ZEROth*-order, to start with.
First-order PRESUMES all that IN ONE handwave!

[George Greene]

On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> RESOLUTION IS STATED AS:
>
> ((p v q) ^ (!p v r)) -> (q v r)
>
> So you have to get
>
> xRr <-> !xRr
> p = xRr
> !p = xRr
>
> ???
>
> Mind you, only 1 inference rule is needed, modus ponens

Resolution is also complete as an "only needed" inference rule, but
these things
are not complete in the way you think. If you are using MP as your
only inference rule
then --> IS YOUR ONLY CONNECTIVE, so you have to RE-WRITE any and
everything
that started out using /\ , V , or <--> TO USE --> INSTEAD,
IF you are going to use nothing but MP.

Similarly, since resolution ONLY operates on conjunctions of
disjunctions,
IF you are going to use resolution as your only inference rule, THEN
you AGAIN
have TO REWRITE everything that PREVIOUSLY had <--> or /\ in it AS a
collection
of disjunctions.

In particular (going for resolution),
p <--> q becomes
p --> q And q --> p; so, therefore,

rRr <--> ~rRr
becomes
(rRr --> ~rRr) and (~rRr --> rRr).

--> is the wrong connective for resolution; you have to translate -->
to V in order to use resolution.
Since, by definition, p --> q means ~p V q, the above pair of converse
conditionals become
~rRr V ~rRr and rRr V rRr .
Since disjunction is idempotent, each of these two-disjunct
disjunctions becomes a ONE-junct -junction (a "unit clause"), and the
two things you are trying to "resolve" become

~rRr resolved with rRr.
If you resolve THOSE two WITH EACH OTHER then you very quickly get
THE EMPTY CLAUSE, which is a "proof of false", which proves that the
original collection
of disjunctions was inherently contradictory, which is exactly the
result you want,
since this REALLY IS a paradox.

[George Greene]

On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> You still owe me some BASE THEOREMS, otherwise all your "proofs" are
> Oracular.

No, I don't. I can just say that rule "EM" (that is what I choose to
call it)
allows me to infer P V ~P *FROM*NOTHING*.
Moreover, I can call the universal generalization of that (with P as
the variable) an inference rule (if I want to)
and say that if P is ANY WFF WHATSOEVER in the first-order langauge I
am using, then
P V ~P is inferred, as the conclusion of this inference rule, and as a
theorem,
FROM NOTHING.
That does NOT make anything "oracular" and it does NOT make anything a
"logical axiom".

I can [AND DO] JUST say that it is an inference rule that any
instance of a propositional tautology is a theorem.

[Graham Cooper]

George, I don't care!

*I* use MODUS PONENS for inference and ANY OLE AXIOM and ANY THEOREM
SO FAR.

a & (a->b) --> b

*I* use double arrow --> for NEW THEOREM

If you want to use a list of inferences distinct from axioms, may I
suggest

(P ^ Q) --> Q

so we know it's not a THEOREM/AXIOM

The only lesson here is that there is SOME / ONE rule that operates ON
the theory by creating --> new formula which is distinct from the
theorems.

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

In MY TERMINOLOGY, since you use "model" to mean "deduction sequence"
is meaningless.

A MODEL is CREATED in the theory like so:

a & (a ->[p->q]) -> [p->q]

NOW you have a 2ND LEVEL OF INFERENCE RULES [p->q]

You could JUST USE MODUS PONENS TO DO THIS and a set of tautology
formula

but you like to have a list

1 P --> P
2 !P --> !P
...

which forces the prover into a single model.




Herc

[George Greene]

On Oct 13, 8:20 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> George, I don't care!

Then you are not going to be able to communicate!
You HAVE to use terms in AT LEAST APPROXIMATELY the way they are
already being used, by people who ALREADY KNOW (which YOU DON'T yet)
HOW
to use them!

> *I* use MODUS PONENS for inference

Fine.

> and ANY OLE AXIOM and ANY THEOREM SO FAR.

But BEFORE YOU can say "so far", YOU OWE US some "base theorems".
It is perfectly fine if you want to say that modus ponens is the only
inference rule you are using.
But the only connective in modus ponens is ->, so HOW ARE YOU EVER
going to prove ANY
*conjunction* if the only inference rule you have is modus ponens?
YOU are going to HAVE to
have something else!

We were doing this in a context of FIRST-order logic. You
unfortunately appear to be reverting TO *0*-th-order, to
PROPOSITIONAL, logic.
THERE IS A DIFFERENT THING GOING ON down at that level. At the first-
order level, the reasonable thing to do is to just take ALL
of 0th/propositional as just GIVEN, as just SOLVED, as just NOT WORTH
BOTHERING WITH, and to just CONCENTRATE on the first-order
piece. You, unfortunately, cannot tell one order from another and
keep mixing them up.

> a & (a->b) --> b
>
> *I* use double arrow --> for NEW THEOREM

That ISN'T double arrow -- double arrow is ==>.
You basically can't use -> because a hyphen is too short to be an
arrow-shaft.
If you want this to be readable (in a proportional font) then --> is a
single-arrow and ==> is a double-arrow.

> If you want to use a list of inferences distinct from axioms, may I
> suggest

> (P ^ Q) --> Q
>
> so we know it's not a THEOREM/AXIOM

( P /\ Q) --> Q is a TAUTOLOGY.
It's a ZEROth-order validity. HOW YOU INFERRED OR PROVED IT is NOT
important TO ANYbody doing FIRST-order logic!
The only people who care about how you proved this theorem are people
doing PROPOSITIONAL logic, are STUDENTS!

> The only lesson here is that there is SOME / ONE rule that operates ON
> the theory by creating --> new formula which is distinct from the
> theorems.

Lesson FOR WHOM? WHOM DO YOU THINK *YOU* are teaching!
I already have two degrees in this and (newsflash) the teachers who
already gave me good grades in all this stuff were FAR MORE
INTELLIGENT THAN YOU ARE!
The rule that "operates on the theory by creating --> new formula"
does NOT create formulas that are distinct from the theorems!
The new formulas that the inference rule infers from the old ones ARE
the theorems! That IS THE DEFINITION of "theorem"!
A theorem is a WFF *with*a* PROOF!
You prove a theorem by inferring/deriving it FROM THE AXIOMS, USING
the inference rules!
But the axioms ARE NOT *logical* axioms!
Anything YOU might want TO CALL a "logical axiom" would BE BETTER
thought of as an inference rule!
And there is NO reason for you to limit yourself to ONE of them!
You CAN do that, but it requires EFFORT AND TRANSLATION, which is not
normally going to be considered natural!
Natural treatments do NOT normally confine themselves to --> (MP) or V
(resolution) as their only connective!
But you HAVE TO REWRITE EVERYTHING in that single-connective style IF
you are going to restrict yourself to
the one inference rule!

> In MY TERMINOLOGY, since you use "model" to mean "deduction sequence" is meaningless.

That sentence is ungrammatical, in your terminology or anyone else's.
And STOP talking about what *I* use.
You DON'T KNOW. ONLY I can say what "I use".

[George Greene]

On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> I'll print the table here, nice one!
>
> http://en.wikipedia.org/wiki/List_of_rules_of_inference

You don't know what you were printing.
You DIDN'T print a table! You just linked a whole article!
And that article had TWO tables! The first of
those are SENTENTIAL rules of inference.
Those are from ZEROth-order logic.
Those are from PROPOSITIONAL logic.
Those are from sentential/propositional calculus AS OPPOSED to
PREDICATE calculus, which was what WE were TRYING to talk about!
IT DOES NOT MATTER HOW ANYbody treats propositional calculus!
Propositional calculus is a KNOWN, WELL-UNDERSTOOD, SIMPLE
thing. It is NP-hard (and nobody knows exactly how hard that is) but
that is LESS hard than exponential, and it is therefore SIMPLE.
It DOES NOT BEAR BELABORING in any context where we are talking about
a powerful FIRST-order theory like SET theory!

It's the SECOND table, the one about FIRST-order rules of inference,
that was relevant.
And it listed a lot more than just one (resolution), I repeat, MORE
than just one (modus ponens), FOR THOSE.
One of the most important first-order rules is that you can infer
ANYthing that is an instance of a zeroth-order tautology, FROM
NOTHING.

[Alan Smaill]

camg...@hush.com writes:

> On Oct 13, 9:39 am, George Greene <gree...@email.unc.edu> wrote:
>> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
>>
>> > deductive system is a list of formulas,
>> > each of which is a logical axiom
>>
>> NO, a deductive system IS NOT a list of formulas.
>>
>> JEEzus.
>
> That's a quote from WIKI

Actually wiki says something quite different:

"A deduction in a Hilbert-style deductive system is a list of formulas,
each of which is ..."

>
> Herc
>

--
Alan Smaill

[George Greene]

On Oct 13, 3:36 pm, Graham Cooper

> you can't follow the context of this quote?

----8<----------------------------

> On Oct 12, 3:02 am, Graham Cooper <grahamcoop...@gmail.com> wrote:

> > >http://en.wikipedia.org/wiki/First-order_logic

> deductive system is a list of formulas, each of which is a logical axiom

> (taken from full paragraph in previous post which you didn't read)

Idiot, YOU didn't read it. YOU cannot follow the context!
IF you had read it, you would've KNOWN that you had deleted SO MUCH
context that you don't even have THE WHOLE SENTENCE, let ALONE
a full paragraph! YOU DELETED so much "context" to produce this
HORSESHIT that you have gotten THE SUBJECT of the verb-phrase
"is a list of formulas" WRONG! The article DID NOT SAY that a
"deductive system" is a list of formulas! It said *A*DEDUCTION* is a
list of formulas!
Said deduction is occurring INSIDE/UNDER/WITHIN-the-framework-of a
deductive system, but the deductive system IS NOT the list of
formulas!
YOU SAID IT WAS!
AND THEN you claimed that it was "a quote from wiki" that it was!
IT WASN'T!
STOP QUOTING SHIT THAT YOU HAVEN'T EVEN BOTHERED TO READ!
Stop taking stuff so far out of context that you can't even match THE
SUBJECT TO THE VERB of THE SAME SENTENCE!
AT LEAST QUOTE *A*COMPLETE*SENTENCE*!!!

Clue: when it SAYS "a deduction", it MEANS, "A *PROOF*". A proof
is something that EVERY theorem HAS to have, EVEN if it's as trivial a
proof as "it's an axiom".

[George Greene]

> >> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

> >> > deductive system is a list of formulas,
> >> > each of which is a logical axiom

> > On Oct 13, 9:39 am, George Greene <gree...@email.unc.edu> wrote:
> >> NO, a deductive system IS NOT a list of formulas.
> >> JEEzus.

> >> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com>
wrote:
> > That's a quote from WIKI

On Oct 14, 1:40 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:

> camgi...@hush.com writes:
> Actually wiki says something quite different:
>
> "A deduction in a Hilbert-style deductive system is a list of formulas,
>  each of which is ..."

> Alan Smaill

To Alan: Thank you kindly for your support.

To Herc: please try to prove that you are smart enough to parse a
complete sentence -- AS OPPOSED to stupid enough to take the object of
a prepositional phrase OUT OF CONTEXT and MISTAKE it for the subject
of the main verb (which subject you were stupid enough to cut, if you
were smart enough to even read it in the first place).

Clue: If you can't hack THE BASIC GRAMMAR OF *YOUR*OWN* native
language then there IS VERY LITTLE point in your even TRYING to deal
with a first-order language or any formal language! GRAMMAR IS
FUNDAMENTAL!

[Graham Cooper]

Hey don't burst an artery!

I quoted the whole paragraph and you ignored it!

You said WHY QUOTE THE DIFFERENCE BETWEEN
NATURAL AND HILBERT SYSTEMS?

so I quoted the part with ... IT HAS LOGIC AXIOMS.

LOGIC AXIOMS! THE TOPIC FOR 2 WEEKS.

the fact I made it look like a LIST OF LIST OF FORMULA
instead of a LIST OF FORMULA

is a typo!

YOU STILL LOSE, LOSERS!

You are a LONG WAY from PROVING

~E(r) xer <-> ~xex

with INFERENCE RULES.

FOR 1 THING - THERE IS A VARIABLE INSTANTIATION

and George is struggling with Supercombinator Theory to even know how
to do that with RULES.

*******

And for the 20th time!

Stop writing novels about OBJECT LANGUAGE CRAP!

What you are saying takes 1 line!

-> is logical implication
--> is implied theorem addition to the physical theory.

REMINDER
The topic is:

~E(r) xer <-> ~xex

is a formula *included* in ZFC (without axioms)

YOU HAVE NOT SHOWN THIS.

I think with a few RELATIONAL ALGEGRA AXIOMS
and VARIABLE INSTANTIATION RULES
you may be able to.

but I win, NO AXIOMS, no ~E(russell set) as a THEOREM in ZFC.



Herc

[Graham Cooper]

On Oct 15, 1:01 am, George Greene <gree...@email.unc.edu> wrote:
> > a & (a->b) --> b
>
> > *I* use double arrow --> for NEW THEOREM
>
>

> > The only lesson here is that there is SOME / ONE rule that operates ON
> > the theory by creating --> new formula which is distinct from the
> > theorems.
>

> You prove a theorem by inferring/deriving it FROM THE AXIOMS, USING
> the inference rules!
> But the axioms ARE NOT *logical* axioms!
> Anything YOU might want TO CALL a "logical axiom" would BE BETTER
> thought of as an inference rule!
> And there is NO reason for you to limit yourself to ONE of them!
> You CAN do that, but it requires EFFORT AND TRANSLATION, which is not
> normally going to be considered natural!
> Natural treatments do NOT normally confine themselves to --> (MP) or V
> (resolution) as their only connective!

No it's really quite simple and 20 years ago was the defacto standard
in theorem provers.

MP

LHS & (LHS->RHS) --> RHS

where --> *ADDS* A NEW THEOREM

where LHS->RHS is any THEOREM with an outermost implication.

IF you make a OBJECT LANGUAGE with a big list of

LHS --> RHS
LHS --> RHS
..

that's really neat but it's going to miss any derived inference rules.

I use

LHS & (LHS -> (a&b->c)) -> a&b->c

to derive models of backward chainable embedded theories that are
recursively provable back to the axioms!

but you are stuck on

ALL(x) x is a set with FOL language in WFF this and object that so
where does !E(x) go?!?

Herc

[Graham Cooper]

> LHS & (LHS -> (a&b->c)) -> a&b->c
>
> to derive models of backward chainable embedded theories that are
> recursively provable back to the axioms!
>

BINARY MODUS PONENS

a & b & (a&b)->c --> c


This not only WORKS! It derives all proofs!

PROOF = backward chainable binary directed acylic graph

You're still stuck on the 'CLASSIC THEOREM'!

******** 10 YEARS DEBUGGING TO FIX THIS **********

> NOT(PA |- P) & NOT(PA |- ~P).
> That is the classical theorem. Duh.
> [...]
> >> I don't see your point. The theorem says that PA can not decide a
> >> particular formula.
> > no, a particular wff (conditions apply)
> When I say "formula", I mean "WFF". I have no reason to talk about
> non-well-formed formulas.


That's why your proof is wrong.
-------------------------------------
[ERROR 1]
By WFF you mean it has a single reduction tree in predicate calculus
from sub predicates and atomic formula, giving it a unique
interpretation. So you have limited the scope of your proof to boolean
formula (true or false).
-------------------------------
[ERROR 2]
THEN: YOU START ADDING FORMULA AT WILL.
"WE CAN CONSTRUCT ANY FORMULA AND TRY TO ADD IT TO THE THEORY"
ERROR!

PA |- P
This is using an axiom-less or inconsistent theory
CONTRADICTION |- ANYTHING
--------------------------------------
[VALID STEP]
Because P is "true" by some rudimentary reductions (P can't be false)
NOT( PA |- P )
NOT( PA |- ~P )
-------------------------------------
[ERROR 3]
P <-> NOT( PA |- P )
so P is TRUE (in PA)
-------------------------------------
[ERROR 4]
P is a WFF in PA
AND
P is TRUE in PA
---> P is a missing theorem of PA

You EQUATE
WFF + TRUE --> THEOREM
-------------------------------------
[ERROR 5]
Because:
(P -> Q) -> (P ^ AXIOM) -> Q
is true for 0 order terms (not formula with quantifiers)
You conclude adding AXIOMS to PA could never filter out the Godel
Statement and call it
MONOTONIC LOGIC!
--------------------------------





Herc

[George Greene]

On Oct 14, 8:06 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> I quoted the whole paragraph and you ignored it!

I DIDN'T ignore it! I read and then ASKED WHY you were going on about
differences between Hilbert
and natural-deduction systems! THAT DOESN'T *MATTER*!!

> You said WHY QUOTE THE DIFFERENCE BETWEEN
> NATURAL AND HILBERT SYSTEMS?
>
> so I quoted the part with ... IT HAS LOGIC AXIOMS.

No, you did NOT do that -- you MISquoted something saying a deductive
system was a list of formulas.

>
> LOGIC AXIOMS!  THE TOPIC FOR 2 WEEKS.
>
> the fact I made it look like a LIST OF LIST OF FORMULA
> instead of a LIST OF FORMULA
>
> is a typo!

No, it ISN'T a typo -- it's QUOTED FROM THE ARTICLE so it CAN'T be a
typo!
You just quoted it WRONG! And then BELIEVED your own wrong misquote!
Herc: just becomes somebody SAID something "has logical axioms" DOES
NOT MEAN
it has them! *I* say it DOESN'T have them and *I* am the one
teaching this course!

ANY logical axiom can BE REPLACED by a rule of inference that simply
infers/produces THE SAME result!
That sort of means that there IS NO POINT IN ANYBODY EVER having
logical axioms! The people who SAY
they have them DON'T NEED THEM. *YOU*ESPECIALLY* don't need them
since YOU ARE NOT SMART ENOUGH TO TELL THE DIFFERENCE
between "a logical axiom" and an axiom (a REAL axiom, an axiom being
used FOR THE RIGHT purpose, for the purpose that axioms ARE FOR,
namely, to serve AS THE BASE upon which to construct the theorems, as
the first things FROM WHICH the inference rules can be used to infer
THEOREMS) IN THE *OBJECT* theory!

> You are a LONG WAY from PROVING
>
> ~E(r)  xer <-> ~xex
>
> with INFERENCE RULES.

Dipshit, I HAVE ALREADY POSTED this proof!

You can infer
~( rer <--> ~rer ) FROM NOTHING (at 1st-order), BECAUSE IT IS A
*ZERO*TH-Order TAUTOLOGY!
If you really want to "prove" that then you can prove it just by
COMPUTING ITS TRUTH-TABLE!
That suffices FOR ALL tautologies!
Once you have that, THERE REALLY IS AN INFERENCE RULE called
"existential generalization" that you can use to generalize 3 of the 4
r's to get
Ex[ ~( xer <--> ~xex ) ]

>
> FOR 1 THING - THERE IS A VARIABLE INSTANTIATION

And for another thing, THERE ARE INFERENCE RULES both for introducing
and eliminating quantifiers and variables, both existential and
universal, in first-order logic, DUMBASS. YOU EVEN QUOTED A TABLE of
them, SO YOU ALLEGE.

> Stop writing novels about OBJECT LANGUAGE CRAP!

Idiot, ANYTHING WITH "e" in it IS IN the object language!
The object language IS RELEVANT! I do NOT MEAN "object language" in
the COMPILER sense!
You are so ignorant about logic that you didn't even know that that
term had another meaning!

> What you are saying takes 1 line!

*I* am the one who TOLD YOU that it only takes one line to infer
~( rer <--> ~rer ) !! To raise that to FIRST-order DOES take SEVERAL
lines!

> -> is logical implication
> --> is implied theorem addition to the physical theory.

SEZ YOU. If you think anybody is going to adopt your notation in this
context, you have another thing coming.
Those symbols look too much alike, and the first one is just too small
to be legible.
IN REAL LIFE, logical/material implication is going to look like -->,
and an inference rule,
something that allows you to add a new theorem to things you've
already derived, is going to look like
(old theorem1 as input)
(old theorem2 as input)
==================
(new theorem as output).

That's right, it's going to be written WITH A HORIZONTAL LINE
SEPARATING the premises from the inferred conclusion.
WHICH YOU WOULD KNOW ALREADY IF YOU HAD BOTHERED TO READ what you were
quoting!

There IS NO "physical theory".

WHY DON'T YOU READ the wikpedia article on first-order logic instead
of falsely assuming that it might say something that might help you
win this argument?
There IS NO argument! It TAKES TWO to argue! You ARE NOT one of the
two becuase YOU DON'T KNOW anything!

[George Greene]

> On Oct 15, 1:01 am, George Greene <gree...@email.unc.edu> wrote:
> > Natural treatments do NOT normally confine themselves to --> (MP) or V
> > (resolution) as their only connective!

On Oct 14, 9:05 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> No it's really quite simple and 20 years ago was the defacto standard
> in theorem provers.

WHOM do you think you are telling?!? Of the two of us, I AND NOT YOU
am the one with
a degree in theorem-proving!
OF COURSE a single inference rule was preferable IN AUTOMATED theorem-
provers!
I *SAID* N A T U R A L T R E A T M E N T S !!!!
Things that reasoners occurring IN NATURE, I.E. THINKING HUMANS, USE!

[George Greene]

On Oct 14, 9:21 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> ******** 10 YEARS DEBUGGING TO FIX THIS **********

How do you HAVE TIME to do this??
You obviously don't know shit about theorem-proving.
How can you be economically supported while working on this?
Or should we conclude from the sheer amateurishness of your efforts
that this was 10 years of your SPARE time, and that you have a real
job
doing some more concrete&applicable kind of programming??

[Graham Cooper]

I make $5K a week doubling every 12 months.

Hello Cam Affiliate,

Congratulations! You have earned commissions on referrals to
CAMGIRLS.COM

Your commission is

TOTAL: $2515 2012-10-07 Sun
TOTAL: $1807 2012-10-08 Mon
TOTAL: $1902 2012-10-09 Tue
TOTAL: $2420 2012-10-10 Wed
TOTAL: $1598 2012-10-11 Thu
TOTAL: $2578 2012-10-12 Fri
TOTAL: $1984 2012-10-13 Sat

7 DAY TOTAL: $14808 (35% = $5182)


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

George you are a SUB-HUMAN MORON!

You are talking to GENESIS ADAM of KINGS BEACH QUEENSLAND

I only talked to you to get the derivation of !EXIST(RS)

because *I* posted it was a axiomless fact 12 MONTHS AGO

and I need it to STRATIFY OUT RS FROM *MY* PROVABLE SET THEORY.

A(S) xeS <-> DERIVE( E(x) xeS )

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


THE 1ST ABSOLUTE TRUTH! <<<<<<<<<<
Graham Cooper grahamcoop...@gmail.com alt bible alt talk creationism
alt
atheism sci logic alt astrology Firstly, you have the unsupported
assertion that
there is something at the bottom of it all. Let's break LV's meta-
Philosophy into 2.
Unsupported and unsupportable. To make a long story as short as
possible:

May 6 by Graham Cooper - 5 messages - 3 authors

"The first ABSOLUTE TRUTH is actually the non-existence of Russell's
Set, i.e. a 'fundamental paradox that is founding the territory.' "

THANK YOU GEORGE for the AUTOMATED DERIVATION I WAS AFTER.

THAT IS ALL

Herc