Cut-Elimination and Quantification in Canonical Systems View Full Text


Ontology type: schema:ScholarlyArticle      Open Access: True


Article Info

DATE

2006-02

AUTHORS

Anna Zamansky, Arnon Avron

ABSTRACT

Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix. More... »

PAGES

157-176

References to SciGraph publications

  • 1986. Proof Theory and Meaning in HANDBOOK OF PHILOSOPHICAL LOGIC
  • 2001-06-08. Canonical Propositional Gentzen-Type Systems in AUTOMATED REASONING
  • 1998-07. Labeled Calculi and Finite-Valued Logics in STUDIA LOGICA
  • Journal

    TITLE

    Studia Logica

    ISSUE

    1

    VOLUME

    82

    Author Affiliations

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s11225-006-6611-6

    DOI

    http://dx.doi.org/10.1007/s11225-006-6611-6

    DIMENSIONS

    https://app.dimensions.ai/details/publication/pub.1014344808


    Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
    Incoming Citations Browse incoming citations for this publication using opencitations.net

    JSON-LD is the canonical representation for SciGraph data.

    TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

    [
      {
        "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
        "about": [
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/2004", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Linguistics", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/20", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Language, Communication and Culture", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Tel Aviv University", 
              "id": "https://www.grid.ac/institutes/grid.12136.37", 
              "name": [
                "School of Computer Science, Tel-Aviv University, 69978, Ramat Aviv, Israel"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Zamansky", 
            "givenName": "Anna", 
            "id": "sg:person.014366341552.82", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014366341552.82"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Tel Aviv University", 
              "id": "https://www.grid.ac/institutes/grid.12136.37", 
              "name": [
                "School of Computer Science, Tel-Aviv University, 69978, Ramat Aviv, Israel"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Avron", 
            "givenName": "Arnon", 
            "id": "sg:person.014461136355.70", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014461136355.70"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/978-94-009-5203-4_8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002335429", 
              "https://doi.org/10.1007/978-94-009-5203-4_8"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.2307/2274395", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1010852047"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1023/a:1005022012721", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027904430", 
              "https://doi.org/10.1023/a:1005022012721"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/0890-5401(91)90023-u", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1041008858"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-45744-5_45", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051434466", 
              "https://doi.org/10.1007/3-540-45744-5_45"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-45744-5_45", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1051434466", 
              "https://doi.org/10.1007/3-540-45744-5_45"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1093/jigpal/jzi030", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1059797684"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1093/logcom/exi001", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1059875940"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.2307/2271192", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1069855852"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/ismvl.2005.40", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1094760225"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/cbo9780511527340", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1098701229"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2006-02", 
        "datePublishedReg": "2006-02-01", 
        "description": "Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a \u201ccanonical system\u201d to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix.", 
        "genre": "research_article", 
        "id": "sg:pub.10.1007/s11225-006-6611-6", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": true, 
        "isPartOf": [
          {
            "id": "sg:journal.1051009", 
            "issn": [
              "0039-3215", 
              "1572-8730"
            ], 
            "name": "Studia Logica", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "1", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "82"
          }
        ], 
        "name": "Cut-Elimination and Quantification in Canonical Systems", 
        "pagination": "157-176", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "445669a379e022ea1f6fb9b5db0c838d8cc07903bd60b2591d78014c66f83955"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s11225-006-6611-6"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1014344808"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s11225-006-6611-6", 
          "https://app.dimensions.ai/details/publication/pub.1014344808"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-11T12:40", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000363_0000000363/records_70053_00000000.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "http://link.springer.com/10.1007%2Fs11225-006-6611-6"
      }
    ]
     

    Download the RDF metadata as:  json-ld nt turtle xml License info

    HOW TO GET THIS DATA PROGRAMMATICALLY:

    JSON-LD is a popular format for linked data which is fully compatible with JSON.

    curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/s11225-006-6611-6'

    N-Triples is a line-based linked data format ideal for batch operations.

    curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/s11225-006-6611-6'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s11225-006-6611-6'

    RDF/XML is a standard XML format for linked data.

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s11225-006-6611-6'


     

    This table displays all metadata directly associated to this object as RDF triples.

    101 TRIPLES      21 PREDICATES      37 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s11225-006-6611-6 schema:about anzsrc-for:20
    2 anzsrc-for:2004
    3 schema:author N7cba21e27ec14005b91e0e9c5da1aac8
    4 schema:citation sg:pub.10.1007/3-540-45744-5_45
    5 sg:pub.10.1007/978-94-009-5203-4_8
    6 sg:pub.10.1023/a:1005022012721
    7 https://doi.org/10.1016/0890-5401(91)90023-u
    8 https://doi.org/10.1017/cbo9780511527340
    9 https://doi.org/10.1093/jigpal/jzi030
    10 https://doi.org/10.1093/logcom/exi001
    11 https://doi.org/10.1109/ismvl.2005.40
    12 https://doi.org/10.2307/2271192
    13 https://doi.org/10.2307/2274395
    14 schema:datePublished 2006-02
    15 schema:datePublishedReg 2006-02-01
    16 schema:description Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix.
    17 schema:genre research_article
    18 schema:inLanguage en
    19 schema:isAccessibleForFree true
    20 schema:isPartOf N50704ef2d7d648be9f0edb3bfb852172
    21 Nb5aff3fa89824651b22e5e8f4ca778a8
    22 sg:journal.1051009
    23 schema:name Cut-Elimination and Quantification in Canonical Systems
    24 schema:pagination 157-176
    25 schema:productId N30f9c202db0f43f889e1ff623031a61e
    26 N85f1f017c22a424c8294980f97b4778f
    27 N94155d83825746a8a8ee635307d92fa2
    28 schema:sameAs https://app.dimensions.ai/details/publication/pub.1014344808
    29 https://doi.org/10.1007/s11225-006-6611-6
    30 schema:sdDatePublished 2019-04-11T12:40
    31 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    32 schema:sdPublisher N0874739baa41431581a67267b8f26e2b
    33 schema:url http://link.springer.com/10.1007%2Fs11225-006-6611-6
    34 sgo:license sg:explorer/license/
    35 sgo:sdDataset articles
    36 rdf:type schema:ScholarlyArticle
    37 N0874739baa41431581a67267b8f26e2b schema:name Springer Nature - SN SciGraph project
    38 rdf:type schema:Organization
    39 N30f9c202db0f43f889e1ff623031a61e schema:name dimensions_id
    40 schema:value pub.1014344808
    41 rdf:type schema:PropertyValue
    42 N50704ef2d7d648be9f0edb3bfb852172 schema:volumeNumber 82
    43 rdf:type schema:PublicationVolume
    44 N7cba21e27ec14005b91e0e9c5da1aac8 rdf:first sg:person.014366341552.82
    45 rdf:rest N8ad1fdb06b61408c85599539b14cfbde
    46 N85f1f017c22a424c8294980f97b4778f schema:name readcube_id
    47 schema:value 445669a379e022ea1f6fb9b5db0c838d8cc07903bd60b2591d78014c66f83955
    48 rdf:type schema:PropertyValue
    49 N8ad1fdb06b61408c85599539b14cfbde rdf:first sg:person.014461136355.70
    50 rdf:rest rdf:nil
    51 N94155d83825746a8a8ee635307d92fa2 schema:name doi
    52 schema:value 10.1007/s11225-006-6611-6
    53 rdf:type schema:PropertyValue
    54 Nb5aff3fa89824651b22e5e8f4ca778a8 schema:issueNumber 1
    55 rdf:type schema:PublicationIssue
    56 anzsrc-for:20 schema:inDefinedTermSet anzsrc-for:
    57 schema:name Language, Communication and Culture
    58 rdf:type schema:DefinedTerm
    59 anzsrc-for:2004 schema:inDefinedTermSet anzsrc-for:
    60 schema:name Linguistics
    61 rdf:type schema:DefinedTerm
    62 sg:journal.1051009 schema:issn 0039-3215
    63 1572-8730
    64 schema:name Studia Logica
    65 rdf:type schema:Periodical
    66 sg:person.014366341552.82 schema:affiliation https://www.grid.ac/institutes/grid.12136.37
    67 schema:familyName Zamansky
    68 schema:givenName Anna
    69 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014366341552.82
    70 rdf:type schema:Person
    71 sg:person.014461136355.70 schema:affiliation https://www.grid.ac/institutes/grid.12136.37
    72 schema:familyName Avron
    73 schema:givenName Arnon
    74 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014461136355.70
    75 rdf:type schema:Person
    76 sg:pub.10.1007/3-540-45744-5_45 schema:sameAs https://app.dimensions.ai/details/publication/pub.1051434466
    77 https://doi.org/10.1007/3-540-45744-5_45
    78 rdf:type schema:CreativeWork
    79 sg:pub.10.1007/978-94-009-5203-4_8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002335429
    80 https://doi.org/10.1007/978-94-009-5203-4_8
    81 rdf:type schema:CreativeWork
    82 sg:pub.10.1023/a:1005022012721 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027904430
    83 https://doi.org/10.1023/a:1005022012721
    84 rdf:type schema:CreativeWork
    85 https://doi.org/10.1016/0890-5401(91)90023-u schema:sameAs https://app.dimensions.ai/details/publication/pub.1041008858
    86 rdf:type schema:CreativeWork
    87 https://doi.org/10.1017/cbo9780511527340 schema:sameAs https://app.dimensions.ai/details/publication/pub.1098701229
    88 rdf:type schema:CreativeWork
    89 https://doi.org/10.1093/jigpal/jzi030 schema:sameAs https://app.dimensions.ai/details/publication/pub.1059797684
    90 rdf:type schema:CreativeWork
    91 https://doi.org/10.1093/logcom/exi001 schema:sameAs https://app.dimensions.ai/details/publication/pub.1059875940
    92 rdf:type schema:CreativeWork
    93 https://doi.org/10.1109/ismvl.2005.40 schema:sameAs https://app.dimensions.ai/details/publication/pub.1094760225
    94 rdf:type schema:CreativeWork
    95 https://doi.org/10.2307/2271192 schema:sameAs https://app.dimensions.ai/details/publication/pub.1069855852
    96 rdf:type schema:CreativeWork
    97 https://doi.org/10.2307/2274395 schema:sameAs https://app.dimensions.ai/details/publication/pub.1010852047
    98 rdf:type schema:CreativeWork
    99 https://www.grid.ac/institutes/grid.12136.37 schema:alternateName Tel Aviv University
    100 schema:name School of Computer Science, Tel-Aviv University, 69978, Ramat Aviv, Israel
    101 rdf:type schema:Organization
     




    Preview window. Press ESC to close (or click here)


    ...