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 12, 2012 3:02 AM

On Oct 12, 2:06 pm, George Greene <gree...@email.unc.edu> wrote:
> 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

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

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