Intuitionistic logic (original) (raw)
Intuitionismus bezeichnet unterschiedliche philosophische, mathematische und teilweise auch psychologische Positionen, die der Intuition eine Priorität einräumen. Oftmals wird dabei vorausgesetzt, dass bestimmte Sachverhalte unmittelbar erkannt oder bewiesen werden. Zu unterscheiden sind hauptsächlich Wortverwendungen in der Erkenntnistheorie, der und Metaethik sowie ein mathematischer und logischer Intuitionismus.
| Property | Value |
|---|---|
| dbo:abstract | Intuicionistická logika je druh logiky, který nepoužívá princip vyloučeného třetího. Pravdivostní hodnoty 0 a 1 v ní znamenají „není možno zkonstruovat“ a „je možno zkonstruovat“. Na rozdíl od běžné (například aristotelské) logiky neplatí princip negace negace. Například implikace: Něco nemůže neexistovat ⇒ musí to existovat v intuicionistické logice obecně neplatí. Taková implikace je použita například při důkazu věty z matematické analýzy, podle níž z každé omezené posloupnosti lze vybrat konvergentní podposloupnost. Nemožnost takového výběru lze snadno dovést do sporu. Z hlediska intuicionistické logiky je ale takový důkaz chybný, protože nedává obecný návod ke konstrukci limity takové posloupnosti v konečném počtu kroků. Intuicionistická logika úzce souvisí s teorií vyčíslitelnosti. Pravdivost v intuicionistické logice lze ztotožnit s algoritmickou řešitelností. Sémantiku intuicionistické logiky zachycuje Heytingova algebra. (cs) Intuicia logiko aŭ intuiciisma logiko, foje pli ĝenerale nomita konstrua logiko, referencas al sistemoj de simbola logiko kiuj diferencas el la sistemoj uzataj por klasika logiko per pli fermita montrado de la nocio de konstrua pruvaro. Partikulare, sistemoj de intuicia logiko ne inkludas la leĝon de la ekskludita mezo kaj la nuligon de la duobla neado, kiuj estas fundamentaj reguloj de la inferenco en klasika logiko. Formaligita intuicia logiko estis origine disvolvigita de Arend Heyting por havigi formalan bazon por la programo de intuiciismo de Luitzen Egbertus Jan Brouwer. El pruvteoria perspektivo, la kalkuloj de Heyting estas limigo de klasika logiko en kiu la leĝo de la ekskludita mezo kaj la nuligo de la duobla neado estis forigitaj. La ekskludita mezo kaj la nuligo de la duobla neado povas ankoraŭ esti pruvataj por kelkaj propozicioj en ia kazo pre de kazbazo, tamen, sed tio ne estu universala kiel ĉe la klasika logiko. (eo) Intuitionismus bezeichnet unterschiedliche philosophische, mathematische und teilweise auch psychologische Positionen, die der Intuition eine Priorität einräumen. Oftmals wird dabei vorausgesetzt, dass bestimmte Sachverhalte unmittelbar erkannt oder bewiesen werden. Zu unterscheiden sind hauptsächlich Wortverwendungen in der Erkenntnistheorie, der und Metaethik sowie ein mathematischer und logischer Intuitionismus. (de) La lógica intuicionista, o lógica constructivista, es el sistema lógico originalmente desarrollado por Arend Heyting para proveer una base formal para el proyecto intuicionista de Brouwer. El sistema enfatiza las pruebas, en vez de la verdad, a lo largo de las transformaciones de las proposiciones. La lógica intuicionista rechaza el principio del tercero excluido, pero conserva el principio de explosión. Esto se debe a una observación de Brouwer de que si enfatizamos las pruebas en vez de la verdad, entonces en los conjuntos infinitos el principio del tercero excluido falla cuando se aplica a una proposición para la que no existe demostración, ni de su verdad ni de su falsedad. En los conjuntos finitos siempre es posible verificar si una proposición es cierta o falsa; en los infinitos, no. (es) Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic. Formalized intuitionistic logic was originally developed by Arend Heyting to provide a formal basis for L. E. J. Brouwer's programme of intuitionism. From a proof-theoretic perspective, Heyting’s calculus is a restriction of classical logic in which the law of excluded middle and double negation elimination have been removed. Excluded middle and double negation elimination can still be proved for some propositions on a case by case basis, however, but do not hold universally as they do with classical logic. The standard explanation of intuitionistic logic is the BHK interpretation. Several systems of semantics for intuitionistic logic have been studied. One of these semantics mirrors classical Boolean-valued semantics but uses Heyting algebras in place of Boolean algebras. Another semantics uses Kripke models. These, however, are technical means for studying Heyting’s deductive system rather than formalizations of Brouwer’s original informal semantic intuitions. Semantical systems claiming to capture such intuitions, due to offering meaningful concepts of “constructive truth” (rather than merely validity or provability), are Kurt Gödel’s dialectica interpretation, Stephen Cole Kleene’s realizability, Yurii Medvedev’s logic of finite problems, or Giorgi Japaridze’s computability logic. Yet such semantics persistently induce logics properly stronger than Heyting’s logic. Some authors have argued that this might be an indication of inadequacy of Heyting’s calculus itself, deeming the latter incomplete as a constructive logic. (en) La logique intuitionniste est une logique qui diffère de la logique classique par le fait que la notion de vérité est remplacée par la notion de preuve constructive. Une proposition telle que « la constante d'Euler-Mascheroni est rationnelle ou la constante d'Euler-Mascheroni n'est pas rationnelle » n'est pas démontrée de manière constructive (intuitionniste) dans le cadre de nos connaissances mathématiques actuelles, car la tautologie classique « P ou non P » (tiers exclu) n'appartient pas à la logique intuitionniste. La logique intuitionniste établit, entre autres, un distinguo entre « être vrai » et « ne pas être faux » (formulation plus faible) car ¬¬P → P n'est pas non plus démontrable en logique intuitionniste. (fr) 논리학에서 직관 논리(直觀論理, 영어: intuitionistic logic)는 수학적 직관주의에 근거하여 귀류법을 배척하는 논리 체계이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만 그 역은 일반적으로 성립하지 않는 특징이있다.이처럼 직관주의 논리학은 이중부정의 일부법칙이 성립하지 않는다. (ko) Logika intuicjonistyczna (konstruktywna) – system logiczny oparty na filozoficznej koncepcji intuicjonizmu. Za prekursora formalizacji logiki intuicjonistycznej uważa się Arenda Heytinga. Podstawową cechą logiki intuicjonistycznej jest założenie, że prawdziwość zdania jest oparta na istnieniu dla niego dowodu, a nie na wartościowaniu poszczególnych jego składowych. Z tego powodu logika intuicjonistyczna odrzuca m.in. prawo wyłączonego środka, silne prawo podwójnego przeczenia, , jedno z praw czy pierwsze prawo de Morgana. Wynikiem tych zabiegów jest w szczególności rezygnacja z dwu-, a wręcz skończonej wartościowości logiki (tw. o braku skończonej dla intuicjonizmu zdaniowego). (pl) 直観主義論理（ちょっかんしゅぎろんり、英: intuitionistic logic）または直観論理（ちょっかんろんり）、あるいは構成的論理（こうせいてきろんり、英: constructive logic）とは、ある種の論理体系であり、伝統的な真理値の概念がの概念に置き換わっている点で古典論理とは異なる。例えば古典論理では、全ての論理式に真か偽の真理値 が割り当てられる。このときその真理値に対する直接的なエビデンスを持つか否かは問題にしない。これはどのような曖昧な命題においても「真か偽かが決定可能である」ということを意味する。対照的に直観主義論理では確定的に論理式に真理値を割り当てるのではなく、それが真であるとは「直接的なエビデンス」つまり「証明」があることと見做す。 証明論的な視点から見ると、直観主義論理は古典論理の制限であって排中律や二重否定除去が公理として許容されないものである。排中律や二重否定除去はいくつかの論理式に対しては個別に証明できることがあるけれども、古典論理のように普遍的に成立することはない。 直観主義論理の色々な意味論が研究されている。ひとつの意味論は古典的なを写しとったものでブール代数の代わりにハイティング代数を用いる。別の意味論ではクリプキ・モデルを用いる。 直観主義論理は実際的な有用性を持つ。何故ならばこの制限によってを持つ証明が作られるからであり、これは直観主義論理が数学的構成主義のある形態として適当なものとする。非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。 形式化された直観主義論理はアレン・ハイティングによってヤン・ブラウワーの直観主義プログラムの形式的な基礎として発展せられたものである。 (ja) La logica intuizionista (o intuizionistica), o logica costruttiva, è la logica dell'intuizionismo matematico e di altre forme di costruttivismo matematico. Secondo la prospettiva intuizionista, la logica e la matematica sono le applicazioni di metodi internamente coerenti per la realizzazione di costrutti mentali di complessità crescente. La logica intuizionista si propone come una rigorosa e formale logica matematica. Benché non sia chiaro se un calcolo logico formale esaurisca gli aspetti più spiccatamente filosofici dell'intuizionismo, esso mostra delle proprietà piuttosto utili nella pratica scientifica. (it) Интуициони́стская ло́гика — формальная система, отражающая некоторые способы рассуждений, приемлемые с точки зрения интуиционизма. Предложена А. Гейтингом в 1930. Основное отличие от привычного исчисления высказываний заключается в том, что отсутствует закон исключённого третьего. Схемы аксиом 1-10 и правило «модус поненс» задают интуиционистское исчисление высказываний. Все 12 схем аксиом и все 3 правила вывода задают интуиционистское исчисление предикатов. Интуиционистское исчисление предикатов отличается от классического тем, что в последнем вместо схемы аксиом 10 используется схема аксиом .. (ru) Den intuitionistiska logiken har sitt ursprung i intuitionismen som grundar sig på uppfattningen att existensen av ett (matematiskt) objekt endast kan fastställas genom att i någon mening konstruera objektet. I intuitionistisk logik är lagen om det uteslutna tredje inte en giltig princip, d.v.s., man kan inte i allmänhet sluta sig till att utsagan P eller icke P är sann. Idag är intuitionistisk logik inte bara tillämpad inom intuitionismen, utan även i exempelvis toposteori. (sv) Lógica intuicionista, ou lógica construtivista, é o sistema de lógica simbólica desenvolvido por Arend Heyting para prover uma base formal para o intuicionismo de Brouwer. O sistema preserva, também, a justificação, e não apenas a verdade, no processo que leva de hipóteses a proposições derivadas - se as hipóteses são verdadeiras e justificáveis então a conclusão também será verdadeira e justificável. De um ponto de vista prático, há, também, uma forte motivação para usar a lógica intuicionista, já que ela possui a propriedade existencial, tornando-a adequada para outras formas de . (pt) Інтуїтивна логіка (інколи конструктивна логіка) — система символічної логіки, яка відрізняється від класичної логіки, замінюючи традиційне поняття істини поняттям конструктивно доказової істини. Наприклад, у класичній логіці, пропозиціональні формули (предикати) завжди приймають значення істинності з множини двох тривіальних елементів тверджень («істина» і «хиба» відповідно) незалежно від того, чи є у нас прямий доказ для будь-якого випадку. Навпаки, пропозиціональним формулам (предикатам) в інтуїтивній логіці взагалі не надається жодного певного значення істинності: натомість вони вважаються «істинними» лише тоді, коли у нас є прямий доказ. (Замість «формула істинна на основі прямого доказу» можна також сказати, що формула доказом у сенсі Каррі — Говарда). Тому операції в інтуїтивній логіці зберігають , щодо доказу та доказової операції, а не оцінки істини. Недоведеним твердженням в інтуїтивній логіці не надаються проміжні значення істинності (як іноді помилково стверджується). Справді, можна довести, що у них немає третього значення істинності, що було визначено Гливенком у 1928. Замість цього вони залишаються з невідомим значенням істинності, доти, доки вони або не доведені, або не спростовані. Твердження спростовуються, виводом з них протиріччя. Наслідком цього погляду є те, що в інтуїтивної логіки немає інтерпретації як двозначної логіки, або навіть як логіки з кінцевим знаком. Попри те, що інтуїтивна логіка зберігає тривіальні судження наслідувані від класичної логіки, кожен доказ пропозиціональної формули вважається допустимим пропозиціональним значенням, таким чином, за поняттям твердження про множини, пропозиціональні формули (потенційні чи не кінцеві) — це множини особистих доказів. Семантично, інтуїтивна логіка є обмеженням класичної логіки, в якій закон виключеного третього та усунення подвійного заперечення не допускаються як аксіоми. Закон виключеного третього та усунення подвійного заперечення можуть все ще бути доведені для деяких висловлювань на індивідуальній основі, але не виконуватися універсально, як вони це робили з класичною логікою. Кілька семантик інтуїтивної логіки було вивчено. Одна семантика відбиває класичну , але використовує алгебру Гейтінга замість булевої алгебри. Інша семантика використовує модель Кріпке. Інтуїтивна логіка практично корисна, бо її обмеження створюють докази, у яких є , роблячи її також відповідною для інших форм математичного конструктивізму. Неофіційно, це означає, що, якщо у Вас є конструктивний доказ того, що об'єкт існує, то Ви можете перетворити цей конструктивний доказ в алгоритм для генерації його прикладу. Формалізована інтуїтивна логіка була спочатку розроблена Арендом Гейтінгом, щоб забезпечити формальну основу для програми інтуїтивізму Брауера. (uk) 直觉主义逻辑或构造性逻辑是最初由阿蘭德·海廷开发的为鲁伊兹·布劳威尔的数学直觉主义计划提供形式基础的符号逻辑。这个系统保持跨越生成导出命题的变换的而不是真理性。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有，这使它还适合其他形式的数学构造主义。 (zh) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Rieger-Nishimura.svg?width=300 |
| dbo:wikiPageExternalLink | http://plato.stanford.edu/entries/logic-intuitionistic/ http://teachinglogic.liglab.fr/INT1/index.php https://dx.doi.org/10.1016/j.jal.2004.07.016 https://www.oxfordhandbooks.com/view/10.1093/oxfordhb/9780195325928.001.0001/oxfordhb-9780195325928 https://www.oxfordhandbooks.com/view/10.1093/oxfordhb/9780195325928.001.0001/oxfordhb-9780195325928-e-10 http://www.illc.uva.nl/j50/contribs/troelstra/troelstra.pdf http://ftp.cs.toronto.edu/pub/bonner/papers/hypotheticals/naclp89.ps http://www.cs.le.ac.uk/people/nb118/Publications/ESSLLI'05.pdf https://web.archive.org/web/20120404002639/http:/www.phil.uu.nl/~dvdalen/articles/Blackwell(Dalen).pdf https://www.princeton.edu/~hhalvors/restricted/kripke_intuitionism.pdf |
| dbo:wikiPageID | 169262 (xsd:integer) |
| dbo:wikiPageLength | 35880 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1121794640 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Propositional_calculus dbr:Propositional_formula dbr:Saul_Kripke dbr:Modal_logic dbr:Sheffer_stroke dbr:David_Hilbert dbc:Constructivism_(mathematics) dbc:Intuitionism dbr:Relevance_theory dbr:Robert_Lee_Constable dbr:Currying dbr:University_of_Amsterdam dbr:Valery_Glivenko dbr:De_Morgan's_laws dbr:Infinite-valued_logic dbr:Inhabited_set dbr:Intermediate_logic dbr:Interpretation_(logic) dbr:Intuitionism dbr:Intuitionistic_type_theory dbr:Peirce's_law dbr:Complement_(set_theory) dbr:Conditional_(computer_programming) dbr:Coq dbr:Material_conditional dbr:Smooth_infinitesimal_analysis dbr:Kripke_frame dbr:Functionally_complete dbr:Gerhard_Gentzen dbr:Constructive_proof dbr:Theory_of_justification dbr:Brouwer-Heyting-Kolmogorov dbr:Linear_logic dbr:Logical_conjunction dbr:Stanford_Encyclopedia_of_Philosophy dbr:Stephen_Cole_Kleene dbr:Computability_logic dbr:Embedding dbr:Kripke_semantics dbr:BHK_interpretation dbr:Propositional_logic dbr:Symbolic_logic dbr:Many-valued_logic dbr:Brouwer–Hilbert_controversy dbr:Admissible_rule dbr:Truth_value dbr:Disjoint_sets dbr:Disjunctive_syllogism dbr:Game_semantics dbr:Giorgi_Japaridze dbr:Join_and_meet dbr:Minimal_logic dbr:Paraconsistent_logic dbr:Agda_(programming_language) dbr:Curry–Howard_correspondence dbr:Duality_(mathematics) dbc:Non-classical_logic dbc:Systems_of_formal_logic dbr:First-order_logic dbr:Dialectica_interpretation dbr:Dirk_van_Dalen dbr:Four_color_theorem dbr:Logical_connective dbr:Proof_by_contradiction dbr:Logical_disjunction dbr:Quantifier_(logic) dbr:Grenoble dbr:Heyting_algebra dbr:Jan_Łukasiewicz dbr:Tautology_(logic) dbr:Arend_Heyting dbc:Logic_in_computer_science dbr:Law_of_bivalence dbr:Syntax dbr:Modal_companion dbr:Modus_ponens dbr:Realizability dbr:Double_negation_elimination dbr:Boolean_algebra dbr:Boolean_algebra_(structure) dbr:Boolean_function dbr:Sole_sufficient_operator dbr:Classical_logic dbr:Constructivism_(mathematics) dbr:Interior_(topology) dbr:Kurt_Gödel dbr:Generalization_(logic) dbr:Valuation_(logic) dbr:Walter_Carnielli dbr:Evidence dbr:Finite-valued_logic dbr:Semantic_theory_of_truth dbr:Normal_modal_logic dbr:Luitzen_Egbertus_Jan_Brouwer dbr:Boolean-valued_semantics dbr:Proof-theoretic dbr:Proof_assistants dbr:Mathematical_constructivism dbr:Peirce_arrow dbr:Simply-typed_lambda_calculus dbr:Intermediate_logics dbr:Law_of_non-contradiction dbr:Law_of_the_excluded_middle dbr:Gödel–Gentzen_negative_translation dbr:Curry–Howard_isomorphism dbr:Existence_property dbr:Hilbert-style_deduction_system dbr:Logical_negation dbr:File:Rieger-Nishimura.svg |
| dbp:wikiPageUsesTemplate | dbt:Authority_control dbt:Main dbt:Portal dbt:Refbegin dbt:Refend dbt:Reflist dbt:Section_link dbt:Short_description dbt:Snd dbt:Non-classical_logic |
| dct:subject | dbc:Constructivism_(mathematics) dbc:Intuitionism dbc:Non-classical_logic dbc:Systems_of_formal_logic dbc:Logic_in_computer_science |
| rdf:type | owl:Thing yago:Abstraction100002137 yago:EducationalInstitution108276342 yago:Group100031264 yago:Institution108053576 yago:Organization108008335 yago:YagoLegalActor yago:YagoLegalActorGeo yago:YagoPermanentlyLocatedEntity yago:School108276720 yago:SocialGroup107950920 yago:WikicatPhilosophicalSchoolsAndTraditions |
| rdfs:comment | Intuitionismus bezeichnet unterschiedliche philosophische, mathematische und teilweise auch psychologische Positionen, die der Intuition eine Priorität einräumen. Oftmals wird dabei vorausgesetzt, dass bestimmte Sachverhalte unmittelbar erkannt oder bewiesen werden. Zu unterscheiden sind hauptsächlich Wortverwendungen in der Erkenntnistheorie, der und Metaethik sowie ein mathematischer und logischer Intuitionismus. (de) La logique intuitionniste est une logique qui diffère de la logique classique par le fait que la notion de vérité est remplacée par la notion de preuve constructive. Une proposition telle que « la constante d'Euler-Mascheroni est rationnelle ou la constante d'Euler-Mascheroni n'est pas rationnelle » n'est pas démontrée de manière constructive (intuitionniste) dans le cadre de nos connaissances mathématiques actuelles, car la tautologie classique « P ou non P » (tiers exclu) n'appartient pas à la logique intuitionniste. La logique intuitionniste établit, entre autres, un distinguo entre « être vrai » et « ne pas être faux » (formulation plus faible) car ¬¬P → P n'est pas non plus démontrable en logique intuitionniste. (fr) 논리학에서 직관 논리(直觀論理, 영어: intuitionistic logic)는 수학적 직관주의에 근거하여 귀류법을 배척하는 논리 체계이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만 그 역은 일반적으로 성립하지 않는 특징이있다.이처럼 직관주의 논리학은 이중부정의 일부법칙이 성립하지 않는다. (ko) Logika intuicjonistyczna (konstruktywna) – system logiczny oparty na filozoficznej koncepcji intuicjonizmu. Za prekursora formalizacji logiki intuicjonistycznej uważa się Arenda Heytinga. Podstawową cechą logiki intuicjonistycznej jest założenie, że prawdziwość zdania jest oparta na istnieniu dla niego dowodu, a nie na wartościowaniu poszczególnych jego składowych. Z tego powodu logika intuicjonistyczna odrzuca m.in. prawo wyłączonego środka, silne prawo podwójnego przeczenia, , jedno z praw czy pierwsze prawo de Morgana. Wynikiem tych zabiegów jest w szczególności rezygnacja z dwu-, a wręcz skończonej wartościowości logiki (tw. o braku skończonej dla intuicjonizmu zdaniowego). (pl) La logica intuizionista (o intuizionistica), o logica costruttiva, è la logica dell'intuizionismo matematico e di altre forme di costruttivismo matematico. Secondo la prospettiva intuizionista, la logica e la matematica sono le applicazioni di metodi internamente coerenti per la realizzazione di costrutti mentali di complessità crescente. La logica intuizionista si propone come una rigorosa e formale logica matematica. Benché non sia chiaro se un calcolo logico formale esaurisca gli aspetti più spiccatamente filosofici dell'intuizionismo, esso mostra delle proprietà piuttosto utili nella pratica scientifica. (it) Den intuitionistiska logiken har sitt ursprung i intuitionismen som grundar sig på uppfattningen att existensen av ett (matematiskt) objekt endast kan fastställas genom att i någon mening konstruera objektet. I intuitionistisk logik är lagen om det uteslutna tredje inte en giltig princip, d.v.s., man kan inte i allmänhet sluta sig till att utsagan P eller icke P är sann. Idag är intuitionistisk logik inte bara tillämpad inom intuitionismen, utan även i exempelvis toposteori. (sv) Lógica intuicionista, ou lógica construtivista, é o sistema de lógica simbólica desenvolvido por Arend Heyting para prover uma base formal para o intuicionismo de Brouwer. O sistema preserva, também, a justificação, e não apenas a verdade, no processo que leva de hipóteses a proposições derivadas - se as hipóteses são verdadeiras e justificáveis então a conclusão também será verdadeira e justificável. De um ponto de vista prático, há, também, uma forte motivação para usar a lógica intuicionista, já que ela possui a propriedade existencial, tornando-a adequada para outras formas de . (pt) 直觉主义逻辑或构造性逻辑是最初由阿蘭德·海廷开发的为鲁伊兹·布劳威尔的数学直觉主义计划提供形式基础的符号逻辑。这个系统保持跨越生成导出命题的变换的而不是真理性。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有，这使它还适合其他形式的数学构造主义。 (zh) Intuicionistická logika je druh logiky, který nepoužívá princip vyloučeného třetího. Pravdivostní hodnoty 0 a 1 v ní znamenají „není možno zkonstruovat“ a „je možno zkonstruovat“. Na rozdíl od běžné (například aristotelské) logiky neplatí princip negace negace. Například implikace: Něco nemůže neexistovat ⇒ musí to existovat v intuicionistické logice obecně neplatí. Intuicionistická logika úzce souvisí s teorií vyčíslitelnosti. Pravdivost v intuicionistické logice lze ztotožnit s algoritmickou řešitelností. Sémantiku intuicionistické logiky zachycuje Heytingova algebra. (cs) Intuicia logiko aŭ intuiciisma logiko, foje pli ĝenerale nomita konstrua logiko, referencas al sistemoj de simbola logiko kiuj diferencas el la sistemoj uzataj por klasika logiko per pli fermita montrado de la nocio de konstrua pruvaro. Partikulare, sistemoj de intuicia logiko ne inkludas la leĝon de la ekskludita mezo kaj la nuligon de la duobla neado, kiuj estas fundamentaj reguloj de la inferenco en klasika logiko. (eo) La lógica intuicionista, o lógica constructivista, es el sistema lógico originalmente desarrollado por Arend Heyting para proveer una base formal para el proyecto intuicionista de Brouwer. El sistema enfatiza las pruebas, en vez de la verdad, a lo largo de las transformaciones de las proposiciones. (es) Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic. (en) 直観主義論理（ちょっかんしゅぎろんり、英: intuitionistic logic）または直観論理（ちょっかんろんり）、あるいは構成的論理（こうせいてきろんり、英: constructive logic）とは、ある種の論理体系であり、伝統的な真理値の概念がの概念に置き換わっている点で古典論理とは異なる。例えば古典論理では、全ての論理式に真か偽の真理値 が割り当てられる。このときその真理値に対する直接的なエビデンスを持つか否かは問題にしない。これはどのような曖昧な命題においても「真か偽かが決定可能である」ということを意味する。対照的に直観主義論理では確定的に論理式に真理値を割り当てるのではなく、それが真であるとは「直接的なエビデンス」つまり「証明」があることと見做す。 証明論的な視点から見ると、直観主義論理は古典論理の制限であって排中律や二重否定除去が公理として許容されないものである。排中律や二重否定除去はいくつかの論理式に対しては個別に証明できることがあるけれども、古典論理のように普遍的に成立することはない。 直観主義論理の色々な意味論が研究されている。ひとつの意味論は古典的なを写しとったものでブール代数の代わりにハイティング代数を用いる。別の意味論ではクリプキ・モデルを用いる。 (ja) Интуициони́стская ло́гика — формальная система, отражающая некоторые способы рассуждений, приемлемые с точки зрения интуиционизма. Предложена А. Гейтингом в 1930. Основное отличие от привычного исчисления высказываний заключается в том, что отсутствует закон исключённого третьего. (ru) Інтуїтивна логіка (інколи конструктивна логіка) — система символічної логіки, яка відрізняється від класичної логіки, замінюючи традиційне поняття істини поняттям конструктивно доказової істини. Наприклад, у класичній логіці, пропозиціональні формули (предикати) завжди приймають значення істинності з множини двох тривіальних елементів тверджень («істина» і «хиба» відповідно) незалежно від того, чи є у нас прямий доказ для будь-якого випадку. Навпаки, пропозиціональним формулам (предикатам) в інтуїтивній логіці взагалі не надається жодного певного значення істинності: натомість вони вважаються «істинними» лише тоді, коли у нас є прямий доказ. (Замість «формула істинна на основі прямого доказу» можна також сказати, що формула доказом у сенсі Каррі — Говарда). Тому операції в інтуїтивній ло (uk) |
| rdfs:label | Intuicionistická logika (cs) Intuitionismus (de) Intuicia logiko (eo) Lógica intuicionista (es) Intuitionistic logic (en) Logique intuitionniste (fr) Logica intuizionista (it) 직관 논리 (ko) 直観主義論理 (ja) Logika intuicjonistyczna (pl) Интуиционистская логика (ru) Lógica intuicionista (pt) Intuitionistisk logik (sv) Інтуїціоністська логіка (uk) 直觉主义逻辑 (zh) |
| owl:sameAs | freebase:Intuitionistic logic dbpedia-de:Intuitionistic logic http://d-nb.info/gnd/4162199-2 yago-res:Intuitionistic logic wikidata:Intuitionistic logic dbpedia-cs:Intuitionistic logic dbpedia-eo:Intuitionistic logic dbpedia-es:Intuitionistic logic dbpedia-et:Intuitionistic logic dbpedia-fa:Intuitionistic logic dbpedia-fr:Intuitionistic logic http://hy.dbpedia.org/resource/Կոնստրուկտիվ_տրամաբանություն dbpedia-it:Intuitionistic logic dbpedia-ja:Intuitionistic logic dbpedia-ko:Intuitionistic logic dbpedia-mk:Intuitionistic logic http://ml.dbpedia.org/resource/അന്തഃപ്രജ്ഞ dbpedia-pl:Intuitionistic logic dbpedia-pms:Intuitionistic logic dbpedia-pt:Intuitionistic logic dbpedia-ru:Intuitionistic logic dbpedia-sv:Intuitionistic logic dbpedia-tr:Intuitionistic logic dbpedia-uk:Intuitionistic logic dbpedia-zh:Intuitionistic logic https://global.dbpedia.org/id/iLhk |
| prov:wasDerivedFrom | wikipedia-en:Intuitionistic_logic?oldid=1121794640&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Rieger-Nishimura.svg |
| foaf:isPrimaryTopicOf | wikipedia-en:Intuitionistic_logic |
| is dbo:knownFor of | dbr:Joan_Moschovakis dbr:Arend_Heyting |
| is dbo:wikiPageRedirects of | dbr:Semantics_for_intuitionistic_logic dbr:Semantics_of_intuitionistic_logic dbr:Intuitionist_logic dbr:Intuitionistic_Logic dbr:Intuitionistic_Prop_Calc dbr:Intuitionistic_propositional_calculus dbr:Constructive_logic dbr:Constructivist_logic |
| is dbo:wikiPageWikiLink of | dbr:Categorical_logic dbr:Benedict_Freedman dbr:Proof_complexity dbr:Propositional_calculus dbr:Saul_Kripke dbr:List_of_academic_fields dbr:Monad_(category_theory) dbr:Łukasiewicz–Moisil_algebra dbr:MINLOG dbr:Monoidal_category dbr:Principle_of_bivalence dbr:Deductive_reasoning dbr:Dependence_logic dbr:Dependent_type dbr:Algebraic_semantics_(mathematical_logic) dbr:Anti-realism dbr:List_of_Dutch_discoveries dbr:List_of_pioneers_in_computer_science dbr:Relevance dbr:Cut-elimination_theorem dbr:Victoria,_Lady_Welby dbr:De_Morgan's_laws dbr:Definitions_of_mathematics dbr:Double-negation_translation dbr:Double_negation dbr:Dutch_philosophy dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(I–Q) dbr:Infinite-valued_logic dbr:Inhabited_set dbr:Institution_(computer_science) dbr:Interior_algebra dbr:Intermediate_logic dbr:Interpretation_(logic) dbr:Intuition dbr:Intuition_and_decision-making dbr:Intuitionism dbr:Intuitionistic_type_theory dbr:Ivan_Orlov_(philosopher) dbr:Lindenbaum–Tarski_algebra dbr:List_of_mathematical_logic_topics dbr:List_of_mathematical_proofs dbr:Peirce's_law dbr:Timeline_of_Polish_science_and_technology dbr:Timeline_of_category_theory_and_related_mathematics dbr:Combinatory_logic dbr:Constructivism_(philosophy_of_mathematics) dbr:Craig_interpolation dbr:Material_conditional dbr:Mathematical_logic dbr:Mathematics dbr:Max_Euwe dbr:Negation dbr:Prenex_normal_form dbr:Susanne_Bobzien dbr:Second_Conference_on_the_Epistemology_of_the_Exact_Sciences dbr:Classifying_space dbr:Alexander_Zinoviev dbr:Glossary_of_areas_of_mathematics dbr:Constructive_analysis dbr:Constructive_set_theory dbr:Continuation-passing_style dbr:Continuum_hypothesis dbr:Contradiction dbr:Contraposition dbr:Ordinal_analysis dbr:Andrey_Kolmogorov dbr:Andrzej_Grzegorczyk dbr:Anne_Sjerp_Troelstra dbr:Linear_logic dbr:Logic dbr:Calculus_of_constructions dbr:Call-with-current-continuation dbr:Simply_typed_lambda_calculus dbr:Stephen_Cole_Kleene dbr:Computability_logic dbr:Friedman_translation dbr:Harrop_formula dbr:Kripke_semantics dbr:Leon_Henkin dbr:Many-valued_logic dbr:Markov's_principle dbr:Admissible_rule dbr:Truth dbr:Truth_value dbr:Type_theory dbr:Disjunctive_syllogism dbr:Distributive_lattice dbr:Drinker_paradox dbr:Fuzzy_logic dbr:Game_semantics dbr:Giorgi_Japaridze dbr:Gödel's_completeness_theorem dbr:Hausdorff_space dbr:Is_Logic_Empirical? dbr:Joan_Moschovakis dbr:Lambda-mu_calculus dbr:Law_of_excluded_middle dbr:Law_of_thought dbr:Law_of_trichotomy dbr:Logical_intuition dbr:Logics_for_computability dbr:Minimal_logic dbr:Paraconsistent_logic dbr:No-cloning_theorem dbr:Three-valued_logic dbr:Algebraic_logic dbr:Curry–Howard_correspondence dbr:Edmund_Husserl dbr:False_(logic) dbr:Field_of_sets dbr:Finite_set dbr:First-order_logic dbr:Brouwer_fixed-point_theorem dbr:Brouwer–Heyting–Kolmogorov_interpretation dbr:Dialectica_interpretation dbr:Dialetheism dbr:Dialogical_logic dbr:Dick_de_Jongh dbr:Discrete_mathematics dbr:Focused_proof dbr:History_of_logic dbr:History_of_topos_theory dbr:Logical_connective dbr:Proof_by_contradiction dbr:List_of_Hilbert_systems dbr:List_of_PSPACE-complete_problems dbr:Natural_deduction dbr:Possibility_theory dbr:Proof_theory dbr:Haskell_Curry dbr:Heyting_algebra dbr:Hilbert_system dbr:Involution_(mathematics) dbr:Tautology_(logic) dbr:Hypersequent dbr:Hypothetical_syllogism dbr:Arend_Heyting dbr:Artificial_intuition dbr:Absorption_law dbr:Abstract_algebraic_logic dbr:Heyting_arithmetic dbr:Modal_companion dbr:System_F dbr:B,_C,_K,_W_system dbr:Boolean-valued_model dbr:Boolean_algebra dbr:Bunched_logic dbr:Philosophy_of_mathematics dbr:Grothendieck's_relative_point_of_view dbr:Infinitesimal dbr:Kurt_Gödel dbr:Metamath dbr:Carlo_Dalla_Pozza dbr:Category_theory dbr:Semantics_for_intuitionistic_logic dbr:Semantics_of_intuitionistic_logic dbr:Sergei_N._Artemov dbr:Set_theory dbr:Oskar_Becker dbr:Proof_calculus dbr:Sequent_calculus dbr:Monoidal_t-norm_logic dbr:SKI_combinator_calculus dbr:Sequent dbr:Sheaf_(mathematics) dbr:Neil_Tennant_(philosopher) dbr:Universal_set dbr:Literal_(mathematical_logic) dbr:Philosophical_logic dbr:Steiner–Lehmus_theorem dbr:Rule_of_replacement dbr:Stanisław_Jaśkowski dbr:Structural_synthesis_of_programs dbr:Type_inhabitation dbr:Existence_theorem dbr:Fitch's_paradox_of_knowability dbr:Principle_of_explosion dbr:Vacuous_truth dbr:T-norm_fuzzy_logics dbr:Intuitionist_logic dbr:Intuitionistic_Logic dbr:Non-classical_logic dbr:Philosophy_of_logic dbr:Second-order_propositional_logic dbr:Outline_of_academic_disciplines dbr:Outline_of_formal_science dbr:Outline_of_logic dbr:Outline_of_philosophy dbr:Tagged_union dbr:Significs dbr:William_Alvin_Howard dbr:Substructural_logic dbr:Intuitionistic_Prop_Calc dbr:Intuitionistic_propositional_calculus dbr:Constructive_logic dbr:Constructivist_logic |
| is dbp:knownFor of | dbr:Joan_Moschovakis dbr:Arend_Heyting |
| is foaf:primaryTopic of | wikipedia-en:Intuitionistic_logic |
