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