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 ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Posted: Oct 13, 2012 4:30 PM

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

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

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