05453nam 2200673 a 450 991082437510332120230802004540.0981-4360-96-1(CKB)2550000000087488(EBL)846147(SSID)ssj0000645898(PQKBManifestationID)11370943(PQKBTitleCode)TC0000645898(PQKBWorkID)10683889(PQKB)10698916(MiAaPQ)EBC846147(WSP)00008215(Au-PeEL)EBL846147(CaPaEBR)ebr10529392(CaONFJC)MIL498453(OCoLC)785777991(EXLCZ)99255000000008748820120203d2012 uy 0engurcn|||||||||txtccrThe functional interpretation of logical deduction[electronic resource] /Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. GabbaySingapore World Scientificc20121 online resource (299 p.)Advances in logic ;v. 5Description based upon print version of record.981-4360-95-3 Includes bibliographical references (p. 253-264) and index.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 normalisation1.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 principle3.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 Finale3.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 β reductions4.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 property6.4.2 Confluence propertyThis 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 usAdvances in logic ;v. 5.LogicModality (Logic)Logic.Modality (Logic)004.015113511.3Queiroz Ruy J. G. B. de1691523Oliveira Anjolina G. de1691524Gabbay Dov M.1945-56838MiAaPQMiAaPQMiAaPQBOOK9910824375103321The functional interpretation of logical deduction4067966UNINA