Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:proofs_and_induction [2008/02/21 11:21] vkuncak |
sav08:proofs_and_induction [2008/02/21 17:50] vkuncak |
||
---|---|---|---|
Line 77: | Line 77: | ||
Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | Instead of proving a goal, you can assume its negation and prove any remaining goals (this generalizes proof by contradiction). | ||
\[ | \[ | ||
- | \frac{\lnot P \vdash\} | + | \frac{\lnot P \vdash} |
{\vdash P} | {\vdash P} | ||
\] | \] | ||
Line 93: | Line 93: | ||
If you have a universally quantified assumption, you can instantiate universal quantifier with any value, denoted by term //t// (this is what "for all" means). You keep the original quantified assumption in case you need to instantiate it multiple times. | If you have a universally quantified assumption, you can instantiate universal quantifier with any value, denoted by term //t// (this is what "for all" means). You keep the original quantified assumption in case you need to instantiate it multiple times. | ||
\[ | \[ | ||
- | \frac{P(t), \forall x.P(x)} | + | \frac{P(t), \forall x.P(x) \vdash} |
{\forall x.P(x) \vdash} | {\forall x.P(x) \vdash} | ||
\] | \] | ||
Line 109: | Line 109: | ||
When you have an existentially quantified assumption, you can pick a witness for existential statement and denote it by fresh variable "x_0". Informally we would say "let $x_0$ be such $x$". | When you have an existentially quantified assumption, you can pick a witness for existential statement and denote it by fresh variable "x_0". Informally we would say "let $x_0$ be such $x$". | ||
\[ | \[ | ||
- | \frac{P(x_0)} | + | \frac{P(x_0) \vdash} |
{\exists x. P(x) \vdash} | {\exists x. P(x) \vdash} | ||
\] | \] | ||
Line 137: | Line 137: | ||
More information: [[http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf|Isabelle tutorial]], Chapter 5 "The Rules of the Game". | More information: [[http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf|Isabelle tutorial]], Chapter 5 "The Rules of the Game". | ||
- | Demo: Proving above example in Isabelle. | + | Demo: Proving above example in Isabelle. A working Isabelle script: |
+ | <code> | ||
+ | theory ForallExists imports Main | ||
+ | begin | ||
+ | |||
+ | lemma fe1: "(EX x. ALL y. F x y) --> (ALL u. EX v. F v u)" | ||
+ | apply (rule "impI") | ||
+ | apply (rule "allI") | ||
+ | apply (erule "exE") | ||
+ | apply (erule "allE") | ||
+ | apply (rule "exI") | ||
+ | apply assumption | ||
+ | done | ||
+ | |||
+ | lemma fe2: "(EX x. ALL y. F x y) --> (ALL u. EX v. F v u)" | ||
+ | apply auto | ||
+ | done | ||
+ | |||
+ | end | ||
+ | </code> | ||
===== Completeness for First-Order Logic ===== | ===== Completeness for First-Order Logic ===== | ||
Line 163: | Line 182: | ||
{\forall n \in \mathbb{N}. P(n)} | {\forall n \in \mathbb{N}. P(n)} | ||
\] | \] | ||
- | |||
==== Structural Induction ===== | ==== Structural Induction ===== | ||
+ | |||
+ | Stepwise induction allows us to prove properties of natural numbers by proving that it holds for 0 and that it extends with each successor. Structural induction similarly allows us to prove that if property holds for basic structures and that if it holds for smaller structures then it also holds for larger structures. Examples of such structures are terms or expression trees. | ||
+ | |||
+ | Consider a language $L$ of function symbols. Let $ar(f)$ denote the number of arguments (arity) of a function symbol $f \in L$. Let ${\it Terms}(L)$ denote the set of all terms in this language. To prove a property for all terms, we show that if the property holds for subterms, then it holds for the term built from these subterms. | ||
+ | \[ | ||
+ | \frac{\bigwedge_{f \in L} \forall t_1,\ldots,t_{ar(f)}.\ (\bigwedge_{i=1}^{ar(f)} P(t_i)) \rightarrow P(f(t_1,\ldots,t_n))} | ||
+ | {\forall t \in {\it Terms}(L). P(t)} | ||
+ | \] | ||
+ | Note that if $c$ is a constant we assume $ar(c)=0$. Therefore, structural induction requires us to prove $P(c)$ for all constants $c \in L$. | ||
+ | |||
* [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now) | * [[Calculus of Computation Textbook]], Chapter 4 (some example refer to previous chapters, if you do not understand them, ignore them for now) |