Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Replies: 39   Last Post: Oct 14, 2012 11:56 PM

 Messages: [ Previous | Next ]
 camgirls@hush.com Posts: 12 Registered: 4/8/11
Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Posted: Oct 12, 2012 8:37 PM

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

Date Subject Author
10/5/12 Graham Cooper
10/5/12 Frederick Williams
10/7/12 Charlie-Boo
10/5/12 Graham Cooper
10/5/12 Frederick Williams
10/5/12 Graham Cooper
10/7/12 Graham Cooper
10/8/12 Graham Cooper
10/9/12 Graham Cooper
10/11/12 Graham Cooper
10/12/12 Graham Cooper
10/12/12 Graham Cooper
10/12/12 camgirls@hush.com
10/12/12 Richard Tobin
10/12/12 camgirls@hush.com
10/13/12 george
10/13/12 Graham Cooper
10/14/12 george
10/13/12 Graham Cooper
10/13/12 george
10/13/12 george
10/13/12 Graham Cooper
10/14/12 Graham Cooper
10/14/12 Graham Cooper
10/14/12 Graham Cooper
10/5/12 Scott Berg
10/5/12 Curt Welch
10/6/12 Mike Terry
10/6/12 Graham Cooper