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