In this blog, 25.000 books will be uploaded, so far more than 1400 books are available. Books, will be added daily, please check this blog daily.
Wednesday, November 16, 2011
A Short Introduction to Intuitionistic Logic
Contents
Introduction
Intuitionistic Propositional Logic
Preliminaries
Natural Deduction for Propositional Logic
Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Intuitionistic Propositional System NJp . . . . . . . . . . . . . .
Classical Propositional System NKp . . . . . . . . . . . . . . . .
Abbreviated Notation for Natural Deductions . . . . . . . . . . .
Derivable Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Direct Chaining and Analysis into Subgoals . . . . . . . . . . . .
Heuristics for Natural Deduction . . . . . . . . . . . . . . . . . .
Replacement of Equivalents . . . . . . . . . . . . . . . . . . . . .
Classical Propositional Logic . . . . . . . . . . . . . . . . . . . .
Semantics:Truth Tables . . . . . . . . . . . . . . . . . . .
Logical Computations . . . . . . . . . . . . . . . . . . . .
Negative Translation: Glivenko’s Theorem
Program Interpretation of Intuitionistic Logic
BHK-Interpretation . . . . . . . . . . . . . . . . . . . . . . . . .
Assignment of Deductive Terms . . . . . . . . . . . . . . . . .
4.2.1. Assignment Rules . . . . . . . . . . . . . . . . . . . . . .
Properties of Term Assignment . . . . . . . . . . . . . . . . . . .
Computations with Deductions
Conversions and Reductions of Deductive Terms . . . . . . . . .
Conversions and Reductions of Natural Deductions . . . . . . . .
Normalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Consequences of Normalization . . . . . . . . . . . . . . . . . . .
Coherence Theorem 41
Structure of Normal Deduction . . . . . . . . . . . . . . . . . . .
-reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Coherence Theorem . . . . . . . . . . . . . . . . . . . . . . . . .
Kripke Models
Soundness of the System NJp . . . . . . . . . . . . . . . . . . . .
Pointed Frames, Partial Orders . . . . . . . . . . . . . . . . . . .
Frame Conditions . . . . . . . . . . . . . . . . . . . . . . . . . . .
Gentzen-type Propositional System LJpm
Soundness of the System LJpm . . . . . . . . . . . . . . . . . . .
Completeness and Admissibility of Cut . . . . . . . . . . . . . . .
Translation into the Predicate Logic . . . . . . . . . . . . . . . .
Algebraic Models . . . . . . . . . . . . . . . . . . . . . . . . . . .
Filtration, Finite Matrices . . . . . . . . . . . . . . . . . . . . . .
8.5.1.
8.5.2.
8.5.3.
Filtration . . . . . . . . . . . . . . . . . . . . . . . . . . .
Lindenbaum Algebra . . . . . . . . . . . . . . . . . . . . .
Finite Truth Tables . . . . . . . . . . . . . . . . . . . . .
Topological Completeness
Proof- Search
Tableaux: System LJpm* . . . . . . . . . . . . . . . . . . . . . .
Proof-Search Procedure . . . . . . . . . . . . . . . . . . . . . . .
Complete Proof-Search Strategy . . . . . . . . . . . . . . . . . .
System LJp
Translating LJpm into LJp . . . . . . . . . . . . . . . . . . . . .
A Disjunctive translation . . . . . . . . . . . . . . . . . . . . . .
Pruning, Permutability of Rules . . . . . . . . . . . . . . . . . . .
Interpolation Theorem
12.1. Beth Definability Theorem . . . . . . . . . . . . . . . . . . . . . .
Intuitionistic Predicate Logic
Natural Deduction System NJ
Derivable Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Gödel’s Negative Translation . . . . . . . . . . . . . . . . . . . .
Program Interpretation of NJ . . . . . . . . . . . . . . . . . . . .
Kripke Models for Predicate Logic
14.1. Pointed Models, Frame Conditions . . . . . . . . . . . . . . . . .Systems LJm, LJ 109
15.0.1. Canonical Model, Admissibility of Cut . . . . . . . . . . . 109
Translation into the Classical Logic . . . . . . . . . . . . . . . . .
System LJ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
15.2.1. Translating LJpm into LJp . . . . . . . . . . . . . . . . .
Interpolation Theorem . . . . . . . . . . . . . . . . . . . . . . . .
Proof-Search in Predicate Logic 119
125
129
References
Index
Another Logic Books
Download
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment