Date: Oct 12, 2012 8:37 PM
Author: camgirls@hush.com
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




> 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