Utilizator:Andrei Stroe/Logică de ordinul întâi

Logica de ordinul întâi — cunoscută și sub numele de logica predicatelor de ordinul întâi, logica cuantificativă sau calculul cu predicate de ordinul întâi — este o colecție de sisteme formale utilizate în matematică, filozofie, lingvistică și informatică. Logica de ordinul întâi folosește variabile cuantificate peste obiecte nelogice și permite utilizarea propozițiilor care conțin variabile, astfel încât în locul unor propoziții precum „Socrate este un om”, pot apărea expresii sub forma „există x astfel încât x este Socrate și x este un om”, unde „există” este un cuantificator logic, în timp ce x este o variabilă.^[1] Aceasta o deosebește de logica propozițională, care nu folosește cuantificatori sau relații;^[2] în acest sens, logica propozițională este fundamentul logicii de ordinul întâi.

O teorie pe un subiect, cum ar fi teoria mulțimilor, o teorie pentru grupuri,^[3] sau o teorie formală a aritmeticii, sunt de obicei logici de ordinul întâi împreună cu un domeniu specificat de definiție (din care își pot lua valori variabilele cuantificate), un număr finit de funcții definite pe acel domeniu cu valori în el însuși, un număr finit de predicate definite pe acel domeniu și un set de axiome despre care se crede că sunt valabile. Uneori, termenul de „teorie” se înțelege într-un sens mai formal decât doar un set de propoziții în logica de ordinul întâi.

Adjectivul „de ordinul întâi” face distincția între logica de ordinul întâi și logicile de ordin superior, în care există predicate care au ca argument alte predicate sau funcții, sau în care sunt permise cuantificarea peste predicate sau funcții.^[4]^:56 În teoriile de ordinul întâi, predicatele sunt adesea asociate mulțimilor. În teoriile de ordin superior interpretate, predicatele pot fi interpretate ca mulțimi de mulțimi.

Există multe sisteme deductive pentru logica de ordinul întâi care sunt atât corecte (adică toate afirmațiile demonstrabile sunt adevărate în toate modelele) cât și complete (adică toate afirmațiile care sunt adevărate în toate modelele sunt demonstrabile). Deși relația de consecință logică este doar semicidabilă, s-au făcut multe progrese în domeniul demonstrării automate de teoreme în logica de ordinul întâi. Logica de ordinul întâi mai satisface și mai multe teoreme metalogice care o fac accesibilă analizei în teoria demonstrațiilor, cum ar fi teorema Löwenheim–Skolem și teorema compactității.

Logica de ordinul întâi este standardul pentru formalizarea matematicii în axiome și este studiată în fundamentele matematicii. Aritmetica Peano și teoria mulțimilor Zermelo–Fraenkel sunt axiomatizări ale teoriei numerelor și, respectiv, ale teoriei mulțimilor în logica de ordinul întâi. Nicio teorie de ordinul întâi, însă, nu are puterea de a descrie în mod unic o structură cu un domeniu infinit, cum ar fi numerele naturale sau dreapta reală. Sistemele de axiome care descriu pe deplin aceste două structuri (adică sisteme de axiome categorice) pot fi obținute în logici mai puternice, cum ar fi logica de ordinul al doilea.

Bazele logicii de ordinul întâi au fost dezvoltate independent de Gottlob Frege și Charles Sanders Peirce.^[5] Pentru o istorie a logicii de ordinul întâi și a modului în care aceasta a ajuns să domine logica formală, vezi José Ferreirós (2001).

Introducere[modificare | modificare sursă]

În timp ce logica propozițională se ocupă de propoziții declarative simple, logica de ordinul întâi acoperă în plus predicatele și cuantificarea.

Un predicat ia o entitate sau entități din domeniul de definiție și o evaluează drept adevărată sau falsă. Dacă se iau în considerare cele două propoziții „Socrate este un filozof” și „Platon este un filosof”, în logica propozițională, aceste propoziții sunt privite ca neînrudite și ar putea fi notate, de exemplu, prin variabile precum p și q. Predicatul „este un filozof” apare în ambele propoziții, care au structura comună „a este un filozof”. Variabila a este instanțiată ca „Socrate” în prima propoziție și ca „Platon” în a doua propoziție. În timp ce logica de ordinul întâi permite utilizarea predicatelor, cum ar fi „este un filozof” în acest exemplu, logica propozițională nu o face.^[6]

Relațiile dintre predicate pot fi enunțate folosind conectori logici. În cazul formulei de ordinul întâi „dacă a este un filosof, atunci a este un savant”, ea este o afirmație condiționată cu „a este un filozof” drept ipoteză și „a este un savant” drept concluzie. Adevărul acestei formule depinde de ce obiect este notat cu a, și de interpretările predicatelor „este un filosof” și „este un savant”.

Variabilelor dintr-o formulă li se pot aplica cuantificatori. Variabila a din formula anterioară poate fi cuantificată universal, de exemplu, cu propoziția de ordinul întâi „Pentru orice a, dacă a este un filosof, atunci a este un savant”. Cuantificatorul universal „orice” din această propoziție exprimă ideea că afirmația „dacă a este un filosof, atunci a este un savant” este valabilă pentru toate valorile posibile ale lui a.

Negarea propoziției „Pentru orice a, dacă a este un filosof, atunci a este un savant” este echivalentă logic cu propoziția „Există a astfel încât a este un filosof și a nu este un savant”. Cuantificatorul existențial „există” exprimă ideea că afirmația „a este un filosof și a nu este un savant” este valabilă pentru unele variante de a.

Predicatele „este un filozof” și „este un savant” primesc fiecare o singură variabilă. În general, predicatele pot lua mai multe variabile. În propoziția de ordinul întâi „Socrate este profesorul lui Platon”, predicatul „este profesorul lui” primește două variabile.

O interpretare (sau un model) a unei formule de ordinul întâi specifică ce înseamnă fiecare predicat și ce entități pot instanția variabilele. Aceste entități formează domeniul de definiție sau universul, care de obicei este necesar să fie o mulțime nevidă. De exemplu, într-o interpretare cu domeniul alcătuit din toate ființele umane și predicatul „este un filosof” înțeles ca „a fost autorul Republicii”, se vede propoziția „Există a astfel încât a este un filozof” ca fiind adevărată, așa cum este exemplificată de Platon.

Există două părți cheie ale logicii de ordinul întâi. Sintaxa determină ce secvențe finite de simboluri sunt expresii bine formate în logica de ordinul întâi, în timp ce semantica determină semnificațiile din spatele acestor expresii.

Sintaxă[modificare | modificare sursă]

Alfabet[modificare | modificare sursă]

Spre deosebire de limbajele naturale, cum ar fi limba română, limbajul logicii de ordinul întâi este complet formal, astfel încât se poate determina mecanic dacă o anumită expresie este bine formată. Există două tipuri importante de expresii bine formate: termeni, care reprezintă în mod intuitiv obiecte și formule, care exprimă intuitiv afirmații care pot fi adevărate sau false. Termenii și formulele logicii de ordinul întâi sunt șiruri de simboluri, în care toate simbolurile împreună formează alfabetul limbajului. Ca și în cazul tuturor limbajelor formale, natura simbolurilor în sine este în afara domeniului de aplicare a logicii formale; ele sunt adesea considerate pur și simplu ca litere și simboluri de punctuație.

Simbolurile alfabetului se împart de regulă în simboluri logice, care au întotdeauna aceeași semnificație, și simboluri nelogice, a căror semnificație variază în funcție de interpretare. De exemplu, simbolul logic $\land$ reprezintă întotdeauna „și”; nu este niciodată interpretat ca „sau”, care este reprezentat de simbolul logic $\lor$ . Cu toate acestea, un simbol predicat nelogic, cum ar fi Phil(x), ar putea fi interpretat ca însemnând „x este filozof”, „x este un om pe nume Philip” sau orice alt predicat unar, în funcție de interpretarea de lucru.

Simboluri logice[modificare | modificare sursă]

Simbolurile logice sunt un set de caractere care variază în funcție de autor, dar de obicei includ următoarele:^[7]

Simboluri cuantificatoare : $\forall$ pentru cuantificare universală și $\exists$ pentru cuantificare existențială
Conectori logici: $\land$ pentru conjuncție, $\lor$ pentru disjuncție, $\to$ pentru implicație, $\leftrightarrow$ pentru bicondițional, $\neg$ pentru negație. Unii autori^[8] folosesc Cpq în loc de $\to$ și Epq în loc de $\leftrightarrow$ , mai ales în contexte în care simbolul → este folosit în alte scopuri. Mai mult, potcoava $\supset$ poate înlocui $\to$ ; bara triplă $\equiv$ poate înlocui $\leftrightarrow$ ; o tildă ( $~$ ), Np sau Fp poate înlocui $\neg$ ; bara dublă $\|$ , $+$ , $\bigwedge pq$ ,^[9] sau Apq poate înlocui $\lor$ ; și un ampersand $&$ , K pq, sau punctul din mijloc $\cdot$ poate înlocui $\land$ , mai ales dacă aceste simboluri nu sunt disponibile din motive tehnice. (Simbolurile menționate mai sus Cpq, Epq, Np, Apq și Kpq sunt folosite în notația poloneză.)
Parantezele rotunde, parantezele drepte și alte simboluri de punctuație. Alegerea unor astfel de simboluri variază în funcție de context.
Un set infinit de variabile, adesea notate cu litere mici de la sfârșitul alfabetului x, y, z ,.... Pentru a distinge variabilele, se folosesc deseori indici: $x 0, x 1, x 2, ... .$
Un simbol de egalitate (uneori, simbol de identitate ) $=$ (vezi § Egalitatea și axiomele ei mai jos).

Nu toate aceste simboluri sunt necesare în logica de ordinul întâi. Oricare dintre cuantificatori, împreună cu negația, conjuncția (sau disjuncția), variabilele, parantezele și egalitatea sunt suficiente.

Printre alte simboluri logice se mai numără și:

Constante de adevăr: T, V sau $⊤$ pentru „adevărat” și F, O sau $⊥$ pentru „fals” (V și O sunt din notația poloneză). Fără astfel de operatori logici de valență 0, aceste două constante pot fi exprimate numai folosind cuantificatori.
Conexiuni logice suplimentare, cum ar fi bara Sheffer, Dpq (NAND) și sau exclusiv, Jpq.

Simboluri nelogice[modificare | modificare sursă]

Simbolurile nelogice reprezintă predicate (relații), funcții și constante. Folosirea unei mulțimi fixe, infinite de simboluri non-logice pentru toate scopurile era o practică standard:

Pentru fiecare număr întreg n ≥ 0, există o colecție de simboluri predicat n-are. Deoarece reprezintă relații între n elemente, ele sunt numite și simboluri de relație. Pentru fiecare aritate n, există o ofertă infinită de astfel de simboluri:
Pⁿ⁰, Pⁿ₁, Pⁿ₂_, Pⁿ_3, ...
Pentru fiecare număr întreg n ≥ 0, există infinit de multe simboluri de funcție n-are:
fⁿ₀, fⁿ₁, fⁿ₂, fⁿ₃, . . .

Când aritatea unui simbol predicat sau a unui simbol de funcție este clară din context, indicele n este adesea omis.

În această abordare tradițională, există un limbaj unic al logicii de ordinul întâi.^[10] Această abordare este încă obișnuită, mai ales în cărțile cu orientare filosofică.

O practică mai recentă este utilizarea diferitelor simboluri nelogice în funcție de aplicația pe care o are în vedere. Prin urmare, a devenit necesară denumirea setului de simboluri nelogice utilizate într-o anumită aplicație. Această alegere se face printr-o signatură.^[11]

Signaturile tipice din matematică sunt {1, ×} sau doar {×} pentru grupuri,^[3] sau {0, 1, +, ×, <} pentru corpurile ordonate. Nu există restricții privind numărul de simboluri nelogice. Signatura poate fi vidă, finită sau infinită, chiar nenumărabilă. Signaturi nenumărate apar, de exemplu, în demonstrațiile moderne ale teoremei Löwenheim–Skolem.

Deși semnăturile ar putea în unele cazuri să implice modul în care simbolurile nelogice trebuie interpretate, interpretarea simbolurilor nelogice din signatura este separată (și nu neapărat fixă). Signaturile privesc mai degrabă sintaxa decât semantica.

În această abordare, fiecare simbol non-logic este de unul dintre următoarele tipuri:

Un simbol de predicat (sau simbol de relație) cu o anumită valență (sau aritate, număr de argumente) mai mare sau egal cu 0. Acestea sunt adesea notate cu litere mari, cum ar fi P, Q și R. Exemple:
- În P (x), P este un simbol predicat de valență 1. O interpretare posibilă este „x este bărbat”.
- În Q (x, y), Q este un simbol predicat de valență 2. Printre interpretările posibile se num ar a „x este mai mare decât y” sau „x este tatăl lui y”.
- Relațiile de valență 0 pot fi identificate cu variabile propoziționale, care pot reprezenta orice afirmație. O posibilă interpretare a lui R este „Socrate este un om”.
Un simbol de funcție, cu o anumită valență mai mare sau egală cu 0. Acestea sunt adesea notate cu litere latinești mici, cum ar fi f, g și h. Exemple:
- f (x) poate fi interpretat ca „tatăl lui x”. În aritmetică, poate reprezenta „-x”. În teoria mulțimilor, poate reprezenta „mulțimea părților lui x”.
- În aritmetică, g (x, y) poate reprezenta „x + y”. În teoria mulțimilor, poate reprezenta „reuniunea dintre x și y”.
- Simbolurile de funcție de valență 0 se numesc simboluri de constantă și sunt adesea notate cu litere mici de la începutul alfabetului, cum ar fi a, b și c. Simbolul a l-ar putea, de exemplu, reprezenta pe Socrate. În aritmetică, poate reprezenta 0. În teoria mulțimilor, poate reprezenta mulțimea vidă.

Abordarea tradițională poate fi recuperată în abordarea modernă, doar specificând că signatura „personalizată” este formată din secvențele tradiționale de simboluri nelogice.

Reguli de formare[modificare | modificare sursă]

Gramatica BNF

<index>       ::= "" 
           | <index> "'"
<variable>     ::= "x" <index>
<constant>     ::= "c" <index>
<unary function>  ::= "f1" <index>
<binary function>  ::= "f2" <index>
<ternary function> ::= "f3" <index>
<unary predicate>  ::= "p1" <index>
<binary predicate> ::= "p2" <index>
<ternary predicate> ::= "p3" <index>
<term>       ::= <variable> 
           | <constant> 
           | <unary function> "(" <term> ")" 
           | <binary function> "(" <term> "," <term> ")" 
           | <ternary function> "(" <term> "," <term> "," <term> ")"
<atomic formula>  ::= "TRUE" 
           | "FALSE"
           | <term> "=" <term>
           | <unary predicate> "(" <term> ")" 
           | <binary predicate> "(" <term> "," <term> ")" 
           | <ternary predicate> "(" <term> "," <term> "," <term> ")"
<formula>      ::= <atomic formula> 
           | "¬" <formula>
           | <formula> "∧" <formula>
           | <formula> "∨" <formula>
           | <formula> "⇒" <formula>
           | <formula> "⇔" <formula>
           | "(" <formula> ")"
           | "∀" <variable> <formula>
           | "∃" <variable> <formula>

Gramatica independentă de context de mai sus în forma Backus-Naur definește limbajul formulelor de ordinul întâi valide din punct de vedere sintactic cu simboluri de funcție și simboluri de predicat până la aritatea 3. Pentru arități superioare, trebuie adaptat în consecință.^[12]

Exemplul de formulă ∀x ∃x' (¬x=c) ⇒ f2(x,x')=c' descrie inversele multiplicative atunci când f2', c, și c' sunt interpretate ca înmulțire, zero și, respectiv, unu.

Regulile de formare definesc termenii și formulele logicii de ordinul întâi.^[13] Când termenii și formulele sunt reprezentate ca șiruri de simboluri, aceste reguli pot fi folosite pentru a scrie o gramatică formală pentru termeni și formule. Aceste reguli sunt, în general independente de context (fiecare producție are un singur simbol în partea stângă), cu excepția faptului că mulțimea simbolurilor poate fi și infinită și pot exista multe simboluri de început, de exemplu variabilele în cazul termenilor.

Terminologie[modificare | modificare sursă]

Mulțimea de termeni este definită inductiv prin următoarele reguli:^[14]

Variabile. Orice simbol de variabilă este un termen.
Funcții. Dacă f este un simbol al funcției n-are și t₁, ..., t_n sunt termeni, atunci f(t₁,...,t_n) este un termen. În particular, simbolurile cu care se notează constante individuale sunt simboluri de funcție nulară și, prin urmare, sunt termeni.

Numai expresiile care pot fi obținute printr-un număr finit de aplicări ale regulilor 1 și 2 sunt termeni. De exemplu, nicio expresie care implică un simbol de predicat nu este un termen.

Formule[modificare | modificare sursă]

Mulțimea formulelor (numit și formule bine formate^[15] sau FBF) este definită inductiv prin următoarele reguli:

Simboluri predicat. Dacă P este un simbol predicat n-ar și t₁, ..., t_n sunt termeni atunci P(t₁,..., t_n) este o formulă.
Egalitatea. Dacă simbolul de egalitate este considerat parte a logicii și t₁ și t₂ sunt termeni, atunci t₁ = t₂ este o formulă.
Negație. Dacă $\varphi$ este o formulă, atunci $\lnot \varphi$ este o formulă.
Conectori binari. Dacă $\varphi$ și $\psi$ sunt formule, atunci ( $\varphi \rightarrow \psi$ ) este o formulă. Reguli similare se aplică altor conectori logici binari.
Cuantificatori. Dacă $\varphi$ este o formulă și x este o variabilă, atunci $\forall x\varphi$ (pentru orice x, este adevărată $\varphi$ ) și $\exists x\varphi$ (există x astfel încât $\varphi$ ) sunt formule.

Numai expresiile care pot fi obținute printr-un număr finit de aplicări ale regulilor 1–5 sunt formule. Formulele obținute din primele două reguli se spune că sunt formule atomice.

De exemplu,

\forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))

este o formulă, dacă f este un simbol de funcție unar, P un simbol de predicat unar și Q un simbol de predicat ternar. $\forall x\,x\rightarrow$ nu este însă o formulă, deși este un șir de simboluri din alfabet.

Rolul parantezelor în definiție este de a se asigura că orice formulă poate fi obținută doar într-un singur mod — urmând definiția inductivă (adică, există un arbore de parsare unic pentru fiecare formulă). Această proprietate este denumită lizibilitatea unică a formulelor. Există multe convenții pentru cazul în care parantezele sunt folosite în formule. De exemplu, unii autori folosesc două puncte sau punctul în loc de paranteze sau schimbă locurile în care sunt introduse parantezele. Definiția particulară a fiecărui autor trebuie să fie însoțită de o demonstrație de lizibilitate unică.

Această definiție a unei formule nu acceptă definirea unei funcții if-then-else ite(c, a, b), unde „c” este o condiție exprimată ca formulă, care ar returna „a” dacă c este adevărat și „ b" dacă este fals. Aceasta din cauza faptului că atât predicatele, cât și funcțiile pot accepta doar termeni ca parametri, dar primul parametru este o formulă. Unele limbaje construite pe logica de ordinul întâi, cum ar fi SMT-LIB 2.0, adaugă această posibilitate.^[16]

Convenții de notare[modificare | modificare sursă]

Pentru comoditate, au fost dezvoltate convenții cu privire la precedența operatorilor logici, pentru a evita necesitatea scrierii de paranteze în unele cazuri. Aceste reguli sunt similare cu ordinea operațiilor din aritmetică. O convenție comună este:

$\lnot$ este evaluat mai întâi
$\land$ și $\lor$ sunt evaluate următoarele
Cuantificatorii sunt evaluați următorii
$\to$ este evaluat ultimul.

Mai mult, pot fi introduse semne de punctuație suplimentare care nu sunt cerute de definiție, pentru a face formulele mai ușor de citit. Astfel formula

\lnot \forall xP(x)\to \exists x\lnot P(x)

ar putea fi scrisă sub forma

(\lnot [\forall xP(x)])\to \exists x[\lnot P(x)].

În unele domenii, se obișnuiește să se folosească notația infixă pentru relații și funcții binare, în loc de notația de prefix definită mai sus. De exemplu, în aritmetică, se scrie de obicei „2 + 2 = 4” în loc de „=(+(2,2),4)”. De regulă, se consideră formulele în notație infixă ca fiind abrevieri pentru formulele corespunzătoare în notație prefixă.

Definițiile de mai sus folosesc notația infixă pentru conectori binari, cum ar fi $\to$ . O convenție mai puțin obișnuită este notația poloneză, în care se scriu simbolurile $\rightarrow$ , $\wedge$ și așa mai departe în fața argumentelor lor și nu între ele. Această convenție este avantajoasă prin faptul că permite eliminarea tuturor simbolurilor de punctuație. Ca atare, notația poloneză este compactă și elegantă, dar rar folosită în practică, deoarece oamenilor le este greu să o citească. În notație poloneză, formula

\forall x\forall y(P(f(x))\rightarrow \neg (P(x)\rightarrow Q(f(y),x,z)))

devine "∀x∀y→Pfx¬→ PxQfyxz".

Variabile libere și legate[modificare | modificare sursă]

Într-o formulă, o variabilă poate apărea ca liberă sau legată (sau și una și alta). O formalizare a acestei noțiuni se datorează lui Quine: mai întâi se definește conceptul de apariție a variabilei, apoi dacă o apariție este liberă sau legată, apoi dacă un simbol variabil în ansamblu este liber sau legat. Pentru a distinge diferite apariții ale simbolului identic x, fiecare apariție a unui simbol variabil x într-o formulă φ este identificată cu subșirul inițial al lui φ până la punctul în care apare respectiva instanță a simbolului x.^[17]^p.297 Apoi, se spune că o apariție a lui x este legată dacă acea apariție a lui x se află în domeniul de aplicare a cel puțin unuia dintre $\exists x$ sau $\forall x$ . În cele din urmă, x este legat în φ dacă toate aparițiile lui x în φ sunt legate.^[17]^pp.142--143

Intuitiv, un simbol variabil este liber într-o formulă dacă nu este cuantificat în niciun moment:^[17]^pp.142-143 în $\forall y P (x, y)$ , singura apariție a variabilei x este liberă în timp ce cea a lui y este legată. Aparițiile variabilelor libere și legate într-o formulă sunt definite inductiv după cum urmează.

Formule atomice: Dacă φ este o formulă atomică, atunci x apare liber în φ dacă și numai dacă x apare în φ. În plus, nu există variabile legate în nicio formulă atomică.
Negare: x apare liber în ¬φ dacă și numai dacă x apare liber în φ. x apare legat în ¬φ dacă și numai dacă x apare legat în φ
Conectori binari: x apare liber în (φ → ψ) dacă și numai dacă x apare liber în φ sau ψ. x apare legat în (φ → ψ) dacă și numai dacă x apare legat fie în φ, fie în ψ. Aceeași regulă se aplică oricărui alt conector binar în locul lui →.
Cuantificatori: x apare liber în $\forall y φ$ , dacă și numai dacă x apare liber în φ și x este un simbol diferit de y. De asemenea, x apare legat în $\forall y φ$ , dacă și numai dacă x este y sau x apare legat în φ. Aceeași regulă este valabilă cu $\exists$ în loc de $\forall$ .

De exemplu, în $\forall x \forall y (P (x) \to Q (x, f (x), z))$ , x și y apar numai legate,^[18] z apare numai liber, iar w nu este nici liber, nici legat, pentru că nu apare în formulă.

Variabilele libere și legate ale unei formule nu trebuie să fie mulțimi disjuncte: în formula $P (x) \to \forall x Q (x)$ , prima apariție a lui x, ca argument al lui P, este liberă în timp ce a doua, ca argument al lui Q, este legată.

O formulă în logica de ordinul întâi fără apariții de variabile libere se numește propoziție de ordinul întâi. Acestea sunt formulele care vor avea valori de adevăr bine definite în raport cu o interpretare. De exemplu, dacă o formulă precum Phil(x) este adevărată trebuie să depindă de ce reprezintă x. Dar propoziția $\exists x Phil(x)$ va fi fie adevărată, fie falsă într-o interpretare dată.

Exemplu: grupuri abeliene ordonate[modificare | modificare sursă]

În matematică, limbajul grupurilor abeliene ordonate are un simbol constant 0, un simbol de funcție unară −, un simbol de funcție binară + și un simbol de relație binară ≤. Atunci:

Expresiile +( x, y ) și +( x, +( y, −( z ))) sunt termeni. Acestea sunt de obicei scrise ca x + y și x + y - z .
Expresiile +( x, y ) = 0 și ≤(+( x, +( y, −( z ))), +( x, y )) sunt formule atomice. Acestea sunt de obicei scrise ca x + y = 0 și x + y - z ≤ x + y .
Expresia $(\forall x\forall y\,[\mathop {\leq } (\mathop {+} (x,y),z)\to \forall x\,\forall y\,\mathop {+} (x,y)=0)]$ este o formulă, care este de obicei scrisă ca $\forall x\forall y(x+y\leq z)\to \forall x\forall y(x+y=0).$ Această formulă are o variabilă liberă, z .

Axiomele pentru grupurile abeliene ordonate pot fi exprimate ca un set de propoziții în acest limbaj. De exemplu, axioma care spune că grupul este comutativ se scrie de obicei: $(\forall x)(\forall y)[x+y=y+x].$

Semantica[modificare | modificare sursă]

O interpretare a unui limbaj de ordinul întâi atribuie o notație fiecărui simbol nelogic (simbol de predicat, simbol de funcție sau simbol constant) în limbajul respectiv. De asemenea, ea determină un univers de discurs care specifică domeniul cuantificatorilor. Rezultatul este că fiecărui termen i se atribuie un obiect pe care îl reprezintă, fiecărui predicat i se atribuie o proprietate a obiectelor și fiecărei propoziții i se atribuie o valoare de adevăr. În acest fel, o interpretare oferă sens semantic termenilor, predicatelor și formulelor limbajului. Studiul interpretărilor limbajelor formale se numește semantică formală. Ceea ce urmează este o descriere a semanticii standard sau tarskiene pentru logica de ordinul întâi. (Se poate defini și semantica de joc pentru logica de ordinul întâi, dar în afară de necesitatea axiomei alegerii, semantica jocului este în acord cu semantica tarskiană pentru logica de ordinul întâi, deci semantica jocului nu va fi elaborată aici.)

Structuri de ordinul întâi[modificare | modificare sursă]

Cel mai comun mod de a specifica o interpretare (în special în matematică) este specificarea unei structuri (numită și model). Structura constă dintr-un univers de discurs D și o funcție de interpretare $I$ care transformă simboluri nelogice în predicate, funcții și constante.

Universul de discurs D este o mulțime nevidă de „obiecte” de un fel. Intuitiv, dată fiind o interpretare, o formulă de ordinul întâi devine o afirmație despre aceste obiecte; de exemplu, $\exists xP(x)$ afirmă existența unui obiect în D pentru care predicatul P este adevărat (sau, mai precis, pentru care predicatul atribuit simbolului de predicat P prin interpretare este adevărat). De exemplu, se poate lua D ca fiind mulțimea numerelor întregi.

Simbolurile nelogice sunt interpretate după cum urmează:

Interpretarea unui simbol de funcție n-ară este o funcție de la Dⁿ la D. De exemplu, dacă universul de discurs este mulțimea numerelor întregi, un simbol al funcției f de aritate 2 poate fi interpretat ca funcția care dă suma argumentelor sale. Cu alte cuvinte, simbolul f este asociat cu funcția $I(f)$ care, în această interpretare, este adunarea.

Interpretarea unui simbol constant (un simbol al funcției de aritate 0) este o funcție de la D⁰ (o mulțime al cărei singur membru este tuplul vid) la D, care poate fi identificat pur și simplu cu un obiect din D. De exemplu, o interpretare poate atribui valoarea $I(c)=10$ simbolului constant $c$ .

Interpretarea unui simbol predicat n-ar este o mulțime de n-tuple de elemente ale lui D, dând argumentele pentru care predicatul este adevărat. De exemplu, o interpretare $I(P)$ al unui simbol de predicat binar P poate fi mulțimea de perechi de numere întregi astfel încât primul să fie mai mic decât al doilea. Conform acestei interpretări, predicatul P ar fi adevărat dacă primul său argument este mai mic decât al doilea argument. În mod echivalent, simbolurilor de predicate li se pot atribui funcții cu valori booleene definite pe Dⁿ cu valori în $\{\mathrm {adevarat,fals} \}$ .

Evaluarea valorilor de adevăr[modificare | modificare sursă]

O formulă se evaluează la adevărat sau fals având în vedere o interpretare și o atribuire de variabilă μ care asociază un element din universul de discurs cu fiecare variabilă. Motivul pentru care este necesară o atribuire de variabilă este acela de a da semnificație formulelor cu variabile libere, cum ar fi $y=x$ . Valoarea de adevăr a acestei formule se schimbă după cum cu x și y se notează același individ sau nu.

În primul rând, atribuirea variabilei μ poate fi extinsă la toți termenii limbajului, cu rezultatul că fiecare termen este asociat cu un singur element din universul de discurs. Pentru a face aceasta, se folosesc următoarele reguli:

Variabile. Fiecare variabilă x se evaluează la μ(x)
Funcții. Termenii dați $t_{1},\ldots ,t_{n}$ care au fost evaluate la elemente $d_{1},\ldots ,d_{n}$ a domeniului discursului și un simbol al funcției n-are f, termenul $f(t_{1},\ldots ,t_{n})$ se evaluează la $(I(f))(d_{1},\ldots ,d_{n})$ .

În continuare, fiecărei formule i se atribuie o valoare de adevăr. Definiția inductivă folosită pentru a face această atribuire se numește schema T.

Formule atomice (1). Unei formule $P(t_{1},\ldots ,t_{n})$ i se asociaza valoarea adevărat sau fals după cum $\langle v_{1},\ldots ,v_{n}\rangle \in I(P)$ sau nu, unde $v_{1},\ldots ,v_{n}$ sunt evaluarea termenilor $t_{1},\ldots ,t_{n}$ și $I(P)$ este interpretarea lui $P$ , care din ipoteză este o submulțime a lui $D^{n}$ .
Formule atomice (2) . Unei formule $t_{1}=t_{2}$ i se atribuie valoarea adevărat dacă $t_{1}$ și $t_{2}$ se evaluează la același obiect din universul de discurs (vezi secțiunea despre egalitate de mai jos).
Conectori logici. O formulă de forma $\neg \varphi$ , $\varphi \rightarrow \psi$ , etc. se evaluează conform tabelei de adevăr pentru conectorul respectiv, ca în logica propozițională.
Cuantificatori existențiali. O formulă $\exists x\varphi (x)$ este adevărată după M și $\mu$ dacă există o evaluare $\mu '$ a variabilelor care diferă de $\mu$ numai în ceea ce privește evaluarea lui x și astfel încât φ să fie adevărată în raport cu interpretarea M și cu atribuirea variabilei $\mu '$ . Această definiție formală surprinde ideea că $\exists x\varphi (x)$ este adevărată dacă și numai dacă există o modalitate de a alege o valoare pentru x astfel încât φ( x ) să fie satisfăcută.
Cuantificatori universali. O formulă $\forall x\varphi (x)$ este adevărată după M și $\mu$ dacă φ( x ) este adevărată pentru fiecare pereche compusă din interpretarea M și o anumită atribuire a variabilei $\mu '$ care diferă de $\mu$ numai prin valoarea lui x. Aceasta surprinde ideea că $\forall x\varphi (x)$ este adevărată dacă orice alegere posibilă a unei valori pentru x face ca φ(x) să fie adevărată.

Dacă o formulă nu conține variabile libere, și este deci o propoziție, atunci alocarea inițială a variabilei nu îi afectează valoarea de adevăr. Cu alte cuvinte, o propoziție este adevărată după M și $\mu$ dacă și numai dacă este adevărată în raport cu M și cu orice altă atribuire de variabilă $\mu '$ .

Există o a doua abordare comună pentru definirea valorilor de adevăr care nu se bazează pe funcții de atribuire a variabilelor. În schimb, dată fiind o interpretare M, se adaugă mai întâi semnăturii o colecție de simboluri constante, câte unul pentru fiecare element al universului de discurs în M; se spune că pentru orice d din univers, simbolul constant c_d este fix. Interpretarea se extinde astfel încât oricărui nou simbol constant să îi fie atribuit elementul său corespunzător din univers. Se definește acum adevărul pentru formulele cuantificate din punct de vedere sintactic, după cum urmează:

Cuantificatori existențiali (alternativă). O formulă $\exists x\varphi (x)$ este adevărată după M dacă există un d în domeniul discursului astfel încât $\varphi (c_{d})$ este adevărată. Aici $\varphi (c_{d})$ este rezultatul înlocuirii lui c_d în fiecare apariție liberă a lui x în φ.
Cuantificatori universali (alternativă). O formulă $\forall x\varphi (x)$ este adevărată după M dacă, pentru fiecare d din universul de discurs, $\varphi (c_{d})$ este adevărată după M.

Această abordare alternativă oferă exact aceleași valori de adevăr tuturor propozițiilor ca abordarea prin atribuiri de variabilă.

Validitate, satisfiabilitate și consecință logică[modificare | modificare sursă]

Dacă o propoziție φ se evaluează ca adevărată în raport cu o interpretare dată M, se spune că M satisface φ; aceasta se notează cu^[19] $M\vDash \varphi$ . O propoziție este satisfiabilă dacă există o interpretare conform căreia este adevărată. Acesta este puțin diferit de simbolul $\vDash$ din teoria modelelor, unde cu $M\vDash \phi$ se notează satisfiabilitatea într-un model, adică „există o atribuire adecvată a valorilor în domeniul lui $M$ cu simboluri variabile ale lui $\phi$ ”.^[20]

Satisfabilitatea formulelor cu variabile libere este mai complicată, deoarece o interpretare în sine nu determină valoarea de adevăr a unei astfel de formule. Cea mai comună convenție este aceea că o formulă φ cu variabile libere $x_{1}$ , ..., $x_{n}$ se spune că este satisfăcută de o interpretare dacă formula φ rămâne adevărată, indiferent de indivizii din universul de discurs care sunt alocați variabilelor sale libere $x_{1}$ , . . ., $x_{n}$ . Acest lucru are același efect ca a spune că o formulă φ este satisfăcută dacă și numai dacă închiderea sa universală $\forall x_{1}\dots \forall x_{n}\phi (x_{1},\dots ,x_{n})$ este satisfacută.

O formulă este validă din punct de vedere logic (sau pur și simplu validă) dacă este adevărată în orice interpretare.^[21] Aceste formule joacă un rol similar cu tautologiile din logica propozițională.

O formulă φ este o consecință logică a unei formule ψ dacă orice interpretare care face ca ψ să fie adevărată face și φ adevărată. În acest caz se spune că φ este logic implicat de ψ.

Algebrizări[modificare | modificare sursă]

O abordare alternativă a semanticii logicii de ordinul întâi derivă din algebra abstractă. Această abordare generalizează algebrele Lindenbaum-Tarski ale logicii propoziționale. Există trei moduri de eliminare a variabilelor cuantificate din logica de ordinul întâi care nu implică înlocuirea cuantificatorilor cu alți operatori de termeni de legare a variabilelor:

Algebra cilindrică, a lui Alfred Tarski și a colegilor lui;
Algebra poliadică, a lui Paul Halmos ;
Logica predicat functor, în principal datorită lui Willard Quine.

Aceste algebre sunt toate latice care extind în mod corespunzător algebra booleană cu două elemente.

Tarski și Givant (1987) au arătat că fragmentul logicii de ordinul întâi care nu are nicio propoziție atomică care se află în domeniul de aplicare a mai mult de trei cuantificatori are aceeași putere expresivă ca și algebra relațiilor.^[22]^:32–33 Acest fragment este de mare interes deoarece este suficient pentru aritmetica Peano și cea mai mare parte din teoria axiomatică a mulțimilor, inclusiv ZFC canonic. Ei demonstrează și că logica de ordinul întâi cu o pereche ordonată primitivă este echivalentă cu o algebră de relații cu funcțiile de proiecție de două perechi ordonate.^[23]^:803

Teorii de ordinul întâi, modele și clase elementare[modificare | modificare sursă]

O teorie de ordinul întâi de o anumită signatură este o mulțime de axiome care sunt propoziții formate din simboluri din acea semnătură. Mulțimea de axiome este adesea finită sau recursiv enumerabilă, caz în care teoria se numește efectivă. Unii autori impun ca teoriile să includă și toate consecințele logice ale axiomelor. Se consideră că axiomele sunt valabile în cadrul teoriei și din ele pot fi derivate alte propoziții care sunt valabile în cadrul teoriei.

Se spune că o structură de ordinul întâi care satisface toate propozițiile dintr-o anumită teorie este un model al teoriei. O clasă elementară este mulțimea tuturor structurilor care satisfac o anumită teorie. Aceste clase sunt un subiect principal de studiu în teoria modelelor.

Multe teorii au o interpretare intenționată, un anumit model de care se ține cont atunci când se studiază teoria. De exemplu, interpretarea intenționată a aritmeticii Peano constă în numerele naturale obișnuite cu operațiile lor obișnuite. Cu toate acestea, teorema Löwenheim–Skolem arată că majoritatea teoriilor de ordinul întâi vor avea și alte modele nestandard.

O teorie este consistentă dacă nu se poate demonstra o contradicție din axiomele teoriei. O teorie este completă dacă, pentru orice formulă din signatura ei, fie acea formulă, fie negația ei este o consecință logică a axiomelor teoriei. Teorema de incompletitudine a lui Gödel arată că teoriile eficiente de ordinul întâi care includ o porțiune suficientă din teoria numerelor naturale nu pot fi niciodată și complete și consistente.

Domenii vide[modificare | modificare sursă]

Definiția de mai sus impune ca universul de discurs al oricărei interpretări să fie nevid. Există contexte, cum ar fi logica incluzivă, în care sunt permise universuri vide. Mai mult, dacă o clasă de structuri algebrice include o structură vidă (de exemplu, există o multime parțial ordonată vidă), acea clasă poate fi o clasă elementară în logica de ordinul întâi numai dacă universurile vide sunt permise sau structura vidă este eliminată din clasă.

Cu toate acestea, există mai multe dificultăți cu universurile vide:

Multe reguli de inferență comune sunt valabile numai atunci când universul de discurs trebie neapărat să fie nevid. Un exemplu este regula care spune că $\varphi \lor \exists x\psi$ implică $\exists x(\varphi \lor \psi )$ când x nu este o variabilă liberă în $\varphi$ . Această regulă, care este folosită pentru a pune formule în forma normală prenexă, este corectă în universurile nevide, dar nu are sens dacă este permis universul vid.
Definiția adevărului într-o interpretare care utilizează o funcție de atribuire a variabilelor nu poate funcționa cu universuri vide, deoarece nu există funcții de atribuire a variabilelor al căror domeniu de definiție este vid. (În mod similar, nu se pot atribui interpretări simbolurilor constante.) Această definiție a adevărului necesită selectarea unei funcții de alocare a variabilelor (μ mai sus) înainte de a putea fi definite valorile de adevăr chiar și pentru formule atomice. Apoi valoarea de adevăr a unei propoziții este definită ca fiind valoarea sa de adevăr în cadrul oricărei atribuiri variabile și se demonstrează că această valoare de adevăr nu depinde de ce atribuire este aleasă. Această tehnică nu funcționează dacă nu există nicio funcție de atribuire; trebuie schimbată pentru a face loc posibilității universurilor vide.

Astfel, atunci când se permite universul vid, acesta trebuie adesea tratat ca un caz special. Majoritatea autorilor exclud pur și simplu domeniul vid prin definiție.

Sisteme deductive[modificare | modificare sursă]

Un sistem deductiv este folosit pentru a demonstra, pe o bază pur sintactică, că o formulă este consecința logică a unei alte formule. Există multe astfel de sisteme pentru logica de ordinul întâi, inclusiv sistemele deductive în stil Hilbert, deducția naturală, calculul cu secvenți, metoda tablourilor și rezoluția. Acestea au proprietatea comună că o deducție este un obiect sintactic finit; formatul acestui obiect și modul în care este construit variază foarte mult. Aceste deducții finite în sine sunt adesea numite derivări în teoria demonstrației. Ele sunt numite adesea și demonstrații, dar sunt complet formalizate spre deosebire de demonstrațiile matematice în limbaj natural.

Un sistem deductiv este corect (în engleză sound) dacă orice formulă care poate fi derivată în sistem este validă din punct de vedere logic. În schimb, un sistem deductiv este complet dacă fiecare formulă validă din punct de vedere logic este derivabilă. Toate sistemele discutate în acest articol sunt atât corecte, cât și complete. Ele au în comun și proprietatea că este posibil să se verifice efectiv că o deducție pretins validă este în fapt o deducție; astfel de sisteme de deducție se numesc efective.

O proprietate cheie a sistemelor deductive este că sunt pur sintactice, astfel încât derivările pot fi verificate fără a lua în considerare nicio interpretare. Astfel, un argument corect este corect în orice interpretare posibilă a limbajului, indiferent dacă acea interpretare este despre matematică, economie sau vreun alt domeniu.

În general, consecința logică în logica de ordinul întâi este doar semidecidabilă: dacă o propoziție A implică logic o propoziție B, atunci aceasta poate fi descoperită (de exemplu, prin căutarea unei demonstrații până când se găsește un sistem de demonstrații eficient, corect și complet). Totuși, dacă A nu implică logic B, aceasta nu înseamnă că A implică logic negația lui B. Nu există nicio procedură efectivă care, pornind de la formulele A și B, să decidă întotdeauna corect dacă A implică logic B.

Reguli de inferență[modificare | modificare sursă]

O regulă de inferență afirmă că, pornind de la o anumită formulă (sau un set de formule) cu o anumită proprietate ca ipoteză, o altă formulă specifică (sau un set de formule) poate fi derivat drept concluzie. Regula este corectă (sau conservă adevărul) dacă își păstrează validitatea în sensul că ori de câte ori orice interpretarea satisface ipoteza, acea interpretare satisface și concluzia.

De exemplu, o regulă comună de inferență este regula substituției. Dacă t este un termen și φ este o formulă care poate conține variabila x, atunci φ[ t / x ] este rezultatul înlocuirii tuturor instanțelor libere ale lui x cu t în φ. Regula substituției spune că pentru orice φ și orice termen t, se poate concluziona φ[ t / x ] din φ cu condiția ca nicio variabilă liberă a lui t să nu devină legată în timpul procesului de substituție. (Dacă o variabilă liberă a lui t devine legată, atunci pentru a înlocui t cu x, este mai întâi necesar să se schimbe variabilele legate ale lui φ pentru a fi diferite de variabilele libere ale lui t.)

Pentru a vedea de ce este necesară restricția asupra variabilelor legate, fie formula validă logic φ dată de $\exists x(x=y)$ , din signatura (0,1,+,×,=) a aritmeticii. Dacă t este termenul "x + 1", formula φ[ t / y ] este $\exists x(x=x+1)$ , ceea ce va fi fals în multe interpretări. Problema este că variabila liberă x a lui t a devenit legată în timpul substituției. Înlocuirea intenționată poate fi obținută prin redenumirea variabilei legate x a lui φ la altceva, să spunem z, astfel încât formula după substituție să fie $\exists z(z=x+1)$ , care este din nou corectă din punct de vedere logic.

Regula de substituție demonstrează câteva aspecte comune ale regulilor de inferență. Este în întregime sintactică; se poate spune dacă a fost corect aplicată fără a face apel la vreo interpretare. Are limitări (definite sintactic) cu privire la momentul în care poate fi aplicată, care trebuie respectate pentru a păstra corectitudinea derivărilor. Mai mult, așa cum este adesea cazul, aceste limitări sunt necesare din cauza interacțiunilor dintre variabilele libere și cele legate care apar în timpul manipulărilor sintactice ale formulelor implicate în regula de inferență.

Sisteme în stil Hilbert și deducția naturală[modificare | modificare sursă]

O deducție într-un sistem deductiv în stil Hilbert este o listă de formule, fiecare fiind o axiomă logică, o ipoteză care a fost presupusă pentru derivarea efectuată la acel moment sau care decurge din formulele anterioare printr-o regulă de inferență. Axiomele logice constau din mai multe scheme axiomatice de formule logic valide; acestea cuprind o cantitate semnificativă de logică propozițională. Regulile de inferență permit manipularea cuantificatorilor. Sistemele tipice în stil Hilbert au un număr mic de reguli de inferență, împreună cu câteva scheme infinite de axiome logice. Este obișnuit să avem ca reguli de inferență doar modus ponens și generalizarea universală.

Sistemele naturale de deducție seamănă cu sistemele în stil Hilbert prin aceea că o deducție este o listă finită de formule. Sistemele naturale de deducție nu au însă axiome logice; ele compensează prin adăugarea unor reguli suplimentare de inferență care pot fi folosite pentru a manipula conexiunile logice din formulele din demonstrație.

Calculul cu secvenți[modificare | modificare sursă]

Calculul cu secvenți a fost dezvoltat pentru a studia proprietățile sistemelor naturale de deducție.^[24] În loc să lucreze cu o singură formulă la un moment dat, se folosesc secvenți, care sunt expresii de forma

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},

unde A ₁, . . ., A _n, B ₁, . . ., B _k sunt formule și simbolul $\vdash$ este folosit ca punct de punctuație pentru a separa cele două jumătăți. Intuitiv, un secvent exprimă ideea că $(A_{1}\land \cdots \land A_{n})$ implică $(B_{1}\lor \cdots \lor B_{k})$ .

Formule atomice (1). Unei formule $P(t_{1},\ldots ,t_{n})$ i se asociaza valoarea adevărat sau fals după cum $\langle v_{1},\ldots ,v_{n}\rangle \in I(P)$ sau nu, unde $v_{1},\ldots ,v_{n}$ sunt evaluarea termenilor $t_{1},\ldots ,t_{n}$ și $I(P)$ este interpretarea lui $P$ , care din ipoteză este o submulțime a lui $D^{n}$ .
Formule atomice (2) . Unei formule $t_{1}=t_{2}$ i se atribuie valoarea adevărat dacă $t_{1}$ și $t_{2}$ se evaluează la același obiect din universul de discurs (vezi secțiunea despre egalitate de mai jos).
Conectori logici. O formulă de forma $\neg \varphi$ , $\varphi \rightarrow \psi$ , etc. se evaluează conform tabelei de adevăr pentru conectorul respectiv, ca în logica propozițională.
Cuantificatori existențiali. O formulă $\exists x\varphi (x)$ este adevărată după M și $\mu$ dacă există o evaluare $\mu '$ a variabilelor care diferă de $\mu$ numai în ceea ce privește evaluarea lui x și astfel încât φ să fie adevărată în raport cu interpretarea M și cu atribuirea variabilei $\mu '$ . Această definiție formală surprinde ideea că $\exists x\varphi (x)$ este adevărată dacă și numai dacă există o modalitate de a alege o valoare pentru x astfel încât φ( x ) să fie satisfăcută.
Cuantificatori universali. O formulă $\forall x\varphi (x)$ este adevărată după M și $\mu$ dacă φ( x ) este adevărată pentru fiecare pereche compusă din interpretarea M și o anumită atribuire a variabilei $\mu '$ care diferă de $\mu$ numai prin valoarea lui x. Aceasta surprinde ideea că $\forall x\varphi (x)$ este adevărată dacă orice alegere posibilă a unei valori pentru x face ca φ(x) să fie adevărată.

Universul de discurs D este o mulțime nevidă de „obiecte” de un fel. Intuitiv, dată fiind o interpretare, o formulă de ordinul întâi devine o afirmație despre aceste obiecte; de exemplu, $\exists xP(x)$ afirmă existența unui obiect în D pentru care predicatul P este adevărat (sau, mai precis, pentru care predicatul atribuit simbolului de predicat P prin interpretare este adevărat). De exemplu, se poate lua D ca fiind mulțimea numerelor întregi. [[Categorie:Pagini cu traduceri nerevizuite]]

^ Hodgson, Dr. J. P. E., "First Order Logic" (archive.org), Saint Joseph's University, Philadelphia, 1995.
^ Hughes, G. E., & Cresswell, M. J., A New Introduction to Modal Logic (London: Routledge, 1996), p.161.
^ ^a ^b A. Tarski, Undecidable Theories (1953), p.77. Studies in Logic and the Foundation of Mathematics, North-Holland
^ Mendelson, Elliott (1964). Introduction to Mathematical Logic. Van Nostrand Reinhold. p. 56.
^ Eric M. Hammer: Semantics for Existential Graphs, Journal of Philosophical Logic, Volume 27, Issue 5 (October 1998), page 489: "Development of first-order logic independently of Frege, anticipating prenex and Skolem normal forms"
^ Goertzel, B., Geisweiller, N., Coelho, L., Janičić, P., & Pennachin, C., Real-World Reasoning: Toward Scalable, Uncertain Spatiotemporal, Contextual and Causal Inference (Amsterdam & Paris: Atlantis Press, 2011), p. 29.
^ „Predicate Logic | Brilliant Math & Science Wiki”. brilliant.org (în engleză). Accesat în 20 august 2020.
^ „Introduction to Symbolic Logic: Lecture 2”. cstl-cla.semo.edu. Accesat în 4 ianuarie 2021.
^ Hans Hermes (1973). Introduction to Mathematical Logic. Hochschultext (Springer-Verlag). London: Springer. ISBN 3540058192.
^ More precisely, there is only one language of each variant of one-sorted first-order logic: with or without equality, with or without functions, with or without propositional variables, ....
^ The word language is sometimes used as a synonym for signature, but this can be confusing because "language" can also refer to the set of formulas.
^ Eberhard Bergmann and Helga Noll (1977). Mathematische Logik mit Informatik-Anwendungen. Heidelberger Taschenbücher, Sammlung Informatik (în germană). 187. Heidelberg: Springer. pp. 300–302.
^ Smullyan, R. M., First-order Logic (New York: Dover Publications, 1968), p. 5.
^ G. Takeuti, 'Proof Theory' (1989, p.6)
^ Some authors who use the term "well-formed formula" use "formula" to mean any string of symbols from the alphabet. However, most authors in mathematical logic use "formula" to mean "well-formed formula" and have no term for non-well-formed formulas. In every context, it is only the well-formed formulas that are of interest.
^ Clark Barrett; Aaron Stump; Cesare Tinelli. „The SMT-LIB Standard: Version 2.0”. SMT-LIB. Accesat în 15 iunie 2019.
^ ^a ^b ^c W. V. O. Quine, Mathematical Logic (1981). Harvard University Press, 0-674-55451-5.
^ y occurs bound by rule 4, although it doesn't appear in any atomic subformula
^ It seems that symbol $\vDash$ was introduced by Kleene, see footnote 30 in Dover's 2002 reprint of his book Mathematical Logic, John Wiley and Sons, 1967.
^ F. R. Drake, Set theory: An introduction to large cardinals (1974)
^ Rogers, R. L., Mathematical Logic and Formalized Theories: A Survey of Basic Concepts and Results (Amsterdam/London: North-Holland Publishing Company, 1971), p. 39.
^ Brink, C., Kahl, W., & Schmidt, G., eds., Relational Methods in Computer Science (Berlin / Heidelberg: Springer, 1997), pp. 32–33.
^ Anon., Mathematical Reviews (Providence: American Mathematical Society, 2006), p. 803.
^ Shankar, N., Owre, S., Rushby, J. M., & Stringer-Calvert, D. W. J., PVS Prover Guide 2.4 (Menlo Park: SRI International, November 2001).

[1] Hodgson, Dr. J. P. E., "First Order Logic" (archive.org), Saint Joseph's University, Philadelphia, 1995.

[2] Hughes, G. E., & Cresswell, M. J., A New Introduction to Modal Logic (London: Routledge, 1996), p.161.

[Tarski53-3] A. Tarski, Undecidable Theories (1953), p.77. Studies in Logic and the Foundation of Mathematics, North-Holland

[4] Mendelson, Elliott (1964). Introduction to Mathematical Logic. Van Nostrand Reinhold. p. 56.

[5] Eric M. Hammer: Semantics for Existential Graphs, Journal of Philosophical Logic, Volume 27, Issue 5 (October 1998), page 489: "Development of first-order logic independently of Frege, anticipating prenex and Skolem normal forms"

[6] Goertzel, B., Geisweiller, N., Coelho, L., Janičić, P., & Pennachin, C., Real-World Reasoning: Toward Scalable, Uncertain Spatiotemporal, Contextual and Causal Inference (Amsterdam & Paris: Atlantis Press, 2011), p. 29.

[7] „Predicate Logic | Brilliant Math & Science Wiki”. brilliant.org (în engleză). Accesat în 20 august 2020.

[8] „Introduction to Symbolic Logic: Lecture 2”. cstl-cla.semo.edu. Accesat în 4 ianuarie 2021.

[9] Hans Hermes (1973). Introduction to Mathematical Logic. Hochschultext (Springer-Verlag). London: Springer. ISBN 3540058192.

[10] More precisely, there is only one language of each variant of one-sorted first-order logic: with or without equality, with or without functions, with or without propositional variables, ....

[11] The word language is sometimes used as a synonym for signature, but this can be confusing because "language" can also refer to the set of formulas.

[12] Eberhard Bergmann and Helga Noll (1977). Mathematische Logik mit Informatik-Anwendungen. Heidelberger Taschenbücher, Sammlung Informatik (în germană). 187. Heidelberg: Springer. pp. 300–302.

[13] Smullyan, R. M., First-order Logic (New York: Dover Publications, 1968), p. 5.

[14] G. Takeuti, 'Proof Theory' (1989, p.6)

[15] Some authors who use the term "well-formed formula" use "formula" to mean any string of symbols from the alphabet. However, most authors in mathematical logic use "formula" to mean "well-formed formula" and have no term for non-well-formed formulas. In every context, it is only the well-formed formulas that are of interest.

[16] Clark Barrett; Aaron Stump; Cesare Tinelli. „The SMT-LIB Standard: Version 2.0”. SMT-LIB. Accesat în 15 iunie 2019.

[Quine81-17] W. V. O. Quine, Mathematical Logic (1981). Harvard University Press, 0-674-55451-5.

[18] y occurs bound by rule 4, although it doesn't appear in any atomic subformula

[19] It seems that symbol $\vDash$ was introduced by Kleene, see footnote 30 in Dover's 2002 reprint of his book Mathematical Logic, John Wiley and Sons, 1967.

[20] F. R. Drake, Set theory: An introduction to large cardinals (1974)

[21] Rogers, R. L., Mathematical Logic and Formalized Theories: A Survey of Basic Concepts and Results (Amsterdam/London: North-Holland Publishing Company, 1971), p. 39.

[22] Brink, C., Kahl, W., & Schmidt, G., eds., Relational Methods in Computer Science (Berlin / Heidelberg: Springer, 1997), pp. 32–33.

[23] Anon., Mathematical Reviews (Providence: American Mathematical Society, 2006), p. 803.

[24] Shankar, N., Owre, S., Rushby, J. M., & Stringer-Calvert, D. W. J., PVS Prover Guide 2.4 (Menlo Park: SRI International, November 2001).

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]