A Short Introduction to Intuitionistic LogicSpringer Science & Business Media, 31.10.2000 - 131 Seiten Intuitionistic logic is presented here as part of familiar classical logic which allows mechanical extraction of programs from proofs. to make the material more accessible, basic techniques are presented first for propositional logic; Part II contains extensions to predicate logic. This material provides an introduction and a safe background for reading research literature in logic and computer science as well as advanced monographs. Readers are assumed to be familiar with basic notions of first order logic. One device for making this book short was inventing new proofs of several theorems. The presentation is based on natural deduction. The topics include programming interpretation of intuitionistic logic by simply typed lambda-calculus (Curry-Howard isomorphism), negative translation of classical into intuitionistic logic, normalization of natural deductions, applications to category theory, Kripke models, algebraic and topological semantics, proof-search methods, interpolation theorem. The text developed from materal for several courses taught at Stanford University in 1992-1999. |
Inhalt
Intuitionistic Propositional Logic | 5 |
Coherence Theorem | 6 |
Glivenkos Theorem | 23 |
Computations with Deductions | 31 |
ProofSearch | 75 |
System | 83 |
Natural Deduction System | 95 |
Kripke Models for Predicate Logic | 106 |
Systems LJm LJ | 109 |
ProofSearch in Predicate Logic | 119 |
References | 125 |
129 | |
Andere Ausgaben - Alle anzeigen
Häufige Begriffe und Wortgruppen
1-sequents accessibility relation apply assume assumption atomic formulas axiom bound variables Coherence Theorem complete sequent component conclusion Consider constructed Craig interpolant Curry–Howard isomorphism deductive terms DEFINITION denoted derivable in NJp derivable sequent direct chaining disjunction eigenvariable elimination rule EXAMPLE extended falsified finite formula is derivable free variables function symbols goal iff is derivable implies induction base induction hypothesis induction step inference introduction rule intuitionistic logic intuitionistic propositional logic invertible rules Kripke frame Kripke model Lemma main branch monotonicity movable rule multisets natural deduction negative translation non-invertible rules obtained occurrence predicate logic premise principal formula proof proof-search tree Proof.Part propositional logic propositional variable prove pruned quantifier rules R-closed realizations redex rule of LJpm satisfying saturated for invertible Section sequent is derivable sequents is saturated subformulas subgoal system NJp tableau tautology tree extension steps truth tables truth value truth value assignment underivable weakenings