First-order logic (original) (raw)

About DBpedia

منطق الرتبة الأولى (First-order logic FOL) أو المنطق الإسنادي عبارة عن نظام للمنطق الرياضي يستخدم في الرياضيات والفلسفة والذكاء الصناعي وعلوم الحاسب. وهو يستخدم في التعبير عن الجمل المنطقية بشكل غير مبهم وبهذا يخالف عن اللغات الطبيعية والتي قد تحتوي على جمل مبهمة. ذلك يسهل الاستنتاج واجراء العمليات المنطقية على الجمل أو المعادلات التي تنشاء باستخدامه.و يعتبر منطق الرتبة الأولى هو تمديد منطق القضايا (منطق العبارات) propositional logic وذلك بإضافة القياس سواء كان عالمي أو وجودي. يعتبر بمنطق الرتبة الثانية تمديد لمنطق الرتبة الأولى وذلك بإضافة القياس على المجموعات. يدعى منطق الرتبة الأولى أحيانا : بمنطق الرتبة الأولى الإسنادي أو first-order predicate calculus (FOPC.

thumbnail

Property Value
dbo:abstract منطق الرتبة الأولى (First-order logic FOL) أو المنطق الإسنادي عبارة عن نظام للمنطق الرياضي يستخدم في الرياضيات والفلسفة والذكاء الصناعي وعلوم الحاسب. وهو يستخدم في التعبير عن الجمل المنطقية بشكل غير مبهم وبهذا يخالف عن اللغات الطبيعية والتي قد تحتوي على جمل مبهمة. ذلك يسهل الاستنتاج واجراء العمليات المنطقية على الجمل أو المعادلات التي تنشاء باستخدامه.و يعتبر منطق الرتبة الأولى هو تمديد منطق القضايا (منطق العبارات) propositional logic وذلك بإضافة القياس سواء كان عالمي أو وجودي. يعتبر بمنطق الرتبة الثانية تمديد لمنطق الرتبة الأولى وذلك بإضافة القياس على المجموعات. يدعى منطق الرتبة الأولى أحيانا : بمنطق الرتبة الأولى الإسنادي أو first-order predicate calculus (FOPC. (ar) La lògica de primer ordre, també anomenada lògica de predicats o càlcul de predicats, és un sistema formal dissenyat per estudiar la inferència en els llenguatges de primer ordre. Els llenguatges de primer ordre són, al seu torn, llenguatges amb quantificador que arriben només a variables d'individu, i amb funcions els arguments de les quals són només constants o variables d'individu. La lògica de primer ordre té el poder expressiu suficient per definir a pràcticament totes les matemàtiques. Com el desenvolupament històric i les aplicacions de la lògica de primer ordre estan molt lligats a la matemàtica, en el que segueix es farà una introducció que contempli i il·lustre aquesta relació, prenent exemples tant de la matemàtica com del llenguatge natural. Primer s'introdueixen cada un dels conceptes bàsics del sistema, i després es mostra com utilitzar-los per analitzar arguments. (ca) Predikátová logika prvního řádu je používaný v matematice, filozofii, lingvistice a informatice. Často se pro její označení používá kratší a méně přesný termín predikátová logika. Predikátová logika prvního řádu se odlišuje od výrokové logiky zavedením kvantifikovaných proměnných. Teorie o určitém tématu bývá obvykle právě predikátová logika prvního řádu společně se: specifickou univerzální množinou (též. univerzem), ze které jsou brány proměnné, dále pak konečně mnoha funkcemi a predikáty nad touto množinou, a konečně množinou rekurzivních axiomů, jež jsou v rámci teorie pokládány za platné. Někdy pojmem teorie formálně rozumíme množinu vět (sentencí) zapsaných v predikátové logice. Kromě predikátové logiky prvního řádu existují logiky vyšších řádů. Tyto logiky se odlišují tím, že povolují predikáty uvnitř predikátů, kvantifikování predikátu i funkcí (případně predikátů a funkcí zároveň). U teorií predikátové logiky prvního řádu jsou predikáty svázány s teorií množin, kdežto v případě logik vyšších řádů bývají predikáty interpretovány jako množiny množin. Existuje velké množství deduktivních systémů pro predikátovou logiku prvního řádu, které jsou korektní (všechna dokazatelná tvrzení jsou pravdivá) a úplné (všechna pravdivá tvrzení jsou dokazatelná). Velký pokrok byl zaznamenán na poli automatických dokazovačů postavených právě na této logice, a to i přes její semi-rozhodnutelnost v oblasti dokazovačů. A v neposlední řadě splňuje několik vět, např. Löwenheim-Skolemovu větu nebo větu o kompaktnosti. Predikátová logika prvního řádu je nesmírně důležitá již pro samotné základy matematiky, protože je standardní logikou pro . Mnoho běžných axiomatických systémů, jako Peanova aritmetika a axiomatická teorie množin (včetně Zermel-Fraenkelovy teorie množin), lze formalizovat pomocí predikátové logiky. Zato žádná teorie prvního řádu nemá sílu plně a kategoricky popsat struktury s nekonečnou doménou, např. celá čísla nebo reálná čísla. K tomu jsou zapotřebí logiky vyšších řádů. (cs) Η λογική πρώτου βαθμού είναι μια τυπική λογική που χρησιμοποιείται στα μαθηματικά, τη φιλοσοφία, τη γλωσσολογία και την επιστήμη υπολογιστών. Συναντάται με διάφορα ονόματα, όπως κατηγορηματικός λογισμός πρώτου βαθμού ή κατηγορηματική λογική. Η πρωτοβάθμια λογική διαφέρει από την προτασιακή λογική στη χρήση ποσοτικών τελεστών: κάθε ερμηνεία της λογικής πρώτου βαθμού περιλαμβάνει ένα πεδίο τιμών όπου κυμαίνονται οι ποσοτικοί τελεστές. Υπάρχουν πολλά συμπερασματικά συστήματα για την πρωτοβάθμια λογική που είναι συνεπή (παράγουν μόνο σωστά αποτελέσματα) και πλήρη (ικανά να παράγουν οποιαδήποτε ορθή πρόταση). Αν και η σχέση λογικής συνέπειας είναι μόνο ημι-αποφασίσιμη, έχει επιτευχθεί μεγάλη πρόοδος στην αυτόματη απόδειξη θεωρημάτων για τη λογική πρώτου βαθμού. Η λογική πρώτου βαθμού ικανοποιεί επίσης αρκετά θεωρήματα μετα-λογικής που την κάνουν επιδεκτική ανάλυσης στην , όπως το και το . Η λογική πρώτου βαθμού έχει μεγάλη σημασία για τα θεμέλια των μαθηματικών, όπου αποτελεί την πρότυπη τυπική λογική για . Έχει ικανή εκφραστική ισχύ ώστε να μπορεί να διατυπώσει δύο σημαντικές μαθηματικές θεωρίες: τη και την (πρωτοβάθμια) αριθμητική Πεάνο. Εντούτοις, κανένα αξιωματικό σύστημα στην πρωτοβάθμια λογική δεν είναι αρκετά ισχυρό ώστε να περιγράψει κατηγορικά άπειρες δομές όπως οι φυσικοί αριθμοί ή η . Κατηγορικά αξιωματικά συστήματα για τέτοιες δομές μπορούν να παραχθούν σε ισχυρότερες λογικές όπως η λογική δευτέρου βαθμού. (el) Unuaranga logiko, nomita ankaŭ predikatlogiko, aŭ predikatkalkulo, estas formala sistemo desegnita por studi la inferencon en la unuarangaj lingvaĵoj.​ La unuarangaj lingvaĵoj estas siavice formalaj lingvaĵoj kun kvantigiloj kiuj atingas nur unuopajn variablojn, kaj kun predikatoj kaj funkcioj kies argumentoj estas nur konstantoj aŭ unuopaj variabloj. La logiko unuaranga havas espriman povon superan al tiu de la propozicia logiko. Logiko de supera ordo estas formo de predikatkalkulo kiu estas distingata el la unuaranga logiko pere de aldonaj kvantigiloj kaj, foje, per pli forta semantiko. (eo) Una lógica de primer orden, también llamada lógica predicativa, lógica de predicados o cálculo de predicados, es un sistema formal diseñado para estudiar la inferencia en los lenguajes de primer orden.​ Los lenguajes de primer orden son, a su vez, lenguajes formales con cuantificadores que alcanzan solo a variables de individuo, y con predicados y funciones cuyos argumentos son solo constantes o variables de individuo.​ La lógica de primer orden tiene un poder expresivo superior al de la lógica proposicional. (es) Die Prädikatenlogik erster Stufe ist ein Teilgebiet der mathematischen Logik. Sie befasst sich mit der Struktur gewisser mathematischer Ausdrücke und dem logischen Schließen, mit dem man von derartigen Ausdrücken zu anderen gelangt. Dabei gelingt es, sowohl die Sprache als auch das Schließen rein syntaktisch, das heißt ohne Bezug zu mathematischen Bedeutungen, zu definieren.Das dadurch ermöglichte Zusammenspiel von rein syntaktischen Überlegungen einerseits und semantischen Betrachtungen andererseits führt zu wichtigen Erkenntnissen, die Bedeutung für die gesamte Mathematik haben, denn diese lässt sich mittels der Zermelo-Fraenkel-Mengenlehre in der Prädikatenlogik erster Stufe formulieren. Im Unterschied zur Aussagenlogik macht die Prädikatenlogik von Quantoren Gebrauch. (de) First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic. A theory about a topic is usually a first-order logic together with a specified domain of discourse (over which the quantified variables range), finitely many functions from that domain to itself, finitely many predicates defined on that domain, and a set of axioms believed to hold about them. Sometimes, "theory" is understood in a more formal sense as just a set of sentences in first-order logic. The adjective "first-order" distinguishes first-order logic from higher-order logic, in which there are predicates having predicates or functions as arguments, or in which quantification over predicates or functions, or both, are permitted. In first-order theories, predicates are often associated with sets. In interpreted higher-order theories, predicates may be interpreted as sets of sets. There are many deductive systems for first-order logic which are both sound (i.e., all provable statements are true in all models) and complete (i.e. all statements which are true in all models are provable). Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first-order logic. First-order logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem. First-order logic is the standard for the formalization of mathematics into axioms, and is studied in the foundations of mathematics.Peano arithmetic and Zermelo–Fraenkel set theory are axiomatizations of number theory and set theory, respectively, into first-order logic.No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the natural numbers or the real line. Axiom systems that do fully describe these two structures (that is, categorical axiom systems) can be obtained in stronger logics such as second-order logic. The foundations of first-order logic were developed independently by Gottlob Frege and Charles Sanders Peirce. For a history of first-order logic and how it came to dominate formal logic, see José Ferreirós (2001). (en) Lehen mailako logika, predikatuen logika, logika kuantifikatzailea edo predikatuen kalkulua ere deitzen dena, lehen ordenako hizkuntzen inferentzia aztertzeko diseinatutako sistema formala da. Predikatuak, haien propietateak eta eragiketak aztertzen dituen logika. Aldagai eta kuantifikatzaileen bidez lan egiten du. Predikatuen logikak proposizioen barne-egitura hartzen du kontuan. Lehen ordenako lengoaiak, era berean, banakako aldagaiei bakarrik eragiten dien zenbatzaileak dituzten dira, eta argumentuak, konstanteak edo aldagai indibidualak dituzten predikatuak eta funtzioak baino ez dira. Lehen ordenako logikak, logika proposizionala baino adierazkortasun-maila altuagoa du. (eu) Le calcul des prédicats du premier ordre, ou calcul des relations, logique du premier ordre, logique quantificationnelle, ou tout simplement calcul des prédicats, est une formalisation du langage des mathématiques, proposée par Gottlob Frege, entre la fin du XIXe siècle et le début du XXe siècle. La logique du premier ordre comporte deux parties : * la syntaxe définit le vocabulaire symbolique de base ainsi que les règles permettant de construire des énoncés complexes, * la sémantique interprète ces énoncés comme exprimant des relations entre les éléments d'un domaine, également appelé modèle. Sur le plan syntaxique, les langages du premier ordre opposent deux grandes classes linguistiques : * les constituants servant à identifier ou nommer des éléments du domaine : variables, symboles de constantes, termes ; * les constituants servant à exprimer des propriétés ou des relations entre ces éléments : prédicats et formules. Un prédicat est une expression linguistique qui peut être reliée à un ou plusieurs éléments du domaine pour former une phrase. Par exemple, dans la phrase « Mars est une planète », l'expression « est une planète » est un prédicat qui est relié au nom (symbole de constante) « Mars » pour former une phrase. Et dans la phrase « Jupiter est plus grand que Mars », l'expression « est plus grand que » est un prédicat qui se relie aux deux noms, « Jupiter » et « Mars », pour former une phrase. En logique mathématique, lorsqu'un prédicat est lié à une expression, on dit qu'il exprime une propriété (telle que la propriété d'être une planète), et lorsqu'il est lié à deux ou plusieurs expressions, on dit qu'il exprime une relation (telle que la relation d'être plus grand). Ainsi on peut raisonner sur des énoncés comme « Tout est gentil » et « Il existe un tel que pour tout , est ami avec », ce qui exprimé symboliquement se traduit par la formule : et . Il convient de noter cependant que la logique du premier ordre ne contient aucune relation spécifique (comme telle relation d'ordre, d'inclusion ou d'égalité) ; en fait, il ne s'agit que d'étudier la façon dont on doit parler et raisonner avec les expressions du langage mathématique. Les traits caractéristiques de la logique du premier ordre sont : * l'utilisation de variables comme , etc. pour dénoter des éléments du domaine d'interprétation ; * l'utilisation de prédicats (ou relations) sur les éléments ; * l'utilisation de connecteurs logiques (et, ou, implique etc.) ; * l'utilisation de deux quantificateurs, l'un universel (« Quel que soit », « pour tout » noté ∀) et l'autre existentiel (« il existe au moins un … tel que », noté ∃), appliqués aux variables uniquement. Le calcul des prédicats du premier ordre égalitaire adjoint au calcul des prédicats un symbole de relation, l'égalité, dont l'interprétation est l'affirmation que deux éléments sont les mêmes, et qui est axiomatisée en conséquence. Suivant le contexte, on peut parler simplement de calcul des prédicats pour le calcul des prédicats égalitaire. On parle de logique du premier ordre par opposition aux logiques d'ordre supérieur, où l'on peut aussi appliquer les quantificateurs et les prédicats aux prédicats ou aux fonctions, en plus des variables. En outre, cet article ne traite que de la logique du premier ordre classique, mais on notera qu'il existe aussi une logique du premier ordre intuitionniste. (fr) Logika predikat tingkat pertama adalah sistem deduksi formal yang digunakan dalam matematika, filosofi, linguistika, dan ilmu komputer. Jika kalkulus proposisional membahas proposisi sederhana, LTP menambahkan predikat dan kuantor. Misalnya: * Sokrates adalah seorang manusia * Plato adalah seorang manusia Kedua kalimat di atas dalam kalkulus proposisional adalah dua proposisi yang tidak berhubungan, misalnya dilambangkan dengan p dan q. Dalam LTP, keduanya dihubungkan dengan satu sifat, yaitu Manusia(x), artinya x adalah seorang manusia. Bila x = Socrates kita mendapatkan proposisi pertama, p; dan jika x = Plato kita mendapatkan proposisi kedua, q. Contoh berikut menjabarkan perbedaan kalkulus proposisional dan LTP: * Semua manusia perlu makan * Sokrates adalah manusia * Sokrates perlu makan Dalam kalkulus proposisional, ketiga kalimat di atas diterjemahkan sebagai: * A * B * C ( artinya "maka") Ketiga kalimat di atas tidak dapat dihubungkan dalam kalkulus proposisional. Dalam LTP, kita dapat menerjemahkan ketiga kalimat itu sebagai: * * * (in) 一階述語論理（英: first-order predicate logic）とは、個体の量化のみを許す述語論理 (predicate logic) である。述語論理とは、数理論理学における論理の数学的モデルの一つであり、命題論理を拡張したものである。個体の量化に加えて述語や関数の量化を許す述語論理を二階述語論理（英: second-order predicate logic）と呼び、さらなる一般化を加えた述語論理を高階述語論理（英: higher-order predicate logic）という。本項では主に一階述語論理について解説する。二階述語論理や高階述語論理についての詳細はそれぞれの記事を参照。 (ja) Nella logica matematica, una teoria del primo ordine (o calcolo dei predicati) è un particolare sistema formale, cioè una teoria formale, in cui è possibile esprimere enunciati e dedurre le loro conseguenze logiche in modo del tutto formale e meccanico. La teoria del prim'ordine estende di fatto la logica proposizionale con l'introduzione di quantificatori esistenziali e universali, predicati, funzioni, variabili e costanti, che apportano maggiore potenza espressiva al calcolo dei predicati. Come per la logica proposizionale, la teoria del primo ordine può essere scissa in due parti separate: * la sintassi, che definisce il vocabolario simbolico di base e le regole per la costruzione di enunciati complessi, * la semantica, che interpreta questi enunciati come espressione delle relazioni tra gli elementi di un dominio, aggregati mediante un assegnamento. Un predicato è un'espressione linguistica che può essere collegata a uno o più elementi del dominio per formare una frase. Ad esempio, nella frase "Marte è un pianeta", l'espressione "è un pianeta" è un predicato che è legato al nome (un simbolo costante) "Marte" per formare una frase. Nella frase "Giove è più grande di Marte", l'espressione "è più grande di" è un predicato che collega i due nomi, "Giove" e "Marte", per formare una frase. In logica matematica, quando un predicato è legato a un'espressione, si dice che esprime una proprietà (come la proprietà di essere un pianeta nell'esempio precedente), e quando è legato a due o più espressioni, si dice che esprime una relazione (come la relazione per un pianeta di essere più grande di un altro). Così è ragionare su affermazioni come "Ogni x è bello" e "Esiste un x tale che per ogni y, x è amico di y", che simbolicamente è espresso dalla formula: . Va notato che la teoria del primo ordine non contiene in sé nessuna relazione specifica (come una relazione d'ordine, inclusione o uguaglianza). (it) 1차 논리(一次論理, 영어: first-order logic)는 원소에만 한정 기호를 가할 수 있고, 술어에는 한정 기호를 가할 수 없는 술어 논리이다. 명제 논리와 달리 변수에 대하여 한정 기호를 사용할 수 있으나, 2차 논리와 달리 변수들의 집합에 대하여 한정 기호를 사용할 수 없다. 1차 논리의 경우, (2차 논리와 달리) 괴델의 완전성 정리 · 콤팩트성 정리 · 뢰벤하임-스콜렘 정리와 같은 중요한 성질들이 성립한다. 이외에 1차 술어 논리, 1계 논리 등으로도 불린다. 간단히 술어 논리(predicate logic)라 하면 1차 논리를 가리키는 경우가 많다. (ko) Rachunek predykatów pierwszego rzędu (ang. first order predicate calculus) – system logiczny, w którym zmienna, na której oparty jest kwantyfikator, może być elementem pewnej wybranej dziedziny (zbioru), nie może natomiast być zbiorem takich elementów. Tak więc nie mogą występować kwantyfikatory typu „dla każdej funkcji z X na Y...” (gdyż funkcja jest podzbiorem X × Y), „istnieje własność p, taka że...” czy „dla każdego podzbioru X zbioru Z...”. Rachunek ten nazywa się też krótko rachunkiem kwantyfikatorów, ale często używa się też nazwy logika pierwszego rzędu (szczególnie wśród matematyków zajmujących się logiką matematyczną). Na przykład w rachunku predykatów pierwszego rzędu można zapisać zdanie „dla dowolnej liczby rzeczywistej istnieje liczba większa”, jednak nie można zapisać „każdy zbiór liczb rzeczywistych ma kres górny”, gdyż wówczas kwantyfikator ogólny musiałby przebiegać wszystkie możliwe podzbiory zbioru liczb rzeczywistych i potrzebny byłby rachunek predykatów co najmniej drugiego rzędu. Rachunek predykatów pierwszego rzędu w ogólnym przypadku nie jest rozstrzygalny (w przeciwieństwie do rachunku zdań), lecz półrozstrzygalny (czyli rekurencyjnie przeliczalny), ale jeszcze nadaje się do komputerowej analizy (co już niekoniecznie można powiedzieć o rachunku predykatów wyższych rzędów, które dopuszczają kwantyfikatory dla zbiorów). Znaczna część rozważań matematycznych może być sformalizowana na gruncie logiki pierwszego rzędu. Ponadto logika ta ma wiele własności czyniących ją bardziej użyteczną od innych logik, co ma wpływ na pewne preferowanie teorii formalizowalnych na jej gruncie. W literaturze istnieje szereg równoważnych rozwinięć tego tematu. Prezentacja przedstawiona poniżej jest do pewnego stopnia oparta na książce Martina Goldsterna i Haima Judaha. Wśród innych źródeł omawiających te zagadnienia należy wymienić podręcznik Witolda Pogorzelskiego, czy też książkę Zofii Adamowicz i Pawła Zbierskiego. Bardzo popularnym jest też opracowanie Josepha Shoenfielda. (pl) A lógica de primeira ordem (LPO), conhecida também como cálculo de predicados de primeira ordem (CPPO), é um sistema lógico que estende a lógica proposicional (lógica sentencial) e que é estendida pela lógica de segunda ordem. As sentenças atômicas da lógica de primeira ordem têm o formato P (t1,…, tn) (um predicado com um ou mais "argumentos") ao invés de serem símbolos sentenciais sem estruturas. O ingrediente novo da lógica de primeira ordem não encontrado na lógica proposicional é a quantificação: dada uma sentença φ qualquer, as novas construções e -- leia "para todo x, φ" e "para algum x, φ", respectivamente—são introduzidas. significa que φ é verdadeiro para todo valor de x e significa que há pelo menos um x tal que φ é verdadeiro. Os valores das variáveis são tirados de um universo de discurso pré-determinado. Um refinamento da lógica de primeira ordem permite variáveis de diferentes tipos, para tratar de diferentes classes de objetos. A lógica de primeira ordem tem poder expressivo suficiente para formalizar praticamente toda a matemática. Uma teoria de primeira ordem consiste em um conjunto de axiomas (geralmente finito ou recursivamente enumerável) e de sentenças dedutíveis a partir deles. A teoria dos conjuntos de Zermelo-Fraenkel é um exemplo de uma teoria de primeira ordem, e aceita-se geralmente que toda a matemática clássica possa ser formalizada nela. Há outras teorias que são normalmente formalizadas na lógica de primeira ordem de maneira independente(embora elas admitam a implementação na teoria dos conjuntos) tais como a aritmética de Peano. (pt) Första ordningens logik (FOL) är ett formellt deduktivt system som används i matematik, filosofi, lingvistik och datavetenskap. Det har ett flertal olika namn på engelska: first-order predicate calculus (FOPC), the lower predicate calculus, the language of first-order logic och predicate logic. Till skillnad från naturliga språk, som svenska, använder sig FOL av ett helt otvetydigt formellt språk som tolkas av matematiska strukturer. FOL är ett deduktivt system som går bortom satslogiken genom att tillåta kvantifiering av objekt inom en given domän. Man kan exempelvis med FOL uttrycka satsen "Varje individ har egenskapen P". Medan satslogik endast behandlar enkla propositioner så inkluderar första ordningens logik även predikat och kvantifikatorer. Inom satslogiken är de två satserna "Sokrates är en man" och "Platon är en man" helt orelaterade och uttrycks till exempel med p och q. Med FOL uttrycks dock båda dessa satser med samma predikat: Man(x) där Man(x) betyder att x är en man. När x=Sokrates får vi den första satsen, p, och när x=Platon får vi den andra satsen, q. Detta språk blir mycket kraftfullt då man introducerar kvantifikatorer, då man kan uttrycka satser som "för varje x...", som i "för varje x gäller det att, om Man(x), så...". Utan kvantifikatorer är varje giltigt argument i FOL även giltigt i satslogik och vice versa. En första ordningens teori består av en uppsättning axiom (vanligtvis ändlig eller rekursivt räknebar) och de uttryck som går att deducera från dem givet ett antal regler för giltig deduktion inom systemet. Ett första ordningens språk har tillräcklig uttryckskraft för att formalisera två viktiga matematiska teorier: Zermelo-Fraenkels mängdteori och Peanos axiom (första ordningens). Ett första ordningens språk kan emellertid inte kategoriskt uttrycka uppräknelighet. Det kan uttryckas kategoriskt med andra ordningens logik. (sv) Логика первого порядка — формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций и предикатов. Расширяет логику высказываний. Помимо логики первого порядка существуют также логики высших порядков, в которых кванторы могут применяться не только к переменным, но и к предикатам. Термины логика предикатов и исчисление предикатов могут означать как логику первого порядка, так и логики первого и высшего порядка вместе; в первом случае иногда говорится о чистой логике предикатов или чистом исчислении предикатов. (ru) Логіка першого порядку (числення предикатів) — це формальна система в математичній логіці, в якій допускаються висловлення відносно змінних, фіксованих функцій, і предикатів. Є розширенням логіки висловлювань. В свою чергу є частковим випадком . (uk) 一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统，也可以稱為：一阶斷言演算、低階斷言演算、量化理論或谓词逻辑。一階邏輯和命題邏輯的不同之處在於，一階邏輯包含量詞。 高階邏輯和一階邏輯不同之處在於，高階邏輯的斷言符號可以有斷言符號或函數符號當做引數，且容許斷言量詞或函數量詞。在一階邏輯的語義中，斷言被解釋為關係。而高階邏輯的語義裡，斷言則會被解釋為集合的集合。 在通常的語義下，一階邏輯是可靠（所有可證的敘述皆為真）且完備（所有為真的敘述皆可證）。雖然一階邏輯的只是半可判定性的，但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的定理，如勒文海姆–斯科倫定理及緊緻性定理。 一階邏輯是數學基礎中很重要的一部份。許多常見的公理系統，如一階皮亞諾公理、冯诺伊曼-博内斯-哥德尔集合论和策梅洛-弗蘭克爾集合論都是一階理論。然而一階邏輯不能控制其無窮模型的基數大小，因根據勒文海姆–斯科倫定理和康托爾定理，可以構造出一種＂病態＂集合論模型，使整個模型可數，但模型內卻會覺得自己有「不可數集」。類似地，可以證明實數系的普通一階理論既有可數模型又有不可數模型。這類的悖論被稱為斯科倫悖論。但一階的直覺主義邏輯裡，勒文海姆–斯科倫定理不可證明，故不會有以上之現象。 (zh)
dbo:thumbnail wiki-commons:Special:FilePath/Prop-tableau-4.svg?width=300
dbo:wikiPageExternalLink http://john.fremlin.de/schoolwork/logic/index.html http://www.fecundity.com/logic/ http://www.umsu.de/logik/trees/ http://plato.stanford.edu/entries/logic-classical/ http://us.metamath.org/index.html http://jstor.org/stable/2687794 http://www.ltn.lv/~podnieks/ https://books.google.com/books%3Fid=4sbSBwAAQBAJ&printsec=frontcover&hl=iw&source=gbs_ge_summary_r&cad=0%23v=onepage&q&f=false%7C''Mathematical https://books.google.com/books%3Fid=b0Fvrw9tBcMC&pg=PA5 https://books.google.com/books%3Fid=nV4zAsWAvT0C&printsec=frontcover%23v=onepage&q=%22first-order%20logic%22&f=false https://doi.org/10.1007/978-1-4684-9452-5
dbo:wikiPageID 10983 (xsd:integer)
dbo:wikiPageLength 91748 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID 1124506241 (xsd:integer)
dbo:wikiPageWikiLink dbr:Power_set dbr:Principia_Mathematica dbr:Prolog dbr:Proof_assistant dbr:Propositional_calculus dbr:Elementary_class dbr:Entscheidungsproblem dbr:Mizar_system dbr:Modal_logic dbr:Model_theory dbr:Löwenheim_number dbr:Metalogic dbr:Sheffer_stroke dbr:Universal_quantification dbr:Principles_of_Mathematical_Logic dbr:Universal_closure dbr:Nonstandard_model dbr:David_Hilbert dbr:Algorithm dbr:Aristotelian_logic dbr:Paul_Halmos dbr:Peano_arithmetic dbr:Relational_algebra dbr:Republic_(Plato) dbr:Resolution_(logic) dbr:Cylindric_algebra dbr:Decidability_(logic) dbr:Decision_problem dbr:Interpretation_(logic) dbr:Intuitionistic_logic dbr:Prior_Analytics dbr:Universal_quantifier dbr:Lindenbaum–Tarski_algebra dbr:List_of_logic_symbols dbr:Quantification_(logic) dbr:Consistency dbr:Context-free_grammar dbr:Countable_set dbr:Counting_quantifiers dbr:Material_conditional dbr:Mathematical_proofs dbr:Mathematics dbr:Negation dbr:Order_of_operations dbr:Prenex_normal_form dbr:Skolem_normal_form dbr:Peter_B._Andrews dbr:Plural_quantification dbr:George_Boolos dbr:Gottlob_Frege dbr:Graph_(discrete_mathematics) dbr:Bounded_quantifier dbr:Branching_quantifier dbr:Model_checking dbr:Congruence_relation dbr:Equiconsistency dbr:Ordered_field dbr:Arity dbr:Bernays–Schönfinkel_class dbr:Logic_of_graphs dbr:Logical_conjunction dbr:Löwenheim–Skolem_theorem dbr:Skolemization dbr:Stanford_Encyclopedia_of_Philosophy dbr:Compactness_theorem dbr:Complete_theory dbr:Completeness_(logic) dbr:Computational_complexity dbr:Computational_complexity_theory dbr:Computer_science dbr:Zermelo–Fraenkel_set_theory dbr:Empty_set dbr:Deductive_system dbr:Identity_of_indiscernibles dbr:Ordered_pair dbr:Polish_notation dbr:Propositional_logic dbr:Mathematical_Tripos dbr:Automated_theorem_proving dbr:Axiomatic_set_theory dbr:Backus-Naur_form dbr:Topology dbr:Truth_table dbr:Truth_value dbr:Tuple dbr:Type_theory dbr:Wilfrid_Hodges dbr:Wilhelm_Ackermann dbr:Willard_Van_Orman_Quine dbr:Game_semantics dbr:Gödel's_completeness_theorem dbr:Heinz-Dieter_Ebbinghaus dbr:John_Etchemendy dbr:Lattice_(order) dbr:Lindström's_theorem dbr:Linguistics dbr:Logical_biconditional dbr:Two-variable_logic dbr:Morley's_categoricity_theorem dbr:ACL2 dbr:Abelian_groups dbr:Alan_Turing dbr:Alfred_Tarski dbr:Algebra dbr:Alonzo_Church dbr:Data_type dbc:Systems_of_formal_logic dbr:Equivalence_relation dbr:Exclusive_or dbr:FO(.) dbr:False_(logic) dbr:Finitary_relation dbr:First-order_logic dbr:Formal_semantics_(logic) dbr:Formal_verification dbr:Number_theory dbr:Pairing_function dbr:Cardinal_number dbr:Cardinality dbr:Directed_graph dbr:Formal_grammar dbr:Formal_language dbr:Formal_specification dbr:Formal_system dbr:Formation_rule dbr:Foundations_of_mathematics dbr:Logical_connective dbr:Logical_consequence dbr:Natural_deduction dbr:Logical_equality dbr:Uniqueness_quantification dbr:Predicate_functor_logic dbr:Universal_generalization dbr:Well-formed_formula dbr:Predicate_(mathematical_logic) dbr:Proof_theory dbr:Quantifier_(logic) dbr:Recursively_enumerable dbr:Relation_algebra dbr:Relational_model dbr:Group_(mathematics) dbr:Gödel's_incompleteness_theorem dbr:Halting_problem dbr:Atomic_formula dbr:Atomic_sentence dbc:Predicate_logic dbr:Tautology_(logic) dbr:Term_(logic) dbr:Arithmetic dbr:Abstract_algebra dbc:Model_theory dbr:Charles_Sanders_Peirce dbr:Józef_Maria_Bocheński dbr:Latin_script dbr:Syntax dbr:Herbrandization dbr:Higher-order_logic dbr:Parse_tree dbr:Modus_ponens dbr:Domain_of_discourse dbr:Axiom dbr:Axiom_of_choice dbr:Axiom_of_extensionality dbr:Axiom_schema dbr:Axiomatic_system dbr:Boolean-valued_function dbr:Philosophy dbr:Poset dbr:Springer_Science+Business_Media dbr:Connected_component_(graph_theory) dbr:Integer dbr:Intended_interpretation dbr:Kurt_Gödel dbr:Metamath dbr:Method_of_analytic_tableaux dbr:Natural_number dbr:New_York_City dbr:Categorical_theory dbr:Search_algorithm dbr:Second-order_logic dbr:Semidecidability dbr:Semidecidable dbr:Set_theory dbr:CPU dbr:Sequent_calculus dbr:Rule_of_inference dbr:Second-order_arithmetic dbr:Semantics dbr:Sentence_(mathematical_logic) dbr:Signature_(logic) dbr:Soundness dbr:Type_(model_theory) dbr:Undergraduate_Texts_in_Mathematics dbr:Non-logical_symbols dbr:Extension_(predicate_logic) dbr:Extension_by_definitions dbr:Per_Lindström dbr:Propositional_variable dbr:Two-element_Boolean_algebra dbr:Existential_quantification dbr:Nonfirstorderizability dbr:Polyadic_algebra dbr:Real_line dbr:Tarski's_World dbr:T-schema dbr:T-norm_fuzzy_logics dbr:Partial_order dbr:Isabelle_(theorem_prover) dbr:Uncountable dbr:Skolem's_paradox dbr:Proof_verification dbr:Springer-Verlag dbr:Disjunction dbr:Ehrenfeucht-Fraisse_game dbr:Guarded_fragment dbr:Inclusive_logic dbr:Inductive_definition dbr:Formula_(mathematical_logic) dbr:Description_logics dbr:Heuristic_function dbr:Peirce_arrow dbr:Projection_function dbr:Decision_procedure dbr:Definitional_extension dbr:Monadic_predicate_logic dbr:Unification_(computing) dbr:Semantic_tableaux dbr:Existential_quantifier dbr:Hilbert-style_deductive_system dbr:Knowledge_representation_language dbr:Predicate_symbol dbr:True_(logic) dbr:Truth_definition dbr:File:Prop-tableau-4.svg
dbp:id p/p074360 (en)
dbp:title Predicate calculus (en)
dbp:wikiPageUsesTemplate dbt:Springer dbt:Jstor dbt:= dbt:Citation dbt:Citation_needed dbt:Cite_book dbt:Colend dbt:Doi dbt:Further dbt:ISBN dbt:Main dbt:Math dbt:Mono dbt:Mvar dbt:Portal dbt:Redirect dbt:Reflist dbt:Rp dbt:Sdash dbt:Section_link dbt:See_also dbt:Seealso dbt:Sfn dbt:Short_description dbt:Tmath dbt:Mathematical_logic dbt:Cols
dcterms:subject dbc:Systems_of_formal_logic dbc:Predicate_logic dbc:Model_theory
gold:hypernym dbr:Collection
rdf:type owl:Thing yago:Ability105616246 yago:Abstraction100002137 yago:Cognition100023271 yago:Know-how105616786 yago:Logic105664069 yago:Method105660268 yago:PsychologicalFeature100023100 dbo:Book yago:System105661996 yago:WikicatSystemsOfFormalLogic
rdfs:comment منطق الرتبة الأولى (First-order logic FOL) أو المنطق الإسنادي عبارة عن نظام للمنطق الرياضي يستخدم في الرياضيات والفلسفة والذكاء الصناعي وعلوم الحاسب. وهو يستخدم في التعبير عن الجمل المنطقية بشكل غير مبهم وبهذا يخالف عن اللغات الطبيعية والتي قد تحتوي على جمل مبهمة. ذلك يسهل الاستنتاج واجراء العمليات المنطقية على الجمل أو المعادلات التي تنشاء باستخدامه.و يعتبر منطق الرتبة الأولى هو تمديد منطق القضايا (منطق العبارات) propositional logic وذلك بإضافة القياس سواء كان عالمي أو وجودي. يعتبر بمنطق الرتبة الثانية تمديد لمنطق الرتبة الأولى وذلك بإضافة القياس على المجموعات. يدعى منطق الرتبة الأولى أحيانا : بمنطق الرتبة الأولى الإسنادي أو first-order predicate calculus (FOPC. (ar) Unuaranga logiko, nomita ankaŭ predikatlogiko, aŭ predikatkalkulo, estas formala sistemo desegnita por studi la inferencon en la unuarangaj lingvaĵoj.​ La unuarangaj lingvaĵoj estas siavice formalaj lingvaĵoj kun kvantigiloj kiuj atingas nur unuopajn variablojn, kaj kun predikatoj kaj funkcioj kies argumentoj estas nur konstantoj aŭ unuopaj variabloj. La logiko unuaranga havas espriman povon superan al tiu de la propozicia logiko. Logiko de supera ordo estas formo de predikatkalkulo kiu estas distingata el la unuaranga logiko pere de aldonaj kvantigiloj kaj, foje, per pli forta semantiko. (eo) Una lógica de primer orden, también llamada lógica predicativa, lógica de predicados o cálculo de predicados, es un sistema formal diseñado para estudiar la inferencia en los lenguajes de primer orden.​ Los lenguajes de primer orden son, a su vez, lenguajes formales con cuantificadores que alcanzan solo a variables de individuo, y con predicados y funciones cuyos argumentos son solo constantes o variables de individuo.​ La lógica de primer orden tiene un poder expresivo superior al de la lógica proposicional. (es) Die Prädikatenlogik erster Stufe ist ein Teilgebiet der mathematischen Logik. Sie befasst sich mit der Struktur gewisser mathematischer Ausdrücke und dem logischen Schließen, mit dem man von derartigen Ausdrücken zu anderen gelangt. Dabei gelingt es, sowohl die Sprache als auch das Schließen rein syntaktisch, das heißt ohne Bezug zu mathematischen Bedeutungen, zu definieren.Das dadurch ermöglichte Zusammenspiel von rein syntaktischen Überlegungen einerseits und semantischen Betrachtungen andererseits führt zu wichtigen Erkenntnissen, die Bedeutung für die gesamte Mathematik haben, denn diese lässt sich mittels der Zermelo-Fraenkel-Mengenlehre in der Prädikatenlogik erster Stufe formulieren. Im Unterschied zur Aussagenlogik macht die Prädikatenlogik von Quantoren Gebrauch. (de) 一階述語論理（英: first-order predicate logic）とは、個体の量化のみを許す述語論理 (predicate logic) である。述語論理とは、数理論理学における論理の数学的モデルの一つであり、命題論理を拡張したものである。個体の量化に加えて述語や関数の量化を許す述語論理を二階述語論理（英: second-order predicate logic）と呼び、さらなる一般化を加えた述語論理を高階述語論理（英: higher-order predicate logic）という。本項では主に一階述語論理について解説する。二階述語論理や高階述語論理についての詳細はそれぞれの記事を参照。 (ja) 1차 논리(一次論理, 영어: first-order logic)는 원소에만 한정 기호를 가할 수 있고, 술어에는 한정 기호를 가할 수 없는 술어 논리이다. 명제 논리와 달리 변수에 대하여 한정 기호를 사용할 수 있으나, 2차 논리와 달리 변수들의 집합에 대하여 한정 기호를 사용할 수 없다. 1차 논리의 경우, (2차 논리와 달리) 괴델의 완전성 정리 · 콤팩트성 정리 · 뢰벤하임-스콜렘 정리와 같은 중요한 성질들이 성립한다. 이외에 1차 술어 논리, 1계 논리 등으로도 불린다. 간단히 술어 논리(predicate logic)라 하면 1차 논리를 가리키는 경우가 많다. (ko) Логика первого порядка — формальное исчисление, допускающее высказывания относительно переменных, фиксированных функций и предикатов. Расширяет логику высказываний. Помимо логики первого порядка существуют также логики высших порядков, в которых кванторы могут применяться не только к переменным, но и к предикатам. Термины логика предикатов и исчисление предикатов могут означать как логику первого порядка, так и логики первого и высшего порядка вместе; в первом случае иногда говорится о чистой логике предикатов или чистом исчислении предикатов. (ru) Логіка першого порядку (числення предикатів) — це формальна система в математичній логіці, в якій допускаються висловлення відносно змінних, фіксованих функцій, і предикатів. Є розширенням логіки висловлювань. В свою чергу є частковим випадком . (uk) 一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统，也可以稱為：一阶斷言演算、低階斷言演算、量化理論或谓词逻辑。一階邏輯和命題邏輯的不同之處在於，一階邏輯包含量詞。 高階邏輯和一階邏輯不同之處在於，高階邏輯的斷言符號可以有斷言符號或函數符號當做引數，且容許斷言量詞或函數量詞。在一階邏輯的語義中，斷言被解釋為關係。而高階邏輯的語義裡，斷言則會被解釋為集合的集合。 在通常的語義下，一階邏輯是可靠（所有可證的敘述皆為真）且完備（所有為真的敘述皆可證）。雖然一階邏輯的只是半可判定性的，但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的定理，如勒文海姆–斯科倫定理及緊緻性定理。 一階邏輯是數學基礎中很重要的一部份。許多常見的公理系統，如一階皮亞諾公理、冯诺伊曼-博内斯-哥德尔集合论和策梅洛-弗蘭克爾集合論都是一階理論。然而一階邏輯不能控制其無窮模型的基數大小，因根據勒文海姆–斯科倫定理和康托爾定理，可以構造出一種＂病態＂集合論模型，使整個模型可數，但模型內卻會覺得自己有「不可數集」。類似地，可以證明實數系的普通一階理論既有可數模型又有不可數模型。這類的悖論被稱為斯科倫悖論。但一階的直覺主義邏輯裡，勒文海姆–斯科倫定理不可證明，故不會有以上之現象。 (zh) La lògica de primer ordre, també anomenada lògica de predicats o càlcul de predicats, és un sistema formal dissenyat per estudiar la inferència en els llenguatges de primer ordre. Els llenguatges de primer ordre són, al seu torn, llenguatges amb quantificador que arriben només a variables d'individu, i amb funcions els arguments de les quals són només constants o variables d'individu. La lògica de primer ordre té el poder expressiu suficient per definir a pràcticament totes les matemàtiques. (ca) Predikátová logika prvního řádu je používaný v matematice, filozofii, lingvistice a informatice. Často se pro její označení používá kratší a méně přesný termín predikátová logika. Predikátová logika prvního řádu se odlišuje od výrokové logiky zavedením kvantifikovaných proměnných. (cs) Η λογική πρώτου βαθμού είναι μια τυπική λογική που χρησιμοποιείται στα μαθηματικά, τη φιλοσοφία, τη γλωσσολογία και την επιστήμη υπολογιστών. Συναντάται με διάφορα ονόματα, όπως κατηγορηματικός λογισμός πρώτου βαθμού ή κατηγορηματική λογική. Η πρωτοβάθμια λογική διαφέρει από την προτασιακή λογική στη χρήση ποσοτικών τελεστών: κάθε ερμηνεία της λογικής πρώτου βαθμού περιλαμβάνει ένα πεδίο τιμών όπου κυμαίνονται οι ποσοτικοί τελεστές. (el) First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic. (en) Lehen mailako logika, predikatuen logika, logika kuantifikatzailea edo predikatuen kalkulua ere deitzen dena, lehen ordenako hizkuntzen inferentzia aztertzeko diseinatutako sistema formala da. Predikatuak, haien propietateak eta eragiketak aztertzen dituen logika. Aldagai eta kuantifikatzaileen bidez lan egiten du. Predikatuen logikak proposizioen barne-egitura hartzen du kontuan. Lehen ordenako lengoaiak, era berean, banakako aldagaiei bakarrik eragiten dien zenbatzaileak dituzten dira, eta argumentuak, konstanteak edo aldagai indibidualak dituzten predikatuak eta funtzioak baino ez dira. (eu) Le calcul des prédicats du premier ordre, ou calcul des relations, logique du premier ordre, logique quantificationnelle, ou tout simplement calcul des prédicats, est une formalisation du langage des mathématiques, proposée par Gottlob Frege, entre la fin du XIXe siècle et le début du XXe siècle. La logique du premier ordre comporte deux parties : Sur le plan syntaxique, les langages du premier ordre opposent deux grandes classes linguistiques : et . Les traits caractéristiques de la logique du premier ordre sont : (fr) Logika predikat tingkat pertama adalah sistem deduksi formal yang digunakan dalam matematika, filosofi, linguistika, dan ilmu komputer. Jika kalkulus proposisional membahas proposisi sederhana, LTP menambahkan predikat dan kuantor. Misalnya: * Sokrates adalah seorang manusia * Plato adalah seorang manusia Contoh berikut menjabarkan perbedaan kalkulus proposisional dan LTP: * Semua manusia perlu makan * Sokrates adalah manusia * Sokrates perlu makan Dalam kalkulus proposisional, ketiga kalimat di atas diterjemahkan sebagai: * A * B * C ( artinya "maka") * * * (in) Nella logica matematica, una teoria del primo ordine (o calcolo dei predicati) è un particolare sistema formale, cioè una teoria formale, in cui è possibile esprimere enunciati e dedurre le loro conseguenze logiche in modo del tutto formale e meccanico. La teoria del prim'ordine estende di fatto la logica proposizionale con l'introduzione di quantificatori esistenziali e universali, predicati, funzioni, variabili e costanti, che apportano maggiore potenza espressiva al calcolo dei predicati. Come per la logica proposizionale, la teoria del primo ordine può essere scissa in due parti separate: (it) Rachunek predykatów pierwszego rzędu (ang. first order predicate calculus) – system logiczny, w którym zmienna, na której oparty jest kwantyfikator, może być elementem pewnej wybranej dziedziny (zbioru), nie może natomiast być zbiorem takich elementów. Tak więc nie mogą występować kwantyfikatory typu „dla każdej funkcji z X na Y...” (gdyż funkcja jest podzbiorem X × Y), „istnieje własność p, taka że...” czy „dla każdego podzbioru X zbioru Z...”. Rachunek ten nazywa się też krótko rachunkiem kwantyfikatorów, ale często używa się też nazwy logika pierwszego rzędu (szczególnie wśród matematyków zajmujących się logiką matematyczną). (pl) A lógica de primeira ordem (LPO), conhecida também como cálculo de predicados de primeira ordem (CPPO), é um sistema lógico que estende a lógica proposicional (lógica sentencial) e que é estendida pela lógica de segunda ordem. As sentenças atômicas da lógica de primeira ordem têm o formato P (t1,…, tn) (um predicado com um ou mais "argumentos") ao invés de serem símbolos sentenciais sem estruturas. (pt) Första ordningens logik (FOL) är ett formellt deduktivt system som används i matematik, filosofi, lingvistik och datavetenskap. Det har ett flertal olika namn på engelska: first-order predicate calculus (FOPC), the lower predicate calculus, the language of first-order logic och predicate logic. Till skillnad från naturliga språk, som svenska, använder sig FOL av ett helt otvetydigt formellt språk som tolkas av matematiska strukturer. FOL är ett deduktivt system som går bortom satslogiken genom att tillåta kvantifiering av objekt inom en given domän. Man kan exempelvis med FOL uttrycka satsen "Varje individ har egenskapen P". (sv)
rdfs:label منطق الرتبة الأولى (ar) Lògica de primer ordre (ca) Predikátová logika prvního řádu (cs) Prädikatenlogik erster Stufe (de) Λογική πρώτου βαθμού (el) Predikatkalkulo (eo) Lógica de primer orden (es) Lehen mailako logika (eu) First-order logic (en) Logika predikat tingkat pertama (in) Calcul des prédicats (fr) Teoria del primo ordine (it) 1차 논리 (ko) 一階述語論理 (ja) Rachunek predykatów pierwszego rzędu (pl) Lógica de primeira ordem (pt) Логика первого порядка (ru) Första ordningens logik (sv) 一阶逻辑 (zh) Логіка першого порядку (uk)
rdfs:seeAlso dbr:Alphabet_(formal_languages) dbr:Satisfiability
owl:sameAs freebase:First-order logic yago-res:First-order logic wikidata:First-order logic dbpedia-ar:First-order logic dbpedia-ca:First-order logic dbpedia-cs:First-order logic dbpedia-de:First-order logic dbpedia-el:First-order logic dbpedia-eo:First-order logic dbpedia-es:First-order logic dbpedia-eu:First-order logic dbpedia-fa:First-order logic dbpedia-fr:First-order logic dbpedia-he:First-order logic dbpedia-hu:First-order logic http://hy.dbpedia.org/resource/Պրեդիկատների_տրամաբանություն dbpedia-id:First-order logic dbpedia-it:First-order logic dbpedia-ja:First-order logic dbpedia-ko:First-order logic dbpedia-no:First-order logic dbpedia-pl:First-order logic dbpedia-pt:First-order logic dbpedia-ru:First-order logic dbpedia-sh:First-order logic dbpedia-simple:First-order logic dbpedia-sr:First-order logic dbpedia-sv:First-order logic http://tl.dbpedia.org/resource/Lohika_ng_unang_orden dbpedia-uk:First-order logic dbpedia-vi:First-order logic dbpedia-zh:First-order logic https://global.dbpedia.org/id/3ke7a
prov:wasDerivedFrom wikipedia-en:First-order_logic?oldid=1124506241&ns=0
foaf:depiction wiki-commons:Special:FilePath/Prop-tableau-4.svg
foaf:isPrimaryTopicOf wikipedia-en:First-order_logic
is dbo:wikiPageDisambiguates of dbr:FO dbr:FOL dbr:First-order
is dbo:wikiPageRedirects of dbr:Predicate_logic dbr:Quantification_theory dbr:Deductive_systems_for_first-order_logic dbr:First-order_theory dbr:First-order_predicate_calculus dbr:First-order_language dbr:First-Order_Logic dbr:FOPC dbr:FOPL dbr:Predicate_calculus dbr:Satisfaction_relation dbr:Predicate_Logic dbr:Equational_first-order_logic dbr:Semantics_of_first-order_logic dbr:1st_order_logic dbr:First-order-logic dbr:First-order_Peano_arithmetic dbr:First-order_logic_with_equality dbr:First-order_predicate_logic dbr:First-order_sentence dbr:First_Order_Language dbr:First_Order_Logic dbr:First_order_language dbr:First_order_logic dbr:First_order_logic_with_equality dbr:First_order_predicate_calculus dbr:First_order_predicate_logic dbr:Tarskian_semantics dbr:Classical_predicate_logic dbr:Polyadic_predicate_calculus dbr:Quantification_calculus dbr:Lower_Predicate_Calculus dbr:Many-sorted_first-order_logic dbr:Predicate_Calculus dbr:Predicate_logic_(Philosophy) dbr:Predicate_logic_(philosophy)
is dbo:wikiPageWikiLink of dbr:Cantor's_first_set_theory_article dbr:Begriffsschrift dbr:Predicate_logic dbr:Primitive_recursive_function dbr:Probabilistic_soft_logic dbr:Program_synthesis dbr:Prolog dbr:Proof_sketch_for_Gödel's_first_incompleteness_theorem dbr:Propositional_calculus dbr:Quantification_theory dbr:Queue_number dbr:Quine–Putnam_indispensability_argument dbr:Saul_Kripke dbr:Elementary_class dbr:Elementary_definition dbr:Elementary_diagram dbr:Elementary_equivalence dbr:Elementary_sentence dbr:Elementary_theory dbr:Epistemic_humility dbr:FO dbr:FOL dbr:List_of_first-order_theories dbr:Modal_logic dbr:Model_theory dbr:Monadic_predicate_calculus dbr:Natural_language_processing dbr:Normalisation_by_evaluation dbr:László_Kalmár dbr:Löwenheim_number dbr:MINLOG dbr:Mereology dbr:Mereotopology dbr:Meta-ontology dbr:Metalogic dbr:Metamathematics dbr:Metatheorem dbr:Omega-categorical_theory dbr:Ontological_commitment dbr:Universal_quantification dbr:Prover9 dbr:Principles_of_Mathematical_Logic dbr:Problem_of_multiple_generality dbr:1928_in_science dbr:Decider_(Turing_machine) dbr:Description_logic dbr:Algebraic_sentence dbr:Algebraic_structure dbr:Algebraic_theory dbr:Algebraically_closed_field dbr:Algorithmic_logic dbr:Alloy_(specification_language) dbr:Homotopy_type_theory dbr:Beth_definability dbr:List_of_pioneers_in_computer_science dbr:Paul_Halmos dbr:Peano_axioms dbr:Regular_category dbr:Resolution_(logic) dbr:Resolvent_cubic dbr:Characteristica_universalis dbr:CycL dbr:DPLL_algorithm dbr:Unification_(computer_science) dbr:Universe_(mathematics) dbr:Vadalog dbr:Vampire_(theorem_prover) dbr:Von_Neumann–Bernays–Gödel_set_theory dbr:Davis–Putnam_algorithm dbr:Decidability_(logic) dbr:Decidability_of_first-order_theories_of_the_real_numbers dbr:Decision_Model_and_Notation dbr:Deduction_theorem dbr:Deductive_language dbr:Default_logic dbr:Definite_clause_grammar dbr:Descriptive_Complexity dbr:Descriptive_complexity_theory dbr:Donkey_sentence dbr:Double-negation_translation dbr:Dynamic_logic_(modal_logic) dbr:EXPSPACE dbr:E_(theorem_prover) dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(D–H) dbr:Indiscernibles dbr:Induction,_bounding_and_least_number_principles dbr:Inference_engine dbr:Infinitary_logic dbr:Infinite-valued_logic dbr:Institution_(computer_science) dbr:Institutional_model_theory dbr:Intensional_logic dbr:Internal_set_theory dbr:International_Workshop_on_First-Order_Theorem_Proving dbr:Interpretation_(model_theory) dbr:Interval_temporal_logic dbr:Intuitionistic_logic dbr:Intuitionistic_type_theory dbr:Number dbr:Lincos_language dbr:List_of_incomplete_proofs dbr:List_of_logic_symbols dbr:List_of_mathematical_abbreviations dbr:List_of_mathematical_logic_topics dbr:List_of_rules_of_inference dbr:Ontology_engineering dbr:Numbering_(computability_theory) dbr:Tarski's_axioms dbr:Possible_world dbr:Predicate_transformer_semantics dbr:Predicate_variable dbr:Presburger_arithmetic dbr:Reasoning_system dbr:Propositional_representation dbr:Star-free_language dbr:Robinson's_joint_consistency_theorem dbr:String_diagram dbr:Timeline_of_category_theory_and_related_mathematics dbr:Combinatory_logic dbr:Completeness_(knowledge_bases) dbr:Computability_theory dbr:Computable_function dbr:Consistency dbr:Context-free_grammar dbr:Corresponding_conditional dbr:Craig_interpolation dbr:Ancestral_relation dbr:Mathematical_induction dbr:Mathematical_logic dbr:Russell's_paradox dbr:Ruth_Barcan_Marcus dbr:General_set_theory dbr:Geometric_logic dbr:Negation dbr:Nominal_terms_(computer_science) dbr:Nouvelle_AI dbr:Object-role_modeling dbr:Order_(mathematics) dbr:Otter_(theorem_prover) dbr:Prenex_normal_form dbr:Skolem_normal_form dbr:Susanne_Bobzien dbr:Sahlqvist_formula dbr:Trakhtenbrot's_theorem dbr:Pure_inductive_logic dbr:Quantifier_rank dbr:Quasi-quotation dbr:Rado_graph dbr:Timeline_of_mathematical_logic dbr:Entitative_graph dbr:Frank_Ramsey_(mathematician) dbr:Game_theory dbr:George_Boolos dbr:Gettier_problem dbr:Glossary_of_areas_of_mathematics dbr:Glossary_of_artificial_intelligence dbr:Glossary_of_computer_science dbr:Glossary_of_set_theory dbr:Branching_quantifier dbr:Model_checking dbr:Mu_(negative) dbr:NL_(complexity) dbr:Conceptual_graph dbr:Conjunctive_normal_form dbr:Conjunctive_query dbr:Connectionism dbr:Constructive_set_theory dbr:Contradiction dbr:Contraposition dbr:Controlled_natural_language dbr:Converse_(logic) dbr:Thoralf_Skolem dbr:Epsilon dbr:Epsilon_calculus dbr:Equality-generating_dependency dbr:Equational_logic dbr:Equivalent_definitions_of_mathematical_structures dbr:L_(complexity) dbr:Open_formula dbr:Ordinal_arithmetic dbr:Andrzej_Grzegorczyk dbr:Arithmetical_set dbr:Bernays–Schönfinkel_class dbr:Linear_logic dbr:Logic dbr:Logic_of_graphs dbr:Logical_conjunction dbr:Löwenheim–Skolem_theorem dbr:ML_(programming_language) dbr:Stanisław_Leśniewski dbr:Straight-line_program dbr:Structural_induction dbr:Clock_(model_checking) dbr:Clone_(algebra) dbr:Common_Algebraic_Specification_Language dbr:Common_Logic dbr:Completeness_(logic) dbr:Computation_tree_logic dbr:Zermelo–Fraenkel_set_theory dbr:Zohar_Manna dbr:Embedded_dependency dbr:Empty_domain dbr:Empty_set dbr:Deductive_systems_for_first-order_logic dbr:Identity_of_indiscernibles dbr:Joseph_Sgro dbr:Kripke_semantics dbr:Kripke–Platek_set_theory dbr:Leon_Henkin dbr:P_(complexity) dbr:Phi dbr:Pocket_set_theory dbr:Primitive_recursive_arithmetic dbr:Spectrum_of_a_sentence dbr:Structure_(mathematical_logic) dbr:Substitution_(logic) dbr:Superposition_calculus dbr:Symbol_(formal) dbr:Theorem_Proving_System dbr:Matching_logic dbr:Mathematics,_Form_and_Function dbr:Mutilated_chessboard_problem dbr:Occurs_check dbr:Automated_theorem_proving dbr:Total_order dbr:Transitive_closure dbr:Transitive_relation dbr:Truth_table dbr:Type_theory dbr:Data_integration dbr:Data_model dbr:Database_normalization dbr:Database_theory dbr:Wanda_Szmielew dbr:Web_Ontology_Language dbr:Wedge_(symbol) dbr:Where_Mathematics_Comes_From dbr:Wilhelm_Ackermann dbr:Willard_Van_Orman_Quine dbr:William_Lane_Craig dbr:Disjunction_and_existence_properties dbr:Disquotational_principle dbr:Fuzzy_logic dbr:Game_Description_Language dbr:Game_semantics dbr:Giorgi_Japaridze dbr:Gödel's_completeness_theorem dbr:HYPO_CBR dbr:June_1919 dbr:Lambda_cube dbr:Larch_Prover dbr:Large_countable_ordinal dbr:Lattice_(order) dbr:Law_of_identity dbr:Law_of_thought dbr:Laws_of_Form dbr:Least_fixed_point dbr:Lindström's_theorem dbr:Linear_temporal_logic dbr:List_of_Boolean_algebra_topics dbr:Logic_form dbr:Logic_in_computer_science dbr:Logicism dbr:Robinson_arithmetic dbr:Tennenbaum's_theorem dbr:Two-variable_logic dbr:Non-standard_model_of_arithmetic dbr:True_arithmetic dbr:ACL2 dbr:Alfred_Tarski dbr:Algebraic_geometry dbr:Algebraic_logic dbr:Cyc dbr:DE-9IM dbr:Data_type dbr:Datalog dbr:Alternating-time_temporal_logic dbr:Equivalence_relation dbr:Exclusive_or dbr:FO(.) dbr:Field_(mathematics) dbr:Finite_set dbr:First-order_logic dbr:First-order_theory dbr:Forcing_(mathematics) dbr:Barwise_compactness_theorem dbr:Diagonal_lemma dbr:Diagrammatic_reasoning dbr:Dictum_de_omni_et_nullo dbr:Differential_(mathematics) dbr:Direct_proof dbr:Dis-unification_(computer_science) dbr:Educational_software dbr:Fallacy_of_the_undistributed_middle dbr:Fluent_(artificial_intelligence) dbr:Fluent_calculus dbr:Formal_ethics dbr:Formal_language dbr:Formal_linguistics
is rdfs:seeAlso of dbr:Equality_(mathematics)
is foaf:primaryTopic of wikipedia-en:First-order_logic