CSE 360: Lecture 1

Different Domains, Different Logics

There is not just one logic, although, historically, one logic (classical logic) has dominated.

Different subjects have different concerns for which logic has been employed.

  • Mathematics --- foundations, set theory, correct proof methods

  • Philosophy --- wide ranging concerns: logic of common sense, of discourse, of scientific discovery, of mathematics, etc.

  • Computer Science

    1. Specification languages: descriptions of what should be true about a program's behavior

    2. Abstractions of program properties: types as in ML and lambda Prolog

    3. Programming languages: such as logic programming languages such as lambda Prolog.

    Some Particular logics

    We shall focus on these logics in this class (mostly intuitionistic logic).

  • Classical logic: Captures ``truth.'' Used by mathematicians and many others. Truth-tables are part of the analysis of classical logic.

  • Intuitionistic logic: Captures ``provability.'' Makes distinctions between ``necessary'' and ``contingent'' truths.

  • Linear logic (1987): Captures ``computations.'' This logic is resource sensitive.

    In computer science and cognitive science, many other logics are also considered: modal, temporal, relevant, minimal, etc.

    Syntactic issues of logic formulas

    1. Logical categories

      1. constants: top (true), bot (false)

      2. connectives: and (and, conjunction), or (or, disjunction), => (implication), neg (negation)

      3. quantifiers: forall (universal quantifier, for all), exists (existential quantifier, there exists)

    2. Non-logical categories

      1. individual constants: a, b, c, ...

      2. function constants: f, g, h, ... (of fixed arity)

      3. predicate constants: p, q, r, ... (of fixed arity)

      4. built-in constants: integers, reals, strings, etc.

    For example:

    pand q => r, forall yforall x(p x and q x y => exists z (q z a)), forall P (P a => P b)

    Quantification Restriction

  • Propositional logic: No quantification. Also, no non-logical constants except predicate constants of arity 0. pand q => r

  • First-order logic: Quantification over individual constant positions. forall yforall x(p x and q x y => exists z (q z a))

  • Higher-order logic: Quantification over function and/or predicate constant positions as well. forall P (P a => P b)

    We shall eventually present a version of higher-order logic where the distinctions between these syntactic categories is represented by a distinction in type.

    Expressiveness of logic: Necessary and Contingent Truths

    Consider the truth of the following two statements.

  • All US presidents are native born US citizens.

  • All US presidents are at least 40 years old when elected.

    Both statements are true of the 42 current presidents.

    Only the first is necessarily true (if the Constitution is not amended). There could be a president elected in the future that is between the age of 35 and 40 years old.

    Such distinctions are important in data bases.

    Classical logic does not address these issues directly. Intuitionistic logic and some modal logics do address these distinctions.

    Expressiveness of logic: Sensitivity to Resources

    Consider the following two sentences.

  • If I have a dollar then I can buy a coke. [dollar implies coke]

  • If I have a dollar then I can buy a pepsi. [dollar implies pepsi]

    In classical and intuitionistic logics, we would be able to infer [dollar implies (coke and pepsi)], which is, in a certain sense, not a sensible conclusion. More appropriate would be [(dollar and dollar] implies (coke and pepsi)]. Clearly, dollar and dollar and dollar should not be equivalent, although they are if we are only modeling truth.

    Linear logic will provide a setting were this distinct is directly supported.

    Provability and Truth

    Provability always refers to a finite demonstration (proof, argument) that a statement holds. Proofs are syntactic and can be encoded in and checked by machine (in fact, such checks should be ``simple'' polynomial-time computations). The following rewriting can serve as a proof that (p=> q)or p holds (in classical logic).

    (p => q) or p equiv (neg p or q) or p equiv (q or neg p) or p equiv q or (neg p or p) equiv q or top equiv top

    Truth is generally defined by use of mathematical structures, called models, which are often infinite. Computational tractability is not generally a concern.

    p      q    (p => q) or p 
    top   top      top  
    top   bot      top  
    bot   top      top  
    bot   bot      top  

    Checking truth-tables for propositional formulas requires exponential algorithms.

    Soundness and Completeness

    The depth of a logic formalism is often revealed by these two theorems, stated generally as:

  • Soundness: If B is provable then B is true.

  • Completeness: If B is true then B is provable.

    Soundness proofs are generally easier to prove, often by structural induction on proofs.

    Completeness proofs are generally hard to prove and require deep understanding of both models and proofs.

    The issue of soundness and completeness is echoed whenever we build machines/software for performing tasks. Consider a combination lock, for example.

  • Soundness: If I enter 15-6-29 then the lock opens.

  • Completeness: If the lock opens, then I entered 15-9-26.

    Lecture Directory / Module Directory / CSE360 Syllabus