38
$\begingroup$

An apology might be in due for asking another question about prerequisites, but I was confused about the starting points. I have come across various terms such as "Modal Logic", "Temporal logic", "First -order Logic", "Second order Logic" and "Higher order logic".

What exactly does "Logic" mean in this context? How do we rigorously define the word "Logic"?

After going through the beginning pages of few books I can roughly conclude that a "Logic is a way to decide what follows from what and is significant in designing programming languages as it dictates and facilitates designing of programs to automatically reason and understand programs. I want to understand about the second point in a bit elaborated manner.

Now coming to these logics.

Are all these logics, "temporal Logic", "Modal Logic", "First order Logic", "Higher order Logic" independent of each other or we need to understand few of these logic to understand a few others in this group? In a nutshell, what will be the prerequisites for them? (It will be great if I can get suggestions on some materials also.)

P.S : Thanks a ton for your kindness

| cite | improve this question | |
$\endgroup$
  • 18
    $\begingroup$ Ironic that a question like this would be asked by somebody called Kripke. :-) $\endgroup$ – David Richerby Mar 25 '18 at 12:28
  • 2
    $\begingroup$ I must say that your reaction isn't strange. I was pretty surprised myself when I encountered a formal definition of 'an algebra'. $\endgroup$ – Discrete lizard♦ Mar 25 '18 at 14:02
  • 3
    $\begingroup$ @Discretelizard "Algebra" is probably even more surprising, since it has absolutely nothing to do with that thing they call algebra in high school. $\endgroup$ – David Richerby Mar 25 '18 at 15:48
  • $\begingroup$ @DavidRicherby I did too, "linear algebra" is just an algebra. $\endgroup$ – Niklas Mar 25 '18 at 16:00
  • 1
    $\begingroup$ @MartinRosenau Why do you think that would be a barrier to fitting fuzzy logic into a general notion of logic? $\endgroup$ – Derek Elkins left SE Mar 26 '18 at 20:31
39
$\begingroup$

Fundamentally, a logic consists of two things.

  • Syntax is a set of rules that determine what is and is not a formula.
  • Semantics is a set of rules that determine what formulae are "true" and what are "false". To a model theorist, this is expressed by relating formulas to the mathematical structures that they're true in; to a proof theorist, truth corresponds to provability from a chosen set of axioms with a chosen set of proof rules (techniques).

The difference between different logics is, most simply, in the choice of syntax and semantics. Most logics are extensions of propositional logic or first-order logic. In a sense, you can see these extensions as "adding more features" to the logic. For example, temporal logics deal with truths that can vary over time.

In general, these features could be expressed in a simpler logic, at the cost of having to write longer formulas. For example, the temporal concept "$\varphi$ is true from this point for eternity" can be expressed in a first-order way by adding a time parameter to all your propositions and saying "For all times $t$, if $t$ is greater than or equal to the current time, then $\varphi$ is true at time $t$." In a sense, you can think of these logics as adding libraries to a basic programming language so you can say things more easily.

Since pretty much all logics are based on propositional and first-order logic, I'd recommend learning about those first.

| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ As a computer scientist I've also found considering the connection to type theory very useful for learning logic. A type system can be thought of as an alternative presentation of an equivalent logic, via the Howard-Curry correspondence. I recommend Pierce's book to get started. $\endgroup$ – phs Mar 25 '18 at 18:15
  • 1
    $\begingroup$ There's more to syntax in logic than just formulas, and there's more to semantics than the mere determination of truth. $\endgroup$ – Andrej Bauer Mar 25 '18 at 19:30
  • $\begingroup$ A formal perspective that roughly corresponds to the view mentioned in this answer and does try to provide a unifying definition (and was designed to address issues in computer science) is the theory of institutions. $\endgroup$ – Derek Elkins left SE Mar 25 '18 at 20:02
  • $\begingroup$ Not so incidentally, institutions are described in a paper titled What is a Logic? $\endgroup$ – Derek Elkins left SE Mar 25 '18 at 20:16
  • 1
    $\begingroup$ @phs Wow... I don't know how I got this far, but this is the first time I ever considered the idea that Currying a function could be a reference to anything besides the spice. $\endgroup$ – Cort Ammon Mar 26 '18 at 5:13
23
$\begingroup$

While fields such as computer science, mathematics and physics are relatively well-organized, Logic has a chaotic history. Its organization is really confusing so I think it's important to read some history to understand the dense structure of the field.

The path you should choose will depend on your background and aims.

What is a logic ?

  1. The traditional point of view says that a logic is a formal system with a formal language (syntax), a semantic (external meaning, think of interpreters of programs) and a set of rules to deduce statements from other ones (think of the rules of reductions of programs). A logic is purely seen as a mere mathematical object.

  2. The modern point of view, says, through the famous Curry-Howard isomorphism that a logic is a coherent type system (proofs are programs and types are formulas). More precisely : a system of inferences rules enjoying the cut-elimination theorem and the Church-Rosser theorem/confluence theorem implying that the underlying programming system will behave well.

  3. About orders, propositional logic can be seen as a 0-order system (let's say that variables for propositions are noted $p, q$). They behave like function without arguments (constants).

    • When we go to first-order logic, the variables for propositions become variable of predicates $P, Q$ and takes an object as argument $P(x_1, ..., x_n)$, $Q(x_1, ..., x_n)$. They behave like functions taking objects (pairs, integer, string) are arguments. Think of the C language.
    • In the second order logic, variable for predicates becomes kind of functions taking first-order ones. They behave like functions taking first-order functions as argument. For instance we can have predicates and quantification over predicates.
    • Same reasoning for third-order etc. Higher-order logics accept any order. Think of Haskell and OCaml which have functions taking functions of functions of functions etc as argument.

  4. In general, there is no consensus about what a logic trully is. Some philosophers use systems which doesn't have a coherent underlying programming system. Actually, I would say that every field using Logic has it's own conception of logic. And most mathematicians probably don't care about what a logic is.

The structure of the field

The history of Logic is too large so I will just give the structure of the field. The field of formal logic is splitted in : the philosophical, mathematical and computational use. Formal logic begin in the 19-20th century.

  • You should study propositional logic and first-order logic first. They are the most standard ones. They were created to give a formal/mathematical account to the old logic of the time of Ancient Greece.

    • Model theory (semantics), study mathematical structures from the perspective of logic
    • Proof theory (syntax), independently, study proofs as a mathematical object.

  • Second-order logic is an extension of first-order logic which is an extension of propositional logic. It is particularly interesting because arithmetics "live" in the second order (predicates on predicates with induction). Similarly, topology lives in the "third-order" (predicates on sets which can be seen as predicates themselves).

  • Then came L.E.J Brouwer which splitted logic in two :

    • Classical Logic is the usual logic as defined a before. In particular, for all $A$, $A \lor \lnot A$ holds (excluded middle).
    • Intuitionistic Logic is a kind of logic rejecting the excluded middle and all equivalent laws (for technical and philosophical reasons I won't explain here).

  • In other context, philosophers became interested in formal logic and thought it could answer philosophical questions (analystic philosophy). They made their own independent logical systems (paraconsistent logics, relevance logics, and modal logics such as deontic logics, temporal logics, epistemic logics, ...). Modal logics doesn't work with truth but with modalities such as possibility, necessity, time, knowledge. They are all independent of the above logics.

  • The Curry-Howard correspondence gives a formal correspondence (isomorphism) between proofs and programs. Now a lot of logics could be seen as programming systems and vice-versa. Intuitionistic logic which was a bit ignored is now seen as a functional programming system ($\lambda$-calculus). It leads to the study of Type Theory. It is a currently active topic of research.

  • Computer scientists wanted to verify and prove the soudness of systems in a formal way and it seems that modal logics are relevant. Today they use temporal logics and modal logics to reason on systems (see : formal methods, model checking). Systems are modelled through Automata Theory (for instance) and are verified using logical tools. It led to Linear Temporal Logic (LTL) and Computational Tree Logic (CTL).

  • In the same motivation, computer scientists wanted to verify the soundness and prove properties about programs. So we invented the Hoare Logic for imperative programs and more generally, Separation Logics.

  • By studying, the Curry-Howard isomorphism, a new logic emerged : Linear Logic which restricts structural rules (weakening and contraction) seen as the erasure and duplication operating in proofs and programs. The potential infinity of truth are explicited. It seems that this logic is a generalization of classical and intuitionistic logic and gives a whole new conception of Logic based on computation and a procedural paradigm. It is mostly studied by computer scientists.

  • Linear Logic also comes from what we call Substructural logics rejecting structural rules of Logic. Relevant Logic and Affine Logic are examples for such systems.

Summary and path selection

  • Any logic can be : propositional logic, first-order, second-order, third-order, ..., higher order (each extending the preceding one).

  • We can add or remove rules to make variants of existing systems :

    • Remove excluded-middle : intuitionistic logic
    • Add modalities : modal logics
    • Restrict contradiction and weakening : linear logic
    • Remove contraction : affine logic
    • Remove weakening : relevant logic
    • Handle negation differently : paraconsistent logic

  • Learn propositional and first order logic first and :

    • model theory, second order, higher order if you're interested in mathematics
    • proof theory, intuitionistic logic, second order, linear logic if you're interested in the foundation of computer science
    • modal logics, hoare logics, separation logics if you're interested in the verfication of systems and programs
    • modal logics, non-classical logics in general if you're interested in philosophy

References (Books)

I personally recommend to mix references, if possible.

  • Mathematical Logic (Chiswell & Hodges) : very concise and simple book to start with.
  • A first course in Logic (Hedman) : a bit like the above one but give more details and take computability into account.
  • Handbook of Practical Logic and Automated Reasoning (Harrison) : If you want to understand how some logic-related concepts are implemented in practice. More oriented to automated reasoning.
  • Logic in Computer Science (Huth & Ryan) : very clear and oriented to computer scientists (verification of programs and systems, Hoare logic, practical use of modal logic, temporal logics, model checking).
  • Introduction to Proof Theory (Buss) : an introduction to proof theory. It should be better to read this after some general logic.

References (Wikipedia)

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Well, this is very ... comprehensive, I'd say. Thanks for taking the time to write this! $\endgroup$ – Discrete lizard♦ Mar 25 '18 at 15:51
  • 5
    $\begingroup$ This looks very comprehensive but I really wouldn't bring in Curry-Howard as the second thing you say about logic to somebody who's just learning what it is. Unless you're actually studying type theory, Curry-Howard isn't "the modern definition of logic"; it's just something that some people do with logic. $\endgroup$ – David Richerby Mar 25 '18 at 16:06
  • 2
    $\begingroup$ @DavidRicherby Ok. I understand but I think Curry-Howard is important enough for computer scientists (also because we are in cs.stackexchange). It is not really a modern definition of logic but I think it is for some computer scientists. What a logic really is may be subjective anyway. I know it is not always a good idea to expose the original poster to so many things but I don't really expect a full understanding, rather a comprehensive panorama of the branches of Logic (a bit biased by CS) which can act as a reference to be aware of what kind of logic exists and where it is used. $\endgroup$ – Boris Mar 25 '18 at 16:51
  • $\begingroup$ I was under the impression that higher order logic in Haskell would be type operators, rather than functions that could take functions as input. $\endgroup$ – martin Mar 26 '18 at 9:31
  • $\begingroup$ @martin Hm... It was just a simple analogy to grasp the idea of the mechanism but it should not be taken too seriously. I wanted to describe the idea of "higher order" rather than precisely "higher order logic" (taking the original poster's background into consideration). $\endgroup$ – Boris Mar 26 '18 at 17:02
0
$\begingroup$

All of these logics are coming underneath of Mathematical Logic.

Mathematical logic is often divided into the fields of set theory, model theory, recursion theory, and proof theory. These areas share basic results on logic, particularly first-order logic, and definability. In computer science (particularly in the ACM Classification) mathematical logic encompasses additional topics not detailed in this article; see Logic in computer science for those.

Moreover, if you want to know about the logic in general terms this article could be useful.

Logic, originally meaning "the word" or "what is spoken", but coming to mean "thought" or "reason", is a subject concerned with the most general laws of truth, and is now generally held to consist of the systematic study of the form of valid inference. A valid inference is one where there is a specific relation of logical support between the assumptions of the inference and its conclusion.

| cite | improve this answer | |
$\endgroup$
  • 4
    $\begingroup$ Hmm, I'm not sure if this is very helpful here. Would you say that David's post makes yours 'superseded'? If not, why? Try to expand on that. $\endgroup$ – Discrete lizard♦ Mar 25 '18 at 14:03
  • $\begingroup$ @OmG : Can you recommend a list of materials to learn from ? $\endgroup$ – Sheldon Kripke Mar 31 '18 at 3:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.