| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910824375103321 |
|
|
Autore |
Queiroz Ruy J. G. B. de |
|
|
Titolo |
The functional interpretation of logical deduction [[electronic resource] /] / Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. Gabbay |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Singapore, : World Scientific, c2012 |
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Descrizione fisica |
|
1 online resource (299 p.) |
|
|
|
|
|
|
Collana |
|
Advances in logic ; ; v. 5 |
|
|
|
|
|
|
Altri autori (Persone) |
|
OliveiraAnjolina G. de |
GabbayDov M. <1945-> |
|
|
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
|
|
Soggetti |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Description based upon print version of record. |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references (p. 253-264) and index. |
|
|
|
|
|
|
Nota di contenuto |
|
Contents; Preface; Overview; Introduction; Labels and Gentzen's programme; Labels and computer programming; Labels and information flow; Labels and 'constructivity as explicitation'; Labels, connectives, consequence relation and structures; Labels and non-normal modal logics; Labeling: A new paradigm for the functional interpretation; 1. Labelled Natural Deduction; 1.1 The role of the labels; 1.1.1 Dividing the tasks: A functional calculus on the labels, a logical calculus on the formula; 1.1.2 Reassessing Frege's two-dimensional calculus; 1.2 Canonical proofs and normalisation |
1.2.1 Canonical proofs 1.2.2 Normalisation; 1.2.2.1 β-type reductions; 1.2.2.2 β-equality; 1.2.2.3 η-type reductions; 1.2.2.4 η-equality; 2. The Functional Interpretation of Implication; 2.1 Introduction; 2.2 Origins; 2.3 Types and propositions; 2.4 λ-abstraction and implication; 2.5 Consistency proof; 2.6 Systems of implication and combinators; 2.7 Finale; 3. The Existential Quantifier; Preamble; 3.1 Motivation; 3.1.1 The pairing interpretation; 3.2 Quantifiers and normalisation; 3.2.1 Introducing variables for the Skolem dependency functions; 3.2.2 The hiding principle |
3.3 Other approaches to existential quantification 3.3.1 Systems of natural deduction based on direct existential instantiation; 3.3.1.1 Quine's system; 3.3.1.2 Fine's generalised system; 3.3.1.3 |
|
|
|
|
|
|
|
|
|
|
|
Incorporating annotations into the object language; 3.3.2 Axiomatic systems based on the notion of 'such that'; 3.3.2.1 Hilbert's η- and ε-calculi; 3.3.2.2 Hailperin's ν-calculus; 3.4 Model-theoretic semantics; 3.4.1 Constants versus variables revisited; 3.4.1.1 Skolem resolution; 3.4.1.2 Herbrand resolution; 3.4.2 Eliminability and conservative extensions; 3.5 Finale |
3.5.1 Extensions to higher-order existentials 3.5.2 Further connections to model-theoretic interpretations; 3.6 Examples of deduction; 3.6.1 Generic examples; 3.6.2 Specific examples; 4. Normalisation; Preamble; 4.1 Introduction; 4.2 Proof transformations in labelled deduction; 4.3 Equivalences between proofs in LND; 4.4 The term rewriting system for LND; 4.4.1 Defining the LND-TRS; 4.4.2 The sort decreasing property; 4.4.3 Defining an order; 4.4.3.1 Analyzing the ζ-reductions; 4.4.4 Proving the termination property; 4.4.4.1 Proof for the subset of β reductions |
4.4.4.2 Proof for the subset of η reductions 4.4.4.3 Proof for the subset of ζ reductions:; 4.4.5 Proving the confluence property; 4.5 Examples of transformations between proofs; 4.6 Final remarks; Appendix: Proof of confluence of LND-TRS; 5. Natural Deduction for Equality; 5.1 Introduction; 5.2 Labelled deduction; 5.2.1 Identifiers for (compositions of) equalities; 5.2.2 The proof rules; 5.3 Finale; 6. Normalisation for the Equality Fragment; Preamble; 6.1 General rules; 6.2 The 'subterm substitution' rule; 6.3 The ξ- and μ-rules; 6.4 Term rewriting systems; 6.4.1 Termination property |
6.4.2 Confluence property |
|
|
|
|
|
|
Sommario/riassunto |
|
This comprehensive book provides an adequate framework to establish various calculi of logical inference. Being an 'enriched' system of natural deduction, it helps to formulate logical calculi in an operational manner. By uncovering a certain harmony between a functional calculus on the labels and a logical calculus on the formulas, it allows mathematical foundations for systems of logic presentation designed to handle meta-level features at the object-level via a labeling mechanism, such as the D Gabbay's Labelled Deductive Systems. The book truly demonstrates that introducing 'labels' is us |
|
|
|
|
|
|
|
| |