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

No comments:

Post a Comment

Related Posts with Thumbnails

Put Your Ads Here!