Difference between revisions of "Logic and Computation"
From Wiki Notes @ WuJiewen.com, by Jiewen Wu
m (→Semantics) |
|||
| (31 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
== Introduction == | == Introduction == | ||
| − | This page is | + | This page is to summarize fundamentals of basic logics. |
| − | |||
| − | Every logic consists of its syntax, | + | Every logic consists of its syntax, semantics and proof theories. |
| − | == | + | == Propositional Logic == |
| − | + | A countably infinite alphabet of boolean variables can take two values either true or false. | |
===Syntax=== | ===Syntax=== | ||
*Constants: true and false; | *Constants: true and false; | ||
| Line 15: | Line 14: | ||
A well-formed formula (wff) is defined inductively as follows: | A well-formed formula (wff) is defined inductively as follows: | ||
* prime propositions including proposition letters, constants; | * prime propositions including proposition letters, constants; | ||
| − | * any compound propositions for formulas p and q: | + | * any compound propositions for formulas p and q: <math>\neg p, p\land q, p\lor q, p \to q, p \leftrightarrow q</math>. |
| − | Normally we assume the precedence of operators as | + | Normally we assume the precedence of operators as <math>(), \neg, \land, \lor, \to, \leftrightarrow</math>. The right associativity is assumed too, e.g., <math>p\to (q\to r)</math>. |
====Formalization==== | ====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. | 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 " | + | * unless: it is usually disjunction <math>\lor</math>, e.g., I die unless I breathe. It means in order to guarantee that "I die", I must not breathe. Hence, it is: "die <math>\lor</math> breathe", which is logically equivalent to "<math>\neg</math>breathe <math>\to</math> die". |
| − | * implications: it is debatable whether implications like p | + | * implications: it is debatable whether implications like p<math>\to</math>q correspond to "if p then q", as it is better known as an variant to "<math>\neg</math>p <math>\lor</math> 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 "<math>p\to q</math>", and "p only if q" is "p<math>\to</math>q".''' |
===Semantics=== | ===Semantics=== | ||
| Line 28: | Line 27: | ||
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. | 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. | ||
| − | * | + | * <math>\vdash</math> is read "proves", i.e., this introduces a proof for some argument. p1, p2,...pn <math>\vdash</math> 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. |
| − | * | + | * <math>\vDash</math> is read "logic consequence" or "logical/semantic implication" or "entails", i.e., <math>\vDash</math>p means formula p is always true. Hence "p1,...,pn <math>\vDash</math> q" reads "from the premises p1,...,pn we can conclude q". |
| − | * satisfiability: a formula | + | * satisfiability: a formula <math>\psi</math> is satisfiable if there is at least one valuation that makes ψ true. Obviously, every atomic proposition is satisfiable. |
| − | * tautology: a formula | + | * tautology: a formula <math>\psi</math> is valid (a tautology) if all the valuations make <math>\psi</math> true. Obviously, no atomic proposition can be a tautology. A tautology can be written as <math>\vDash\psi</math> (shorthand for "true <math>\vDash\psi</math>"). Logic implications are defined as follows: p <math>\vDash</math> q iff for all valuations if p is true then q is true. Note that "p <math>\vDash</math> q" is equivalent to "<math>\vDash p\to q</math>": logical implication means that the implication "<math>p\to q</math>" is a tautology. |
| − | * contradiction: a formula | + | * contradiction: a formula <math>\psi</math> 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. | * consistent: a set of formulas is consistent if there is a model in which all formulas can be true simultaneously. | ||
| − | * Relations: | + | * Relations: <math>\psi</math> is not satisfiable; to wit, <math>\psi</math> is a contradiction; to wit, <math>\neg\psi</math> is a tautology. Then, if <math>\psi</math> is a tautology; to wit, <math>\neg\psi</math> is not satisfiable. |
| − | A note about equivalence: < | + | Some sample questions were posed to students in CS245 to clarify the relationship between satisfiable and valid. The image was scanned from my handwritten slide. |
| + | <!--[[Image:questionSV.jpg|500px]]--> | ||
| + | |||
| + | A note about equivalence: <math>\leftrightarrow</math> is syntactic (the same truth value), i.e., it is a 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 <math>\Leftrightarrow</math> q. That is, "p <math>\Leftrightarrow</math> q" means "<math>\vDash p\leftrightarrow q</math>". Formulas can be syntactically different but semantically the same (logical equivalence), e.g., <math>p\land q</math> is logically equivalent to <math>q\land p</math>. | ||
===Proof Theories=== | ===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. | 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 | + | * A proof procedure is '''sound''' if p1,...,pn <math>\vdash</math> q then p1,...,pn <math>\vDash</math> q. A proof procedure is '''complete''' if p1,...,pn <math>\vDash</math> q then p1,...,pn <math>\vdash</math> 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==== | + | The following proof theories are both sound and complete. |
| + | |||
| + | ====[[Hilbert System]]==== | ||
| + | |||
| + | ====[[Natural Deduction]]==== | ||
ND is a form of forward proof developed by Gerhard Gentzen, showing the validity of an argument. | ND is a form of forward proof developed by Gerhard Gentzen, showing the validity of an argument. | ||
| − | ====Tableaux ==== | + | |
| + | ====[[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. | 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==== | ====Transformational Proof==== | ||
| − | == | + | ===[[Modal Logic]]=== |
| − | |||
| − | |||
| − | == | ||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | + | ==[[Predicate Logic]]== | |
| − | |||
| − | |||
| − | |||
| − | |||
==References== | ==References== | ||
[[Category:Logic and Reasoning]] | [[Category:Logic and Reasoning]] | ||
Latest revision as of 20:40, 13 August 2012
Contents
Introduction
This page is to summarize fundamentals of basic logics.
Every logic consists of its syntax, semantics and proof theories.
Propositional Logic
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: <math>\neg p, p\land q, p\lor q, p \to q, p \leftrightarrow q</math>.
Normally we assume the precedence of operators as <math>(), \neg, \land, \lor, \to, \leftrightarrow</math>. The right associativity is assumed too, e.g., <math>p\to (q\to r)</math>.
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 <math>\lor</math>, e.g., I die unless I breathe. It means in order to guarantee that "I die", I must not breathe. Hence, it is: "die <math>\lor</math> breathe", which is logically equivalent to "<math>\neg</math>breathe <math>\to</math> die".
- implications: it is debatable whether implications like p<math>\to</math>q correspond to "if p then q", as it is better known as an variant to "<math>\neg</math>p <math>\lor</math> 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 "<math>p\to q</math>", and "p only if q" is "p<math>\to</math>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.
- <math>\vdash</math> is read "proves", i.e., this introduces a proof for some argument. p1, p2,...pn <math>\vdash</math> 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.
- <math>\vDash</math> is read "logic consequence" or "logical/semantic implication" or "entails", i.e., <math>\vDash</math>p means formula p is always true. Hence "p1,...,pn <math>\vDash</math> q" reads "from the premises p1,...,pn we can conclude q".
- satisfiability: a formula <math>\psi</math> is satisfiable if there is at least one valuation that makes ψ true. Obviously, every atomic proposition is satisfiable.
- tautology: a formula <math>\psi</math> is valid (a tautology) if all the valuations make <math>\psi</math> true. Obviously, no atomic proposition can be a tautology. A tautology can be written as <math>\vDash\psi</math> (shorthand for "true <math>\vDash\psi</math>"). Logic implications are defined as follows: p <math>\vDash</math> q iff for all valuations if p is true then q is true. Note that "p <math>\vDash</math> q" is equivalent to "<math>\vDash p\to q</math>": logical implication means that the implication "<math>p\to q</math>" is a tautology.
- contradiction: a formula <math>\psi</math> 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: <math>\psi</math> is not satisfiable; to wit, <math>\psi</math> is a contradiction; to wit, <math>\neg\psi</math> is a tautology. Then, if <math>\psi</math> is a tautology; to wit, <math>\neg\psi</math> is not satisfiable.
Some sample questions were posed to students in CS245 to clarify the relationship between satisfiable and valid. The image was scanned from my handwritten slide.
A note about equivalence: <math>\leftrightarrow</math> is syntactic (the same truth value), i.e., it is a 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 <math>\Leftrightarrow</math> q. That is, "p <math>\Leftrightarrow</math> q" means "<math>\vDash p\leftrightarrow q</math>". Formulas can be syntactically different but semantically the same (logical equivalence), e.g., <math>p\land q</math> is logically equivalent to <math>q\land p</math>.
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 <math>\vdash</math> q then p1,...,pn <math>\vDash</math> q. A proof procedure is complete if p1,...,pn <math>\vDash</math> q then p1,...,pn <math>\vdash</math> 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.
The following proof theories are both sound and complete.
Hilbert System
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.
