Formal system (original) (raw)
Στην λογική, ένα τυπικό σύστημα (formal system), ή λογικό σύστημα (logic system), ή απλά λογική αποτελείται από μια τυπική γλώσσα σε συδυασμό με ένα συμπερασματικό σύστημα, που αποτελείται από ένα σύνολο από συμπερασματικούς κανόνες και/ή αξιώματα. Ένα τυπικό σύστημα χρησιμοποιείται για να μια έκφραση από μια ή περισσότερες άλλες εκφράσεις που διατυπώνονται ως υποθέσεις. Οι εκφράσεις αυτές λέγονται αξιώματα, στην περίπτωση που υποτίθεται ότι είναι αληθείς, ή θεωρήματα, στην περίπτωση που παράγονται. Ένα τυπικό σύστημα μπορεί να διατυπωθεί και να μελετηθεί για τις εγγενείς του ιδιότητες, ή μπορεί να έχει στόχο την περιγραφή εξωτερικών φαινομένων.
| Property | Value |
|---|---|
| dbo:abstract | Un sistema formal o axiomàtic és un artifici matemàtic compost de símbols que s'uneixen entre si formant cadenes que, al seu torn, poden ser manipulades segons regles per produir altres cadenes. D'aquesta manera, el sistema formal és capaç de representar cert aspecte de la realitat. El terme «formalisme» s'utilitza, de vegades, com a sinònim de sistema formal, per a un determinat propòsit. Un sistema formal matemàtic consisteix en el següent: 1. * Un conjunt finit de símbols que poden ser usats per a la construcció de fórmules. 2. * Una gramàtica, és a dir, un mecanisme per a la construcció de fórmules ben formades (WFF). També s'ha de proporcionar un algorisme de decisió per conèixer si una determinada fórmula és ben formada o no. 3. * Un conjunt d'axiomes que han de ser fórmules WFF. 4. * Un conjunt de regles d'inferència. 5. * Un conjunt de teoremes. Aquest conjunt inclou tots els axiomes, més totes les WFF que poden ser derivades dels axiomes o d'altres teoremes per mitjà de les regles d'inferència. La gramàtica no necessàriament garanteix la decidibilitat de si una fórmula és teorema o no. En les ciències formals de la lògica i les matemàtiques, així com en altres disciplines relacionades, com són la informàtica, la teoria de la informació, i l'estadística, un sistema formal és una gramàtica formal usada per a la modelització de diferents propòsits. S'anomena formalització l'acte de crear un sistema formal, i es tracta d'una acció amb la qual pretenem capturar i abstreure l'essència de determinades característiques del món real, en un model conceptual expressat en un determinat llenguatge formal. En matemàtiques, les proves formals són el resultat de sistemes formals, consistents en axiomes i regles de deducció. Els teoremes poden ser obtinguts per mitjà de proves formals. Aquest punt de vista de les matemàtiques ha estat anomenat formalista, encara que moltes vegades aquest terme comporta una accepció pejorativa. En aquest sentit, David Hilbert va crear la disciplina anomenada metamatemàtica, dedicada a l'estudi dels sistemes formals, entenent que el llenguatge utilitzat per a això, anomenat metallenguatge, era diferent del llenguatge del sistema formal que es pretenia estudiar. Amb una altra denominació, el metallenguatge o llenguatge obtingut mitjançant la gramàtica formal es diu també, a vegades, llenguatge objecte. Un sistema així és la reducció d'un llenguatge formalitzat a mers símbols, llenguatge formalitzat i simbolitzat sense cap contingut material; un llenguatge reduït a mera forma que s'expressa mitjançant fórmules que reflecteixen les relacions sintàctiques entre els símbols i les regles de formació i transformació que permeten construir les fórmules del sistema i passar d'una fórmula a una altra. L'objectiu d'un sistema formal és assenyalar com a vàlides determinades cadenes. Aquestes cadenes vàlides es denominen teoremes. Per a obtenir els teoremes, es fan servir les regles de producció que converteixen una cadena en una altra. Hi ha certs teoremes inicials que no s'obtenen de cap regla, aquests són els axiomes que se suposen vàlids per definició i es converteixen en el germen de producció de teoremes. (ca) يتم تعريف النظام الشكلي بشكل واسع النطاق على أنه أي نظام تفكير تجريدي قائم على نموذج رياضيات. ويتم في الغالب النظر إلى أصول إقليدس على أنها أول نظام شكلي وعلى أنها تعرض سمات النظام الشكلي. وتعد القضية الشرطية للنظام من خلال الأساس المنطقي له هي ما تميز النظام الشكلي عن غيره مما يمكن أن تكون قد أصبحت أسسًا في نموذج تجريدي. وفي الغالب، يكون النظام الشكلي أساسًا لنظرية أكبر أو مجال أكبر ويمكن التعرف عليه من خلالهما (على سبيل المثال هندسة إقليدس) بما يتوافق مع الاستخدام في الرياضيات الحديثة مثل نظرية النموذج. ويجب أن يكون النظام الشكلي رياضيًا، وبالتالي، فإن كتاب علم الأخلاق لسبينوزا على سبيل المثال يقلد شكل أصول إقليدس. وكل نظام شكلي له لغة شكلية، تتكون من خلال رموز بدائية. وتعمل هذه الرموز على أساس قواعد تكوين محددة ويتم تطويرها من خلال الاستدلال من مجموعة من البديهيات. وبالتالي، يتكون النظام من مجموعة من الصيغ التي يتم بناؤها من خلال مجموعات نهائية من الرموز البدائية، والتي تكون عبارة عن مجموعة يتم تشكيلها من البديهيات بما يتوافق مع القواعد المحددة. وتتكون الأنظمة الشكلية في الرياضيات من العناصر التالية: 1. * مجموعة متناهية من الرموز (أي الأبجدية)، والتي يمكن استخدامها من أجل وضع الصيغ (أي السلاسل النهائية من الرموز). 2. * قواعد لغة، تحدد كيفية تكوين الصيغ جيدة التكوين (اختصارًا wff) من الرموز الموجودة في الأبجدية. ويكون من الضروري غالبًا أن يكون هناك إجراء لاتخاذ القرارات لتحديد ما إذا كانت الصيغة جيدة التكوين أم لا. 3. * مجموعة من البديهيات أو مخطط البديهيات: يجب أن تكون كل بديهية عبارة عن صيغة جيدة التكوين. 4. * مجموعة من قواعد الاستدلال. يقال إن النظام الشكلي يكون متميزًا بالاستدعاء الذاتي (أي الفاعلية) إذا كانت مجموعة البديهيات ومجموعة قواعد الاستدلال عبارة عن مجموعات يمكن تقريرها أو مجموعات شبه محددة، حسب السياق. وتستخدم بعض النظريات المصطلح الشكلية كمرادف تقريبي للنظام الشكلي، إلا أن المصطلح يستخدم كذلك للإشارة إلى نمط محدد للمصطلحات، على سبيل المثال رمز براكيت لبول ديراك. (ar) Ein formales System ist ein System von Symbolketten und Regeln. Die Regeln sind Vorschriften für die Umwandlung einer Symbolkette in eine andere, also Produktionen einer formalen Grammatik. Die Anwendung der Regeln kann dabei ohne Kenntnis der Bedeutung der Symbole, also rein syntaktisch erfolgen. Formale Systeme werden in verschiedenen wissenschaftlichen Disziplinen wie der Logik, Mathematik, Informatik und Linguistik verwendet, insbesondere um neue Aussagen aus bereits bekanntem Wissen herzuleiten. Kalkül wird oft in derselben Bedeutung wie formales System verwendet; manchmal wird unter einem Kalkül jedoch ein formales System mit bestimmten Einschränkungen verstanden. (de) Στην λογική, ένα τυπικό σύστημα (formal system), ή λογικό σύστημα (logic system), ή απλά λογική αποτελείται από μια τυπική γλώσσα σε συδυασμό με ένα συμπερασματικό σύστημα, που αποτελείται από ένα σύνολο από συμπερασματικούς κανόνες και/ή αξιώματα. Ένα τυπικό σύστημα χρησιμοποιείται για να μια έκφραση από μια ή περισσότερες άλλες εκφράσεις που διατυπώνονται ως υποθέσεις. Οι εκφράσεις αυτές λέγονται αξιώματα, στην περίπτωση που υποτίθεται ότι είναι αληθείς, ή θεωρήματα, στην περίπτωση που παράγονται. Ένα τυπικό σύστημα μπορεί να διατυπωθεί και να μελετηθεί για τις εγγενείς του ιδιότητες, ή μπορεί να έχει στόχο την περιγραφή εξωτερικών φαινομένων. (el) Un sistema formal o sistema lógico es un sistema abstracto compuesto por un lenguaje formal, axiomas, reglas de inferencia y a veces una semántica formal, que se utiliza para deducir o demostrar teoremas y dar una definición rigurosa del concepto de demostración. Un sistema formal es una formalización rigurosa y completa del concepto de sistema axiomático, los cuales se pueden expresar en lenguaje formal o en lenguaje natural formalizado. Al crear un sistema formal se pretende capturar y abstraer la esencia de determinadas características del mundo real, en un modelo conceptual expresado en un determinado lenguaje formal. Algunos de los sistemas formales más conocidos son la lógica proposicional, la lógica de primer orden y la lógica modal. En la teoría de la demostración, las demostraciones formales se pueden expresar en el lenguaje de los sistemas formales, consistentes en axiomas y reglas de inferencia. Los teoremas pueden ser obtenidos por medio de demostraciones formales. Este punto de vista de las matemáticas ha sido denominado formalista; aunque en muchas ocasiones este término conlleva una acepción peyorativa. En ese sentido, David Hilbert creó la metamatemática para estudiar los sistemas formales, entendiendo que el lenguaje utilizado para ello, denominado metalenguaje era distinto del lenguaje del sistema formal que se pretendía estudiar, al que se llama lenguaje objeto. Un sistema así es la reducción de un lenguaje formalizado a meros símbolos, lenguaje formalizado y simbolizado sin contenido material alguno; un lenguaje reducido a mera forma que se expresa mediante fórmulas que reflejan las relaciones sintácticas entre los símbolos y las reglas de formación y transformación que permiten construir las fórmulas del sistema y pasar de una fórmula a otra. Una teoría axiomática es un conjunto de fórmulas en un determinado lenguaje formal y todas las fórmulas deducibles de dichas expresiones mediante las reglas de inferencia posibles en dicho sistema formal. El objetivo de las teorías axiomáticas es construir sistemas formales que representen las características esenciales de ramas enteras de las matemáticas. Si se selecciona un conjunto más amplio o menos amplio de axiomas el conjunto de teoremas deducibles cambian. El interés de la teoría de modelos es que en un modelo en que satisfagan los axiomas de determinada teoría también se satisfacen los teoremas deducibles de dicha teoría. Es decir, si un teorema es deducible en una cierta teoría, entonces ese teorema es universalmente válido en todos los modelos que satisfacen los axiomas. Esto es interesante porque en principio la clase de modelos que satisface una cierta teoría es difícil de conocer, ya que las teorías matemáticas interesantes en general admiten toda clase infinita de modelos no isomorfos, por lo que su clasificación en general resulta difícilmente abordable si no existe un sistema formal y un conjunto de axiomas que caracterice los diferentes tipos de modelos. En el siglo XX, Hilbert y otros sostuvieron que la matemática es un sistema formal. Pero en 1931, Kurt Gödel demostró que ningún sistema formal con suficiente poder expresivo para capturar la aritmética de Peano puede ser a la vez consistente y completo. El teorema de la incompletitud de Gödel, junto con la demostración de Alonzo Church de que la matemática tampoco es decidible, terminó con el programa de Hilbert. Sin embargo, a pesar de sus limitaciones, el enfoque sigue siendo ampliamente usado, básicamente porque no se ha encontrado ninguna alternativa mejor al enfoque formalista de Hilbert y la pretensión de trabajar en el seno de teorías matemáticas explícitamente axiomatizadas, aun con sus limitaciones. Los sistemas formales también han encontrado aplicación dentro de la informática, la teoría de la información y la estadística. (es) A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A formal system is essentially an "axiomatic system". In 1921, David Hilbert proposed to use such a system as the foundation for the knowledge in mathematics. A formal system may represent a well-defined system of abstract thought. The term formalism is sometimes a rough synonym for formal system, but it also refers to a given style of notation, for example, Paul Dirac's bra–ket notation. (en) Un système formel est une modélisation mathématique d'un langage en général spécialisé. Les éléments linguistiques, mots, phrases, discours, etc., sont représentés par des objets finis (entiers, suites, arbres ou graphes finis…). Le propre d'un système formel est que la correction au sens grammatical de ses éléments est vérifiable algorithmiquement, c'est-à-dire que ceux-ci forment un ensemble récursif. Les systèmes formels s'opposent aux langues naturelles pour lesquels les algorithmes de traitement sont extrêmement complexes et surtout doivent évoluer dans le temps pour s'adapter aux transformations du langage. Les systèmes formels sont apparus en logique mathématique afin de représenter mathématiquement le langage et le raisonnement mathématique, mais peuvent se trouver également dans d'autres contextes : informatique, chimie… (fr) 형식 체계(形式體系, 영어: formal system)는 공리들로부터 추론 규칙들을 통해 정리를 이끌어낼 수 있는 논리적 체계를 가리킨다. 또한 이를 표기하기 위한 기호들(alphabets)과 그로부터 문장을 구성하기 위한 문법(grammar)을 필요로 한다. 형식체계는 20세기 초 수학기초론을 세우는 과정에서 성립하였으며 현대 기호논리학의 기초적 개념으로 쓰인다. 이를 모든 논리의 기초로 보는 입장을 형식주의(formalism)이라 한다. (ko) In logica matematica, la nozione di sistema formale è utilizzata per fornire una definizione rigorosa del concetto di dimostrazione. In altri termini, la nozione di sistema formale corrisponde ad una formalizzazione rigorosa e completa della nozione di sistema assiomatico. (it) 形式体系（けいしきたいけい、Formal System）は、数学のモデルに基づいた任意の well-defined な抽象思考体系と定義される。エウクレイデスの『原論』は史上初の形式体系とされることが多く、形式体系の特徴をよく表している。その論理的基盤による体系の命題と帰結の関係（論理包含）は、他の抽象モデルを何らかの基盤とする体系から形式体系を区別するものである。形式体系は大きな理論や分野（例えばユークリッド幾何学）の基盤またはそのものとなることが多く、現代数学では証明論やモデル理論などと同義に扱われる。ただし形式体系は必ずしも数学的である必然性はなく、例えばスピノザの『エチカ』はエウクレイデスの『原論』の形式を模倣した哲学（倫理学）書である。 形式体系には形式言語があり、その形式言語は基本的な記号（シンボル）で構成される。形式言語の文（式）は公理群を出発点として、所定の構成規則（推論規則）に従って発展する。従って形式体系は基本的な記号群の有限の組み合わせを通して構築された任意個の数式で構成され、その組み合わせは公理群と構成規則群から作り出される。 数学における形式体系は以下の要素から構成される: 1. * 式を構成するのに使われる有限個の記号（アルファベット）。 2. * 文法。すなわち、正しい式を記号から構成するための方法。例えば、論理学で言えば任意の式（記号を適当に並べたもの）が整式かどうかを決定する何らかの手順が存在する。 3. * 公理群または公理スキーマ。各公理は整式でなければならない。 4. * 推論規則群。 5. * 定理群。 形式体系が帰納的であるとは、公理群と推論規則群が（文脈によって）帰納的集合または帰納的可算集合である場合を意味する。 人によっては「形式主義」と「形式体系」をほぼ同義に扱うが、「形式主義」は数学や論理学以外にも適用される用語である。例えば、ポール・ディラックのブラ-ケット記法は物理学における形式主義である。 (ja) Een formeel systeem is een combinatie van een formele taal en een verzameling afleidings- of transformatieregels of axioma's die zinnen in de formele taal omzetten in nieuwe zinnen. Formele systemen worden gebruikt als formeel bewijs. Vrijwel alle formele systemen maken gebruik van de axiomatische methode om nieuwe uitdrukkingen af te leiden uit oude die eerder in het systeem zijn uitgedrukt. De oude uitdrukkingen die worden verondersteld waar te zijn worden axioma's genoemd, de nieuwe uitdrukkingen heten stellingen. Voorbeelden van formele systemen zijn de propositie-, predicaten- en andere logica's. Een formeel systeem kan zelf worden bestudeerd aan de hand van zijn intrinsieke eigenschappen, of worden gebruikt als model om externe verschijnselen mee te beschrijven. (nl) System formalny – język formuł (logiki) wraz ze zbiorem (wywodu) i zwykle zbiorem aksjomatów. Systemy formalne są tworzone i badane zarówno jako samodzielne abstrakcyjne twory, jak i systemy opisu rzeczywistości. W matematyce formalnie dowody twierdzeń konstruuje się w systemach formalnych zawierających aksjomaty oraz reguły dedukcji (wyprowadzania). Twierdzenia są wtedy „ostatnimi liniami” takich dowodów. Zbiór aksjomatów i wszystkich możliwych twierdzeń nazywa się domknięciem zbioru aksjomatów ze względu na wyprowadzanie. Takie podejście do matematyki nazywane jest formalizmem matematycznym. David Hilbert nazwał metamatematyką naukę badającą systemy formalne. System formalny w matematyce zawiera następujące elementy: 1. * Skończony zbiór symboli, z którego konstruowane są formuły. 2. * Gramatykę opisującą jakie formuły są poprawnie skonstruowane i pozwalającą zweryfikować poprawność dowolnej formuły. 3. * Zbiór aksjomatów, będących poprawnie skonstruowanymi formułami. 4. * Zbiór reguł wyprowadzania. 5. * Zbiór twierdzeń zawierający wszystkie aksjomaty oraz wszystkie poprawnie skonstruowane formuły, które da się wyprowadzić z aksjomatów za pomocą reguł wyprowadzania. Należy pamiętać, że nawet jeżeli dana formuła jest poprawną formułą systemu, to nie oznacza to, że istnieje procedura decyzyjna określająca, czy jest ona twierdzeniem. (pl) Um sistema formal ou sistema lógico é, por assim dizer, qualquer sistema de pensamento abstrato bem definido, em um modelo matemático. Tecnicamente, Os Elementos de Euclides, com um modelo consistindo de 23 definições e 10 postulados/axiomas publicados em 13 livros de teoremas com provas, é frequentemente considerado o primeiro sistema formal e mostra as características de um sistema formal. A implicação de um sistema por sua base lógica é o que distingue o sistema formal de outros que podem ter alguma base em um modelo abstrato. Muitas vezes, o sistema formal será a base, ou será identificado por si só, como uma teoria maior ou um campo consistente com o uso da matemática moderna, como a teoria dos modelos. (pt) Форма́льная систе́ма (форма́льная тео́рия, аксиоматическая теория, аксиоматика, дедуктивная система) — результат строгой формализации теории, предполагающей полную абстракцию от смысла слов используемого языка, причём все условия, регулирующие употребление этих слов в теории, явно высказаны посредством аксиом и правил, позволяющих вывести одну фразу из других. Формальная система — это совокупность абстрактных объектов, не связанных с внешним миром, в которой представлены правила оперирования множеством символов в строго синтаксической трактовке без учёта смыслового содержания, то есть семантики.Строго описанные формальные системы появились после того, как была поставлена задача Гильберта. Первые ФС появились после выхода книг Рассела и Уайтхеда «Формальные системы»[уточнить]. Этим ФС были предъявлены определенные требования. (ru) Ett formellt system, även kallat axiomatiskt system, är ursprungligen en symbolisk representation av en matematisk teori. En uppsättning axiom formuleras i ett begränsat symboliskt språk och med hjälp av bestämda härledningsregler kan därefter vissa formler härledas. Sådana härledbara formler kallas teorem. Även axiomen själva räknas som teorem. Det finns formella system för första ordningens logik, satslogik, modallogik, relationell logik etc. Det finns också formella system, som ZF och ZFC, som formaliserar mängdteori genom att omfatta både första ordningens logik och ett antal mängdteoretiska axiom. Inget hindrar att man skapar ett formellt system utan att ha en matematisk teori i åtanke. Det formella systemet har då en närmast kombinatorisk tolkning. Ett exempel på ett sådant system är om man tar följande formler som axiom: 1. * AB 2. * CB och inför följande "härledningsregler": 1. * På alla ställen där det står B får man lägga till B direkt efter. 2. * Man får ta bort C var man vill. Då är "formeln" BBB härledbar: CB -(H1)→ CBB -(H1)→ CBBB -(H2)→ BBB Den här typen av formella system har visst intresse i datorvetenskap och som verktyg inom matematisk logik, men det filosofiska intresset är begränsat. (sv) 在邏輯與數學中，一個形式系統（英語：Formal system）是由兩個部分組成的，一個形式语言加上一個推理規則或轉換規則的集合。大衛·希爾伯特在1921年推动以形式系統来描述数学知识。 一個形式系統也許是純粹抽象地制定出來，只是為了研究其自身。另一方面，也可能是為了描述真實現象或客觀現實的領域而設計的。命題邏輯是最简单的形式系統。 (zh) Форма́льна систе́ма (форма́льна тео́рія, аксіомати́чна тео́рія, англ. formal system) — результат строгої формалізації теорії, яка передбачає повну абстракцію від сенсу слів мови, що використовується, причому всі умови, що регулюють вживання цих слів у теорії, явно висловлено за допомогою аксіом і правил, що дозволяють вивести одну фразу з інших. Формальна система — це сукупність абстрактних об'єктів, не пов'язаних із зовнішнім світом, в якій представлено правила оперування множиною символів у строго синтаксичному трактуванні без врахування смислового змісту, тобто семантики. Строго описані формальні системи з'явилися після того, як було поставлено задачу розв'язності Гільберта. Перші ФС з'явилися після виходу книг Рассела та Вайтгеда «Формальні системи». Цим формальним системам було пред'явлено певні вимоги. (uk) |
| dbo:wikiPageExternalLink | http://www.cs.indiana.edu/~port/teach/641/formal.sys.haug.html http://www.earlham.edu/~peters/courses/logsys/machines.htm https://web.archive.org/web/20110524103726/http:/www.earlham.edu/~peters/courses/logsys/machines.htm https://www.britannica.com/eb/article-9034889/formal-system |
| dbo:wikiPageID | 396102 (xsd:integer) |
| dbo:wikiPageLength | 13881 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1115325710 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Propositional_calculus dbr:Pāṇini dbr:Rules_of_inference dbr:Modal_logic dbr:Model_theory dbr:Metamathematics dbr:Metatheorem dbr:Nonnegative_integer dbr:Belief dbr:Bra–ket_notation dbr:David_Hilbert dbr:Deductive_reasoning dbr:Paul_Dirac dbr:Peano_axioms dbr:Decidability_(logic) dbr:Interpretation_(logic) dbr:Notation dbr:Mathematical_logic dbr:Mathematics dbr:Generative_grammar dbr:George_Boole dbr:Gottlob_Frege dbr:Theorem dbr:Theory dbr:Theory_of_justification dbc:1st-millennium_BC_introductions dbr:Alphabet_(computer_science) dbr:Stephen_Cole_Kleene dbr:Completeness_(logic) dbr:Computer_science dbr:String_(computer_science) dbr:Symbol_(formal) dbr:Augustus_De_Morgan dbr:Truth dbr:Linguistics dbr:Non-standard_model_of_arithmetic dbr:Abstract_structure dbr:Abstraction dbr:Europe dbr:First-order_logic dbr:Formal_language_theory dbr:Formal_grammar dbr:Formal_language dbr:Formal_proof dbr:Formal_science dbr:Gongsun_Long dbr:Entailment dbr:Well-formed_formula dbr:Mathematical_proof dbr:Gödel's_incompleteness_theorems dbc:Syntax_(logic) dbc:Formal_languages dbr:Lambda_calculus dbr:Syntax dbr:Theory_(mathematical_logic) dbr:Domain_of_discourse dbr:Douglas_Hofstadter dbr:Axiom dbr:Axiom_schema dbr:Axiomatic_system dbc:4th_century_BC_in_India dbc:Formal_systems dbc:Metalogic dbr:Philosophy_of_mathematics dbr:Intended_interpretation dbr:Metalanguage dbr:Recursive_set dbr:Recursively_enumerable_set dbr:Set_(mathematics) dbr:Predicate_calculus dbr:Rule_of_inference dbr:Semantics dbr:Semantics_of_logic dbr:Soundness dbr:Euclidean_geometry dbr:Rules_of_formation dbr:Analytic_grammar dbr:Syntactic_consequence dbr:Formal_method dbr:Formula_(mathematical_logic) dbr:Raymond_M._Smullyan dbr:Rewriting_system dbr:Decidable_set dbr:Gödel,_Escher,_Bach:_An_Eternal_Golden_Braid dbr:Model_(model_theory) dbr:Substitution_instance |
| dbp:date | 2011-05-24 (xsd:date) September 2017 (en) |
| dbp:reason | This section doesn't really do a group job stating what an entailment actually is. (en) |
| dbp:url | https://web.archive.org/web/20110524103726/http:/www.earlham.edu/~peters/courses/logsys/machines.htm |
| dbp:wikiPageUsesTemplate | dbt:Clarify dbt:Commons_category-inline dbt:Div_col dbt:Div_col_end dbt:Expand_section dbt:ISBN dbt:Main dbt:Portal dbt:Reflist dbt:Short_description dbt:Webarchive dbt:Wiktionary dbt:Systems dbt:Mathematical_logic dbt:Computable_knowledge dbt:Foundations-footer |
| dct:subject | dbc:1st-millennium_BC_introductions dbc:Syntax_(logic) dbc:Formal_languages dbc:4th_century_BC_in_India dbc:Formal_systems dbc:Metalogic |
| rdf:type | yago:WikicatTheorems yago:Ability105616246 yago:Abstraction100002137 yago:Artifact100021939 yago:Cognition100023271 yago:Communication100033020 yago:Instrumentality103575240 yago:Know-how105616786 yago:Language106282651 yago:Message106598915 yago:Method105660268 yago:Object100002684 yago:PhysicalEntity100001930 yago:Proposition106750804 yago:PsychologicalFeature100023100 yago:Statement106722453 yago:System104377057 yago:Theorem106752293 yago:Whole100003553 yago:WikicatFormalLanguages yago:WikicatFormalMethods yago:WikicatFormalSystems |
| rdfs:comment | Στην λογική, ένα τυπικό σύστημα (formal system), ή λογικό σύστημα (logic system), ή απλά λογική αποτελείται από μια τυπική γλώσσα σε συδυασμό με ένα συμπερασματικό σύστημα, που αποτελείται από ένα σύνολο από συμπερασματικούς κανόνες και/ή αξιώματα. Ένα τυπικό σύστημα χρησιμοποιείται για να μια έκφραση από μια ή περισσότερες άλλες εκφράσεις που διατυπώνονται ως υποθέσεις. Οι εκφράσεις αυτές λέγονται αξιώματα, στην περίπτωση που υποτίθεται ότι είναι αληθείς, ή θεωρήματα, στην περίπτωση που παράγονται. Ένα τυπικό σύστημα μπορεί να διατυπωθεί και να μελετηθεί για τις εγγενείς του ιδιότητες, ή μπορεί να έχει στόχο την περιγραφή εξωτερικών φαινομένων. (el) 형식 체계(形式體系, 영어: formal system)는 공리들로부터 추론 규칙들을 통해 정리를 이끌어낼 수 있는 논리적 체계를 가리킨다. 또한 이를 표기하기 위한 기호들(alphabets)과 그로부터 문장을 구성하기 위한 문법(grammar)을 필요로 한다. 형식체계는 20세기 초 수학기초론을 세우는 과정에서 성립하였으며 현대 기호논리학의 기초적 개념으로 쓰인다. 이를 모든 논리의 기초로 보는 입장을 형식주의(formalism)이라 한다. (ko) In logica matematica, la nozione di sistema formale è utilizzata per fornire una definizione rigorosa del concetto di dimostrazione. In altri termini, la nozione di sistema formale corrisponde ad una formalizzazione rigorosa e completa della nozione di sistema assiomatico. (it) Um sistema formal ou sistema lógico é, por assim dizer, qualquer sistema de pensamento abstrato bem definido, em um modelo matemático. Tecnicamente, Os Elementos de Euclides, com um modelo consistindo de 23 definições e 10 postulados/axiomas publicados em 13 livros de teoremas com provas, é frequentemente considerado o primeiro sistema formal e mostra as características de um sistema formal. A implicação de um sistema por sua base lógica é o que distingue o sistema formal de outros que podem ter alguma base em um modelo abstrato. Muitas vezes, o sistema formal será a base, ou será identificado por si só, como uma teoria maior ou um campo consistente com o uso da matemática moderna, como a teoria dos modelos. (pt) 在邏輯與數學中，一個形式系統（英語：Formal system）是由兩個部分組成的，一個形式语言加上一個推理規則或轉換規則的集合。大衛·希爾伯特在1921年推动以形式系統来描述数学知识。 一個形式系統也許是純粹抽象地制定出來，只是為了研究其自身。另一方面，也可能是為了描述真實現象或客觀現實的領域而設計的。命題邏輯是最简单的形式系統。 (zh) يتم تعريف النظام الشكلي بشكل واسع النطاق على أنه أي نظام تفكير تجريدي قائم على نموذج رياضيات. ويتم في الغالب النظر إلى أصول إقليدس على أنها أول نظام شكلي وعلى أنها تعرض سمات النظام الشكلي. وتعد القضية الشرطية للنظام من خلال الأساس المنطقي له هي ما تميز النظام الشكلي عن غيره مما يمكن أن تكون قد أصبحت أسسًا في نموذج تجريدي. وفي الغالب، يكون النظام الشكلي أساسًا لنظرية أكبر أو مجال أكبر ويمكن التعرف عليه من خلالهما (على سبيل المثال هندسة إقليدس) بما يتوافق مع الاستخدام في الرياضيات الحديثة مثل نظرية النموذج. ويجب أن يكون النظام الشكلي رياضيًا، وبالتالي، فإن كتاب علم الأخلاق لسبينوزا على سبيل المثال يقلد شكل أصول إقليدس. (ar) Un sistema formal o axiomàtic és un artifici matemàtic compost de símbols que s'uneixen entre si formant cadenes que, al seu torn, poden ser manipulades segons regles per produir altres cadenes. D'aquesta manera, el sistema formal és capaç de representar cert aspecte de la realitat. El terme «formalisme» s'utilitza, de vegades, com a sinònim de sistema formal, per a un determinat propòsit. Un sistema formal matemàtic consisteix en el següent: (ca) A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A formal system is essentially an "axiomatic system". In 1921, David Hilbert proposed to use such a system as the foundation for the knowledge in mathematics. A formal system may represent a well-defined system of abstract thought. (en) Ein formales System ist ein System von Symbolketten und Regeln. Die Regeln sind Vorschriften für die Umwandlung einer Symbolkette in eine andere, also Produktionen einer formalen Grammatik. Die Anwendung der Regeln kann dabei ohne Kenntnis der Bedeutung der Symbole, also rein syntaktisch erfolgen. Formale Systeme werden in verschiedenen wissenschaftlichen Disziplinen wie der Logik, Mathematik, Informatik und Linguistik verwendet, insbesondere um neue Aussagen aus bereits bekanntem Wissen herzuleiten. (de) Un sistema formal o sistema lógico es un sistema abstracto compuesto por un lenguaje formal, axiomas, reglas de inferencia y a veces una semántica formal, que se utiliza para deducir o demostrar teoremas y dar una definición rigurosa del concepto de demostración. Un sistema formal es una formalización rigurosa y completa del concepto de sistema axiomático, los cuales se pueden expresar en lenguaje formal o en lenguaje natural formalizado. Al crear un sistema formal se pretende capturar y abstraer la esencia de determinadas características del mundo real, en un modelo conceptual expresado en un determinado lenguaje formal. Algunos de los sistemas formales más conocidos son la lógica proposicional, la lógica de primer orden y la lógica modal. (es) Un système formel est une modélisation mathématique d'un langage en général spécialisé. Les éléments linguistiques, mots, phrases, discours, etc., sont représentés par des objets finis (entiers, suites, arbres ou graphes finis…). Le propre d'un système formel est que la correction au sens grammatical de ses éléments est vérifiable algorithmiquement, c'est-à-dire que ceux-ci forment un ensemble récursif. (fr) 形式体系（けいしきたいけい、Formal System）は、数学のモデルに基づいた任意の well-defined な抽象思考体系と定義される。エウクレイデスの『原論』は史上初の形式体系とされることが多く、形式体系の特徴をよく表している。その論理的基盤による体系の命題と帰結の関係（論理包含）は、他の抽象モデルを何らかの基盤とする体系から形式体系を区別するものである。形式体系は大きな理論や分野（例えばユークリッド幾何学）の基盤またはそのものとなることが多く、現代数学では証明論やモデル理論などと同義に扱われる。ただし形式体系は必ずしも数学的である必然性はなく、例えばスピノザの『エチカ』はエウクレイデスの『原論』の形式を模倣した哲学（倫理学）書である。 形式体系には形式言語があり、その形式言語は基本的な記号（シンボル）で構成される。形式言語の文（式）は公理群を出発点として、所定の構成規則（推論規則）に従って発展する。従って形式体系は基本的な記号群の有限の組み合わせを通して構築された任意個の数式で構成され、その組み合わせは公理群と構成規則群から作り出される。 数学における形式体系は以下の要素から構成される: 形式体系が帰納的であるとは、公理群と推論規則群が（文脈によって）帰納的集合または帰納的可算集合である場合を意味する。 (ja) Een formeel systeem is een combinatie van een formele taal en een verzameling afleidings- of transformatieregels of axioma's die zinnen in de formele taal omzetten in nieuwe zinnen. Formele systemen worden gebruikt als formeel bewijs. Vrijwel alle formele systemen maken gebruik van de axiomatische methode om nieuwe uitdrukkingen af te leiden uit oude die eerder in het systeem zijn uitgedrukt. De oude uitdrukkingen die worden verondersteld waar te zijn worden axioma's genoemd, de nieuwe uitdrukkingen heten stellingen. (nl) Форма́льная систе́ма (форма́льная тео́рия, аксиоматическая теория, аксиоматика, дедуктивная система) — результат строгой формализации теории, предполагающей полную абстракцию от смысла слов используемого языка, причём все условия, регулирующие употребление этих слов в теории, явно высказаны посредством аксиом и правил, позволяющих вывести одну фразу из других. (ru) System formalny – język formuł (logiki) wraz ze zbiorem (wywodu) i zwykle zbiorem aksjomatów. Systemy formalne są tworzone i badane zarówno jako samodzielne abstrakcyjne twory, jak i systemy opisu rzeczywistości. System formalny w matematyce zawiera następujące elementy: Należy pamiętać, że nawet jeżeli dana formuła jest poprawną formułą systemu, to nie oznacza to, że istnieje procedura decyzyjna określająca, czy jest ona twierdzeniem. (pl) Ett formellt system, även kallat axiomatiskt system, är ursprungligen en symbolisk representation av en matematisk teori. En uppsättning axiom formuleras i ett begränsat symboliskt språk och med hjälp av bestämda härledningsregler kan därefter vissa formler härledas. Sådana härledbara formler kallas teorem. Även axiomen själva räknas som teorem. Inget hindrar att man skapar ett formellt system utan att ha en matematisk teori i åtanke. Det formella systemet har då en närmast kombinatorisk tolkning. Ett exempel på ett sådant system är om man tar följande formler som axiom: 1. * AB 2. * CB (sv) Форма́льна систе́ма (форма́льна тео́рія, аксіомати́чна тео́рія, англ. formal system) — результат строгої формалізації теорії, яка передбачає повну абстракцію від сенсу слів мови, що використовується, причому всі умови, що регулюють вживання цих слів у теорії, явно висловлено за допомогою аксіом і правил, що дозволяють вивести одну фразу з інших. Формальна система — це сукупність абстрактних об'єктів, не пов'язаних із зовнішнім світом, в якій представлено правила оперування множиною символів у строго синтаксичному трактуванні без врахування смислового змісту, тобто семантики. (uk) |
| rdfs:label | نظام شكلي (ar) Sistema formal (ca) Formales System (de) Τυπικό σύστημα (el) Sistema formal (es) Formal system (en) Système formel (fr) Sistema formale (it) 형식 체계 (ko) 形式体系 (ja) Formeel systeem (nl) System formalny (pl) Sistema formal (pt) Формальная система (ru) Formellt system (sv) Формальна система (uk) 形式系統 (zh) |
| owl:sameAs | freebase:Formal system yago-res:Formal system wikidata:Formal system dbpedia-als:Formal system dbpedia-ar:Formal system dbpedia-ca:Formal system http://cv.dbpedia.org/resource/Формаллĕ_тытăм dbpedia-da:Formal system dbpedia-de:Formal system dbpedia-el:Formal system dbpedia-es:Formal system dbpedia-fa:Formal system dbpedia-fr:Formal system dbpedia-gd:Formal system dbpedia-he:Formal system dbpedia-hu:Formal system http://hy.dbpedia.org/resource/Աքսիոմատիկ_մեթոդ dbpedia-it:Formal system dbpedia-ja:Formal system dbpedia-kk:Formal system dbpedia-ko:Formal system http://ky.dbpedia.org/resource/Аксиоматикалык_метод dbpedia-mk:Formal system dbpedia-ms:Formal system dbpedia-nl:Formal system dbpedia-pl:Formal system dbpedia-pt:Formal system dbpedia-ru:Formal system dbpedia-sq:Formal system dbpedia-sr:Formal system dbpedia-sv:Formal system dbpedia-uk:Formal system dbpedia-zh:Formal system https://global.dbpedia.org/id/4qDeq |
| prov:wasDerivedFrom | wikipedia-en:Formal_system?oldid=1115325710&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Formal_system |
| is dbo:wikiPageDisambiguates of | dbr:Formal |
| is dbo:wikiPageRedirects of | dbr:Deductive_system dbr:Formal_System dbr:Formal_systems dbr:Logical_system dbr:Finite_logic-system dbr:Finite_logic_system dbr:System_of_logic dbr:Systems_of_logic dbr:Formal_deduction_system dbr:Formal_logical_system dbr:Deduction_system dbr:Deductive_apparatus dbr:General_logic-system dbr:General_logic_system dbr:Logic-system dbr:Logic-systems dbr:Logic_systems dbr:Logical_calculus |
| is dbo:wikiPageWikiLink of | dbr:Begriffsschrift dbr:Principia_Mathematica dbr:Program_synthesis dbr:Proof_(truth) dbr:Proof_sketch_for_Gödel's_first_incompleteness_theorem dbr:Propositional_calculus dbr:Propositional_formula dbr:Pāṇini dbr:Science dbr:List_of_formal_language_and_literal_string_topics dbr:List_of_formal_systems dbr:Modal_logic dbr:Model_theory dbr:Multiverse dbr:Scientific_modelling dbr:Mereological_essentialism dbr:Metalogic dbr:Metamathematics dbr:Metatheorem dbr:Metatheory dbr:Sheffer_stroke dbr:On_the_Cruelty_of_Really_Teaching_Computer_Science dbr:Participant_observation dbr:Branches_of_science dbr:Algorithm dbr:Algorithmic_information_theory dbr:Antimatroid dbr:Argument_map dbr:History_of_artificial_intelligence dbr:List_of_mathematical_jargon dbr:Peter_Ludlow dbr:Reuben_Goodstein dbr:Cultural_anthropology dbr:DSRP dbr:Decidability_(logic) dbr:Deep_inference dbr:Descriptive_interpretation dbr:Destructive_dilemma dbr:Dynamical_systems_theory dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(D–H) dbr:International_Sign dbr:List_of_mathematical_logic_topics dbr:Tarski's_axioms dbr:Pseudomathematics dbr:Reasoning_system dbr:Timeline_of_artificial_intelligence dbr:Timeline_of_computing_hardware_before_1950 dbr:Timeline_of_historic_inventions dbr:What_We_Cannot_Know dbr:Crispin_Wright dbr:Material_conditional dbr:Mathematics dbr:Mathesis_universalis dbr:Gematria dbr:Ordinal_collapsing_function dbr:Systems_theory dbr:Tarski–Grothendieck_set_theory dbr:Church–Turing_thesis dbr:Effect_system dbr:Entitative_graph dbr:G._Spencer-Brown dbr:Glossary_of_artificial_intelligence dbr:Glossary_of_computer_science dbr:Glossary_of_philosophy dbr:Good_and_evil dbr:Concept dbr:Conceptual_model dbr:Conjunction_elimination dbr:Conjunction_introduction dbr:Constructive_dilemma dbr:Contour_set dbr:Correctness_(computer_science) dbr:Criteria_of_truth dbr:Theorem dbr:Theory dbr:Epsilon_calculus dbr:Proof-theoretic_semantics dbr:Logic dbr:Logical_NOR dbr:Stanisław_Leśniewski dbr:Strange_loop dbr:Commutativity_of_conjunction dbr:Completeness_(logic) dbr:Functional_predicate dbr:Functional_programming dbr:Deductive_system dbr:Kripke_semantics dbr:Leon_Henkin dbr:Paradoxes_of_set_theory dbr:Physical_symbol_system dbr:Primitive_recursive_arithmetic dbr:Process_Specification_Language dbr:Static_program_analysis dbr:Superposition_calculus dbr:Symbol_(formal) dbr:Syntax_(logic) dbr:Meaning–text_theory dbr:Admissible_rule dbr:Truth dbr:Truth_function dbr:Turing's_proof dbr:Type_theory dbr:Where_Mathematics_Comes_From dbr:Disjunction_elimination dbr:Disjunction_introduction dbr:Disjunctive_syllogism dbr:Distrust dbr:Doxastic_logic dbr:Fuzzy_concept dbr:Fuzzy_logic dbr:Gödel's_completeness_theorem dbr:Gödel_numbering dbr:Irrealism_(philosophy) dbr:Karl-Georg_Niebergall dbr:Large_countable_ordinal dbr:List_of_Boolean_algebra_topics dbr:Logic_and_dialectic dbr:Logical_cube dbr:Logical_form dbr:Logical_graph dbr:Logical_truth dbr:Robinson_arithmetic dbr:Adaptive_grammar dbr:Alan_Ross_Anderson dbr:Algorithm_characterizations dbr:4th_century_BC dbr:Curry–Howard_correspondence dbr:Evil dbr:Fallibilism dbr:Ferdinand_de_Saussure dbr:Fexpr dbr:Finite_set dbr:First-order_logic dbr:Formalism_(philosophy_of_mathematics) dbr:Diagrammatic_reasoning dbr:Dialetheism dbr:Force_dynamics dbr:Formal_methods dbr:Formal_proof dbr:Formal_science dbr:Formalism_(linguistics) dbr:Formalism_(philosophy) dbr:Foundations_of_mathematics dbr:Hilbert's_axioms dbr:Hilbert's_tenth_problem dbr:History_of_computer_science dbr:History_of_the_Church–Turing_thesis dbr:Judgment_(mathematical_logic) dbr:Kappa_calculus dbr:Kolmogorov_complexity dbr:Logical_consequence dbr:Logical_constant dbr:Logical_equivalence dbr:Scientific_formalism dbr:Primitive_notion dbr:Refinement_(computing) dbr:Syntactic_predicate dbr:Grigore_Roșu dbr:Gödel's_incompleteness_theorems dbr:Haskell_Curry dbr:Hilbert's_problems dbr:Hindley–Milner_type_system dbr:Iota_and_Jot dbr:Jacques_Bouveresse dbr:Cox's_theorem dbr:Hypothetical_syllogism dbr:Absorption_(logic) dbr:Abstract_logic dbr:Abstract_object_theory dbr:Chinese_room dbr:Kazem_Sadegh-Zadeh dbr:Lambda_calculus dbr:Language dbr:Biconditional_elimination dbr:Biconditional_introduction dbr:Block_diagram dbr:Symbol_grounding_problem dbr:Syntax dbr:System dbr:Hoare_logic dbr:Tautology_(rule_of_inference) dbr:Term_logic dbr:Theory_(mathematical_logic) dbr:Transposition_(logic) dbr:Models_of_scientific_inquiry dbr:Modus_ponens dbr:Augmented_Backus–Naur_form dbr:Axiom dbr:Axiomatic_system dbr:Philosophy_of_artificial_intelligence dbr:Philosophy_of_mathematics dbr:Plankalkül dbr:Clarity_test dbr:Class_logic dbr:Ground_expression dbr:Knowledge_economy dbr:Kurt_Gödel dbr:Metalanguage dbr:Metamath dbr:Natural-language_programming dbr:Ordinal_number dbr:Raymond_Smullyan dbr:Certainty dbr:Chaitin's_constant dbr:Calculus_(disambiguation) dbr:Sequent_calculus dbr:System_identification dbr:MU_puzzle dbr:Mathematical_universe_hypothesis dbr:Meaning_(philosophy) dbr:Model_of_hierarchical_complexity dbr:Modus_tollens dbr:Social_science dbr:Turnstile_(symbol) dbr:Undecidable_problem dbr:Wang_tile dbr:Indeterminacy_in_computation dbr:Logic_system dbr:Explorable_explanation dbr:Exportation_(logic) dbr:Expression_(mathematics) dbr:Formal dbr:Formal_System dbr:Formal_systems dbr:Formal_theory dbr:Formalization dbr:List_of_types_of_systems_theory dbr:List_of_unsolved_problems_in_philosophy dbr:Structural_synthesis_of_programs dbr:Picture_language dbr:Principle_of_explosion dbr:Society_of_Mind dbr:Non-classical_logic dbr:Non-logical_symbol dbr:Philosophy_of_logic dbr:Rules_of_Play dbr:Tarski's_undefinability_theorem dbr:Outline_of_algebraic_structures dbr:Outline_of_logic dbr:Logical_system dbr:Finite_logic-system dbr:Finite_logic_system dbr:System_of_logic dbr:Systems_of_logic dbr:Formal_deduction_system dbr:Formal_logical_system dbr:Deduction_system dbr:Deductive_apparatus dbr:General_logic-system dbr:General_logic_system dbr:Logic-system dbr:Logic-systems dbr:Logic_systems dbr:Logical_calculus |
| is foaf:primaryTopic of | wikipedia-en:Formal_system |