Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
The functional interpretation of logical deduction [[electronic resource] /] / Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. Gabbay
| The functional interpretation of logical deduction [[electronic resource] /] / Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. Gabbay |
| Autore | Queiroz Ruy J. G. B. de |
| Pubbl/distr/stampa | Singapore, : World Scientific, c2012 |
| Descrizione fisica | 1 online resource (299 p.) |
| Disciplina |
004.015113
511.3 |
| Altri autori (Persone) |
OliveiraAnjolina G. de
GabbayDov M. <1945-> |
| Collana | Advances in logic |
| Soggetto topico |
Logic
Modality (Logic) |
| Soggetto genere / forma | Electronic books. |
| ISBN | 981-4360-96-1 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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 |
| Record Nr. | UNINA-9910457540703321 |
Queiroz Ruy J. G. B. de
|
||
| Singapore, : World Scientific, c2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The functional interpretation of logical deduction [[electronic resource] /] / Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. Gabbay
| The functional interpretation of logical deduction [[electronic resource] /] / Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. Gabbay |
| Autore | Queiroz Ruy J. G. B. de |
| Pubbl/distr/stampa | Singapore, : World Scientific, c2012 |
| Descrizione fisica | 1 online resource (299 p.) |
| Disciplina |
004.015113
511.3 |
| Altri autori (Persone) |
OliveiraAnjolina G. de
GabbayDov M. <1945-> |
| Collana | Advances in logic |
| Soggetto topico |
Logic
Modality (Logic) |
| ISBN | 981-4360-96-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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 |
| Record Nr. | UNINA-9910779073503321 |
|
Queiroz Ruy J. G. B. de
|
||
| Singapore, : World Scientific, c2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The functional interpretation of logical deduction [[electronic resource] /] / Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. Gabbay
| The functional interpretation of logical deduction [[electronic resource] /] / Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. Gabbay |
| Autore | Queiroz Ruy J. G. B. de |
| Pubbl/distr/stampa | Singapore, : World Scientific, c2012 |
| Descrizione fisica | 1 online resource (299 p.) |
| Disciplina |
004.015113
511.3 |
| Altri autori (Persone) |
OliveiraAnjolina G. de
GabbayDov M. <1945-> |
| Collana | Advances in logic |
| Soggetto topico |
Logic
Modality (Logic) |
| ISBN | 981-4360-96-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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 |
| Record Nr. | UNINA-9910824375103321 |
|
Queiroz Ruy J. G. B. de
|
||
| Singapore, : World Scientific, c2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||