Curry di Haskell Brooks (1900-1982)

Haskell Brooks Curry era un logico matematico che sviluppò una distinta filosofia della matematica. La maggior parte del suo lavoro era tecnico: fu il principale sviluppatore della logica combinatoria, che oggigiorno gioca un ruolo nell’informatica teorica. Questo formalismo originariamente doveva essere la base per un sistema di logica simbolica nel senso comune, ma il sistema originario si rivelò incoerente, e il nucleo che era consistente è poi diventato un formalismo che è una sorta di prototipo dei linguaggi informatici detti funzionali, in cui i programmi possono applicarsi e modificare altri programmi. È essenzialmente equivalente al lambda-calcolo (Calcolo λ) della Chiesa di Alonzo. (Vedi l'articolo sui λ-calcoli in questa enciclopedia.)

Il lavoro di Curry sulla logica combinatoria lo ha portato a una nozione di sistema formale che è diversa per certi aspetti da quella che da allora è diventata standard. Inoltre, Curry si interessò alla teoria della dimostrazione, soprattutto il lavoro di Gerhard Gentzen. Curry voleva utilizzare queste idee nella sua ricerca di un sistema logico coerente basato sulla logica combinatoria. All'inizio Curry lavorò anche sull'informatica, compreso il lavoro sull'ENIAC (uno dei primi computer elettronici) immediatamente dopo la seconda guerra mondiale. Finalmente, divenne noto anche per una filosofia della matematica che chiamò formalismo, che originariamente considerava come una negazione della matematica come scienza dei sistemi formali (nel suo senso), ma che in seguito estese ai metodi formali in generale. Probabilmente oggi è meglio pensare a questa idea di formalismo come a una forma di strutturalismo.

Sommario
Biografia
Logica combinatoria
Periodo iniziale
Il paradosso di Kleene-Rosser e le sue conseguenze
Periodo Tardo (dopo la seconda guerra mondiale)
Teoria della dimostrazione in stile Gentzen
Lavoro di guerra e informatica
Formalismo: la Filosofia della Matematica
Riferimenti e approfondimenti
Fonti primarie
Fonti secondarie
1. Biografia

Haskell Brooks Curry è nato il 12 settembre, 1900 a Millis, Massachusetts. Suo padre era Samuel Silas Curry, presidente della School of Expression di Boston, Massachusetts. La School of Expression è stata originariamente fondata da Anna Baright nel 1879 come School of Elocution and Expression. Fu ribattezzato nel 1885, dopo che Anna Baright sposò Samuel Silas Curry. Divenne Curry College nel 1943. Sua madre era Anna Baright, che fu Preside della Scuola di Espressione. Si diplomò al liceo nel 1916 ed entrò all'Università di Harvard con l'intenzione di specializzarsi in medicina. Durante il suo primo anno, seguì un corso di matematica su suggerimento del suo relatore e se la cavò molto bene. Nella primavera del 1917, gli Stati Uniti entrarono nella prima guerra mondiale, e Curry rispose arruolandosi nell'esercito, diventando membro del Corpo di addestramento dell'esercito studentesco il 18 ottobre, 1918. Sentiva che non avrebbe mai avuto un ruolo diretto nella guerra se avesse continuato con il suo corso pre-medico, così cambiò la sua specializzazione in matematica con l'idea di entrare nell'artiglieria. La guerra finì l'11 novembre, 1918, e Curry lasciò l'esercito il 9 dicembre, 1918, ma continuò a studiare matematica, ricevendo il suo A. B. laurea nel 1920.

Per i due anni successivi studiò ingegneria elettrica al MIT in un programma che prevedeva di lavorare a metà tempo presso la General Electric Company. Perché di solito era interessato al motivo per cui una risposta era corretta quando gli ingegneri sembravano interessati solo al fatto che fosse corretta, decise che sarebbe stato meglio conseguire una laurea in scienze pure, e nel 1922 passò alla fisica. Tornò ad Harvard, dove per l'anno 1922-23 fu assistente di ricerca a tempo parziale di P. W. Bridgman, che in seguito vinse il premio Nobel per la fisica. Nel 1924 ricevette il suo A.M. nella fisica (da Harvard). Ma a questo punto i suoi interessi si erano spostati ancora di più, e ora passò alla matematica. (Durante questo periodo, entrambi i suoi genitori sono morti, suo padre morì nel 1921 e sua madre nel 1924.)

Continuò a studiare matematica ad Harvard fino al 1927, dove fu istruttore a tempo parziale durante il primo semestre del 1926-27, ma per il resto studiò a tempo pieno. Era anche coinvolto negli affari della sua famiglia, la Scuola dell'Espressione.

Durante questo periodo, Curry si era interessato alla logica. Originariamente, tutta la sua logica era letta di lato, e ad un certo punto avrebbe dovuto lavorare su una tesi su un argomento sulle equazioni differenziali assegnatagli da George D.. Birkhoff. Inoltre, riceveva consigli da vari membri della facoltà di Harvard e altrove di stare lontano dalla logica. Questo consiglio è stato particolarmente forte da parte di Norbert Wiener, che era al MIT e che era membro dello stesso club di birdwatching di Curry. Ma Curry era troppo interessato alla logica per smettere di pensarci. Era particolarmente interessato al primo capitolo dei Principia Mathematica [Russell e Whitehead 1910-1913], che iniziò a leggere nel 1922 quando aveva 21 anni, e dove un sistema di logica proposizionale è definito mediante assiomi e due regole primitive. Il primo è il distacco, che dice che da no- o e da dedurre (ciò equivale a impostare la modalità, che dice che da e dedurre ). La seconda è la sostituzione, che dice che data qualsiasi formula, qualsiasi formula ottenuta sostituendo una variabile con un'altra formula può essere dedotta; Per esempio, se dalla formula , si può sostituire ottenere . Curry notò quando lo vide per la prima volta che la regola della sostituzione è molto più complicata del distacco, nel senso che oggi troveremmo più complicata l'implementazione in un linguaggio informatico. Nel 1926-27, come risultato del tentativo di analizzare la sostituzione fino ai suoi elementi più semplici, Curry ebbe l'idea di utilizzare operatori che chiamò combinatori, il termine che usiamo ancora oggi. Ha utilizzato questi operatori per analizzare questa regola di sostituzione, e concluse che questa idea avrebbe potuto portare a una dissertazione. Quando portò questa idea a diversi professori, ha avuto una reazione diversa da quella che aveva avuto in precedenza riguardo al tenersi lontano dalla logica. Ciò era particolarmente vero per Norbert Wiener al MIT, il quale disse che la sua opinione era che la logica fosse un argomento da evitare “a meno che non si avesse qualcosa da dire,” e poiché Curry aveva chiaramente qualcosa da dire, “forza al tuo braccio destro!"

Tuttavia, non c'era nessun membro della facoltà di Harvard che potesse supervisionare una tesi su questo argomento. Così Curry decise che sarebbe stato utile insegnare per un anno, e, dopo aver ricevuto una raccomandazione per la posizione da George D. Birkhoff, assunse un incarico di istruttore a Princeton per l'anno 1927-28. Durante una ricerca in biblioteca trovò l'articolo di Moses Schönfinkel, [Schönfinkel 1924], resoconto di un discorso tenuto a Gottinga nel 1920, che aveva chiaramente anticipato le sue idee. Curry rimase scioccato da questa anticipazione perché pensava che le sue idee fossero del tutto originali, e corse nell'ufficio di Oswald Veblen, Chi, anche se principalmente un geometra, era interessato ai fondamenti della matematica e che era anche il supervisore del dottorato di ricerca di Alonzo Church, per raccontargli l'attesa. Veblen ha calmato Curry dicendo, "Bene, Sono sempre felice quando qualcuno ha una delle mie idee, perché dimostra che sono sulla strada giusta”. Per saperne di più su Schönfinkel, Veblen poi portò Curry a vedere il topologo russo Pavel Alexandroff, che era in visita a Princeton quell'anno. Alexandroff riferì che Schönfinkel era in un ospedale psichiatrico ed era improbabile che riprendesse il suo lavoro di matematica, ma che a Gottinga c'erano parecchi matematici, compreso Paul Bernays, che probabilmente erano più veloci nel discutere questi argomenti. Fu così deciso che Curry andasse in Germania.

Come parte di una richiesta di sostegno finanziario per quel viaggio, Curry ha scritto il suo primo articolo pubblicato, [Curry 1929]. Prima di partire per la Germania, Curry sposato, il 3 luglio, 1928, Mary Virginia Wheatley di Hurlock, Maryland. (Virginia era stata una studentessa della School for Expression, dove si sono incontrati.) Dopo il matrimonio, i Curry partirono per la Germania, dove trascorsero l'anno 1928-29 a Gottinga. Durante quell'anno, Curry incontrò per la prima volta il logico Alonzo Church, che è stato lì per metà anno.

Quell'anno a Gottinga bastò a Curry per completare la sua tesi. Il suo arbitro era David Hilbert, anche se in realtà ha svolto la maggior parte del suo lavoro con Paul Bernays, ed è stato esaminato il 24 luglio, 1929. A questo esame, Hilbert ha posto a Curry una domanda su un altro argomento (chiamate funzioni automorfe), cosa che Hilbert pensava che Curry non avrebbe saputo. Come è successo, Curry aveva seguito un corso proprio su quell'argomento ad Harvard, e Curry è stato in grado di dare una buona risposta. Hilbert ha risposto chiedendo con grande sorpresa, “Dove l’hanno imparato??" («Dove l'hai imparato??") La tesi è stata pubblicata (in tedesco) COME [Curry 1930].

Curry ora aveva bisogno di un lavoro, e ha assunto una posizione come professore assistente presso il Pennsylvania State College (Penn State - Penn State divenne la Pennsylvania State University nel 1953). Infine, la maggior parte delle persone che conoscevano Curry arrivarono ad associarlo alla Penn State, ma quando vi si recò per la prima volta non aveva intenzione di restarci a lungo. Era stato ad Harvard, Princeton, e Gottinga, e alla Penn State si sentiva tagliato fuori dalla maggior parte della sua ex comunità accademica. Inoltre, in quei giorni, Penn State non ha sostenuto la ricerca. (Dopo, grazie in parte all’influenza di Curry, Penn State ha cambiato la sua politica, ed è ora un importante istituto di ricerca.) Ma il suo arrivo coincise con l’inizio della Grande Depressione, e la richiesta di logici nel mondo accademico non era molto elevata. Così rimase e si stabilì alla Penn State, restando lì, ad eccezione di diverse assenze, fino al suo pensionamento nel 1966. Ha progredito normalmente attraverso i ranghi accademici, diventando professore associato nel 1933 e professore ordinario nel 1941.

Tutti quelli che conoscevano i Curry erano consapevoli di quanto fossero sempre amichevoli e disponibili. Il curry ha sempre fatto di più per colleghi e studenti che essere una fonte di idee importanti (Sebbene, Ovviamente, le sue idee sono state di enorme importanza). Era sempre disposto ad ascoltare chiunque volesse parlare con lui, per discutere le loro idee, e di dare tutto l'incoraggiamento possibile. La porta del suo ufficio era sempre aperta. Ben nota, ovunque vivessero i Curry, era l'ospitalità che entrambi mostravano. C'erano sempre molte feste e altro, meno formale, raduni. Curry aveva anche un senso dell'umorismo giocoso.

La prima delle sue assenze fu un anno presso l'Università di Chicago nel 1931-32 come membro del Consiglio nazionale delle ricerche.. (Il premio originale avrebbe dovuto essere esteso all'anno successivo, ma il secondo anno fu cancellato per Curry perché aveva un lavoro a cui tornare e c'erano altri Fellow del Consiglio Nazionale delle Ricerche che non lo facevano. Era, Dopotutto, gli abissi della Grande Depressione.) Nel 1938-39, Curry risiedeva presso l'Institute for Advanced Study di Princeton.

Altrimenti, Curry trascorse gli anni '30 alla Penn State insegnando e portando avanti le sue ricerche. Durante questo periodo ha fatto parte dello staff di revisione del Central Journal for Mathematics and its Border Areas (1931-1939). Nel 1936, divenne membro fondatore dell'Associazione per la Logica Simbolica; fu Vicepresidente nel 1936-37 e Presidente nel 1938-40 oltre a essere membro del Consiglio come ex-presidente nel 1942-46.

Durante questo periodo, anche i Curry iniziarono la loro famiglia: Anne Wright Curry (più tardi la signora. Riccardo S. Pifferaio) è nato il 27 luglio, 1930, e Robert Wheatley Curry seguirono il 6 luglio, 1934.

Entro la fine degli anni '30, Curry è stato affermato come uno dei più importanti logici matematici negli Stati Uniti e, Infatti, nel mondo intero. In quanto tale, gli fu chiesto di presentare le sue opinioni sulla natura della matematica al Congresso internazionale per l'unità della scienza tenutosi a Cambridge, Massachusetts all'inizio di settembre 1939. Il risultato fu un lungo manoscritto di cui presentò al Congresso una versione più breve, [Curry 1939]. Con questo articolo iniziò una serie di articoli sulla filosofia della matematica che continuarono per il resto della sua vita.

L'anno successivo, 1940, Curry è diventato membro del consiglio di amministrazione del Curry College, già Scuola di Espressione, l'istituzione di cui suo padre era stato presidente. Rimase membro fino al 1951. Dopo, il 5 giugno, 1966, il collegio gli ha conferito la laurea honoris causa di Dottore in Scienze dell'Oratorio.

Quando gli Stati Uniti entrarono nella seconda guerra mondiale, Curry decise di mettere da parte la logica per tutta la durata della guerra. Dal 1940 al 1942 fu membro del Comitato nazionale per la preparazione alla guerra dell'American Mathematical Society e della Mathematical Association of America. Il 25 maggio, 1942, lasciò la Penn State e andò al Frankford Arsenal, dove lavorò come matematico applicato fino al gennaio 1944; poi andò al Laboratorio di Fisica Applicata della Johns Hopkins University, dove rimase fino a marzo, 1945. Successivamente si recò ai laboratori di ricerca balistica dell'Aberdeen Proving Ground, dove rimase fino a settembre, 1946. Durante i suoi ultimi tre mesi lì, è stato Capo della Sezione Teorica del Laboratorio di Informatica e per un mese è stato Direttore ad interim del Laboratorio di Informatica; fu durante questo periodo che si occupò del computer ENIAC. In seguito a questa esperienza è stato consulente nel campo dei metodi informatici presso il Naval Ordinance Laboratory degli Stati Uniti dal 1° giugno., 1948 fino al 30 giugno, 1949.

A settembre, 1946, Curry è tornato alla Penn State. Voleva proseguire il suo lavoro sui computer elettronici, e così ha cercato di interessare l'università all'acquisto di alcune attrezzature informatiche. Non ha avuto successo in questo. Ha insistito finché un collega non gli ha fatto notare che se ci fosse riuscito, probabilmente verrebbe nominato capo del programma senza alcun aumento di stipendio. Decise allora che questo collega aveva ragione e rinunciò al tentativo. Ciò gli ha effettivamente impedito di perseguire la teoria informatica.

Lo era, Tuttavia, tornare alla logica. Ad Amsterdam nell'estate del 1948, durante il X Congresso Internazionale di Filosofia, gli fu proposto di scrivere un libricino di meno di 100 pagine sul tema della logica combinatoria per la nuova serie di logica dell'Olanda Settentrionale. Sentiva che c'erano troppe ricerche inedite sull'argomento per scrivere un libro così breve, e così inviò loro invece il suo manoscritto filosofico del 1939 con alcune piccole revisioni. Questo è apparso come [Curry 1951]. Ma questa idea gli suggerì il progetto che alla fine portò ai suoi due volumi dal titolo Combinatory Logic [Curry e Feys 1958] e [Curry et al.1972]. Sentendo di aver bisogno di un collaboratore, soprattutto uno che era più bravo di lui all'esposizione, ha deciso di lavorare con Robert Feys, che aveva pubblicato alcuni articoli sulla logica combinatoria. Curry ottenne così una borsa di studio Fullbright e trascorse l'anno 1950-51 a Lovanio in Belgio. Dopo il suo ritorno alla Penn State, lui e Feys continuarono il loro lavoro, e il manoscritto di [Curry e Feys 1958] fu completato nel 1956. Il libro è apparso nel 1958, pubblicato da North-Holland.

Nel frattempo, il denaro divenne finalmente disponibile alla Penn State per gli studenti laureati. Edoardo. Cogan si è avvicinato per la prima volta a Curry prima che partisse per Louvain, e lavorò con Curry dopo il suo ritorno nel 1951, terminando la sua tesi nel 1955. Kenneth L. Anche Loewen studiò con lui durante questo periodo, ma lasciò per prendere una posizione accademica altrove nel 1954 e non terminò la sua tesi fino al 1962.

Dopo il completamento di [Curry e Feys 1958] Curry rivolse la sua attenzione alla teoria della dimostrazione in stile Gentzen. Aveva fatto qualche lavoro precedente su questo, inclusa una serie di conferenze tenute alla Notre Dame University in Indiana in aprile, 1948 (che ha portato al suo libro [Curry 1950]), e riteneva che formalizzasse il tipo di ragionamento utilizzato nello sviluppo della parte di logica combinatoria come sistema di logica nel senso comune del termine, e così ha ritenuto che la questione dovesse essere risolta prima di iniziare a lavorare [Curry et al. 1972]. Iniziò così a lavorare su quello che divenne il suo libro [Curry 1963]. Questo lavoro è stato reso più semplice quando, nel 1959, divenne Evan Pugh Research Professor e fu quindi sollevato dagli incarichi di insegnamento universitario. Il manoscritto di [Curry 1963] fu completato nel 1961.

A questo punto, c'erano altri due studenti laureati, Bruce Lercher e Luis E. Sanchis, entrambi completarono la loro tesi nel 1963.

Da febbraio a settembre, 1962, i Curry hanno fatto un viaggio intorno al mondo, visitando una serie di università dove Curry ha tenuto lezioni.

Nel 1964, Curry ha incontrato due nuovi futuri collaboratori. J. Roger Hindley arrivò alla Penn State per un incarico di docente che servì come una sorta di posizione post-dottorato dopo aver terminato la sua laurea a Newcastle-upon-Tyne, e Jonathan P. Seldin arrivò come studente laureato principiante. Curry stava appena iniziando a lavorarci [Curry et al. 1972]. Purtroppo, Feys era morto nel 1961, e curry, lasciato lavorare da solo, presto capì che aveva bisogno di collaboratori. Nel 1965, ha invitato Hindley a unirsi a lui nel progetto.

Nel 1966, Curry si è ritirato dalla Penn State dopo essere rimasto lì per 37 anni. Poi andò ad Amsterdam, dove per i successivi quattro anni fu professore di Logica, Storia della logica, e Filosofia della scienza, e anche direttore dell'Istituto per la ricerca fondamentale e la filosofia delle scienze esatte, entrambi all'Università di Amsterdam. Seldin andò ad Amsterdam con una borsa di studio per laureati della National Science Foundation degli Stati Uniti, e completò la sua tesi nel 1968, dopo di che si unì a Curry e Hindley come coautore del libro che stavano scrivendo. Curry aveva un altro studente laureato ad Amsterdam, Martin W. Bunder, che concluse la sua tesi nel 1969.

Il manoscritto di [Curry et al. 1972], è stato completato a maggio, 1970, poco prima che Curry si ritirasse dall'Università di Amsterdam. Tornò allo State College, Pennsylvania (la città in cui si trova Penn State), dove ha continuato il suo lavoro matematico, scrivere recensioni (soprattutto per le revisioni matematiche) e documenti occasionali. Giovanni A. Lever scrisse lì una tesi di master con lui nel 1977 dopo aver ottenuto un permesso speciale dalle autorità universitarie per lavorare con un professore in pensione. Nel 1971-72, Curry ha accettato una posizione in visita presso l'Università di Pittsburgh. Altrimenti, lui e Virginia rimasero allo State College, salvo qualche viaggio occasionale, fino alla sua morte, avvenuta il 1° settembre, 1982. Curry lasciò i suoi documenti alla biblioteca della Penn State.

L'hobby di Curry per tutta la sua vita è stato il birdwatching, e alla fine della sua vita, Curry aveva la reputazione di ornitologo dilettante.

2. Logica combinatoria
UN. Periodo iniziale

Curry ha inventato la logica combinatoria indipendentemente analizzando l'operazione di sostituzione di una formula ben formata per una variabile proposizionale nel sistema di logica proposizionale del primo capitolo di [Russell e Whitehead 1910-1913]. Voleva che la logica combinatoria fosse il fondamento della logica matematica e forse anche di tutta la matematica. Gran parte dell'argomento è estremamente tecnico. Questa sarà un'introduzione quanto più non tecnica sia possibile scrivere.

L'idea di base qui è quella di una funzione, che è un'operazione matematica che fa qualcosa a un input. Così, Per esempio, c'è la funzione numerica che eleva al quadrato il suo argomento (cioè., lo moltiplica per se stesso). I matematici di solito scrivono che if è la funzione di quadratura, quindi per ogni possibile argomento (ingresso) , . Poi, se questa funzione è applicata al numero 3, otteniamo .

Nella logica combinatoria, l'applicazione di una funzione ad un argomento, ad esempio , è scritto o . Anche, la necessità di funzioni di più di una variabile viene evitata consentendo al valore di una funzione di essere un'altra funzione. Per esempio, supponiamo, nella notazione tradizionale, . Allora lascia dove . Poi . In notazione combinatoria, e . In questa notazione, usiamo l'associazione a sinistra per l'applicazione, affinché .

Questo metodo di utilizzare solo funzioni di un argomento è stato chiamato currying, e spesso viene chiamata la funzione del paragrafo precedente . Lo stesso Curry venne a conoscenza di questo uso del suo nome nei suoi ultimi anni, e protestò perché l'idea gli era venuta da Schönfinkel, ma questo uso del nome Curry è rimasto.

Altri combinatori lo sono:

L'operatore identità , con la proprietà che .
L'operatore di costanza con la proprietà that . Così, è una funzione costante il cui valore per qualsiasi argomento è .
Il compositore , con la proprietà che . Questo dice a cosa rivolgersi , applicare prima e poi applicare al risultato.
Il diagonalizzatore con la proprietà that .
Il distributore con la proprietà che .

Nota che può essere definito in termini di altri operatori, Da , COSÌ . Anche, Da , può essere definito come .

Supponiamo ora di voler dire che un'operazione, dire addizione, è commutativo (cioè. l'ordine di aggiunta non ha importanza). Il modo tradizionale di scriverlo in matematica è . Ma questa non è una proprietà di e ; è una proprietà di +. Per dirlo nel linguaggio della logica combinatoria, scriveremmo . Supponiamo ora di avere un operatore (per “commutatore” con la proprietà che . Poi , e possiamo dire che + è commutativo scrivendo . Questo operatore è chiamato combinatore.

Le regole che definiscono questi combinatori sono state scritte sopra con il simbolo di uguaglianza, che è simmetrico. Ma spesso è utile leggere queste equazioni solo da sinistra a destra. Quindi queste equazioni verrebbero chiamate contrazioni, in modo che i contratti a , contratti a , contratti a , contratti a , contratti a , e contratti a . I termini vengono ridotti ad altri termini eseguendo sequenze di 0 o più contrazioni sui sottotermini del termine originale. Per esempio, la riduzione di a è la seguente:

.

(Qui utilizzo il simbolo “per indicare una riduzione.) Tieni presente che ci sono alcuni termini che non possono essere ridotti. Si dice che questi termini siano in forma normale. D'altra parte, alcuni termini possono portare a riduzioni infinite, Per esempio

.

Curry decise di fondare la logica matematica su un sistema di combinatori i cui combinatori primitivi erano e . (Non ne capiva ancora il ruolo , che ha ottenuto da Schönfinkel.) La parte della logica combinatoria che si occupa delle proprietà di base dei termini combinatori senza riferimento a connettivi e quantificatori logici è ora chiamata logica combinatoria pura. Avrebbe aggiunto connettivi logici e quantificatori finché non avesse sviluppato un sistema logico completo; chiamò questa parte dell'argomento logica combinatoria illativa. Questa parola "illative" è una parola che Curry ha coniato lui stesso, basato sulla parola latina illatum, il participio passato di infero, che significa “concludere”.

Ha dimostrato diversi risultati importanti in questo contesto. Innanzitutto dimostrò che se è una qualsiasi combinazione di combinatori e variabili , c'è un termine in cui le variabili non appaiono in questo modo . Curry ha usato la notazione per questo . Per esempio, Da , possiamo prendere per essere . Fornì anche degli assiomi per il sistema in modo che questo fosse determinato in modo univoco dalle variabili in questione. (L'esistenza di un tale astratto per ogni termine e per tutte le variabili è chiamata completezza combinatoria.) Un'altra delle cose che ha dimostrato presto (nella sua tesi) è questo il sistema base dei combinatori, senza alcun assioma per alcun connettivo logico o quantificatore, è coerente.

Utilizzando la notazione dei combinatori, Curry ha scritto ciò che viene normalmente scritto come , dove . Questo operatore era presente nella sua tesi, ma nessuna delle sue proprietà è stata sviluppata lì. Invece, Curry iniziò a scrivere una serie di articoli che espandevano la logica combinatoria per includere non solo questo quantificatore universale , ma anche (per implicazione, affinché , o se allora ) e uguaglianza , quindi questo significa . Nel 1934, Curry pubblicato [Curry 1934a] dando proprietà di e .

b. Il paradosso di Kleene-Rosser e le sue conseguenze

Nel 1932, Curry venne a conoscenza di un articolo di Alonzo Church, [Chiesa 1932]. Il sistema di Church era basato sull’astrazione, che forma termini da variabili mediante applicazione e astrazione: if è una variabile ed è un termine, allora è un termine. (Le parentesi più esterne possono essere omesse se non si crea confusione.) Per esempio, è la funzione di quadratura, e . Qui, , che è l'abbreviazione di , interpreta il ruolo di Curry . (Per un'introduzione completa sia al calcolo che alla logica combinatoria, Vedere [Hindley e Seldin 2008]. Vedi anche l'articolo su -calculi in questa Enciclopedia.) Anche, le variabili in sono chiamate legate; le variabili che non rientrano nell'ambito di a sono chiamate libere.

La riduzione per il sistema di Church è definita da una regola chiamata da Curry : contratti a , che è il risultato della sostituzione di in , dove altre variabili legate vengono modificate per evitare la cattura. Nella logica ordinaria dei predicati, questo tipo di cambiamento viene effettuato cambiando in se viene sostituito un termine in cui ricorre libero .

Si noti che la riduzione nel sistema di Church differisce dalla riduzione nella logica combinatoria in quanto si riduce a , quindi si riduce a , ma nella logica combinatoria il fatto che si riduce a non implica automaticamente che si riduca a , poiché i sottotermini di spesso non si verificano realmente in .

Nel 1934, Curry ha ricevuto una lettera da Rosser che lo informava che Kleene e Rosser avevano dimostrato incoerente il sistema di [Chiesa 1932] e il sistema di [Curry 1934]. Lo hanno fatto derivando il paradosso di Richard (Vedi l'articolo sul paradosso di Richard in questa Enciclopedia.) in entrambi i sistemi.

Chiesa e i suoi studenti, Kleene e Rosser, rinunciò poi all'idea di costruire un sistema di logica matematica adeguato a tutta la matematica basando il sistema su termini -. Invece, presero quella parte del sistema di Church che coinvolgeva solo termini - e la trattarono separatamente come -calcolo. (Vedi l'articolo su -calculi Ma Curry ha avuto una reazione diversa. Aveva sempre considerato la possibilità che alcuni sistemi da lui proposti potessero risultare incoerenti, e così ha reagito avviando un'attenta analisi del paradosso con l'idea di trovare un modo per definire un sistema coerente.

Questa analisi durò diversi anni, e quando prese un congedo dalla Penn State per studiare matematica applicata per gli Stati Uniti. governo durante la Seconda Guerra Mondiale, aveva sviluppato un piano di ricerca per cercare sistemi coerenti. Aveva già pubblicato [Curry 1941], e aveva trovato un paradosso molto più semplice (ora noto come paradosso di Curry; Vedere [Curry 1942b]). Il piano che aveva sviluppato era quello di esaminare tre diversi tipi di sistemi, che differivano nei connettivi logici e nei quantificatori considerati primitivi. I tipi di sistemi verranno discussi qui nell'ordine in cui Curry li ha forniti [Curry 1942a].

Sistemi basati sulla teoria della funzionalità. Questa è stata un'idea di Curry, risalente al 1930, che ha portato all'assegnazione del tipo. Ha scritto per il predicato delle funzioni che accettano argomenti con valori , e intendeva intendere . Al giorno d'oggi, la categoria (o predicato) è considerato un tipo piuttosto che un predicato, e di solito è scritto .
Sistemi basati sulla teoria della generalità ristretta. Curry aveva notato che la quantificazione più universale non è assoluta, ma è su un dominio limitato. (Questo sembra ovvio al giorno d'oggi, ma negli anni Trenta andava contro la tendenza generalizzante di Frege e Russell.) Ha definito un operatore che rappresenta questa quantificazione ristretta, quindi starebbe per , o (dove qui non occorre libero in o ).
Sistemi basati sulla teoria della generalità universale. Questi erano sistemi basati su e , dove inteso (dove non si presenta libero in ) e significa .

Nel 1942, Curry presupponeva che questi tipi di sistemi aumentassero di forza nell’ordine sopra indicato. La carta [Curry 1942a] era in realtà un abstract della ricerca futura piuttosto che un rapporto sul lavoro completato.

Nella tarda primavera del 1942, Curry finalmente arrivò a capire il combinatore . Rosser aveva pubblicato un articolo sulla logica combinatoria (basato su combinatori di base diversi da quelli utilizzati da Curry), e aveva mostrato come definire per induzione sulla struttura di . Quando Curry lesse questo articolo e tradusse i risultati nel suo formalismo, capì perché Schönfinkel aveva definito tutti i combinatori in termini di e , e ha iniziato a fare lo stesso. L’uso di ha notevolmente aumentato la lunghezza delle definizioni rispetto alla definizione originale di Curry, ma ha notevolmente semplificato l'algoritmo per costruirli. Con l'implementazione del computer si è verificata un'inversione di valori: la velocità di azione di un algoritmo è oggi valutata più della sua semplicità o “bellezza”.

c. Periodo Tardo (dopo la seconda guerra mondiale)

Dopo la seconda guerra mondiale, quando Curry tornò alla Penn State (Per i dettagli, vedere la sezione della sezione Bibliografia di questo articolo per il lavoro di Curry durante la seconda guerra mondiale.), lentamente tornò alla logica. Partecipò al X Congresso Internazionale di Filosofia nell'estate del 1948, e in seguito ad una proposta fattagli lì, decise di scrivere un lungo lavoro sulla logica combinatoria, nella quale intendeva includere tutto ciò che era noto sull'argomento. Sentendo di aver bisogno di un collaboratore, si avvicinò a Robert Feys a Lovanio in Belgio. Curry utilizzò un Fulbright che gli fu assegnato per l'anno 1950-51 per iniziare questo lavoro., e Curry e Feys continuarono a lavorarci dopo che Curry tornò alla Penn State nel 1951. Curry finì per lavorare su quest'opera e su un secondo volume per gran parte del resto della sua vita.

Il primo lavoro su questo libro riguardava l'esposizione di base. Curry e Feys hanno rivisto completamente i fondamenti della logica combinatoria, e ha trascorso molto tempo a spiegare l’approccio di Curry al ragionamento formale e ai sistemi formali. Hanno poi introdotto il calcolo di Church, e ha fornito una nuova dimostrazione e analisi del Teorema di Church-Rosser, il che risulta coerente con il calcolo puro. Il libro ha poi ripreso la logica combinatoria stessa, prima la logica combinatoria pura e poi la logica combinatoria illativa. Il libro si conclude con due capitoli sulla teoria della funzionalità.

Tuttavia, Curry iniziò presto ad avviare nuove ricerche per essere incluso. All'inizio, questo includeva il lavoro che espandeva la teoria della funzionalità. C'è sempre stata più di una di queste teorie, e le diverse teorie dipendevano da quali termini potevano essere quelli che oggi chiameremmo tipi, ma che Curry chiamava F-obs. C'è la teoria di base della funzionalità, in cui i tipi sono formati da tipi atomici mediante l'operazione che forma da e . (Ciò equivale a formare il tipo da e .) Questo sistema si dimostra facilmente coerente.

Poi c'è la teoria completa e libera della funzionalità, in cui qualsiasi termine combinatorio può essere un tipo. Curry pensava che questo sistema fosse coerente, e nel 1954 tentò di dimostrare tale coerenza. Ha trascorso più di quattro mesi in questo tentativo cercando di dimostrarlo, da una serie di ipotesi di tipizzazione (dove possono esserci termini combinatori), si può dimostrare che la detrazione deve assumere una certa forma specifica. Dopo quasi cinque mesi, si rese conto che è la conclusione di ogni deduzione in questa forma speciale, allora il termine è irriducibile in un certo senso. Ma il senso in questione non era quello della riduzione nella logica combinatoria, ma piuttosto il senso di -calcolo. La differenza è che in -calculus, se allora , che è quello che ci si aspetterebbe. Ma nella logica combinatoria, il fatto che ciò non lo implica automaticamente , poiché i sottotermini di non ricorrono necessariamente in .

Per Curry, il fatto che il termine nella conclusione di una deduzione nella teoria della funzionalità dovesse essere irriducibile nel senso di -calcolo non era molto soddisfacente. Il curry di solito viene pensato in combinatori piuttosto che in termini. Così, si proponeva di trovare una riduzione tra termini combinatori che sarebbe più simile a -riduzione. Cominciò con -riduzione, che è -calcolo in cui sono incluse le regole di riduzione (), la regola per i cambiamenti delle variabili legate, (), la riduzione base per -calcolo, che lo dice , il risultato della sostituzione di in , e (), la regola che dice che se non è libero dentro , Poi . Ha poi definito la riduzione forte per la logica combinatoria che equivale a -riduzione. Per ragioni tecniche, aveva bisogno di considerarlo come un combinatore primitivo invece di definirlo come aveva fatto in precedenza, quindi ora la logica combinatoria viene solitamente definita prendendo i tre combinatori , , e come combinatori primitivi.

Curry riuscì presto a dimostrare che la teoria della funzionalità è completamente libera, Infatti, incoerente. Il libro [Curry e Feys 1958] termina con un capitolo che include la prova che l'intera teoria libera è incoerente e anche alcuni risultati veri che sono stati dimostrati come parte del tentativo fallito di dimostrarne la coerenza.

Questo volume include anche la prima dimostrazione pubblicata del Teorema della Forma Normale, che dice che ogni termine con un tipo ha una forma normale. (Un termine si dice in forma normale se non può essere ridotto. Si dice che abbia forma normale se può essere ridotto a un termine in forma normale.) Questo risultato è diventato sempre più importante in vari sistemi di calcoli tipizzati nei decenni successivi alla pubblicazione di questo volume.

Negli anni immediatamente successivi alla pubblicazione di [Curry e Feys 1958], Curry iniziò a lavorare su sistemi di generalità ristretta. Ma ha pubblicato solo un paio di articoli su questo argomento prima di iniziare a lavorarci [Curry et al. 1972]. Questo volume inizia con addendi alla logica combinatoria pura, la maggior parte dei quali sono altamente tecnici. Curry tentò di ideare un quadro generale che includesse sia la logica combinatoria che il calcolo definendo quelli che chiamò sistemi C.. L'idea era quella di creare un quadro che potesse essere utilizzato per dimostrare i risultati di sistemi illativi basati sul calcolo o sulla logica combinatoria senza dover fornire dimostrazioni separate per i due casi. Ma questo tentativo non ebbe pieno successo, poiché in seguito si scoprì che molti risultati necessitavano ancora di una dimostrazione per il calcolo e di un'altra per la logica combinatoria.

Curry ha anche esteso la definizione di logica combinatoria illativa per includere qualsiasi sistema con nuove costanti atomiche a cui sono associati postulati speciali, anche se queste nuove costanti non rappresentano connettivi o quantificatori logici. Ciò gli ha permesso di includere sistemi di aritmetica combinatoria. L'aritmetica era stata rappresentata per la prima volta da Alonzo Church nella logica combinatoria e nel calcolo definendo i numeri naturali come iteratori: il numero è rappresentato da , che vale per i tempi. Ma negli anni '60, erano apparsi altri modi di rappresentare i numeri come combinatori o termini. Per questo motivo, Curry suggerì di rappresentare i numeri prendendo nuove costanti atomiche per rappresentare lo 0 e la funzione successore () e includendo un combinatore che mappava uno di questi numeri all'iteratore corrispondente. Con una qualsiasi di queste rappresentazioni, una funzione può essere rappresentata da un combinatore o da un termine se e solo se è parzialmente ricorsiva, o, equivalentemente, Turing-computabile. (Questo risultato fu dimostrato per la prima volta per il calcolo indipendentemente da Church, Kleene, e Turing nel 1936; Vedere, Per esempio, [Kleene 1936c].)

Curry considerò anche estensioni dei risultati sulla teoria della funzionalità, inclusa l'introduzione di un nuovo operatore di digitazione con la regola che da e segue , in modo che il tipo del valore di una funzione possa dipendere dall'argomento così come dal tipo dell'argomento. Il tipo è il tipo che ora viene solitamente indicato , ed è solitamente chiamato tipo di funzione dipendente. Tuttavia, il tipo è stato solo introdotto, e nessun sistema basato su di esso è stato sviluppato da Curry.

Il resto del libro include materiale sulla teoria della generalità ristretta e della generalità universale. È stato dimostrato che questi tipi di sistemi sono essenzialmente equivalenti. Sono stati dimostrati coerenti sistemi che sono essenzialmente equivalenti ai sistemi logici del primo ordine definendo classi di termini canonici che dovrebbero rappresentare proposizioni e funzioni proposizionali. Sono stati fatti tentativi per trovare sistemi coerenti in cui i presupposti affinché i termini fossero canonici fossero affermati come assiomi della logica, ma la maggior parte dei sistemi coinvolti si è poi rivelata incoerente. Finalmente, la teoria della funzionalità è stata utilizzata per definire sistemi di teoria dei tipi nel senso tradizionale.

Curry trascorse il resto della sua vita continuando questo lavoro e altri lavori che aveva svolto. L'ultimo problema su cui lavorò fu un tentativo di trovare una riduzione per termini combinatori che fosse equivalente a -riduzione, -riduzione in cui le regole di contrazione sono uniche () e (). Al momento della stesura di questo documento, questo problema non è ancora risolto. Vedi le carte di Seldin [Seldin 2011] e [Seldin 2017].

3. Teoria della dimostrazione in stile Gentzen

Curry ha letto il lavoro di Gentzen [Gentzen 1934] due anni dopo la sua comparsa, e non gli ci volle molto per rendersi conto che le idee di quell'articolo potevano essere utili per trovare un sistema logico basato sulla logica combinatoria che potesse dimostrarsi coerente.

Gentzen aveva introdotto due nuove formulazioni di sistemi logici: sistemi di deduzione naturale e calcoli successivi (Sistemi L). I sistemi di deduzione naturale sono trattati nell'articolo Concezioni teoriche-deduttive di conseguenza logica in questa enciclopedia. I calcoli sequenziali equivalgono ai sistemi di deduzione naturale e sono progettati per cercare prove.

La coerenza dei sistemi di deduzione naturale per il calcolo proposizionale e il calcolo dei predicati del primo ordine deriva da quello che viene chiamato teorema di normalizzazione (dovuto originariamente a Prawitz, [Prawitz 1965]). Questo risultato equivale al risultato di Gentzen sui calcoli successivi: il teorema di eliminazione del taglio. Curry ha elaborato la propria dimostrazione di quest'ultimo teorema. Ne usò anche una versione per fornire la prima dimostrazione pubblicata del teorema della forma normale per le funzionalità di base ordinarie. (Una dimostrazione di Turing del 1941 fu pubblicata solo nel 1980; Vedere [Gandy 1980b].)

Curry si convinse che un sistema di logica formale non è propriamente formalizzato a meno che non esista un calcolo successivo per il quale si possa dimostrare il teorema di eliminazione del taglio.

Un’altra caratteristica dell’approccio di Curry è che egli considerava questi sistemi come formalizzazioni della metateoria elementare di quello che chiamava un sistema formale elementare.. Un sistema formale elementare è quello in cui non esistono regole che scarichino le ipotesi. Curry aveva un sistema così formale per la logica combinatoria. Usò l'idea di formalizzare la metateoria elementare di un sistema formale elementare per giustificare tutte le regole operative. Ciò dimostra che Curry era interessato alla semantica.

4. Lavoro di guerra e informatica

Quando Curry lasciò la Penn State per studiare matematica applicata per gli Stati Uniti. Governo, iniziò a lavorare sulla matematica per puntare un proiettile contro un bersaglio in movimento, il cosiddetto problema del controllo del fuoco. Curry aveva studiato questo tipo di matematica da studente, e così non ebbe problemi a svolgere questo lavoro durante la seconda guerra mondiale.

Entro il 1945, quando Curry era all'Aberdeen Proving Ground, si diceva che fosse un computer elettronico, l'ENIAC, veniva costruito allo scopo di calcolare le tabelle di tiro per l'artiglieria. Curry è stato nominato nel comitato che si stava istituendo per valutare l'ENIAC quando è stato consegnato. Questo comitato si è riunito per la prima volta a luglio, 1945, e all'inizio di quel mese Curry partecipò a una conferenza sull'ENIAC tenuta da Herman Goldstine. Il giorno successivo, decise di scrivere un programma per calcolare le cifre di , la base dei logaritmi naturali. Terminò il programma all'inizio del 1946, ma non è chiaro se sia mai stato eseguito. Curry in seguito riferì che nessun altro che conosceva all'epoca e che stava lavorando all'ENIAC nel 1946 poteva vedere il punto di utilizzare un computer per un risultato che si presumeva noto..

Nel 1949, John von Neumann e alcuni colleghi scrissero ed eseguirono programmi per calcolare le cifre di e . (Vedere [Reitwiesner 1950a] e Reitwiesner et al. 1950b].) Di conseguenza, scoprirono che il matematico dilettante William Shanks, che aveva trascorso più di due decenni, a partire dalla metà del XIX secolo, a calcolare le cifre di , e che aveva calcolato fino a 707 cifre, aveva commesso un errore sulla cifra numero 528. Le persone che scrissero il programma nel 1949 sembrano non avere idea che Curry avesse scritto un programma del genere solo pochi anni prima.. D'altra parte, nel 1949 ci furono alcuni cambiamenti nell'ENIAC, e il programma che Curry scrisse nel 1945-1946 potrebbe non essere più compatibile con l'ENIAC.

Curry fu anche coinvolto nella scrittura di programmi per eseguire l'interpolazione inversa sull'ENIAC, programmi utili per gestire i tavoli di cottura. Vedere [di Mol et al. 2010].

Il lavoro di Curry sulla programmazione dell’interpolazione inversa sull’ENIAC lo ha portato a sviluppare una teoria della programmazione. L’approccio di base di Curry era molto simile a quello che aveva adottato vent’anni prima nell’analizzare il processo di sostituzione. Ha suddiviso i programmi nei componenti elementari più semplici possibili e poi ha proposto di utilizzare la composizione del programma per rimetterli insieme. Questo approccio è stato paragonato al successivo sviluppo di compilatori per i linguaggi utente. Vedere [Curry 1954].

Tuttavia, Curry non fu in grado di continuare a lavorare su questo sviluppo perché non riuscì a convincere la Penn State ad acquistare alcuna attrezzatura informatica alla fine degli anni '40..

5. Formalismo: la Filosofia della Matematica

Curry ha sviluppato una filosofia distintiva della matematica. Le sue opinioni si sono sviluppate notevolmente nel corso della sua carriera, ma è conosciuto soprattutto per i suoi primi lavori sull'argomento.

La prima opera filosofica di Curry, risalente al 1939, propose di definire la matematica come la scienza dei sistemi formali. Ma l’approccio di Curry ai sistemi formali non era proprio lo stesso di quello della maggior parte degli altri operatori del settore.

La definizione usuale di un sistema formale inizia definendo gli oggetti formali come parole su un alfabeto di simboli, o, per usare la terminologia più corrente nell'informatica odierna, stringhe di caratteri. Ma poi alcune di queste parole vengono individuate come “formule ben formate” mediante una definizione induttiva con la proprietà che ciascuna formula ben formata ha una costruzione unica dalle “formule atomiche”. Per esempio, per il calcolo proposizionale, ci viene dato un insieme possibilmente infinito di formule atomiche , e una tipica definizione di formula ben formata è la seguente:

Ogni formula atomica è una formula ben formata.
Se è una formula ben formata, allora è una formula ben formata.
Se e sono formule ben formate, Poi , , e sono formule ben formate.
Nient'altro è una formula ben formata.

Se il sistema logico coinvolto include quantificatori, quindi le formule atomiche stesse vengono definite, e tale definizione può dipendere da definizioni induttive. Per esempio, se stiamo definendo un sistema formale per la logica del primo ordine, iniziamo con i termini, che sono costituiti da termini atomici e variabili individuali utilizzando funzioni di base, e poi abbiamo i predicati, da cui si ottengono le formule atomiche applicandole ai termini. Se il sistema del primo ordine è un sistema aritmetico, iniziamo con il termine atomico 0 e le funzioni denotate da (come apice) e e (come infissi), e quindi i termini sono definiti come segue:

Ogni variabile individuale è un termine.
0 è un termine.
Se è un termine, allora è così . (Questo ha lo scopo di denotare il numero che è uno in più di .)
Se e sono termini, allora e sono termini. (Il termine è spesso abbreviato in .)
Nient'altro è un termine.

Una volta definiti i termini, le formule atomiche sono definite come segue:

Se e sono termini, allora è una formula atomica.

E quindi la seguente clausola viene aggiunta alla definizione di formula ben formata:

Se è una variabile individuale ed è una formula ben formata, allora e sono formule ben formate.

Curry ha notato che, nonostante queste definizioni del termine, formula atomica, e formule ben formate dicono che si tratta di stringhe di simboli su qualche alfabeto, non dipendono realmente da questo fatto. Per lui, la cosa cruciale era che ogni termine e ogni formula ben formata avessero una costruzione unica, mentre qualsiasi parola di tre o più lettere ha più di una costruzione.(Per esempio, la corda può essere formata in due modi: può essere aggiunto a destra, o può essere aggiunto a sinistra.) Così mentre ovviamente rappresentiamo gli oggetti formali su una pagina o su una lavagna come stringhe di caratteri, non è necessario che siano effettivamente tali stringhe. Le stringhe possono essere solo i nomi di questi oggetti formali. È solo necessario che siano definiti induttivamente in modo che ciascuno abbia una costruzione unica.

Anche, i sistemi formali non hanno bisogno di essere sistemi logici nel senso ordinario del termine con connettivi logici e quantificatori. È possibile avere un sistema formale più semplice. Un esempio fornito da Curry è quello che ha chiamato il “sistema Sams” per i numeri naturali. (Ha preso questo nome dalla parola ungherese per numero, che è un numero.) In questo sistema, gli oggetti formali vengono interpretati come numeri naturali. C'è un oggetto formale primitivo, che chiamerò “0”. C'è un'operazione, da cui si forma . Le regole per formare i sams sono le seguenti:

0 è un sam.
Se è un sam, allora è così .
Nient'altro è un sam.

C'è un predicato, che forma da sams e . Così, le affermazioni elementari sono quelle della forma , dove e sono sams. C'è un assioma, vale a dire

0 = 0

C'è anche una regola di inferenza: Da dedurre . Questo è un sistema formale molto semplice, ed è facile dimostrare che i teoremi (enunciati elementari dimostrabili) sono quelli del modulo , dov'è un sam.

Nel dire che la matematica è la scienza dei sistemi formali, Curry lo stava affermando (puro) la matematica non ha realmente una materia. Non era quello che lui chiamava un argomento controverso. (La parola contensivo è una parola Curry coniata per esprimere l'idea della parola tedesca inhaltlich.) Naturalmente,, le affermazioni matematiche hanno soggetti e quindi materia, ma Curry affermò che l'unico argomento che qualsiasi affermazione matematica aveva era altra matematica.

L’atteggiamento di Curry nei confronti della verità era che la verità è di due tipi:

La verità all'interno di un sistema formale (o all'interno di una determinata teoria). Ciò dipende da come viene definito il sistema o la teoria.
L'accettabilità di un sistema (o teoria) per qualche scopo. Questo dipende dallo scopo, e Curry l'ha presa in modo pragmatico.

Nel suo lavoro sulla logica combinatoria e sulla teoria della dimostrazione di Gentzen, preferiva usare solo la logica costruttiva nella metateoria, questo sarebbe accettato da più persone rispetto alla logica classica. (In questo, non si rendeva conto che la maggior parte dei matematici non aveva familiarità con la matematica costruttiva.) D'altra parte, non ebbe difficoltà ad accettare la logica classica in matematica per usarla in fisica. In un senso, Curry non credeva davvero in una nozione assoluta di verità.

D'altra parte, sistemi una volta formali (o qualsiasi altro tipo di teoria) vengono creati, hanno proprietà che possono essere studiate, e quindi hanno esistenza oggettiva. In questo senso, Curry credeva nell'idea del terzo mondo introdotta più tardi da Karl Popper. Infatti, Popper presentò questa idea in una sessione del Terzo Congresso Internazionale di Logica, Metodologia, e Filosofia della scienza ad Amsterdam nel 1967, e come è successo Curry era il presidente della sessione. (Vedere [Popper 1968].) Al termine della presentazione di Popper, Curry disse al suo studente laureato Jonathan P. Documentario, che era presente anche lui, che pensava che Popper avesse fatto un grosso problema con qualcosa che era banalmente e ovviamente vero.

Nel corso della sua carriera, Curry ha cambiato più volte le parole che usava per denotare gli oggetti formali di un sistema formale. Nei suoi primi lavori sulla logica combinatoria, li chiamava “entità” (usando la parola tedesca Etwas come sostantivo nella sua tesi, che era scritto in tedesco). Tuttavia, in una discussione con un filosofo (che non nominò nei suoi ultimi anni), gli fu detto che l'uso di quella parola implicava alcune conclusioni filosofiche con le quali non era d'accordo. A quel punto, ha deciso di usare invece la parola “termine”.. È ormai comune fare riferimento a “termini combinati” e “-termini”. Tuttavia, questo gli causò un problema quando aveva a che fare con un sistema logico formale con quantificatori, poiché i termini sarebbero quelle che solitamente vengono chiamate “formule”, e ci sono altri oggetti formali chiamati “termini”. Quindi alla fine, ha coniato la propria parola prendendo la prima sillaba della parola “oggetto”, e ho iniziato a chiamarli obs. Ad alcune persone, la parola ob sembrava riferirsi specificamente alla logica combinatoria, ma in realtà Curry usò la parola per oggetti formali di qualsiasi tipo di sistema formale.

Nella sua opera successiva, Curry ha esteso la sua definizione di sistema formale per includere sistemi i cui oggetti formali sono stringhe di caratteri. Chiamò tali sistemi sistemi sintattici, e chiamò il suo precedente tipo di sistemi formali ob sistemi.

Anche nei suoi lavori successivi, Curry ha anche esteso la sua definizione di matematica dicendo che la matematica è la scienza dei sistemi formali a dire che la matematica è la scienza dei metodi formali.. Questa definizione dovrebbe essere sufficientemente ampia da includere tutta la matematica, poiché se confrontiamo pile di mele e arance vediamo se esiste una corrispondenza biunivoca tra loro, stiamo guardando le forme delle pile piuttosto che il contenuto (mele o arance).

Curry scelse il nome “formalismo” per la sua filosofia della matematica a causa di David Hilbert. Tuttavia, L’idea di formalismo di Curry è molto diversa dall’idea di altri filosofi della matematica che si definiscono formalisti. Probabilmente è meglio pensare al formalismo di Curry come a una sorta di strutturalismo.

6. Riferimenti e approfondimenti
UN. Fonti primarie
[Curry 1929] Curry, Haskell B., Un’analisi della sostituzione logica”, Giornale americano di matematica 51, 363-384.
Il primo articolo pubblicato da Curry, scritto come parte di una domanda di borsa di studio per andare a Gottinga.
[Curry 1930] Curry, Haskell B., Fondamenti di logica combinatoria”, Giornale americano di matematica 52 (1930) 509-536, 789-834.
La tesi di Curry, scritto in tedesco a Gottinga nel 1928-1929. Ripubblicato con una traduzione in inglese e un'introduzione sul lavoro di Curry di Fairouz Kamareddine e Jonathan P.. Seldin come fondamenti della logica combinatoria da parte delle pubblicazioni universitarie, 2016.
[Curry 1934a] Curry, Haskell B., Alcune proprietà di uguaglianza e implicazione nella logica combinatoria”, Annali di matematica (2) 34, 381-404.
Questo è l'articolo che diede a Kleene e Rosser ciò di cui avevano bisogno per dimostrare l'incoerenza dei sistemi di Church e Curry.
[Curry 1934b] Curry, Haskell B., Funzionalità nella logica combinatoria”, Atti della National Academy of Sciences U.S.A., 20, 584-590.
Un estratto esteso della voce 1936 di seguito, che Curry ha avuto qualche difficoltà a farsi accettare per la pubblicazione perché l'approccio originariamente sembrava strano.
[Curry 1936] Curry, Haskell B., Prime proprietà della funzionalità in logica combinatoria," Diario matematico Tohoku 41 Parte II, 371-401.
Il primo articolo di Curry sulla funzionalità. Lo scrisse originariamente nel 1932, ma ha avuto difficoltà a farlo accettare per la pubblicazione. La versione pubblicata nel 1936 contiene numerosi errori di stampa.
[Curry 1939] Curry, Haskell B., Osservazioni sulla definizione e la natura della matematica”, Giornale della scienza unificata 9, 164-169, e da allora ristampato molte volte.
Il primo lavoro di Curry sulla filosofia della matematica.
[Curry 1941] Curry, Haskell B., Il paradosso di Kleene e Rosser”, Transazioni dell'American Mathematical Society, 50, 454-516.
Lo studio di Curry sul paradosso menzionato nel titolo.
[Curry 1942a] Curry, Haskell B., Alcuni progressi nella teoria combinatoria della quantificazione”, Atti della National Academy of Sciences U.S.A. 28, 564-569.
Questo è il documento che Curry scrisse poco prima del suo congedo dalla Penn State per svolgere attività bellica in cui esponeva i suoi piani per cercare di inviare sistemi logici coerenti basati sulla logica combinatoria..
[Curry 1942b] Curry, Haskell B., L’incoerenza di alcune logiche formali”, Giornale di logica simbolica 7, 115-117.
[Curry 1949] Curry, Haskell B., Una semplificazione della teoria dei combinatori”, Sintesi 7, 391-399.
L'articolo in cui Curry pubblicò la sua comprensione del combinatore S.
[Curry 1950] Curry, Haskell B., Una teoria della deducibilità formale, (Stampa dell'Università dell'Indiana).
Il primo libro di Curry sulla teoria della dimostrazione in stile Gentzen.
[Curry 1951] Curry, Haskell B., Lineamenti di una filosofia formalista della matematica (Amsterdam, Olanda Settentrionale).
Questo è stato scritto per lo più nel 1939 ed è essenzialmente il lungo manoscritto da cui è stato preparato l'articolo del 1939 come versione più breve.
[Curry 1954] Curry, Haskell B., La logica della composizione del programma”, Nelle applicazioni scientifiche della logica matematica, Atti del 2° Convegno Internazionale di Logica Matematica, Parigi 25-30 agosto 1952, Istituto Henri Poincaré, (Parigi: Gauthier-Villars e Lovanio: Nauwelaerts). La sintesi di Curry della sua teoria della programmazione.
[Curry e Feys 1958] Curry, Haskell B. e Fey, Roberto, Logica combinatoria, Volume I, (Amsterdam, Olanda Settentrionale).
Il primo volume della grande opera di Curry sulla logica combinatoria.
[Curry 1963] Curry, Haskell B., Fondamenti della logica matematica, (McGraw-Hill, e da allora ristampato da Dover).
Il principale lavoro di Curry sulla teoria della dimostrazione in stile Gentzen.
[Curry et al. 1972] Curry, Haskell B., Hindley, J. Ruggero, e Seldin, Jonathan P., Logica combinatoria, Tomo II, (Amsterdam, Olanda Settentrionale).
Il secondo volume della grande opera di Curry sulla logica combinatoria.
b. Fonti secondarie (per anno)
[Russell e Whitehead 1910-1913] Russell, Bertrand e Whitehead, Alfredo Nord, Principia Matematica, 3 volumi (Pressa dell'Università di Cambridge).
Il primo importante lavoro sulla logica letto da Curry.
[Schönfinkel 1924] Schönfinkel, Mosé, “Sugli elementi costitutivi della logica matematica”, Annali matematici 92, 305-306.
Un'opera che Curry incontrò per la prima volta nel 1927-28 che, con sua grande sorpresa, aveva anticipato la sua idea per i combinatori. L'articolo è stato scritto da Behman, ed era un resoconto di un seminario che Schonnkel aveva tenuto a Gottinga nel 1920. È apparsa una traduzione inglese come “Sugli elementi costitutivi della logica matematica”, in Da Frege a Gödel: Un libro di origine in logica matematica, 1879-1931, a cura di Jean van Heijenoort (Stampa dell'Università di Harvard, 1967), pp. 355-366.
[Hilbert 1925] David Hilbert, Sull’infinito”, Annali matematici 95 (1925) 161-190.
Uno degli articoli più importanti scritti da Hilbert sui fondamenti della matematica. Ristampato (in tedesco) in David Hilbert, Hilbertiana: Cinque saggi (Darmstadt: Società del libro scientifico, 1964), pp. 79-108. Traduzione in inglese pubblicata come “On the infinite” in Jean van Heijenoort (editore), Da Frege a Gödel: Un libro di origine in logica matematica, 1879-1931, (Cambridge, MA e Londra, Inghilterra: Stampa dell'Università di Harvard 1967), pagine 367-392.
[Verso il 1930] Ehi, Aquila, Le regole formali della logica intuizionistica”‘, Atti dell'Accademia prussiana delle scienze, Lezione di Fisico-Matematica 1930, 42-56.
L'articolo in cui Heyting introduce il suo sistema formale di logica intuizionista.
[Chiesa 1932] Chiesa, Alonzo, Un insieme di postulati per la fondazione della logica”, Annali di matematica (2) 33, 346-366.
L’articolo in cui Church per primo introdusse l’astrazione come parte di un sistema più ampio.
[Gentzen 1934] Persone, G., Studi sul ragionamento logico”, Diario matematico 39, 405-431.
L'articolo in cui Gentzen presenta i suoi sistemi di deduzione naturale e i suoi sistemi L (seguono i calcoli).
[Kleine 1935] Kleene, Steven C. e Rosser, J. Barkley, L’incoerenza di alcune logiche formali”, Annali di matematica (2) 36, 630-636.
L'articolo in cui Kleene e Rosser pubblicarono la loro prova della contraddizione nei sistemi Church e Curry.
[Chiesa e Rosser 1936a] Chiesa, Alonzo e Rosser, J. Barkley, Alcune proprietà della conversione”, Transazioni dell'American Mathematical Society 39, 472-482.
L'articolo in cui fu dimostrato per la prima volta il teorema di Church-Rosser per il lambda-calcolo.
[Chiesa 1936b] Chiesa, Alonzo, Un problema indecidibile nella teoria elementare dei numeri’, Giornale americano di matematica 58, 345-363.
L'articolo in cui Church ha dimostrato che esiste un problema nella teoria elementare dei numeri che non può essere risolto da un algoritmo. L'articolo include una dichiarazione di Church secondo cui una funzione è parzialmente ricorsiva se e solo se può essere rappresentata da un termine -, un risultato che lui e Kleene ottennero indipendentemente più o meno nello stesso periodo.
[Kleene 1936c] Kleene, Steven C., “-denabilità e ricorsività”, Diario matematico Duke 2, 340-353.
L'articolo in cui Kleene dimostrò per la prima volta che una funzione è parzialmente ricorsiva se e solo se può essere rappresentata da un termine -, un risultato che scoprì indipendentemente nello stesso periodo di Alonzo Church. Ciò faceva parte della giustificazione della tesi di Church-Turing, che una funzione è calcolabile meccanicamente se e solo se è parzialmente ricorsiva se e solo se è computabile secondo Turing se e solo se è -denable.
[Rosser 1942] Rosser, J. Barkley, Nuovi insiemi di postulati per le logiche combinatorie”, Giornale di logica simbolica 7, 18-27.
L’articolo di Rosser che permise a Curry di comprendere il combinatore S, sebbene Rosser non usasse quel combinatore.
[Reitwiesner 1950a] Reitwiesner, George W., Una determinazione ENIAC di pi ed e con più di 2000 cifre decimali”, Tabelle matematiche e altri aiuti al calcolo, 4, 11-15.
Un documento sul programma eseguito sull'ENIAC per calcolare le cifre di ed e nel 1949-1950. Il documento non mostra alcuna indicazione di conoscenza del programma che Curry scrisse per farlo nel 1945-46..
[Reitwiesner et al. 1950b] Metropoli, N. C., Reitwiesner, G., e von Neumann, J., Trattamento statistico dei valori dei primi 2,000 cifre decimali di e e calcolate sull’ENIAC”, Tabelle matematiche e altri aiuti al calcolo, 4, 109-111.
L'analisi statistica dei risultati del programma viene eseguita sull'ENIAC come descritto da George W. Reitwiesner.
[Prawitz 1965] Prawitz, Giorno, Detrazione naturale: Uno studio teorico-dimostrativo, Almqvist & Wikisell, 1965. Ristampato da Dover nel 2006.
Questa era originariamente la tesi di dottorato di Prawitz, e ha introdotto le idee di Prawitz di riduzione della prova e normalizzazione della prova.
[Popper 1968] Popper, K. R., Epistemologia senza soggetto conoscente”, a Van Rootselaar, B. e Acciaio, J. F. (editori), Logica, Metodologia e filosofia della scienza III: Atti del Terzo Congresso Internazionale di Logica, Metodologia e filosofia della scienza, Amsterdam 1967, (Amsterdam: Olanda Settentrionale), pp. 333{373.
Questo è l'articolo in cui Popper introduce la sua idea del terzo mondo. Il documento era stato presentato nella prima sessione del congresso (11:15:00. alle 12:00 mezzogiorno, con H. B. Curry sulla sedia) sotto il titolo “Epistemologia e conoscenza scientifica”. Vedi il programma del congresso a pag. 543 del procedimento.
[Hindley e Seldin 1980a] Hindley, J. Roger e Seldin, Jonathan P. (editori), A. H. B. Curry: Saggi sulla logica combinatoria, Lambda Calcolo e Formalismo, (Stampa accademica).
Una raccolta di documenti relativi al lavoro di Curry. Include una breve biografia e un elenco completo delle pubblicazioni di Curry.
[Gandy 1980b] Gandy, R. O., Una prima prova di normalizzazione di A. M. Turing”, In [1980a], pp. 453{455.
Questa è la prima dimostrazione di Turing del teorema della forma normale per il calcolo tipizzato con un'introduzione di Gandy.
[Hindley e Seldin 2008] Hindley, J. Roger e Seldin, Jonathan P., Lambda-Calcolo e Combinatori, Un introduzione, (Pressa dell'Università di Cambridge).
Un'introduzione generale al lambda-calcolo e alla logica combinatoria.
[di Mol et al. 2010] di Mol, Liesbeth, Bullynck, Maarten, e Martino, Carlo, “Haskell prima di Haskell. Il contributo di Curry alla programmazione (1946-1950)", a Ferreira, F., Lowe, B, Maggiordomo, E., e Gomes, L.M. (Eds.), Programmi, Prove, Processi, 6a Conferenza sulla Calcolabilità in Europa, CIE, 2010, Ponta Delgada, Azzorre, Portogallo, 30 giugno-4 luglio, 2010, Appunti della lezione Springer in informatica, vol. 6158, pp. 108-117.
Un articolo sulla teoria della programmazione di Curry.
[Seldin 2011] Documentario, Jonathan P., “La ricerca di una riduzione nella logica combinatoria equivalente a -riduzione”, Informatica teorica 412, 4905-4918.
Un articolo che descrive il tentativo di trovare una riduzione nella logica combinatoria equivalente a -riduzione, inclusa una discussione dei problemi tecnici coinvolti.
[Seldin 2017] Documentario, Jonathan P., La ricerca di una riduzione nella logica combinatoria equivale a -riduzione, Parte II, Informatica teorica 663, 34-58.
Un articolo che fornisce le prove delle proprietà chiave delle proposte fornite in Seldin 2011.
Informazioni sull'autore

Jonathan P. Documentario
E-mail: [email protected]
Università di Lethbridge
Canada