| dbo:abstract
|
- Proof-theoretic semantics is an approach to the semantics of logic that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the proposition or logical connective plays within the system of inference. (en)
- La sémantique de la théorie de la preuve est une approche de la sémantique formelle qui tente de localiser le sens des propositions et des connecteurs logiques non pas en termes d'interprétations, comme dans les approches tarskiennes de la sémantique, mais dans le rôle que joue la proposition ou le connecteur logique au sein du système formel. (fr)
- Semântica prova-teórica é uma abordagem para a semântica da lógica que tenta localizar o significado de proposições e conectivos lógicos não em termos de interpretações, como em abordagens tarskianas para semântica, mas no papel que a proposição ou os conectivos lógicos têm dentro do sistema de inferências. Gerhard Gentzen é o criador da semântica prova-teórica, fornecendo sua base formal na sua abordagem à eliminação por corte para o cálculo de sequentes, e algumas observações filosóficas provocativas sobre como localizar o significado de conectivos lógicos em suas regras de introdução dentro de dedução natural. A história dos teóricos da semântica prova-teórica desde então tem se dedicado a explorar as conseqüências dessas idéias. Dag Prawitz estendeu a noção de de Gentzen para a dedução natural, e sugeriu que o valor de uma prova na dedução natural pode ser entendido como a sua forma normal. Esta ideia é a base do isomorfismo de Curry-Howard, e da teoria intuicionistica de tipos. Seu princípio de inversão está no cerne da maioria das abordagens modernas à semântica prova-teórica. Michael Dummett introduziu a ideia muito fundamental da harmonia lógica, montada a partir de uma sugestão de . Resumidamente, uma linguagem, que é entendida como sendo associada com certos padrões de inferência, tem harmonia lógica se é sempre possível recuperar provas analíticas de demonstrações arbitrárias, como pode ser mostrado para o cálculo sequente por meio dos teoremas de eliminação do corte, e para dedução natural por meio de teoremas de normalização. Uma linguagem que carece de harmonia lógica irá sofrer com a existência de formas incoerentes de inferência: ela provavelmente vai ser inconsistente. (pt)
- Теоретико-доказова семантика — це підхід до семантики логіки, яка намагається знайти сенс пропозицій і логічних зв'язок не в термінах інтерпретацій, як в підходах до семантики в стилі Тарського, а в ролі, яку судження або логічна зв'язність грає в системі висновку. Ґергард Ґенцен є засновником теоретичної семантики, надаючи їй офіційну основу в своєму звіті про усунення виключення для секвенційного обчислення і деякі провокаційні філософські зауваження про те, як визначити сенс логічних зв'язок у правилах їх введення в межах природної дедукції. З тих пір історія теоретико-семантичної теорії доказів була присвячена вивченню наслідків цих ідей. поширив поняття Генцена на аналітичний доказ, природну дедукцію і припустив, що значення доказу в природному виведенні можна розуміти як його нормальний вигляд. Ця ідея лежить в основі ізоморфізму Керрі-Говарда та інтуїціоністської теорії типів. Його принцип інверсії лежить в основі більшості сучасних звітів про теоретико-семантичну теорію доказів. Майкл Дамм представив фундаментальну ідею логічної гармонії, спираючись на пропозицію . Мова, яка, як розуміється, пов'язана з певними шаблонами виведення, має логічну гармонію. Якщо завжди можна відновити аналітичні докази від довільних демонстрацій, то можна показати секвенційне обчислення за допомогою теорем виключення вирізу і для природного виведення за допомогою теорем нормування. Мова, у якій відсутня логічна гармонія, буде страждати від наявності некоректних форм виведення-це, ймовірно, буде непослідовним. (uk)
|
| rdfs:comment
|
- Proof-theoretic semantics is an approach to the semantics of logic that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the proposition or logical connective plays within the system of inference. (en)
- La sémantique de la théorie de la preuve est une approche de la sémantique formelle qui tente de localiser le sens des propositions et des connecteurs logiques non pas en termes d'interprétations, comme dans les approches tarskiennes de la sémantique, mais dans le rôle que joue la proposition ou le connecteur logique au sein du système formel. (fr)
- Semântica prova-teórica é uma abordagem para a semântica da lógica que tenta localizar o significado de proposições e conectivos lógicos não em termos de interpretações, como em abordagens tarskianas para semântica, mas no papel que a proposição ou os conectivos lógicos têm dentro do sistema de inferências. (pt)
- Теоретико-доказова семантика — це підхід до семантики логіки, яка намагається знайти сенс пропозицій і логічних зв'язок не в термінах інтерпретацій, як в підходах до семантики в стилі Тарського, а в ролі, яку судження або логічна зв'язність грає в системі висновку. (uk)
|
