Logic is the study of reasoning, primarily, of inference. It also covers entailment, causality, consequence, induction, deduction, truth, falsity, belief, fallacies, paradoxes, probabilities, analysis, tense, modality, necessity, sufficiency, possibility, justification, tolerance, obligation, permission, relevance, assertion, validity, contradiction, provability, and argumentation.
A logistic system is a formal system (syntax and semantics) together with a set of inference rules.
The syntax defines the legal strings of the system, which are called its formulas.
Var ::= 'p' | 'q' | 'r' | ...
Formula ::= 'T' | 'F' | Var
| '~' Forumula
| Formula '∧' Formula
| Formula '∨' Formula
| Formula '⇒' Formula
| Formula '≡' Formula
| '(' Formula ')'
which means that
p
~(p ∧ q) ∨ ~~p
are formulas, but
~≡pp∧))∧~q∨(F
is not.
The semantics is given by a semantic valuation function which maps each formula to a "truth value." The mapping is necessarily relative to some interpretation φ which gives meanings to the symbols in the system.
type Interpretation = Prop → {true, false}
E : Formula → Interpretation → {true, false}
E(T)φ = true
E(F)φ = false
E(p)φ = φ(p)
E(~A)φ = true, if E(A)φ = false; and false otherwise
E(A ∧ B)φ = true, if both E(A)φ = true and E(B)φ = true; and false otherwise
E(A ∨ B)φ = true, if at least one of E(A)φ = true and E(B)φ = true; and false otherwise
E(A ⇒ B)φ = false, if E(A)φ = true and E(B)φ = false; and true otherwise
E(A ≡ B)φ = true, if E(A)φ = E(B)φ; and false otherwise
In some logistic systems, the semantic truth functions may be too expensive or impossible to compute. So inference rules are defined to algorithmically derive formulas out of existing formulas, hopefully in such a way as to mimic a reasoning process. Define
{A1, ..., An} ⊢ B
to mean B is derivable from A1, ..., An. The inference rules of a logistic system define the smallest set of these terms.
If ∅ ⊢ A, we say A is a theorem and write ⊢ A. The sequence of inferences producing a theorem is a proof of that theorem.
------ Truth
Γ ⊢ T
------------ Assumption
Γ ∪ {A} ⊢ A
Γ ∪ {A} ⊢ B
------------ Deduction (Implication Introduction)
Γ ⊢ A ⇒ B
Γ1 ⊢ A ⇒ B Γ2 ⊢ A
---------------------- Modus Ponens (Implication Elimination)
Γ1 ∪ Γ2 ⊢ B
Γ ⊢ A ⇒ F
---------- Negation Introduction
Γ ⊢ ~A
Γ ⊢ ~~A
-------- Negation Elimination
Γ ⊢ A
Γ ⊢ A
-------------------------- Disjunction Introduction
Γ ⊢ A ∨ B Γ ⊢ B ∨ A
Γ1 ⊢ A ∨ B Γ2 ⊢ ~A
---------------------- Disjunction Elimination
Γ1 ∪ Γ2 ⊢ B
Γ1 ⊢ A Γ2 ⊢ B
------------------- Conjunction Introduction
Γ1 ∪ Γ2 ⊢ A ∧ B
Γ ⊢ A ∧ B
----------------- Conjunction Elimination
Γ ⊢ A Γ ⊢ B
Γ1 ⊢ A ⇒ B Γ2 ⊢ B ⇒ A
-------------------------- Equivalence Introduction
Γ1 ∪ Γ2 ⊢ A ≡ B
Γ ⊢ A ≡ B
------------------------ Equivalence Elimination
Γ ⊢ A ⇒ B Γ ⊢ B ⇒ A
The derivation of theorems is a purely mechanical process.
Notice that we (so far) completely ignored what a "truth value" is? In some systems of logic, called bivalent logics, there are only two, usually called true and false. In some there is a third: Unknown. In some truth is a degree of belief (a value ∈ 0.0..1.0). In some it is an interval. And so on. In fact, truth values needn't imply truth or falsity, they could refer to other concepts, like justified and not justified.
There are many systems of logic.
The most widely used. It is characterized by five properties (so say one of the authors of the Wikipedia article on the subject):
In intuitionistic logic we are not concerned with the "truth" of a statement as much as we are about its "justification." Every theorem is something justifiable, constructively. So A means "A is provable" and ~A means "A is refutable" (i.e. it is provable that no proof of A exists — in other words, assuming A leads to the the constant False). Therefore
Classical logic has the principle of explosion: "false implies everything", or "from a contradiction, everything follows." The rationale is: if things are only true or false, and you assume false is true, then everything is true because true is already true and now you say that false is true also.
A proof of (A ∧ ~A) ⇒ B:
A (assume)
~A (assume)
A ∨ B (disj intro (1))
B (disj elim (2,3))
This means the following statements are true in classical logic:
Relevance logic rejects explosion, and requires the antecedent and consequent to be related to each other. There must be some real causality. We say in classical logic, implication is material but in relevance logic it is strict. There are many different ways to encode relevance.
A non-monotonic logic rejects the monotonicity of entailment. If a logic is monotonic, then adding new information can change the set of known facts, causing previously known truths to become falsehoods. These kind of logics are good for cases where you have to retract previous knowledge when new facts are known, as in
A paraconsistent logic is one that allows contradictions, by throwing out the principle of explosion. This means throwing out disjunctive introduction, disjunctive elimination or the transitivity of entailment. At least you can reason about contradictions without throwing out the whole system.
These logics are alternatives to belief revision in non-monotonic logics.
Modal Logics deal with modalities. The basic modalities are necessity and possibility. Modal logics can be based on classical or non-classical logics. The interesting thing is that many other logics are also concerned with modalities, e.g. temporal, dynamic, deontic, epistemic, and provability logics.
A fuzzy logic is one in which facts have a degree of truth between 0 and 1. DO NOT CONFUSE FUZZY LOGIC WITH PROBABILITY THEORY.