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