PineWikiMathematical logic is the discipline that mathematicians invented in the late nineteenth and early twentieth centuries so they could stop talking nonsense. It's the most powerful tool we have for reasoning about things that we can't really comprehend, which makes it a perfect tool for ComputerScience.
1. The basic picture
Reality: Abstract model: herds of sheep piles of rocks ==> natural numbers: 0,1,2,... collections of fingers
We want to model something we see in reality with something we can fit in our heads. Ideally we drop most of the features of the real thing that we don't care about and keep the parts that we do care about. But there is a second problem: if our model is very big (and the natural numbers are very very big), how do we know what we can say about them?
2. Axioms and inference rules
One approach is to true to come up with a list of axioms that are true statements about the model and a list of inference rules that let us derive new true statements from the axioms. The axioms and inference rules together generate a theory that consists of all statements that can be constructed from the axioms by applying the inference rules. The rules of the game are that we can't claim that some statement is true unless it's a theorem: something we can derive as part of the theory.
Simple example: All fish are green (axiom). George Washington is a fish (axiom). From "all X are Y" and "Z is X", we can derive "Z is Y" (inference rule). Thus George Washington is green (theorem). Since we can't do anything else with our two axioms and one inference rule, these three statements together form our entire theory about George Washington, fish, greenness, etc.
3. Soundness, completeness, and consistency
A theory is sound if any statement in it is true for the model we are considering. It's complete if it proves either P or not-P for any statement P we can make. Most theories that are at all useful are not complete (see Gödel's_incompleteness_theorems).
A theory is consistent if it can't prove both P and not-P for any P. Consistency is incredibly important, since all the logics people actually use can prove anything starting from P and not-P.
4. What can go wrong
If we throw in too many axioms, you can get an inconsistency: "All fish are green; all sharks are not green; all sharks are fish; George Washington is a shark" gets us into trouble pretty fast.
If we don't throw in enough axioms, we underconstrain the model. For example, the PeanoAxioms say (among other things) that there is a number 0 and that any number x has a successor S(x) (think of S(x) as x+1). If we stop there, we might have a model that contains only 0, with S(0)=0. If we add in 0≠S(x) for any x, then we can get stuck at S(0)=1=S(1). If we add yet another axiom that says S(x)=S(y) if and only if x=y, then we get all the ordinary natural numbers 0, S(0)=1, S(1)=2, etc., but we could also get some extras: say 0', S(0') = 1', S(1') = 0'. Characterizing the "correct" natural numbers historically took a lot of work to get right, even though we all know what we mean when we talk about them. The situation is of course worse when we are dealing with objects that we don't really understand; here the most we can hope for is to try out some axioms and see if anything strange happens.
Better yet is to use some canned axioms somebody else has already debugged for us. In this respect the core of mathematics acts like a system library—it's a collection of useful structures and objects that are known to work, and (if we are lucky) may even do exactly what we expect.
5. The language of logic
The basis of mathematical logic is PropositionalLogic, which was essentially invented by Aristotle. Here the model is a collection of statements that are either true or false. There is no ability to refer to actual things; though we might include the statement "George Washington is a fish", from the point of view of propositional logic that is an indivisible atomic chunk of truth or falsehood that says nothing in particular about George Washington or fish. If we treat it as an axiom we can prove the truth of more complicated statements like "George Washington is a fish or 2+2=5" (true since the first part is true), but we can't really deduce much else. Still, this is a starting point.
If we want to talk about things and their properties, we must upgrade to PredicateLogic. Predicate logic adds both constants (stand-ins for objects in the model like "George Washington") and predicates (stand-ins for properties like "is a fish"). It also lets use quantify over variables and make universal statements like "For all x, if x is a fish then x is green." As a bonus, we usually get functions ("f(x) = the father of George Washington") and equality ("George Washington = 12" implies "George Washington + 5 = 17"). This is enough machinery to define and do pretty much all of modern mathematics.
6. Standard axiom systems and models
Rather than define our own axiom systems and models from scratch, it helps to use ones that have already proven to be (a) consistent and (b) useful. Almost all mathematics fits in one of the following models:
The natural numbers ℕ. These are defined using the PeanoAxioms, and if all you want to do is count, add, and multiply, you don't need much else. (If you want to subtract, things get messy.)
- The integers ℤ. Like the naturals, only now we can subtract. Division is still a problem.
- The rational numbers ℚ. Now we can divide. But what about √2?
- The real numbers ℝ. Now we have √2. But what about √(-1)?
- The complex numbers ℂ. Now we are pretty much done. But what if we want to talk about more than one complex number at a time?
The universe of sets. These are defined using the axioms of SetTheory, and produce a rich collection of sets that include, among other things, structures equivalent to the natural numbers, the real numbers, collections of same, sets so big that we can't even begin to imagine what they look like, and even bigger sets so big that we can't use the axioms to prove whether they exist or not. Fortunately, in ComputerScience we can mostly stop with finite sets, which makes life less confusing.
Various alternatives to set theory, like lambda_calculus, category_theory or second-order_arithmetic. We won't talk about these much, since they generally don't let you do anything you can't do already with sets.
In practice, the usual way to do things is to start with sets and then define everything else in terms of sets: e.g., 0 is the empty set, 1 is a particular set with 1 element, 2 a set with 2 elements, etc., and from here we work our way up to the fancier numbers. The idea is that if we trust our axioms for sets to be consistent, then the things we construct on top of them should also be consistent (although if we are not careful in our definitions they may not be exactly the things we think they are).