
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/Firstorder_logic
Hilbertstyle systems and natural deduction
A deduction in a Hilbertstyle 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 Hilbertstyle 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 Hilbertstyle systems in that a deduction is a finite list of formulas. However, natural deduction systems have no logical axioms; they compensate by adding additional rules of inference that can be used to manipulate the logical connectives in formulas in the proof.
firstorder 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/Firstorder_logic#Provable_identities
Herc

