Looginen harmonia
Loogisella harmonialla tarkoitetaan yleisesti ehtoja, jotka rajoittavat uusien konnektiivien lisäämistä loogiseen päättelysysteemiin. Ehdot koskevat uusia konnektiiveja määritteleviin päättelysääntöihin. Luonnollisessa päättelyssä tämä tarkoittaa konnektiivin tuonti- ja eliminointisääntöjä, mutta loogista harmoniaa voidaan vaatia myös muunlaisilta päättelysysteemeiltä, kuten sekvenssikalkyyliltä.
Looginen harmonia ymmärretään yleensä tarkoittamaan joko kaikkia päättelysääntöjä koskevia rajoituksia, tai ainoastaan vaatimusta, ettei uusilla konnektiiveilla tule voida päätellä uusia lauseita, jotka eivät sisällä uutta konnektiivia itseään. Tämä ehto on ekvivalentti uuden systeemin normalisoitavuuden (luonnollisessa päättelyssä) tai leikkaussäännön eliminoitavuuden (sekvenssikalkyylissä) kanssa.
Historia[muokkaa | muokkaa wikitekstiä]
Harmonian alkuperä löytyy Gerhard Gentzenin työstä totuusteoreettisen semantiikan parissa 1930-luvulla, jossa kantavana ajatuksena oli, että konnektiivin päättelysäännöt määräävät täydellisesti sen merkityksen.[1] Ajatuksen esikuvana voidaan nähdä Ludwig Wittgensteinin näkemys, että sanat ylipäänsä saavat merkityksensä niiden käytön kautta. Gentzen ei kuitenkaan asettanut mitään rajoitteita sille, millaiset päättelysäännöt olisivat hyväksyttäviä; hän vain katsoi merkityksen ikään kuin "sijaitsevan" säännöissä.
Vuonna 1961 Arthur Prior esitti vastalauseensa ja konstruoi uuden tonk-konnektiivin, joka lainasi säännöikseen yleisesti hyväksytyt disjunktion tuontisäännön ja konjunktion eliminointisäännön, mutta jolla ei tuntunut kuitenkaan olevan mitään mielekästä merkitystä.[2] Säännöt nimittäin johtivat katastrofaalisiin päättelyihin, kun mistä tahansa oletuksesta Asaatettiin tonkin avulla johtaa mikä tahansa lopputulos B, tähän tapaan:
Priorin argumentti oli, että koska tällaisia järjettömiä konnektiiveja voidaan luoda pelkillä päättelysäännöillä, merkitys ei voi syntyä yksin säännöistä.
Pari vuotta myöhemmin Nuel Belnap vastasi Priorin haasteeseen ja esitti, että merkitys voi kyllä määräytyä kokonaan päättelysääntöjen perusteella, mutta että näitä sääntöjä koskevat tietyt rajoitukset, kuten se, ettei uudella konnektiivilla tulisi voida päätellä uusia totuuksia, joissa uusi konnektiivi ei esiinny.[3] Edellä kuvattu tonk-päättely rikkoo juuri tätä sääntöä. Belnap esitti muitakin rajoitteita, joita myöhemmin alettiin myös yhdessä kutsua loogisen harmonian vaatimukseksi.
Lähteet[muokkaa | muokkaa wikitekstiä]
- ↑ Gentzen, Gerhard: Investigations Into Logical Deduction. American Philosophical Quarterly, 1965 (1934), 2. vsk, nro 3, s. 204–2018.
- ↑ Prior, Arthur: The Runabout Inference-Ticket. Analysis, joulukuu 1960, 21. vsk, nro 2, s. 38–39.
- ↑ Belnap, Nuel: Tonk, Plonk and Plink. Analysis, kesäkuu 1962, 22. vsk, nro 6, s. 130–134.