Difference between revisions of "Logic and Computation"

Revision as of 16:28, 28 September 2009

Introduction

This page is to setup to summarize fundamentals of common logics. <math>\Rightarrow</math>

Every logic consists of its syntax, semantic and proof theories.

Boolean Logic

It is also known as propositional logic, where a countably infinite alphabet of boolean variables can take two values either true or false.

Syntax

• Constants: true and false;
• Propositional letters;
• Connectives;
• Brackets.

A well-formed formula (wff) is defined inductively as follows:

• prime propositions including proposition letters, constants;
• any compound propositions for formulas p and q: ~p, p/\q, p\/q, p=>q, p<=>q.

Normally we assume the precedence of operators as brackets, ~, /\, \/, =>, <=>. The right associativity is assumed too, e.g., p=>(q=>r).

Formalization

Natural language is ambiguous, and it remains to discuss how to formalize our language into logic formulas. We simply look at some of the examples. Note that sometimes we are unable to rigorously capture the meaning in natural languages.

• unless: it is usually disjunction \/, e.g., I die unless I breathe. It means in order to guarantee that "I die", I must not breathe. Hence, it is: "die \/ breathe", which is logically equivalent to "~breathe => die".
• implications: it is debatable whether implications like p=>q correspond to "if p then q", as it is better known as an variant to "~p \/ q". Let's take it as "if p then q", or "p only q", or "q when p", or more precisely, p is sufficient for q while q is necessary for p. Note that "q if p" (if p then q) is "p=>q", and "p only if q" is "p=>q".

Semantics

Semantics provides a way for all proof procedures to respect in a logic. It is an interpretation that maps elements in the domain (formulas) to those in the range. In boolean logic, the range contains only true and false. A boolean valuation that assigns formulas to some truth value is a model. The semantics is described using valuations.

Metalanguage or meta-logical is what we will introduce here. The languages we are studying is the logic itself, but the languages (usually informal) that we use to study those languages are called metalanguages. For instance, the following definitions are typical metalanguage elements.

• |- is read "proves", i.e., this introduces a proof for some argument. p1, p2,...pn |- q is meant to say there is a procedure to determine if q is true when we know p1...pn are all true. Proof procedures are purely syntactic, i.e., they are algorithms performing mechanical manipulations on strings of symbols: they don't use the meaning of sentences.
• |= is read "logic implication" or "semantic implication" or "entails", i.e., |-p means formula p is always true. Hence "p1,...,pn |- q" reads "from the premises p1 ... pn we can conclude q".
• satisfiability: a formula ψ is satisfiable if there is at least one valuation that makes ψ true. Obviously, every atomic proposition is satisfiable.
• tautology: a formula ψ is valid (a tautology) if all the valuations make ψ true. Obviously, no atomic proposition can be a tautology. A tautology can be written as |- ψ (shorthand for "true |- ψ"). Logic implications are defined as follows: p |- q iff for all valuations if p is true then q is true. Note that "p |- q" is equivalent to "|- p=>q": logical implication means that the implication "p => q" is a tautology.
• contradiction: a formula ψ is a contradiction if every valuation makes it false.
• consistent: a set of formulas is consistent if there is a model in which all formulas can be true simultaneously.
• Relations: ψ is not satisfiable == ψ is contradiction == ~ψ is a tautology; ψ is a tautology == ~ψ is not satisfiable.

A note about equivalence: <=> is syntactic (the same truth value), i.e., it is material equivalence. We define two formulas p, q to be logical equivalent iff they have the same truth values in all possible valuations, denoted as p <-> q. That is, "p <-> q" means "|- p <=> q". Formulas can be syntactically different but semantically the same (logical equivalence), e.g., p /\ q is logically equivalent to q /\ p.

Proof Theories

We refer to a set of formulas as an argument, consisting of conclusions and premises. If the conclusions can be justified by premises, the argument is deductive. Inductive arguments conclude more general new knowledge from a small number of facts.

• A proof procedure is sound if p1,...,pn |= q then p1,...,pn |- q. A proof procedure is complete if p1,...,pn |- q then p1,...,pn |= q. In other words, if every proof only proves valid argument, then the proof procedure is sound. If every valid statement can be proved, then the proof procedure is complete.

Natural Deduction

ND is a form of forward proof developed by Gerhard Gentzen, showing the validity of an argument.

Tableaux

Invented by E.W. Beth and Hintikka, a tableaux algorithm uses rules to expand formulas and add new formulas to the branches. Easy to show if a formula is satisfiable; refutation-based; backward.

Transformational Proof

FOL

FOL is predicate logic, invented by Frege.

Syntax

It consists of

• constants, which denote particular objects, e.g., Jiewen_Wu;
• variables;
• function symbols with arity of n (n>0);
• predicate symbols with arity of n (n>0), in fact an unary predicate is an attribute.
• connectives like /\, \/, =>, <=>, ~;
• quantifiers like ∀, ∃;
• punctuation and brackets;

A term is either a constant, variable or a function applied to terms "f(t1, ..., tn)". A wff is defined inductively as follows:

• atomic formulas: predicate P(t1,..., tn) where all t's are terms;
• formulas A and B compounded by ~A, A/\B, A\/B, A=>B and A <=>B;
• ∀x.A or ∃x.A where A is a formula.

A variable is bound if it is within the scope of a quantifier over that variable. A free variable does not fall within the scope of a quantifier over it. A wff is closed is it has no free variables.

Semantics

A domain of discourse has all the objects needed for interpretation. An interpretation maps each constant and variable to some element in the domain, maps a function that takes arguments of the domain and returns values of the domain; maps a predicate to true or false. For ∀ (∃) the formulas must be true for all (some) substitutions of an element in the domain for the quantified variable.

• satisfiability: there is at least one interpretation that satisfy the formula;
• tautology: every interpretation satisfies the formula;
• contradiction: every interpretation does not satisfy the formula, denoted as |- A for the formula A. For an argument p1, ..., pn |- A, it is valid if whenever the premises p1, .., pn are true the conclusion A is true.

Proof Theories

It sounds reasonable to check validity by trying all possible interpretations (similar to truth tables in boolean logic), but when the domain is infinite, this is infeasible. Natural deduction can be used again. So is tableaux.

References