Logica matematica: cos’è: tutto sull’argomento

03-XX

03-XX è la sigla della sezione di livello 1 dello schema di classificazione MSC dedicata alla logica matematica e ai fondamenti della matematica.

Logica matematica

La logica matematica è il settore della matematica che studia i sistemi formali dal punto di vista del modo di codificare i concetti intuitivi della dimostrazione e di computazione come parte dei fondamenti della matematica. Essa si occupa delle parti della logica che possono essere modellate matematicamente. Altri termini utilizzati spesso nel passato sono logica simbolica e metamatematica, termine che ora si applica più specificamente a taluni aspetti della teoria della dimostrazione.

Algebra di Heyting

Un’algebra di Heyting è la struttura di verità della logica intuizionista.

Algoritmo di Tison

L’algoritmo di Tison è un algoritmo che permette la riduzione e la semplificazione di funzioni logiche per la determinazione della somma minima. Si compone dei seguenti passi:

1. 1. Si elencano le variabili bivariate della funzione,
   2. Si calcolano i consensi rispetto ad ogni variabile bivariata presente e si sommano alla funzione in esame,

Anello booleano

In matematica un anello booleano (R,+,·) è un anello unitario per il quale x² = x per ogni elemento x del suo sostegno R. In altre parole è un anello costituito solo da elementi idempotenti.

Aritmetica di Peano

L’aritmetica di Peano, denotata anche con l’acronimo PA in logica matematica è una teoria del primo ordine che ha come assiomi propri una versione degli assiomi di Peano espressi nel linguaggio del primo ordine.

Aritmetica di Robinson

L’aritmetica di Robinson, denotata solitamente con Q in logica matematica, è una teoria del primo ordine, definita per la prima volta da Raphael M. Robinson nel 1950 che ha come assiomi propri una versione ridotta degli assiomi di Peano in cui è assente il principio di induzione e c’è l’aggiunta di un assioma che afferma che ogni numero naturale diverso da zero è successore di qualche altro numero. L’interesse dell’aritmetica di Robinson per la logica risiede nel fatto che è la teoria più debole in cui è possibile rappresentare tutte le funzioni ricorsive primitive e di conseguenza è anche la teoria più debole a cui sia applicabile il primo dei teoremi di incompletezza di Gödel.

Asserzione (logica)

L’asserzione logica è una dichiarazione che afferma che una certa premessa è vera. È equivalente ad un sequente senza antecedente.

Assioma (matematica)

In matematica si chiamano postulati o assiomi tutti e soli gli enunciati che, pur non essendo stati dimostrati, sono considerati veri. Generalmente forniscono il punto di partenza per delineare un quadro teorico come può essere quello della teoria degli insiemi, della geometria, dell’aritmetica, della teoria dei gruppi o nel calcolo delle probabilità.

Assioma logico

Gli assiomi logici sono un insieme (infinito) di assiomi di una teoria del primo ordine che formalizzano tutte le deduzioni logiche che solitamente si fanno nelle dimostrazioni matematiche. Ci sono diversi modi di ottenere questo tipo di formalizzazione. Uno di questi è dato dal seguente insieme di assiomi:

Per ogni form

Assioma proprio

Gli assiomi propri di una teoria sono gli assiomi che specificano fatti relativi agli oggetti della teoria che non sono deducibili dalla logica pura e semplice ma che sono invece legati alla particolare natura di quegli oggetti.

Assiomi per l’uguaglianza

Gli assiomi per l’uguaglianza sono un insieme di assiomi che possono far parte di una teoria del primo ordine allo scopo di formalizzare tutte le normali deduzioni che in matematica si fanno con la relazione di uguaglianza. Se il ruolo di “uguaglianza” nella teoria è svolto dal simbolo di relazione binaria  allora gli assiomi per l’uguaglianza per  sono i seguenti:

Autoinformazione

L’autoinformazione di un evento è la quantità d’incertezza associata all’evento, ovvero l’informazione che si ottiene affermando innanzitutto che tale evento si sia realizzato, e rimuovendo quindi l’incertezza associata. Tale concetto viene introdotto nell’ambito della Teoria dell’informazione, ponendone le basi.

Base di connettivi

Con base di connettivi s’intende un sottoinsieme di connettivi logici coi quali è possibile dare la definizione logica di tutti gli altri connettivi. Questa proprietà viene chiamata anche completezza funzionale.

Base di Herbrand

In logica matematica, per ogni linguaggio formale con un insieme di termini dall’universo di Herbrand, la base di Herbrand definisce ricorsivamente l’insieme di tutte le formule atomiche che possono essere composte formando predicati dai termini dell’universo di Herbrand. Una base di Herbrand di un linguaggio del primo ordine  può essere costruita dall’universo di Herbrand di , applicando a ogni suo elemento qualche predicato di . È dunque l’insieme di tutti gli atomi ground che possono essere costruiti usando simboli da . Prende il nome da Jacques Herbrand. Nella base di Herbrand ogni elemento viene chiamato atomo.

Egon Börger

Egon Börger è un matematico e informatico tedesco.

Chiusura deduttiva

In matematica la chiusura deduttiva consiste nell’insieme di deduzioni che possono essere ricavate a partire da un insieme di assiomi.

Chiusura universale

In logica matematica e più in particolare in una teoria del primo ordine si chiama chiusura universale di una formula ben formata  in cui  sono variabili libere, la formula

Codice di Hamming

Nelle telecomunicazioni il codice di Hamming è un codice correttore lineare che prende il nome dal suo inventore Richard Hamming. Il codice di Hamming può rilevare e correggere gli errori di un singolo bit. In altre parole, la distanza di Hamming tra le code-word trasmesse e ricevute deve essere zero o uno per una comunicazione affidabile. In alternativa, il codice può rivelare errori doppi.

Coerenza (logica matematica)

In logica matematica, una teoria formale si dice coerente se in essa è impossibile dimostrare una contraddizione.

Completezza (logica matematica)

Nella logica matematica il concetto di completezza esprime il fatto che un insieme di assiomi è sufficiente a dimostrare tutte le verità di una teoria e quindi a decidere della verità o falsità di qualunque enunciato formulabile nel linguaggio della teoria.

Condizione necessaria e sufficiente

Una condizione necessaria e sufficiente, nella logica di una proposizione, è quell’evento che è vero se e solo se la proposizione è vera.

Connettivo logico

Un connettivo logico o operatore logico, è un elemento grammaticale di collegamento che instaura fra due proposizioni A e B una qualche relazione che dia origine ad una terza proposizione C con un valore vero o falso, in base ai valori delle due proposizioni fattori ed al carattere del connettivo utilizzato.

Correttezza (logica matematica)

In logica matematica, la correttezza o validità è una proprietà fondamentale delle regole logiche e dei calcoli logici.

Decidibilità

Il concetto di decidibilità si trova in logica matematica e in teoria della computabilità con accezioni differenti.

Deduzione naturale

La deduzione naturale è, nel campo della logica, un sistema deduttivo. Un sistema deduttivo è una relazione che può sussistere tra un insieme di formule e una formula: se la relazione vale, diciamo che la formula viene dedotta dall’insieme. La deduzione naturale si propone quindi come un metodo per dimostrare che un’affermazione è conseguenza di certe ipotesi. A differenza dei sistemi assiomatici è un sistema senza assiomi, basato su una serie di regole di inferenza il cui numero dipende dai connettivi che definiamo come primitivi.

Dimostrazione matematica

Una dimostrazione matematica è un processo di deduzione che, partendo da premesse assunte come valide (ipotesi) o da proposizioni dimostrate in virtù di queste premesse, determina la necessaria validità di una nuova proposizione in virtù della (sola) correttezza formale del ragionamento.

Distanza di Hamming

Nella teoria dell’informazione, la distanza di Hamming tra due stringhe di ugual lunghezza è il numero di posizioni nelle quali i simboli corrispondenti sono diversi. In altri termini, la distanza di Hamming misura il numero di sostituzioni necessarie per convertire una stringa nell’altra, o, vista in altro modo, il numero minimo di errori che possono aver portato alla trasformazione di una stringa nell’altra.

Esagono logico

L’esagono logico è un modello concettuale delle relazioni esistenti fra i valore di verità di sei proposizioni. Si tratta di una estensione del quadrato delle opposizioni, derivato da Aristotele.
Per vie parallele e indipendenti, fu scoperto dal logico francese Augustin Sesmat (1885-1957)

Estensione conservativa

In logica matematica, nell’ambito della teoria della dimostrazione, un’estensione conservativa di una teoria logica T₁ è una teoria T₂ tale che:

• tutti i simboli di T₁ sono presenti anche in T₂
• ogni teorema di T₁ è anche un teorema di T₂

Fondamenti della matematica

Per fondamenti della matematica si intende lo studio delle basi logiche e filosofiche della matematica.

Formula ben formata

Nella logica matematica si chiama formula ben formata o – brevemente – FBF di un sistema formale una stringa di simboli che, intuitivamente, rappresenti un’espressione sintatticamente corretta e che viene definita mediante le regole della grammatica del sistema formale stesso.

Formula di Barcan

In logica modale, la formula di Barcan e l’inverso della formula di Barcan definiscono una relazione tra quantificatori e operatori modali.

Funtori di Sheffer

I funtori di Sheffer, sono due connettivi logici molto potenti, poiché ciascuno da solo costituisce una base di connettivi. Essi sono stati ideati da Henry Sheffer.

Funzione di ordine superiore

Una funzione di ordine superiore è una funzione che può prendere altre funzioni come parametri e/o restituire funzioni come risultato. L’operatore differenziale in matematica è un esempio di funzione che mappa una funzione ad un’altra funzione.

Identità (logica moderna)

Diversamente dalla logica classica nella logica moderna l’identità è una relazione definita normalmente come binaria, che intercorre tra una cosa e sé stessa. In altri termini, l’identità è un predicato duale tale che per ogni “x” e “y”, x = y è vero se e solo se x è lo stesso che “y”.

Informazione parziale linearizzata

L’informazione parziale linearizzata (LPI) è un metodo per prendere decisioni basate su informazioni insufficienti, sfumate o incerte. La LPI è stata introdotta nel 1970 dal matematico polacco, naturalizzato svizzero, Edward Kofler, per semplificare i processi di decisione.

Legge di Peirce

In logica, la legge di Peirce deriva il suo nome dal filosofo e logico Charles Sanders Peirce. Essa è compresa tra gli assiomi nella sua prima assiomatizzazione della logica proposizionale. Si può considerare come un tertium non datur scritto in una forma che preveda solo un tipo di connettivo, ossia l’implicazione. È una tautologia della logica proposizionale.

Lemma di König

Il Lemma di König in logica afferma che:

Se un albero, in cui ogni nodo ha un numero finito di successori immediati, ha infiniti nodi allora in esso c’è anche un ramo infinito.

Linguaggio del primo ordine

Nella logica matematica il linguaggio del primo ordine, detto anche logica dei predicati del primo ordine, è un linguaggio formale che serve per gestire meccanicamente enunciati e ragionamenti che coinvolgono i connettivi logici, le relazioni e i quantificatori “per ogni …” (∀) ed “esiste…” (∃). L’espressione “del primo ordine” indica che c’è un insieme di riferimento e i quantificatori possano riguardare solo gli elementi di tale insieme e non i sottoinsiemi; ad esempio si può dire “per tutti gli x elementi dell’insieme vale P(x)” ma non si può dire “per tutti i sottoinsiemi A vale P(A)”.

Linguaggio dell’aritmetica del primo ordine

In logica matematica il linguaggio dell’aritmetica del primo ordine è un linguaggio del primo ordine con cui è possibile sviluppare teorie formali dell’aritmetica elementare come l’aritmetica di Peano e l’aritmetica di Robinson.

Lista di regole di inferenza

Regole di inferenza di uso comune.

• Reductio ad absurdum

Logica libera

Una logica libera è una logica non classica, che ha un minor importo esistenziale della logica del primo ordine. Una logica libera permette ai termini di non denotare alcun membro del dominio di quantificazione; quando, oltre a questa possibilità, si aggiunge quella per il dominio di quantificazione di essere vuoto, si parla di logica inclusiva.

Logica lineare

La logica lineare è una logica substrutturale proposta da Jean-Yves Girard come un raffinamento della logica classica ed intuizionista, coniugando le dualità che caratterizzano i connettivi della prima con le proprietà costruttive della seconda. Sebbene questo sistema logico sia un oggetto di studio fine a se stesso, più in generale le idee della logica lineare hanno influito in settori come i linguaggi di programmazione, la game semantics o la fisica dei quanti e la linguistica, in particolare per la sua enfasi sulle risorse limitate, la dualità e l’interazione.

Logica modale

Nell’ambito della logica formale, si indica come logica modale una qualsiasi logica in cui è possibile esprimere il “modo” in cui una proposizione è vera o falsa. Storicamente, gli studi di logica modale sono iniziati con i concetti di possibilità e necessità. Tuttavia, la logica modale contemporanea si occupa di numerosi altri concetti, come quello di obbligo morale o come quelli di credenza. Esempi di proposizioni modali sono, quindi, “È possibile che piova” o “È necessario che Socrate sia mortale o non mortale”, ma anche “È doveroso andare a votare” o “Socrate crede che piova”.

Logica paraconsistente

In logica, per logica paraconsistente si intende un sistema formale in cui possono verificarsi in modo controllato delle eccezioni al principio di non contraddizione, cioè possono presentarsi delle contraddizioni, senza però che con questo sia possibile derivare nel sistema ogni proposizione, evitando quindi il principio di esplosione.

Logica polivalente

Le logiche polivalenti sono estensioni della logica classica in cui sono presenti più valori di verità rispetto ai canonici vero, falso e pertanto in esse non vale il principio del terzo escluso. Le prime logiche polivalenti furono proposte negli anni 1920 da Emil Post e da Jan Łukasiewicz e in esse erano presenti tre valori di verità: vero, falso, problematico.

Logica temporale lineare

La logica temporale lineare o LTL è un’estensione della logica modale nella quale i mondi sono organizzati in una struttura lineare infinita: ogni mondo può così rappresentare un istante di tempo discreto. La logica LTL prevede dunque una organizzazione del tempo lineare, discreta, orientata al futuro e infinita.

Matematica inversa

La matematica inversa è un ramo della matematica che si occupa di determinare quali sono gli assiomi minimi necessari per dimostrare un particolare teorema e più in generale cerca di determinare la teoria base che costituisce la matematica nel suo complesso. Partendo da una base di assiomi debole, si può scoprire che molte proposizioni matematiche sono equivalenti all’assioma aggiunto ad essa per dimostrarlo, come ad esempio il lemma di Zorn rispetto all’assioma della scelta.

Metamatematica

La metamatematica può definirsi come la parte della filosofia della matematica che si propone di studiare la matematica da punti di vista generali. Essa venne differenziata dal resto della matematica verso la fine del XIX secolo nell’ambito delle discussioni che riguardavano quello che allora veniva chiamato problema dei fondamenti della matematica.

Metodo di Petrick

Il metodo di Petrick è un algoritmo di risoluzione dei mintermini contenuti in una tabella degli implicanti primi ricavata con il metodo di Quine-McCluskey. Tale metodo, che semplifica la copertura trasponendola in forma algebrica, risulta scomodo per tabelle molto grandi, in quanto valuta tutte le possibili soluzioni, ma è facilmente implementabile in un computer tramite algoritmi di branch and bound.

Metodo di Quine-McCluskey

Il metodo di Quine-McCluskey è un algoritmo sviluppato da Willard Van Orman Quine ed Edward McCluskey che viene utilizzato nelle reti combinatorie a due livelli di logica per la minimizzazione di una funzione booleana di n variabili. Il metodo è funzionalmente identico alla mappa di Karnaugh, ma la sua forma tabellare lo rende più efficiente per essere realizzato al computer; inoltre fornisce anche un modo deterministico per testare la minimizzazione di una funzione booleana.

Modus ponens

Nella logica, il modus ponens (MP), accorciamento del latino modus ponendo ponens, è una semplice e valida regola d’inferenza, che afferma in parole:

Se p implica q è una proposizione vera, e anche la premessa p è vera, allora la conseguenza q è vera

Motore inferenziale

In informatica, un motore inferenziale è un algoritmo che simula le modalità con cui la mente umana trae delle conclusioni logiche attraverso il ragionamento. Fa parte dei software detti “sistemi esperti”.

Numero surreale

In matematica i numeri surreali costituiscono un campo che contiene i numeri reali e anche numeri infiniti e infinitesimi, rispettivamente maggiori o minori in valore assoluto di qualunque numero reale positivo. Per questo motivo i numeri surreali sono algebricamente simili ai numeri superreali e iperreali.

Operatore di Sheffer

L’operatore di Sheffer, chiamato anche negazione alternativa o anche NAND, è uno dei due operatori introdotti dal matematico statunitense Henry Maurice Sheffer.

Paradosso di Richard

Il paradosso di Richard è formulato da Jules Antoine Richard nel 1905.

Pi calcolo

Il pi calcolo, o π-calcolo è un sistema formale che descrive e analizza le proprietà della computazione di tipo concorrente. Inizialmente sviluppato da Robin Milner, Joachim Parrow e David Walker come proseguimento del lavoro già svolto sul CCS, rispetto ai formalismi precedenti il pi calcolo è in grado di descrivere la concorrenza anche in sistemi la cui configurazione può cambiare nel tempo, dato che permette comunicazione di nomi di canali sugli stessi canali.

Potenza logica

In logica matematica, con potenza s’intende la capacità che ha un sistema formale, o un assioma, o un linguaggio formale di poter esprimere parte della matematica esistente al suo interno.

Predicato funzionale

In logica matematica, per predicato funzionale o formula funzionale o simbolo funzionale in  si intende un predicato , in cui le variabili  ed  occorrono libere, avente la seguente proprietà:

Principia Mathematica

Principia Mathematica è un’opera sui fondamenti logici della matematica scritta da Alfred North Whitehead e Bertrand Russell. L’opera è divisa in tre volumi pubblicati nel 1910, 1912, e 1913 dalla Cambridge University Press. Nel 1927 è apparsa una seconda edizione con una nuova Introduzione e una nuova Appendice C. Una versione ridotta è apparsa nel 1962 col titolo Principia Mathematica to *56.

Principio d’induzione

Il principio d’induzione è un enunciato sui numeri naturali che in matematica trova un ampio impiego nelle dimostrazioni, per provare che una certa proprietà è valida per tutti i numeri interi. L’idea intuitiva alla sua base è l’effetto domino: affinché le tessere da domino disposte lungo una fila cadano tutte sono sufficienti due condizioni:

• che cada la prima tess

Principio del buon ordinamento

In matematica, il principio del buon ordinamento, talvolta chiamato principio del minimo intero, o più propriamente principio del minimo intero naturale, afferma che:

Ogni insieme di numeri naturali non vuoto contiene un numero che è più piccolo di tutti gli altri.

Principio di Markov

Il Principio di Markov, che deve il nome ad Andrej Andreevič Markov, è una tautologia della logica classica che non è intuizionisticamente valida ma può essere giustificata costruttivamente.

Programma di Hilbert

Il programma di Hilbert consisteva nel formalizzare tutte le teorie matematiche esistenti attraverso un insieme finito di assiomi, e dimostrare che questi assiomi non conducevano a contraddizioni. Prende il nome dal matematico tedesco David Hilbert, che lo propose negli anni venti del XX secolo.

Proprietà dell’intersezione finita

La proprietà dell’intersezione finita in topologia è una proprietà di alcune famiglie non vuote di insiemi non vuoti.

Quantificatore

Nella logica i quantificatori sono espressioni come “qualcosa” e “ogni cosa” e le loro controparti simboliche:

• ∃
• ∀

Rappresentabilità

Nella logica matematica il concetto di rappresentabilità di una funzione o di un predicato è relativo alle teorie formali dell’aritmetica, ovvero alle teorie del primo ordine che hanno come linguaggio il linguaggio dell’aritmetica del primo ordine e che quindi ammettono come modello la struttura dei numeri naturali dotati delle operazioni di addizione e moltiplicazione. Esempi di tali teorie sono l’aritmetica di Peano e l’aritmetica di Robinson.

Regola di inferenza

Nella logica matematica una regola di inferenza è uno schema formale che si applica nell’eseguire un’inferenza. In altre parole, è una regola che permette di passare da un numero finito di proposizioni assunte come premesse a una proposizione che funge da conclusione.

Segnatura (logica)

Nella logica del primo ordine la segnatura è un insieme L di simboli divisi in tre categorie: simboli di costante, simboli di funzione, e simboli di relazione. Più in chiaro, una segnatura elenca e descrive i simboli non logici di un linguaggio formale. Nell’algebra universale, la segnatura elenca le operazioni che caratterizzano una struttura algebrica. Nella teoria dei modelli, è utilizzata per entrambi gli scopi. Raramente è esplicitata in trattamenti più filosofici della logica.

Sequente

Un sequente è un’entità della logica che permette di esprimere legami tra asserzioni complesse facendo uso dei legami metalinguistici e che comporta. Le prime formalizzazioni di sequenti e di calcolo dei sequenti sono dovute al lavoro del logico Gerhard Gentzen, in particolare alle sue scoperte dei primi anni Trenta.

Sillogismo disgiuntivo

Il sillogismo disgiuntivo è una regola d’inferenza derivata che applica alla disgiunzione una proprietà deduttiva di questa forma:

P o Q.

non-P.

Quindi Q.

Simulazione

Nelle scienze applicate per simulazione si intende un modello della realtà che consente di valutare e prevedere lo svolgersi dinamico di una serie di eventi o processi susseguenti all’imposizione di certe condizioni da parte dell’analista o dell’utente. Un simulatore di volo, ad esempio, consente di prevedere il comportamento dell’aeromobile a fronte delle sue caratteristiche e dei

Sistema assiomatico

In matematica, un sistema assiomatico è un insieme di assiomi che possono essere usati per dimostrare teoremi. Una teoria matematica consiste quindi in una assiomatica e tutti i teoremi che ne derivano.

Sistema formale

In logica matematica, la nozione di sistema formale è utilizzata per fornire una definizione rigorosa del concetto di dimostrazione. In altri termini, la nozione di sistema formale corrisponde ad una formalizzazione rigorosa e completa della nozione di sistema assiomatico.

Subitizing

Il termine subitizing è stato coniato nel 1949 da E.L. Kaufman e si riferisce alla capacità di distinguere in modo rapido e accurato la quantità di un ridotto numero di oggetti o elementi. Il termine deriva dall’aggettivo latino subitus (“immediato”) e indica la capacità di individuare quanti elementi sono presenti in una scena visibile, quando il numero di oggetti cade in un subitizing range. L’analoga capacità riferita a numeri grandi si riferisce al conteggio o alla stima, secondo il numero di oggetti visibili e secondo il tempo che si ha per rispondere.

Sussunzione (filosofia)

La sussunzione in filosofia è un termine della logica formale che designa la riconduzione di un concetto nell’ambito di un concetto più generale, nella cui estensione esso è compreso. Tali procedimenti sono detti anche giudizi o sillogismi sussuntivi.

Tacchino induttivista

Il tacchino induttivista è una celebre metafora ideata dal filosofo Bertrand Russell, e ripresa poi anche da Karl Popper, allo scopo di confutare le pretese di validità in senso assoluto dell’inferenza induttiva per enumerazione, cardine del metodo induttivo e dell’empirismo inglese tradizionale di filosofi quali Francesco Bacone, John Stuart Mill e delle disquisizioni del Wiener

Teorema di deduzione

Nella logica matematica, il teorema di deduzione afferma che se una formula F è deducibile da un’altra formula E allora l’implicazione E → F è dimostrabile e, viceversa, che se l’implicazione E → F è dimostrabile, allora la formula F è deducibile da E. In simboli,  se e solo se . Più in generale, esso afferma che, se da un insieme di formule Γ è dimostrabile E → F, allora F è deducibile dall’insieme di premesse [Γ + (E)].

Teorema di eliminazione del taglio

Il Teorema di eliminazione del taglio è il principale risultato che mostra l’importanza del calcolo dei sequenti. Venne dimostrato originariamente da Gerhard Gentzen nel suo storico articolo “Investigations in Logical Deduction” per i sistemi LJ ed LK, in cui sono formalizzate rispettivamente la logica intuizionista e la logica classica. Il teorema di eliminazione del taglio stabilisce che ogni giudizio che possiede nel calcolo dei sequenti una dimostrazione facente uso della regola del taglio possiede anche una dimostrazione senza taglio cioè una dimostrazione che non fa uso della regola del taglio.

Teoria degli insiemi di Zermelo

In teoria degli insiemi, con la lettera maiuscola Z, s’intende la versione assiomatica della teoria (ingenua) degli insiemi di Cantor, costruita dal matematico Ernst Zermelo, e pubblicata nel 1908.

Teoria del primo ordine

Nella logica matematica, una teoria del primo ordine è 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.

Teoria della dimostrazione

La teoria della dimostrazione è la branca della logica matematica che considera le dimostrazioni a loro volta come oggetti matematici, facilitando la loro analisi con tecniche matematiche. Le dimostrazioni sono solitamente presentate come strutture dati definite induttivamente, costruite secondo gli assiomi e le regole di inferenza del sistema logico.

Teoria formale

Una teoria formale è un metodo per produrre asserzioni in forma matematica e per permettere l’induzione di formule derivate a partire da altre formule considerate primarie.

Teoria soddisfacibile

In logica matematica, una teoria del primo ordine  si dice soddisfacibile se esiste una realizzazione  che rende vere tutte le formule di .

Teorie formali degli insiemi

Le teorie formali degli insiemi sono teorie del primo ordine con lo scopo di rappresentare le relazioni insiemistiche e fornire una base per il ragionamento matematico in generale.

Uguaglianza (matematica)

In matematica l’uguaglianza indica comunemente una relazione binaria di equivalenza fra due enti, detti membri dell’uguaglianza. Rappresenta uno dei concetti più importanti e fondamentali introdotti a livello della logica di una teoria.

Unicità

In matematica e logica, l’unicità di un elemento nel soddisfare una certa proprietà sta nel fatto che qualunque oggetto che soddisfi tale proprietà è uguale all’elemento di partenza. In altre parole, non possono esistere due elementi differenti che soddisfano questa proprietà. Tuttavia, dimostrare l’unicità di un elemento non è una condizione sufficiente per dedurre a priori l’esistenza dell’elemento.

Validità (logica)

In logica, la nozione di validità riguarda innanzitutto, ed in senso generale, la connessione tra l’insieme delle premesse di un argomento e la sua conclusione, all’interno di una argomentazione. In un argomento, le premesse devono in qualche modo giustificare l’affermazione della conclusione: esse devono fornire un fondamento all’affermazione della conclusione. Questa giustificazione deve a sua volta inevitabilmente fondarsi su una connessione tra l’insieme delle premesse e la conclusione: è perché le premesse sono connesse in un certo modo alla conclusione, che le premesse rappresentano una ragione per l’affermazione della conclusione.

Variabile libera

In logica matematica e in particolare in un linguaggio del primo ordine si dice che una variabile occorre libera in una formula ben formata  se nella formula tale variabile appare al di fuori del dominio di un quantificatore sulla variabile stessa.