Substructural logic (original) (raw)
In logic, a substructural logic is a logic lacking one of the usual structural rules (e.g. of classical and intuitionistic logic), such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics are relevance logic and linear logic.
| Property | Value |
|---|---|
| dbo:abstract | Les logiques sous-structurelles sont des logiques mathématiques où certaines règles d'inférence ne sont pas utilisées ou ont une utilisation restreinte. En particulier, par rapport à la logique classique ou à la logique intuitionniste, il leur manque la règle de contraction qui dit peu ou prou que si on peut faire un raisonnement avec une même hypothèse invoquée deux fois, on peut faire le même raisonnement sans dupliquer cette hypothèse et la règle d'affaiblissement qui permet d'éliminer de l'ensemble des hypothèses une hypothèse inutilisée dans le raisonnement. La logique linéaire est une logique sous-structurelle. (fr) In logic, a substructural logic is a logic lacking one of the usual structural rules (e.g. of classical and intuitionistic logic), such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics are relevance logic and linear logic. (en) 部分構造論理（ぶぶんこうぞうろんり、英: Substructural logic）は、通常の命題論理を弱くした論理体系群を指し、数理論理学の中でも証明理論と密接に関連する。部分構造論理は使用可能なが命題論理よりも少なく、かつ個々の部分構造論理によってその種類が異なる。構造規則の概念は自然演繹の定式化手法よりもシークエント表現に基づく。主な部分構造論理の例として、適切さの論理と線型論理がある。 シークエント計算では、証明の各行は次のように記される。 ここでの構造規則とは、左辺 のシークエント（命題を表す文字列）の項書き換え規則である。一般にここの文字列は論理積と解釈される。例えば、命題 に対して、以下のようなシークエント表現 は次のように解釈される。 ( かつ ) は を含意する。 ここで、右辺 が単一の命題 であるとしたが（直観主義的なシークエントのスタイル）、全ての操作はターンスタイル記号の左側で行われるので、一般のケースにも当てはまる。 論理積には交換法則と結合法則が成り立つので、シークエント を書き換える構造規則にも同じ法則に対応したもの（転置規則）がある。例えば、 から を導くことができる。他にも冪等に対応した規則（縮約規則）と単調性に対応した規則（弱化規則）が存在する。 から、次を導くことができる（縮約規則）。 また から任意の B を加えて を導くこともできる（弱化規則）。 線型論理では、前提が重複する場合は単一のときとは異なった意味を持つので、これらの規則は除外される。適切さの論理では、弱化規則だけを除外する（ は帰結とは明らかに無関係であるため）。 これらは部分構造論理の基本的な例である。なお、通常の命題論理にこれらの規則を適用することは何ら問題ない。 (ja) Em lógica, uma subestrutura lógica é uma falta lógica das regras estruturais usuais (p.e. da lógica clássica e intuicionista), tal como enfraquecimento, contração ou associatividade. Duas das lógicas subestruturais mais significativas são lógica de relevância e lógica linear. No cálculo de sequentes, se escreve cada linha de uma prova como . Aqui as regras são regras estruturais para reescrever os Γ de um sequente, inicialmente concebido como um string de proposições. A interpretação padrão desta string é como conjunção: nós devemos ler como a notação sequente para (A e B) implica C. Aqui nós estamos tomando os Σ para ser uma simples proposição C (que é o intuicionista estilo de sequente); mas tudo o que se aplica igualmente ao caso geral, uma vez que todas as manipulações estão indo para a esquerda do . Desde que a conjunção é uma operação comutativa e associativa , a criação formal da teoria de sequentes normalmente inclui regras estruturais para reescrever o sequente Γ adequadamente - por exemplo para deduzir de . Existem mais regras estruturais correspondentes a Idempotência e monotônica propriedades de conjunção: de nós podemos deduzir . Também a partir de se pode deduzir, para qualquer B , . Lógica linear, em que hipóteses duplicadas 'contam' de forma diferente a partir de ocorrências individuais, deixa de fora essas duas regras, enquanto a lógica relevante simplesmente deixa de fora a última regra, pelo fato do B ser claramente relevante para a conclusão. Estes são exemplos básicos de regras estruturais. Não que essas regras sejam controversas, quando aplicado no cálculo proposicional convencional. Elas ocorrem naturalmente na teoria da prova, tendo sido notado pela primeira vez lá(antes de receber um nome). (pt) 在数理逻辑中，特别是联合上证明论的时候，一些亚结构逻辑已经作为比常规系统弱的命题演算系统被介入了。同常规系统的不同之处在于它们有更少的结构规则可用：结构规则的概念是基于相继式（sequent）表达，而不是自然演绎的公式化表达。两个重要的亚结构逻辑是相干逻辑和线性逻辑。 在相继式演算中，你可以把证明的每一行写为 。 这里的结构规则是相继式的Γ的规则，Γ是最初被构想为命题的字符串。这个字符串的标准解释是合取式：我们希望把相继式符号 读做 (A 与B)蕴涵C。 这里我们把的Σ采纳为一个单一的命题C（这是直觉主义风格的相继式）;但是所有的东西都同样的适用于一般情况，因为所有的操作都发生在十字转门（turnstile）符号的左边。 因为合取是交换性和结合性的操作，相继式理论的形式架设通常包括相应的结构规则来重写相继式的Γ - 例如 演绎自 。 还有对应于合取特性的幂等性和单调性的进一步的结构规则：从 我们可以演绎出 。 还有从 我们可以演绎出，对于任何B， 。 在线性逻辑中有重复的假设（hypothese）'被认为'不同于单一的出现，它排除了这两个规则。而相干逻辑只排除后者的规则，因为B明显的与结论无关。 这些是结构规则的基本例子。在应用到常规命题演算的时候，这些规则是没有任何争议的。它们自然的出现于证明理论中，并在那里被首次注意到（在获得一个名字之前）。 (zh) |
| dbo:wikiPageExternalLink | https://books.google.com/books%3Fid=NQTm_bRupAgC&printsec=frontcover%23v=onepage&q&f=false https://books.google.com/books%3Fid=RkPsCAAAQBAJ&printsec=frontcover%23v=onepage&q&f=false |
| dbo:wikiPageID | 412909 (xsd:integer) |
| dbo:wikiPageLength | 4504 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1073310284 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Monotonicity_of_entailment dbr:Intuitionistic_logic dbr:Substructural_type_system dbr:Commutative dbr:Rewriting dbr:Structural_rule dbr:Monotonic dbr:Linear_logic dbr:Logic dbr:Logical_conjunction dbr:Idempotency_of_entailment dbc:Non-classical_logic dbc:Substructural_logic dbr:Classical_logic dbr:Idempotent dbr:Associative dbr:Sequent_calculus dbr:Turnstile_(symbol) dbr:Residuated_lattice dbr:Sides_of_an_equation dbr:Intuitionistic dbr:Relevant_logic |
| dbp:wikiPageUsesTemplate | dbt:Commonscat-inline dbt:No_footnotes dbt:Reflist dbt:Cite_SEP dbt:Isbn dbt:Non-classical_logic |
| dct:subject | dbc:Non-classical_logic dbc:Substructural_logic |
| rdfs:comment | In logic, a substructural logic is a logic lacking one of the usual structural rules (e.g. of classical and intuitionistic logic), such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics are relevance logic and linear logic. (en) 在数理逻辑中，特别是联合上证明论的时候，一些亚结构逻辑已经作为比常规系统弱的命题演算系统被介入了。同常规系统的不同之处在于它们有更少的结构规则可用：结构规则的概念是基于相继式（sequent）表达，而不是自然演绎的公式化表达。两个重要的亚结构逻辑是相干逻辑和线性逻辑。 在相继式演算中，你可以把证明的每一行写为 。 这里的结构规则是相继式的Γ的规则，Γ是最初被构想为命题的字符串。这个字符串的标准解释是合取式：我们希望把相继式符号 读做 (A 与B)蕴涵C。 这里我们把的Σ采纳为一个单一的命题C（这是直觉主义风格的相继式）;但是所有的东西都同样的适用于一般情况，因为所有的操作都发生在十字转门（turnstile）符号的左边。 因为合取是交换性和结合性的操作，相继式理论的形式架设通常包括相应的结构规则来重写相继式的Γ - 例如 演绎自 。 还有对应于合取特性的幂等性和单调性的进一步的结构规则：从 我们可以演绎出 。 还有从 我们可以演绎出，对于任何B， 。 在线性逻辑中有重复的假设（hypothese）'被认为'不同于单一的出现，它排除了这两个规则。而相干逻辑只排除后者的规则，因为B明显的与结论无关。 这些是结构规则的基本例子。在应用到常规命题演算的时候，这些规则是没有任何争议的。它们自然的出现于证明理论中，并在那里被首次注意到（在获得一个名字之前）。 (zh) Les logiques sous-structurelles sont des logiques mathématiques où certaines règles d'inférence ne sont pas utilisées ou ont une utilisation restreinte. En particulier, par rapport à la logique classique ou à la logique intuitionniste, il leur manque la règle de contraction qui dit peu ou prou que si on peut faire un raisonnement avec une même hypothèse invoquée deux fois, on peut faire le même raisonnement sans dupliquer cette hypothèse et la règle d'affaiblissement qui permet d'éliminer de l'ensemble des hypothèses une hypothèse inutilisée dans le raisonnement. (fr) 部分構造論理（ぶぶんこうぞうろんり、英: Substructural logic）は、通常の命題論理を弱くした論理体系群を指し、数理論理学の中でも証明理論と密接に関連する。部分構造論理は使用可能なが命題論理よりも少なく、かつ個々の部分構造論理によってその種類が異なる。構造規則の概念は自然演繹の定式化手法よりもシークエント表現に基づく。主な部分構造論理の例として、適切さの論理と線型論理がある。 シークエント計算では、証明の各行は次のように記される。 ここでの構造規則とは、左辺 のシークエント（命題を表す文字列）の項書き換え規則である。一般にここの文字列は論理積と解釈される。例えば、命題 に対して、以下のようなシークエント表現 は次のように解釈される。 ( かつ ) は を含意する。 ここで、右辺 が単一の命題 であるとしたが（直観主義的なシークエントのスタイル）、全ての操作はターンスタイル記号の左側で行われるので、一般のケースにも当てはまる。 論理積には交換法則と結合法則が成り立つので、シークエント を書き換える構造規則にも同じ法則に対応したもの（転置規則）がある。例えば、 から を導くことができる。他にも冪等に対応した規則（縮約規則）と単調性に対応した規則（弱化規則）が存在する。 から、次を導くことができる（縮約規則）。 また から任意の B を加えて を導くこともできる（弱化規則）。 (ja) Em lógica, uma subestrutura lógica é uma falta lógica das regras estruturais usuais (p.e. da lógica clássica e intuicionista), tal como enfraquecimento, contração ou associatividade. Duas das lógicas subestruturais mais significativas são lógica de relevância e lógica linear. No cálculo de sequentes, se escreve cada linha de uma prova como . Aqui as regras são regras estruturais para reescrever os Γ de um sequente, inicialmente concebido como um string de proposições. A interpretação padrão desta string é como conjunção: nós devemos ler como a notação sequente para (A e B) implica C. de . . . (pt) |
| rdfs:label | Substructural logic (en) Logiques sous-structurelles (fr) 部分構造論理 (ja) Lógica subestrutural (pt) 亚结构逻辑 (zh) |
| owl:sameAs | freebase:Substructural logic wikidata:Substructural logic dbpedia-fr:Substructural logic dbpedia-ja:Substructural logic dbpedia-pt:Substructural logic dbpedia-zh:Substructural logic https://global.dbpedia.org/id/4ze3Q |
| prov:wasDerivedFrom | wikipedia-en:Substructural_logic?oldid=1073310284&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Substructural_logic |
| is dbo:wikiPageRedirects of | dbr:Substructural_Logics dbr:Substructural_logics |
| is dbo:wikiPageWikiLink of | dbr:Monotonicity_of_entailment dbr:Jon_Michael_Dunn dbr:Deviant_logic dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(R–Z) dbr:Ivan_Orlov_(philosopher) dbr:List_of_mathematical_logic_topics dbr:List_of_rules_of_inference dbr:Substructural_type_system dbr:Structural_proof_theory dbr:Structural_rule dbr:Linear_logic dbr:Fuzzy_concept dbr:Kappa_calculus dbr:Natural_deduction dbr:Proof_theory dbr:Relevance_logic dbr:Greg_Restall dbr:Łukasiewicz_logic dbr:Absorption_law dbr:Affine_logic dbr:Johan_van_Benthem_(logician) dbr:BL_(logic) dbr:Bunched_logic dbr:Carlo_Dalla_Pozza dbr:Categorial_grammar dbr:Sequent_calculus dbr:Monoidal_t-norm_logic dbr:Sequent dbr:Implicit_computational_complexity dbr:Residuated_lattice dbr:T-norm_fuzzy_logics dbr:Outline_of_logic dbr:Outline_of_philosophy dbr:Substructural_Logics dbr:Substructural_logics |
| is foaf:primaryTopic of | wikipedia-en:Substructural_logic |