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.

- Specification languages: descriptions of what
should be true about a program's behavior
- Abstractions of program properties: types as in
ML and lambda Prolog
- Programming languages: such as logic programming
languages such as lambda Prolog.

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

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

- Logical categories
- constants:
*top*(true),*bot*(false) - connectives:
*and*(and, conjunction),*or*(or, disjunction),*=>*(implication),*neg*(negation) - quantifiers:
*forall*(universal quantifier, for all),*exists*(existential quantifier, there exists)

- constants:
- Non-logical categories
- individual constants:
*a, b, c, ...* - function constants:
*f, g, h, ...*(of fixed arity) - predicate constants:
*p, q, r, ...*(of fixed arity) - built-in constants: integers, reals, strings,
*etc*.

- individual constants:

*pand q => r*,
*forall yforall x(p x and q x y => exists z
(q z a))*,
*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.

Consider the truth of the following two statements.

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.

Consider the following two sentences.

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* 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.

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

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.

Lecture Directory / Module Directory / CSE360 Syllabus