A mathematical introduction to logic

What Hacker News says

1. throwaway81523Apr 2021
   Well, it depends on what you are looking for, but the traditional-style book that I'm used to is H. B. Enderton, "A Mathematical Introduction to Logic", and Enderton also has an accompanying book on set theory. I guess I'd suggest those as a companion rather than an alternative to the Gallier and Quaintance book. The G&Q book is imho more modern and more interesting from a CS-oriented perspective. It just leaves out too many important fundamentals. Alternatively, since it is still a work in progress, maybe some of the missing stuff could be added.

   Boolos and Jeffrey "Logic and Computability", whatever the current edition is, is supposed to be good, but I haven't read it yet.

   The G&Q book is weird in that it is about interesting topics that I'd consider slightly advanced, but written in a way that assumes almost no background, so if it's the only thing you read, you'll still be missing important background. I'd like a book that uses the G&Q approach but that includes the background. If it kept all the current contents and was expanded, it would probably end up as 2 volumes, which is fine. Or it could leave out some of the specialized stuff, but I think that stuff is there because that was what the authors wanted to write about, so I won't judge ;-).

   Show morethread
2. fnrslvrApr 2019
   > Mathematical Logic

   A Mathematical Introduction to Logic, by Herbert Enderton.

   thread
3. danharajSep 2015
   The Stanford Encyclopedia of Philosophy; this article is a perfect start: http://plato.stanford.edu/entries/logic-classical/

   Of course, this is extremely dense! A book that covers this article in a pedagogical and beautiful manner is A Mathematical Introduction to Logic by Enderton.

   But still, this is all formal logic. It lies at the locus of many disciplines and ways of thinking, and there are many, many formal logics to explore. It is the idea of formal logic which is important, and the SEP is a good place to put it in context.

   Show morethread
4. ionfishJul 2010
   ∀ is the standard symbol for the universal quantifier: some proposition is true for all elements in the universe being quantified over. This is stated explicitly in the paper: "The type given for runST above is implicitly universally quantified over both s and a."

   We could thus expand the type given for runST as follows: runST is a function which, for every instance of the type a, and every instance of the type s, accepts a state transformer (with type ST s a) and returns a value of type a.

   If you want to attain a better understanding of the logical concepts and notation used in the article, try getting hold of an introductory logic text. I recommend Enderton's 'A Mathematical Introduction to Logic'.

   http://www.math.ucla.edu/~hbe/amil/index.html

   Show morethread
5. anatolyDec 2009
   I hesitate to say this, because it sounds harsh, but your comment is a heap of confusion. You're using words like "first order", "second order", "axiom system", "true statements", "refuted", with confused understanding of what they mean. They all have clear technical meanings.

   If you're interested in this stuff and can stomach mathematical rigor, I highly recommend Enderton's _A Mathematical Introduction to Logic_ for mathematical logic in general, and Smullyan's own _Goedel's Incompleteness Theorems_ for this topic.

   Now, to back my harsh words a little.

   An axiomatic system, in the context of Goedel's theorems, is a bunch of axioms with some inference rules. Axioms are statements that are automatically taken as proved, while inference rules allow one to infer more proved statements from some already proved statements. Given an axiomatic system, you can define a proof of statement X to be a sequence of statements that starts with axioms and always goes through inference rules until it reaches X.

   All of the above is purely syntactic, meaning it has to do with rules that govern how symbols are written on the paper, and there's no need for any interpretation of what the symbols mean. You could have an axiomatic system where statements would be Tarot cards, axioms some particular cards, and inference rules would govern which card you can place next to ones you already have. It'd be a silly axiomatic system, but it would be one, and you wouldn't need to know anything about what the cards "mean". Similarly, you can write down an axiomatic system with statements that use symbols like "0", "1", "+", "x" "forall", without caring what it means for a statement to be true or false.

   Any axiomatic system really comes with a _logic_ in the background: the logic specifies what kinds of statements you're allowed to write down. The most important and frequently used kind is first-order logic, which lets you use constant symbols like "0", "1", function symbols like "+" (again, as purely abstract marks-on-paper without caring what their meaning is), equality sign "=", variables like "x", "y" etc., and crucially quantifiers "for all" and "exists" that let you say things like "for all x, something-that-depends-on-x".

   Second-order logic, in addition, also lets you quantify over sets or functions. In first-order logic, you can only have a few fixed symbols like + and write some statements about them, but in second-order logic you can express statements about any possible function, like, say, "for every function F on two variables, F(x,y) = F(y,x)". This kind of statement is invalid in first-order logic, for some good reasons. Not "true" or "false", just impossible to write down in the first place.

   This is why when you say "The Incompleteness Theorem shows that no first order axiomatic system is powerful enough to encapsulate all true statements in the second order Peano axioms", this is nonsense, because a first-order axiomatic system cannot prove statements in a second-order system, in general. They come from different logics. Second-order systems contain statements that first-order systems can't express at all, much less prove.

   Now, independently of defining an axiomatic system, we can also define a meaning - "semantics" - for any statement in a particular logic. For example, we can decide, with good reason, that the symbol "0" actually stands for the number 0, the symbol "+" stands for the operation of addition, and so on. The statement "2+2=5" will then not be just a string of five meaningless marks on paper, it will also have a meaning and a truth value (which is false, in this case). We can decide what it means for the more complex statements like "for all x ..." to be true - appropriately enough, it means that if you try to substitute any number for x inside the "...", you'll always get a true statement. Now every statement in our logic is either true or false, although for many of them it's difficult to know which is the case.

   Going back to axiomatic systems, we remember that they have axioms and inference rules. Typically, some of the axioms and all of the inference rules are called "logical" and are independent of the particular math structure we're trying to investigate (natural numbers, in this case). The logical axioms and inference rules say things like "x=x" and "if you proved "for all x, ...", you can also count as proved any version of ... in which you substituted something for x". We regard them as intuitively, tautologically true. The other, remaining non-logical axioms say things like "a+0=a" and "every number except 0 has a predecessor". They could be for example the Peano axioms for natural numbers.

   Godel's Completeness Theorem has absolutely nothing to do with his Incompleteness Theorem, and the "completeness" it talks about is very different from the "incompleteness" the other theorem talks about. Goedel's Completeness Theorem really says something important about the usual bunch of logical axioms and inference rules, the one that form the backbone of pretty much every first-order axiomatic system we study. It says that they're strong enough to prove anything that must always be true in any semantics. For example (trivial example), no matter how we define what the symbol '0' means, it will always be true that "for any x, if x=0, then 0=x". All tautologies like that are better be provable with logical axioms alone, and Goedel's Completeness Theorem ensures that they are. The fact that we have a Goedel's Completeness Theorem is really what allows us to confidently use first-order logic as a conceptual basis for all mathematics. It tells us that axiomatic systems for first-order logic are complete in the sense of "strong enough to prove all tautologies". But it has nothing to do with the Incompleteness Theorems, which are about "complete" in the sense of "strong enough to prove every sentence or its negation".

   So your second paragraph "In fact, his Completeness Theorem proves the opposite of what you claim" is nonsense, too. It's true that you can make up a trivial example of a complete system just by declaring all true statements to be axioms. But that fact has nothing to do with Goedel's Completeness Theorem. The reason that trivial example is inadequate is that, as you mention, it's not manageable - you can't determine what's an axiom and what isn't.

   Finally, your third paragraph is also wrong. To refute means to prove the negation of. If X cannot be refuted, that means you can't prove not-X. From this it only follows that you can prove X if you have a complete axiomatic system. Since normally, in fact, you don't (by virtue of Goedel's incompleteness theorems), it doesn't follow at all. Now what's true and may be confusing you is that there are certain simple kinds of statements for which this is true, because they're very simple. You can prove that e.g. the Peano Axioms are powerful enough to prove any true statement, or refute any false statement, of a particular simple kind. But not in any statement in general - that'd contradict the Goedel's incompleteness theorems.

   Show morethread
6. ionfishJun 2009
   I rate Enderton's A Mathematical Introduction to Logic.

   http://www.math.ucla.edu/~hbe/amil/index.html

   thread