LEADER 05453nam 2200673 a 450 001 9910824375103321 005 20230802004540.0 010 $a981-4360-96-1 035 $a(CKB)2550000000087488 035 $a(EBL)846147 035 $a(SSID)ssj0000645898 035 $a(PQKBManifestationID)11370943 035 $a(PQKBTitleCode)TC0000645898 035 $a(PQKBWorkID)10683889 035 $a(PQKB)10698916 035 $a(MiAaPQ)EBC846147 035 $a(WSP)00008215 035 $a(Au-PeEL)EBL846147 035 $a(CaPaEBR)ebr10529392 035 $a(CaONFJC)MIL498453 035 $a(OCoLC)785777991 035 $a(EXLCZ)992550000000087488 100 $a20120203d2012 uy 0 101 0 $aeng 135 $aurcn||||||||| 181 $ctxt 182 $cc 183 $acr 200 14$aThe functional interpretation of logical deduction$b[electronic resource] /$fRuy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. Gabbay 210 $aSingapore $cWorld Scientific$dc2012 215 $a1 online resource (299 p.) 225 1 $aAdvances in logic ;$vv. 5 300 $aDescription based upon print version of record. 311 $a981-4360-95-3 320 $aIncludes bibliographical references (p. 253-264) and index. 327 $aContents; 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 327 $a1.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 327 $a3.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 327 $a3.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 327 $a4.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 327 $a6.4.2 Confluence property 330 $aThis 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 410 0$aAdvances in logic ;$vv. 5. 606 $aLogic 606 $aModality (Logic) 615 0$aLogic. 615 0$aModality (Logic) 676 $a004.015113 676 $a511.3 700 $aQueiroz$b Ruy J. G. B. de$01691523 701 $aOliveira$b Anjolina G. de$01691524 701 $aGabbay$b Dov M.$f1945-$056838 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910824375103321 996 $aThe functional interpretation of logical deduction$94067966 997 $aUNINA