Links:

First let's cover what's available in formal logic. By 'formal', we mean all of 'rigorous', 'symbolic', and also 'concerned with form, not content'.

By 'logic', we mean the form of correct reasoning with absolute certainty. Philosophically, there is currently some argument whether the 'correctness' of logic stems from a property of reality, from universal properties of the human mind, or from a cultural protocol, but we won't further discuss that here.

Sometimes people talk about multiple 'logics'. Sometimes these 'logics' are meant to be alternative formal models of the universal, correct reasoning process, other times the the term is used to denote systems whose formalism shares a superficial similarity to formalisms of "correct reasoning", but which are not being put forward themselves as such a model. Some philosophers might get annoyed by this use and insist that there may be many formal systems intended to model parts of logical reasoning, but there is only one "logic", meaning there is only one form of correct reasoning with absolute certainty. Perhaps other philosophers might disagree with that.

My phrase "with absolute certainty" needs clarification. There may be "probabalistic logic", which tells you how to correctly reason with probabalities; in such a case, "absolute certainty" refers not the probability attached to each conclusion, but to the correctness of attaching that probability to that conclusion. For example, if i ask you what is the chance that an ideal fair coin lands heads-up, you may answer "50%", and be absolutely certain in this answer.

if you pick up a book on 'formal logic' or 'mathematical logic' expecting it to tell you a system for correct reasoning, you may be surprised. Most of the content under these topics is proving theorems ABOUT formal reasoning systems. For example, one property often desired of a formal reasoning system is consistency; a consistent system is one that will never conclude both "A" and "not A" at the same time, where A is some proposition [for example, "I'm wearing socks" and "I'm not wearing socks"]. A book on mathematical logic might present a proof that some formal logic system is consistent. If you picked up a book on mathematical logic hoping to be told a formal reasoning system and advice on how to use it, you might be surprised to instead find a formal characterization OF a formal reasoning system, and a bunch of theorems about things like consistency.

Other popular properties of a formal logic system are 'soundness' [unless you feed it false assumptions, the system will never conclude anything that is false], and completeness [the system can conclude anything which is true]. Both soundness and completeness are with reference to some formalized model of the sort of things in the world that the formal logic is talking about.

A syllogism is an argument of the form "All men are mortal. Socrates is a man. Therefore, Socrates is mortal."

Predicate logic is one formal logical system. In predicate logic, you have variables which can each take on the boolean values "True" or "False". You then have the unary operator "not", and the binary operators "and" and "or". You put these together to make propositions, for example, "[A and [not B]] or C". If you pick either "true" or "false" for each of the variables [called an "assignment to the variables"], then the "truth value" of the proposition as a whole can be calculated. For example, if A is False and B is False and C is False, then "[A and [not B]] or C" is false.

We see then that each proposition induces a function from assignments of the variables to boolean values.

Starting with "not", "and" and "or" [actually you only need either "nand" (not and) or "nor" (or) and you can define the rest, but that's less intuitive], you can define other commonly used logical connectives, such as "implies" [a implies B is "B or not[A]"], "bidirectionally implies" ["[a and b] or [not[a] and not[b]]"], "nand" ["not[a and b]"], etc.

In addition to variables, we allow boolean constants, so "True" is a valid proposition, as is "A or True". "True" always evaluates to True, "False" always evaluates to False, and when found in a more complex proposition, they are treated as if a variable was there and that variable had been assigned the constant.

Here's our inference rule. If one predicate logic proposition P is known to be true, and if there's aren't any assignment to the variables that make that proposition P true which don't also makes proposition Q true [we can check this by exhaustively enumerating all possible assignments to all the variables found in either P or Q, and then seeing which ones make P true, then seeing if all of these also make Q true], then we can infer [or "deduce"] that proposition Q is true.

Note that some predicates always evaluate to True for all assignments to the variables. For example "A or not[A]" is True no matter if A is True or A is False. Our inference rule always allows us to conclude such propositions, because the proposition "True" is known to be True regardless of the variable assignment, so if any proposition Q is found to also evaluate to True no matter what the variable assignment, then we may always conclude Q. Such propositions Q are called "tautologies".

Note also that the system of predicate logic has the property, sometimes called 'vacous implication' or 'material implication' (although these terms are confusing because they can also refer to the behavior of the 'implies' operator rather than the system itself) that if you mistakenly assumed as true some proposition P which is false on all assignments to the variables, then the inference rule allows you to infer ANY proposition Q. This is because the inference rule to infer Q from P only requires that there aren't any assignments to the variables which make P true without also making Q true. In the case under discussion, this requirement is satisfied because there aren't any assignments to the variables that make P true at all.

From any set of axioms (assumed propositions), we can deduce various other propositions.

Sometimes you see people use a symbol that looks like

- as follows: "a | - b" means "from axiom(s) a, we can deduce b". Both "a" and "b" can either be a single proposition or a whole set of propositions. Often lowercase letters are used for single propositions, and capital letters are used if we mean a set of propositions. You can also read "a | - b" as "b can be derived from a", "b follows from a". If we have multiple things on the left of the | - separated by commas, that means that you might need all of them in order to derive the thing on the right. E.g "a,b | - c" means "if you know that a and b are both true, then you can derive the truth of c". |

We call the set of all propositions that can be deduced from given axioms "the theory (under predicate logic) of those axioms".

The tautologies are the theory resulting from no axioms.

As you probably expect, predicate logic is consistent, sound, and complete. A book on mathematical logic, for example Enderton, will have the proofs.

Now onto our next logic, first-order logic. First order is like predicate logic except that in addition to variables which take boolean values, we have other variables that refer to objects from some other domain. For example if the domain is natural numbers, we might have a variable "x", and an assignment to this variable might be "x = 3". We also have functions and relations over these other objects. Functions are things which take as input one or more domain objects, and return a domain object. For instance, addition takes two numbers and returns a number. Relations are things which take one or more domain objects and return a boolean, for example the "less than or equal" relation returns True if you give it "3" and "4" as inputs. In many treatments we also have the equality relation between domain objects.

We also have two "quantifier" symbol, namely "forall" (spoken "for all") and "exists" (spoken "there exists"). Forall is written like an upside-down A, and "exists" is written like a backwards E. "Forall x" means "the following is true for any choice of x", and "exists x" means "the following is true for at least one choice of x", where x is a domain object variable. For example, if the domain objects are the natural numbers, the following is true: "exists x (forall y (x <= y))". In English that is read, "there exists some natural number x such that, for all natural numbers y, x is less than or equal to y", which can be paraphrased as "there exists some natural number x such that x is less than or equal to every natural number" (this is true because we can take "x = 0", and 0 is less than or equal to every natural number).

Sometimes you'll see a period to the right of a forall or an exists, after the variable it's using; this is just a separator. For example, "exists x . (forall y . (x <= y))".

One fact about "forall" and "exists" is that "forall x . P" is equivalent to "not(exists x . (not P))", and "exists x . P" is equivalent to "not(forall x . (not P))". This makes sense in English; for example, if something is true for every man, then there isn't any man for which it isn't true; and if there is some man that fits some description, then it must not be the case that given any man, that man does not fit that description.

Instead of "propositions" we'll just call the things in first-order logic "formulas".

There are various axioms and inference rules that i won't cover here.

First-order logic is consistent, sound, and complete. A book on mathematical logic, for example Enderton, will have the proofs.

First-order logic alone can't say very much; it can only deduce tautologies (things true for any domain, by virtue of logic alone). In practice we usually use it in conjuction with a set of domain axioms, that is, statements about a particular domain of interest.

One simple domain is Peano arithmetic, which formalizes the concept of the natural numbers, as well as addition, multiplication, and <=. There is a generally accepted proof that Peano arithmetic is consistent, although some people have a problem with it because it uses something called 'transfinite induction', which i won't discuss further.

So, is it complete, that is, are there true statements about the natural numbers that cannot be proved by using first-order logic and Peano arithmetic? No, it is not complete; there are true statements about the natural numbers which cannot be proved with this method.

So we just need more axioms, right? Or maybe we need something stronger than first-order logic?

No, neither suffice. Shockingly, Godel's first incompleteness theorem proves that ANY computable system which is as powerful as first-order logic plus the Peano axioms ("as powerful as" means that the new system allows you to deduce any statement that first-order logic with Peano would allow you to deduce) is either inconsistent or incomplete. (by "computable", i mean that you can write a computer program that executes the deduction process in finite time and memory).

This puts a serious dent in the idea that rigorous thought consists of axioms and proofs from those axioms (not that I have any better alternative to offer). To quote Wikipedia, "There is no algorithmic procedure that can correctly decide whether arbitrary mathematical propositions are true or false".

If you combine that with the hypothesis that, at least at the level required to simulate the operation of the human brain, physics may be algorithmically computable, you would conclude that neither humans nor humans aided by computers can correctly decide whether arbitrary mathematical propositions are true or false.

When one looks at Godel's proof, it's basically a formal variant of the Liar Paradox (if i tell you "I am a liar", is that statement true or is it false?). Godel manages to create a first-order logic formula that means "I cannot be proved by first-order logic with these axioms" (formally proving the existence of such a formula is the hard part). Now, if the theory of the given axioms contains this formula, then the theory is inconsistent (because the formula could be proved, but the truth of the formula implies that it cannot be proved). If the theory of the given axioms do not contain this formula, then the theory is incomplete (because that formula is true but it cannot be proved from those axioms).

One might say, "well that's just a trick, if it's only those sorts of formulas which can't be proved, that's pretty inconsequential". And indeed, first-order logic is very useful for proving all sorts of things from axiom sets that are as powerful or more powerful than Peano, so this criticism may be justified, although it's hard to be sure without a precise characterization of just exactly what can't be proven by this system. You may also say, "if that's the only sort of thing that can't be proved, then we can imagine a logic system with axioms FOLP2 which has axioms or rules of inference that allow one to prove that sort of thing. And then, since Godel's first theorem also applies to FOLP2, we create an FOLP3 that adds in the forbidden yet true formulas identified by Godel's first theorem on FOLP2. And iterate. Wouldn't that solve everything?". I asked my logic teacher something like that once, and he said there were some complications having to do with the difficulty of discovering or specifying transfinite ordinals, and referred me to a paper "Turing in the land of O(z)" which i haven't had a chance to read yet, regarding among other things Turing's thesis, "Systems of Logic Based on Ordinals", which appears to be about exactly this according to http://en.wikipedia.org/wiki/Systems_of_Logic_Based_on_Ordinals : "GĂ¶del showed for that any formal system S powerful enough to represent arithmetic, there is a theorem G which is true but the system is unable to prove. G could be added as an additional axiom to the system in place of a proof. However this would create a new system S' with its own unprovable true theorem G', and so on. Turing's thesis considers iterating the process to infinity, creating a system with an infinite set of axioms."

You may be wondering what the 'first-order' in first-order logic is for. It's because there is another logic called "second-order logic", which is like first-order logic except that you can quantify over (apply 'forall' and 'exists' to variables of type) functions and predicates, not just domain objects. And there are other "higher-order logics" above that.

I think I've heard that various mathematical paradoxes (such as some non-standard models of arithmetic, and Godel's second incompleteness theorem) go away if you accept https://en.wikipedia.org/wiki/Infinitary_logic , that is, logic that permits infinitely long statements and/or infinitely long proofs. See also http://plato.stanford.edu/entries/logic-infinitary/ .

Inference rule specification: when defining a logic, often you'll see a weird notation for inference rule specification:

A B

C

that means, if you have A and B, you may conclude C. This isn't just written "A and B implies C" because "and" and "implies" are operations that appear WITHIN a logical formula, and we are trying to describe an algorithm or procedure for deducing formulas, e.g. by specifying inference rules, we are answering the question: if you currently have such-and-such formulas in your bag of proved formulas, which other new formulas are you justified in adding to that bag? I guess people find it easier to keep these two things separate if you use very different notations.

the implies operator is often written as an arrow, ->. "and" is often written as a caret, ^. "or" is often written as an upside-down caret (which i can't type in ASCII).

Horn clauses: a horn clause is a logical formula of the form "(A and B and ... and D) implies Z"

sequent: a sequent is an extension to the "a

- b" notation given above. In a sequent, you can have multiple things on the left AND on the right, separated by commas: "a, b | - c, d". The meaning of the commas on the right differ from the left; in a sequent, " | -" means If ALL OF the things on the left are true, then you may infer that at least ONE OF the things on the right are true. |

modal logic: this involves the introduction of other symbols called "modal operators". Sometimes these come in pairs that relate to each other similarly to "forall" and "exists". For example, "necessary vs. possible" (note that something whose negation is not possible must be necessary), and "obligatory vs. permissible" (note that if you are not permitted to abtain from some action, then that action is obligatory).

other theories of arithmetic: Peano isn't the only one. See Wikipedia category Formal theories of arithmetic.

Classical logic without the law of the excluded middle, that is, without (P or not(P))

The use is that this eliminates the ability to form a nonconstructive proof.

Various added restrictions to classical logic to prevent "irrelevant" theorems, that is, theorems whose conclusions intuitively seem like they their premises are irrelevant. For example, "If the moon is made of green cheese, then either it is raining in Ecuador now or it is not.".

Many description logics are fragments of first-order logic whose expressiveness is greater than predicate logic. Some have disjoint expressivness than first-order logic, though. Some are much more computationally tractable than predicate logic.

They are designed to be good at expressing taxonomic knowledge, in the sense of computer ontologies.

See http://en.wikipedia.org/wiki/Description_logic , notes-cog-ai-reasoning-descriptionLogics

I don't know much about this and this section may be wrong.

Type theory started out in mathematical logic as a response to Russell's paradox.

Russell's paradox is: "Consider the set of all sets that do not contain themselves. Does this set contain itself?". If it does contain itself, then by it's own definition, it should not contain itself. If it does not contain itself, then by it's own definition, it should contain itself. Therefore such a set ("the set of all sets that do not contain themselves") cannot exist.

In order to avoid this and similar paradoxes, type theory was created, which was a theory that roughly speaking stratifies objects into levels ("types"), and requires that the definition of an object on a given level only refer to lower levels. Then you say that any putative object that doesn't follow the rules is not allowed to be introduced into formal discussion (i.e. such an object is considered to be just a trick of English language that doesn't really exist). For example, the "set of all sets that do not contain themselves" would break the rules and so isn't allowed to be discussed. Now you can avoid the paradox.

There are many different type theories.

The way that type theories tends to work is to present some fundamental types, and also some operations which you are allowed to apply to any type that you already have; these operations produce new types. By this means, starting with the fundamental types and iteratively applying the operations, you can generate lots of types. In addition to the language of types, there is usually an object language by which objects can be constructed, and some correspondence between the two. For any given term in the object language, in order to see if it is admissible as a 'real object', you try to find a corresponding type which can be legally constructed in the type theory. If you can find such a type, then the term is called 'well-typed'. If there is no such type, then the term is called 'ill-typed'. For instance, the term "the set of all sets that do not contain themselves" would be ill-typed in most type theories (however, often there is a term of the form "the ___ of all sets that do not contain themselves"; usually ___ is taken to be 'class', the idea being that you cannot have a SET of all sets that do not contain themselves, because that quantifies over things of the same level as itself, but you can have a collection of all sets that do not contain themselves, provided that this collection is not itself a set).

(many type theories get more detailed than just "levels", e.g. in many programming languages you can give a function a type which indicates that it can only be called on strings, not on booleans.)

We said that type theories typically present some fundamental types, and also some operations which you are allowed to apply to any type that you already have; these operations produce new types.

This is similar to the way that axiomatic systems of logic typically work; you have some fundamental propositions (axioms or assumptions), and also some inference rules that you are allowed to apply to any propositions that you already know to be true, to generate new propositions from the ones you already know to be true.

So say you take a given type theory. Can you make a logic whose inference rules work exactly analogously to the type theory's operations? If you do, will that logic make any sense and do anything interesting?

(i'm not sure that i'm understanding this section correctly, as Curry-Howard is usually described as a correspondence between PROGRAMS and proofs, not type theory and proofs; but the proposition proved by a program is the type of the program, so maybe these are essentially the same as what i say below?)

In fact in many cases the answer is yes, and the logic that you end up with often turns out to be a standard logic that was already known.

So in many cases, for a given type theory, the application of particular type theory operations to types can be formally matched up with particular inference rules in some logic. This means that the resulting types are matched up with proofs.

The Curry-Howard isomorphism proved that such a correspondence exists between the types in simply typed lambda calculus, and intuitionistic logic. Later, other such isomorphisms were shown, matching other type systems with other logics, and the term 'Curry-Howard isomorphism' is often used not just for the particular correspondence between simply typed lambda calculus and intuitionistic logic, but also for the general idea of such correspondences.

I'm not sure about this, but i think that the logic that is matched with a given type system using a Curry-Howard isomorphism does not specify the procedure used for type inference or type checking in a programming language using that type system; proofs in the logic correspond only to the existence of a particular type; further thought may be required to determine which type a term in a programming language has. Furthermore, finding the existence of a type corresponds to proving a particular theorem using that logic; the tactics used in proving that theorem may be more intelligent than using brute force to enumerate all possible proofs. For example, if i write "lambda x: x x", that might be ill-typed in many type systems, but i don't see how that is immediately apparent from the rules of a typical type theory; you have to prove a negative, that is, that there is no sequence of the type operations which arrives at that object term. I'm guessing that the algorithm for finding out that that is ill-typed must be separately discovered even after you know the rules of the logic corresponding to the type theory.

It may be interesting to take as one's foundation for mathematics a logic and also the type theory corresponding to that logic.

To what extent the philosophical import of a given type system corresponds to the philosophical import of its corresponding logic is something that I'm unclear about. To date, i am aware of no such correspondence. However, even without any philosophical meaning, the correspondence is certainly technically useful in that one can translate theorems from metalogic into type theory.

todo inductive types e.g. the type of lists from Vempty and Vcons

Intuitionistic propositional logic ?

Intuitionistic first-order logic ?

(note: "first-order logic" == "predicate logic")

Second-order typed lambda calculus

Like simply typed lambda calculus, but you can quantify over types.

Polymorphic types in programming languages.

Fragment of second-order intuitionistic logic with no existential quantification.

See http://cubeoflambda.wordpress.com/2011/10/01/system-f/

(is this a superset of System F?)

Adds type operators, i.e. functions from types to types

See https://en.wikipedia.org/wiki/System_F#System_F.CF.89

System F plus subtyping.

See https://en.wikipedia.org/wiki/System_F-sub

higher-order predicate logic as a type system

see http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.3947

Intuitionistic logic + System F_w

impredicative

an embedding of higher-order predicate logic; not isomorphic; there are terms in CIC that do not have a meaning in higher-order predicate logic, and there are propositions which are not provable in higher-order predicate logic, but which have corresponding types in CIC. i don't understand this. see http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.3947

Coq: a theorem prover that can represent part of Calculus of Constructions, with some restrictions on inference to make things more tractable?

see also http://mathoverflow.net/questions/69229/proof-strength-of-calculus-of-inductive-constructions

Results about proofs.

random link: http://www.cse.chalmers.se/~coquand/proof.html

A model of a theory is a collection of objects that obeys the theory. Often for a theory there is the informal notion of a 'standard model', that is, the model that everyone at first assumes that the theory is supposed to be about. Often, one might be surprised to discover that a theory that you thought was about its standard model also describeds various non-standard models. For example, the standard model of Peano arithmetic is the natural numbers; but there are also non-standard models which contain additional 'numbers' greater than any natural number (see http://en.wikipedia.org/wiki/Non-standard_model_of_arithmetic ).

Model theory studies the models of theories. Model theory appears to contain more than that these days; see http://en.wikipedia.org/wiki/Model_theory

See http://en.wikipedia.org/wiki/Interpretation_%28model_theory%29

See proj-plbook-plChModelsOfComputation for most of my notes on these.

- https://en.wikipedia.org/wiki/Predicate_functor_logic : Sort of like combinatory calculus in that, the idea is to remove variables from logic, and that, instead of having variables, you have a basis set of operations and you combine them. Except that here the operations are on predicates in first-order logic with identity. "Quine proposed PFL as a way of algebraizing first-order logic in a manner analogous to how Boolean algebra algebraizes propositional logic. He designed PFL to have exactly the expressive power of first-order logic with identity. Hence the metamathematics of PFL are exactly those of first-order logic with no interpreted predicate letters: both logics are sound, complete, and undecidable." [1]. Various basis sets have been proposed; they tend to be a bunch of ways to rearrange the argument list of the predicate (eg delete the first variable, eg rotate the argument list, etc), plus an identity operation that creates a new predicate that (i think; not sure if i'm understanding this part correctly) asks if the value of the old predicate is the same whether some particular argument is set to value1 or value2.

---

3 alternative/historical sets of axioms for propositional logic

---

"For the principia, Russell adapted Frege's rules to the algebraic notation to create the most inefficient proof procedure that has ever been widely taught (but never widely learned). Better proof procedures for the algebraic notation were only invented many years later: natural deduction by Gerhard Gentzen (1935), semantic tableaux by Evert Beth (1955) and resolution by Alan Robinson (1965)." -- "the infinite variety of logics" by sowa

"existential graphs" are an alternative notation for logic by Peirce; his 'beta' graphs are "isomorphic to first-order logic with identity, with all formulas closed;" [2].

---