Cette publication ne fait pas partie de la bibliothèque YouScribe
Elle est disponible uniquement à l'achat (la librairie de YouScribe)
Achetez pour : 73,78 € Lire un extrait

Téléchargement

Format(s) : PDF

avec DRM

A Short Introduction to Intuitionistic Logic

De
0 page

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 tchniques are presented first for propositional logic, then part II inroduces extensions to predicate logic. This material provides an introduction and a 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 and 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; lagebraic and topological semantics; proof-search methods; and interpolation theorem.

Voir plus Voir moins

Vous aimerez aussi

Contents
Introduction
I
1
2
3
4
5
Intuitionistic Propositional Logic
Preliminaries
Natural Deduction for Propositional Logic 2.1.Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2.Intuitionistic Propositional System NJp . . . . . . . . . . . . . . 2.3.. . . . . . . . . . . . . . . .Classical Propositional System NKp 2.4.. . . . . . . . . . .Abbreviated Notation for Natural Deductions 2.5.. . . . . . . . . . . . . . . . . . . . . . . . . . . .Derivable Rules 2.6.. . . . . . . . . . . .Direct Chaining and Analysis into Subgoals 2.7.Heuristics for Natural Deduction . . . . . . . . . . . . . . . . . . 2.8.Replacement of Equivalents . . . . . . . . . . . . . . . . . . . . . 2.9.. . . . . . . . . . . . . . . . . . . .Classical Propositional Logic 2.9.1.Semantics: Truth Tables . . . . . . . . . . . . . . . . . . . 2.9.2.. . . . . . . . . . . . . . . . . . . .Logical Computations
Negative Translation: Glivenko’s Theorem
Program Interpretation of Intuitionistic Logic 4.1.. . . . . . . . . . . . . . . . . . . . . . . .BHK-Interpretation . 4.2.Deductive Terms Assignment of . . . . . . . . . . . . . . . . . 4.2.1.. . . . . . . . . . . . . . . . . . . . . .Assignment Rules 4.3.Properties of Term Assignment . . . . . . . . . . . . . . . . . . .
Computations with Deductions 5.1.. . . . . . . . .Conversions and Reductions of Deductive Terms 5.2.Natural Deductions Conversions and Reductions of . . . . . . . . 5.3.. . . . . . . . . . . . . . . . . . . . . . . . . . . .Normalization . 5.4.Normalization . . . . . . . . . . . . . . . . . . .Consequences of
vii
1
5
7
9 9 10 10 11 13 15 16 18 19 19 20
23
25 25 26 27 29
31 31 32 37 38
viii
6
7
CONTENTS
Coherence Theorem 6.1.Structure of . . . . . . . . . . . . . . . . . . .Normal Deduction 6.2.-reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.3.. . . . . . . . . . . . . . . . . . . . . . . . .Coherence Theorem
Kripke Models 7.1.. . . . . . . . . . . . . . . . . . . .the System NJp Soundness of 7.2.Pointed Frames, Partial Orders . . . . . . . . . . . . . . . . . . . 7.3.Frame Conditions . . . . . . . . . . . . . . . . . . . . . . . . . . .
8Gentzen-type Propositional System LJpm 8.1.the System LJpm Soundness of . . . . . . . . . . . . . . . . . . . 8.2.Completeness and Admissibility of Cut . . . . . . . . . . . . . . . 8.3.Translation into the Predicate Logic . . . . . . . . . . . . . . . . 8.4.Algebraic Models . . . . . . . . . . . . . . . . . . . . . . . . . . . 8.5.. . . . . . . . . . . . . . . . . . . . . .Filtration, Finite Matrices 8.5.1.. . . . . . . . . . . . . . . . . . . . . . . . . .Filtration . 8.5.2.LindenbaumAlgebra. . . . . . . . . . . . . . . . . . . . . 8.5.3.. . . . . . . . . . . . . . . . . . . . .Finite Truth Tables 9Topological Completeness
10Proof- Search 10.1.Tableaux: System LJpm* . . . . . . . . . . . . . . . . . . . . . . 10.2.Proof-Search Procedure . . . . . . . . . . . . . . . . . . . . . . . 10.3.. . . . . . . . . . . . . . . . . .Complete Proof-Search Strategy
11System LJp 11.1.Translating LJpm into LJp . . . . . . . . . . . . . . . . . . . . . 11.2.A Disjunctive translation . . . . . . . . . . . . . . . . . . . . . . 11.3.Pruning, Permutability of Rules . . . . . . . . . . . . . . . . . . .
12Interpolation Theorem 12.1.. . . . . . . . . . . . . . . . . . . . .Beth Definability Theorem .
II
Intuitionistic Predicate Logic
13Natural Deduction System NJ 13.1.. . . . . . . . . . . . . . . . . . . . . . . . . . . .Derivable Rules 13.2.. . . . . . . . . . . . . . . . . . . .Gödel’s Negative Translation 13.3.. . . . . . . . . . . . . . . . . . .Program Interpretation of NJ .
41 41 42 42
47 50 51 52
53 57 57 61 62 65 65 66 67
69
75 75 77 79
83 83 83 84
89 90
93
95 96 97 99
14Kripke Models for Predicate Logic105 14.1. Pointed Models, Frame Conditions . . . . . . . . . . . . . . . . .107
CONTENTS
ix
15Systems LJm, LJ109 15.0.1.Canonical Model, Admissibility of . . . . . . . . . .Cut . 109 15.1.Translation into the Classical Logic . . . . . . . . . . . . . . . . .113 15.2.. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .System LJ 114 15.2.1.TranslatingLJpmintoLJp . . . . . . . . . . . . . . . . .115 15.3.Interpolation Theorem . . . . . . . . . . . . . . . . . . . . . . . .116
16Proof-Search in Predicate Logic References Index
119
125
129
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin