The old Google Groups will be going away soon, but your browser is incompatible with the new version.
If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
 There are currently too many topics in this group that display first. To make this topic appear first, remove this option from another topic. There was an error processing your request. Please try again. Standard view   View as tree
 20 messages

From:
To:
Cc:
Followup To:
Subject:
 Validation: For verification purposes please type the characters you see in the picture below or the numbers you hear by clicking the accessibility icon.

More options Oct 5 2012, 3:59 am
Newsgroups: sci.logic, sci.math, sci.physics, comp.ai.philosophy, rec.org.mensa
From: Graham Cooper <grahamcoop...@gmail.com>
Date: Fri, 5 Oct 2012 00:59:50 -0700 (PDT)
Local: Fri, Oct 5 2012 3:59 am
Subject: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 5 2012, 8:47 am
Newsgroups: sci.logic, sci.math, sci.physics, comp.ai.philosophy, rec.org.mensa
From: Frederick Williams <freddywilli...@btinternet.com>
Date: Fri, 05 Oct 2012 13:47:05 +0100
Local: Fri, Oct 5 2012 8:47 am
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

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.

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 5 2012, 10:09 pm
Newsgroups: sci.logic, sci.math, sci.physics, comp.ai.philosophy, rec.org.mensa
From: "Mike Delanis" <inva...@invalid.com>
Date: Fri, 5 Oct 2012 21:08:49 -0500
Local: Fri, Oct 5 2012 10:08 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

"Graham Cooper" <grahamcoop...@gmail.com> wrote in message

> 20 goto 10

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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 5 2012, 11:45 pm
Newsgroups: sci.logic, sci.math, sci.physics, comp.ai.philosophy, rec.org.mensa
From: c...@kcwc.com (Curt Welch)
Date: 06 Oct 2012 03:45:32 GMT
Local: Fri, Oct 5 2012 11:45 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

"Mike Delanis" <inva...@invalid.com> wrote:
> "Graham Cooper" <grahamcoop...@gmail.com> wrote in message

> > 20 goto 10

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

My first access to computers was with an interpreted basic system in the
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/

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 6 2012, 10:11 am
Newsgroups: sci.logic, sci.math, sci.physics, comp.ai.philosophy, rec.org.mensa
Date: Sat, 6 Oct 2012 15:11:21 +0100
Local: Sat, Oct 6 2012 10:11 am
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
"Curt Welch" <c...@kcwc.com> wrote in message

> "Mike Delanis" <inva...@invalid.com> wrote:
> > "Graham Cooper" <grahamcoop...@gmail.com> wrote in message

> > > 20 goto 10

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

> My first access to computers was with an interpreted basic system in the
> 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.

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 6 2012, 5:09 pm
Newsgroups: sci.logic, sci.math, sci.physics, comp.ai.philosophy, rec.org.mensa
From: Graham Cooper <grahamcoop...@gmail.com>
Date: Sat, 6 Oct 2012 14:09:12 -0700 (PDT)
Local: Sat, Oct 6 2012 5:09 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
On Oct 7, 12:11 am, "Mike Terry"

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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 7 2012, 5:48 pm
Newsgroups: sci.logic, sci.math, sci.physics, comp.ai.philosophy, rec.org.mensa
From: Graham Cooper <grahamcoop...@gmail.com>
Date: Sun, 7 Oct 2012 14:48:06 -0700 (PDT)
Local: Sun, Oct 7 2012 5:48 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
On Oct 8, 6:38 am, George Greene <gree...@email.unc.edu> wrote:

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*

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 7 2012, 7:38 pm
Newsgroups: sci.logic, sci.math, sci.physics, comp.ai.philosophy, rec.org.mensa
From: Charlie-Boo <shymath...@gmail.com>
Date: Sun, 7 Oct 2012 16:38:43 -0700 (PDT)
Local: Sun, Oct 7 2012 7:38 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
On Oct 5, 8:47 am, Frederick Williams <freddywilli...@btinternet.com>
wrote:

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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 11 2012, 4:03 pm
Newsgroups: sci.logic, sci.math, sci.physics
From: Graham Cooper <grahamcoop...@gmail.com>
Date: Thu, 11 Oct 2012 13:03:38 -0700 (PDT)
Local: Thurs, Oct 11 2012 4:03 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
On Oct 12, 1:23 am, George Greene <gree...@email.unc.edu> wrote:

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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 12 2012, 8:37 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: camgi...@hush.com
Date: Fri, 12 Oct 2012 17:37:31 -0700 (PDT)
Local: Fri, Oct 12 2012 8:37 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
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

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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 12 2012, 8:45 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: rich...@cogsci.ed.ac.uk (Richard Tobin)
Date: Sat, 13 Oct 2012 00:43:56 +0000 (UTC)
Local: Fri, Oct 12 2012 8:43 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

<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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 12 2012, 8:52 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: camgi...@hush.com
Date: Fri, 12 Oct 2012 17:52:22 -0700 (PDT)
Local: Fri, Oct 12 2012 8:52 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
On 13 Oct, 10:45, rich...@cogsci.ed.ac.uk (Richard Tobin) wrote:

[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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 13 2012, 11:48 am
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: George Greene <gree...@email.unc.edu>
Date: Sat, 13 Oct 2012 08:48:22 -0700 (PDT)
Local: Sat, Oct 13 2012 11:48 am
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 13 2012, 3:36 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: Graham Cooper <grahamcoop...@gmail.com>
Date: Sat, 13 Oct 2012 12:36:11 -0700 (PDT)
Local: Sat, Oct 13 2012 3:36 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 13 2012, 4:30 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: Graham Cooper <grahamcoop...@gmail.com>
Date: Sat, 13 Oct 2012 13:30:32 -0700 (PDT)
Local: Sat, Oct 13 2012 4:30 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
On Oct 14, 1:48 am, George Greene <gree...@email.unc.edu> wrote:

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!

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

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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 13 2012, 8:13 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: George Greene <gree...@email.unc.edu>
Date: Sat, 13 Oct 2012 17:13:49 -0700 (PDT)
Local: Sat, Oct 13 2012 8:13 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
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.

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 13 2012, 8:16 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: George Greene <gree...@email.unc.edu>
Date: Sat, 13 Oct 2012 17:16:31 -0700 (PDT)
Local: Sat, Oct 13 2012 8:16 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
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.

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 14 2012, 1:40 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: Alan Smaill <sma...@SPAMinf.ed.ac.uk>
Date: Sun, 14 Oct 2012 18:36:34 +0100
Local: Sun, Oct 14 2012 1:36 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 14 2012, 3:58 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: George Greene <gree...@email.unc.edu>
Date: Sun, 14 Oct 2012 12:57:59 -0700 (PDT)
Local: Sun, Oct 14 2012 3:57 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

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

To post a message you must first join this group.
You do not have the permission required to post.
More options Oct 14 2012, 8:06 pm
Newsgroups: sci.logic, sci.math, comp.ai.philosophy, sci.physics
From: Graham Cooper <grahamcoop...@gmail.com>
Date: Sun, 14 Oct 2012 17:06:10 -0700 (PDT)
Local: Sun, Oct 14 2012 8:06 pm
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
On Oct 15, 5:58 am, George Greene <gree...@email.unc.edu> wrote:

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