On Nov 18, 3:11 am, George Greene <gree...@email.unc.edu> wrote: > On Nov 17, 3:50 am, Graham Cooper <grahamcoop...@gmail.com> wrote: > > > FROM AXIOMS you DERIVE THEOREMS! > > True. > > > Nobody CARES if SomeModel |= 'this is not derivable from your > > axioms" > > > looks TRUE! > > Sure they do. > > > IT's not DERIVABLE FROM THE AXIOMS! END OF STORY! > > That's NOT the end of the story! > > It is true that the name of the room is "sci.logic" and that WE > therefore (even if no one else is) > might be entitled to care about&only about what follows from the > axioms. But the PROBLEM is > that the primary USE for formal proof is IN *MATH*. > THEREfore, EVEN though the sign on the door says sci.logic, it is > MATHEMATICIANS > who matter more. > > In the relevant case of models and of |= , the MOST relevant model > around here is > N, is THE (true&actual) NATURAL NUMBERS. > IT DOES matter a WHOLE HECK of a lot if something that is true about N > is NOT > formally derivable from some decent (i.e. recursive) set of axioms. > That is VERY important! > PEOPLE CARE about proving things ABOUT N, *NOT* just about proving > whatever > follows from some axioms. For starters, how would you decide WHICH > axioms were > IMPORTANT? It is NEVER JUST about the axioms themselves! YOU ALWAYS > need SOMEthing > OUTside of logic motivating your investigation! You are always USING > logic to help you reason > ABOUT something ELSE! > > > Nothing Mathematically INCOMPLETE ABOUT IT! > > It is true about all these recursively enumerable formal theories that > THEY ARE incomplete *ABOUT* N. > You are sort of right, however, in that first-order-logic ALSO has a > COMPLETEness theorem. > A small and reasonable set of rules of inference REALLY IS sufficient > to derive&prove, formally, > EVERY theorem that is true in ALL models of the axioms. > But there is no decent set of axioms or rules that is sufficient to > derive&prove every (first-order) sentence that is true *in*N*, > that is true of the natural numbers. THAT is how FOL gets to have > BOTH a "completeness" AND an "incompleteness" > [meta]theorem. > > Prolog > just doesn't have anything to do with this. Prolog can't even do > complete FOL. > Prolog APPROXIMATES first-order negation-AS-failure. >
See this is the problem.
You just BAFFLE WITH BULLSHIT every assertion made that doesn't match your Library Of Logic Facts!