Załozeniowe systemy normalnych logik modalnych.pdf

Zało»eniowesystemynormalnychlogik

modalnych

MarcinTkaczyk

Wniniejszymtek±ciejestzaprezentowanysystemlogikimodalnejKzbu-

dowanymetod¡zało»eniow¡,czylimetod¡dedukcjinaturalnejopracowan¡

przezJ.SłupeckiegoiL.Borkowskiego,atak»edowodyodpowiednichtwier-

dze«orównowa»no±ciprezentowanegosystemuorazaksjomatycznegouj¦cia

logikimodalnejK.Ponadtopokazanajestmetodabudowaniametod¡zało»e-

niow¡wielumocniejszychodKnormalnychsystemówmodalnychwoparciu

orezultatyuzyskanedlasystemuK.

Dotychczasowepróbybudowaniasystemówmodalnychmetod¡zało»e-

niow¡pochodz¡odjednegoztwórcówtejmetody,Borkowskiego. 1 Wyniki

Borkowskiegopodlegaj¡jednakpewnymograniczeniom.

PrzedewszystkimBorkowskiuzyskałjedyniezało»eniowesystemyS4i

S5,nale»¡cedonajmocniejszychsystemówmodalnych.Niewiadomo,jakz

tychsystemówuzyska¢systemysłabsze.PonadtoBorkowskiodwołujesi¦

wsposóbistotnyb¡d¹dopoj¦ciaimplikacji±cisłej ,b¡d¹doindeksowa-

niazmiennychzdaniowych.Cz¦±¢regułprzyj¦tychprzezBorkowskiegoma

wreszciefaktyczniecharakterdeﬁnicjiwpostacidwóchodwrotnychschema-

tówwnioskowania,gwarantowanychprzezdwieimplikacje,składaj¡cesi¦na

deﬁnicyjn¡równowa»no±¢.Tymczasemdospecyﬁkizało»eniowegosystemu

logikiklasycznejnale»yniezawieraniepierwotnychregułzast¦powaniadeﬁ-

nicyjnego.

Wzwi¡zkuzzarysowanymiuwagamizachodzipotrzebakontynuowania

dziełaSłupeckiegoiBorkowskiegoprzezrozbudow¦metodyzało»eniowej.

Jesttocelniniejszegotekstu.

1 Por.L.Borkowski, Oterminachmodalnych ,w:Ten»e, Studialogiczne.Wybór ,TN

KUL,Lublin1990,s.138–173.Ten»e, Opewnymsystemielogicznymopartymnaregułach

ijegozastosowaniuprzynauczaniulogikimatematycznej.R.III.Nieklasycznerachunki

logiczne ,tam»e,s.174–183.

1AksjomatyzacjasystemuK

Doniosło±¢systemulogikimodalnejKbierzesi¦st¡d,»e—u»ywaj¡c

terminologiiE.J.Lemmona—jesttonajsłabsza normalnalogikamodalna .

Wszelkienormalnesystemylogikimodalnej(as¡tosystemynajcz¦±ciejprzez

logikówbadane)zawieraj¡systemK.Standardowa(aczkolwiekniejedyna)

aksjomatyzacjasystemuKprzedstawiasi¦nast¦puj¡co. 2

SystemKjestnadbudowanynadklasycznymrachunkiemzda«izawiera

opróczpodstawie«jegotezjedenaksjomatosobliwy,zwanycz¦stowzorem

(K):

( p ! q ) ! (

p !

q ) (1)

deﬁnicj¦

)=( ¬

¬ ) (2)

oraz—opróczregułpodstawianiaiodrywania—reguł¦procedurydowodo-

wej

` (

)

(3)

SławnysystemT—przykładowo—powstajezsystemuKprzezdoł¡czenie

wzoru(2 p ! p ),asystemD—przezdoł¡czeniewzoru(2 p !

3 p ).

2Zało»eniowysystemklasycznegorachunku

zda«

Zało»eniowysystemklasycznegorachunkuzda«J.SłupeckiegoiL.Bor-

kowskiegoopierasi¦nanast¦puj¡cychzało»eniach:siedempierwotnychreguł

doł¡czanianowychwierszydodowoduodziesi¦ciuschematachorazjedna

pierwotnaregułatworzeniadowodu,mianowicieregułatworzeniazało»enio-

wegodowoduniewprost. 3 Regułydoł¡czanianowychwierszydodowodu

2 Por.G.E.Hughes,M.J.Cresswell, ANewIntroductiontoModalLogic ,Routledge,

LondonandNewYork1996,s.25.

3 Por.L.Borkowski, Wprowadzeniedologikiiteoriimnogo±ci ,TNKUL,Lublin1991,

s.31–38.

pozwalaj¡nawnioskowanieodpowiedniowedługnast¦puj¡cychschematów:

RO ( ! ) , `

DK , ` ( ^ )

OK ( ^ ) `

( ^ ) `

DA ` ( _ )

` ( _ )

OA ( _ ) , ( ¬ ) `

DE ( ! ) , ( ! ) ` ( )

OE ( ) ` ( ! )

( ) ` ( ! )

(4)

Natomiastregułatworzeniazało»eniowegodowoduniewproststwierdza,»e

zatez¦wolnouzna¢wszystkieitylkotakiewyra»eniaopostaci

1 ! ( 2 ! ( 3 !···! ( n − 1 ! n ) ... ))( n 1) (5)

dlaktórychistniejezało»eniowydowódniewprost,toznaczytakisko«czony

ci¡gwyra»e«,»e

• w n − 1jegowierszachwyst¦puj¡wyra»enia 1 , 2 , 3 ,..., n − 1 jako

zało»eniatwierdzenia,

• w n wierszu( ¬ n )jakozało»eniedowoduniewprost,

• wszystkiepozostałewierszes¡uprzedniodowiedzionymitezamilub

zostaj¡uzyskanezwierszywcze±niejszychzapomoc¡regułdoł¡czania

nowychwierszydodowodu(4),oraz

• wdowodziewyst¦puj¡dwawierszesprzeczne.

Wtórnawsystemiejestregułatworzeniazało»eniowegodowoduwprost,ró»-

ni¡casi¦odregułytworzeniadowoduniewprosttym,»ezzało»e«twierdze-

nia,bezzało»eniadowoduniewprost,nale»ywanalogicznysposóbwypro-

wadzi¢wyra»enie n zamiastdwóchwyra»e«sprzecznych.

J.SłupeckiiL.Borkowskiudowodnili,»etakokre±lonysystemjestrówno-

wa»nyklasycznemurachunkowizda«,toznaczyistniejezało»eniowydowód

niewprostdlawszystkichitylkotychwyra»e«klasycznegorachunkuzda«,

»ewyra»eniatesprawdzaj¡si¦wklasycznejmatrycydwuwarto±ciowejczyli

s¡tezamiaksjomatycznychsystemówklasycznegorachunkuzda«.

3Okre±leniezało»eniowegosystemuK

Konstruowanyzało»eniowysystemlogikimodalnejKoprzemynaprzed-

stawionymwparagraﬁe2zało»eniowymsystemieklasycznegorachunkuzda«.

Poniewa»,jakwspomnianowparagraﬁe2istniejedowód,»esystemSłu-

peckiegoiBorkowskiegojestrównowa»nyinnymsystemomklasycznegora-

chunkuzda«,wolnonamuzna¢,»ejestonte»równowa»nysystemowiaksjo-

matycznemuklasycznegorachunkuzda«,naktórymopierasi¦przedstawiony

wparagraﬁe1aksjomatycznysystemlogikimodalnejK.

Poka»emydwasposoby,najakiemo»nauzyska¢zało»eniowysystemlogiki

modalnejKzzało»eniowegosystemuklasycznegorachunkuzda«.Pierwszy

sposóbjestbardziejintuicyjny,drugisposóbjestmniejintuicyjny,aledosko-

nalszyformalnie.Poka»emy,»eobasposobys¡inferencyjnierównowa»ne,tj.

daj¡tensamzbiórtez,oraz»es¡równowa»nesystemowiaksjomatycznemu.

Przypierwszymsposobiewprowadzamyjedn¡pierwotn¡reguł¦doł¡cza-

nianowychwierszydodowodu,uzupełniaj¡clist¦(4).Nowaregułazezwala

nadoł¡czanienowychwierszydodowoduzgodniezeschematem

1 ) , (

2 ) ,..., (

n − 1 )

(6)

n )

je»eliwyra»enie( 1 ! ( 2 ! ( 3 !···! ( n − 1 ! n ) ... )))jestuprzednio

dowiedzion¡tez¡.

Reguła(6)jest,jakpoka»emy,równowa»naaksjomatowi(1)orazregule

(3).Pozostajejednakdeﬁnicja(2),któr¡trzebaprzyj¡¢jakoodr¦bnezało-

»enie.Tutajtkwigłównymankamenttechnicznyomawianegorozwi¡zania.

Dospecyﬁkisystemuzało»eniowegonale»ałobowiemdot¡d,»eniewyst¦-

powaływnimpierwotneregułyzast¦powaniadeﬁnicyjnego.Wprowadzenie

takiejregułyniejest»adn¡katastrof¡,zwłaszcza»eodpowiednieregułyde-

ﬁnicyjnes¡wtórnewzało»eniowymsystemieklasycznegorachunkuzda«.

Ponadtowi¦kszo±¢regułprzyjmowanychdlauzyskaniasystemumodalnego

wpracachBorkowskiegomarównie»faktyczniecharakterdeﬁnicjiprzyj¦tych

wpostacidwóchodwrotnychschematówwnioskowania.Jednak»ewprowa-

dzeniedeﬁnicjistanowiodej±cieodpewnejspecyﬁkisystemuzało»eniowego.

Powstajezatempytanie,czyniemo»nabyzbudowa¢zało»eniowegosys-

temulogikimodalnejKwtakisposób,byunikn¡¢wskazanejniedogodno±ci.

Rzeczywi±cie,jesttakamo»liwo±¢,któr¡obecnieprzedstawimyjakodrugie

rozwi¡zaniezadanegoproblemu.

Zało»eniowysystemlogikimodalnejKmo»nauzyska¢zzało»eniowego

systemuklasycznegorachunkuzda«przezprzyj¦ciedwóchpierwotnychreguł

doł¡czanianowychwierszydodowodu(wzgl¦dniejednejregułyodwóch

(

schematach).Regułytepozwalaj¡nadoł¡czanienowychwierszydodowodu

wedługschematu

1 ) , (

2 ) ,..., (

n − 1 )

(7)

( ¬

¬ n )

orazwedługschematu

( ¬

¬ 1 ) , ( ¬

¬ 2 ) ,..., ( ¬

¬ n − 1 )

(8)

n )

wobuwypadkachpodtymwarunkiem,»ewyra»enie

( 1 ! ( 2 ! ( 3 !···! ( n − 1 ! n ) ... )))

jestuprzedniodowiedzion¡tez¡.Wtakimuj¦ciuuzyskujesi¦systemKbez

potrzebyprzyjmowaniaregułdeﬁnicyjnych.

Podsumowuj¡c,zało»eniowysystemlogikimodalnejKmo»nauzyska¢z

zało»eniowegosystemuklasycznegorachunkuzda«nadwasposoby:przyjmu-

j¡cdodatkow¡reguł¦(6)izarazemprzyjmuj¡czsystemuaksjomatycznego

logikimodalnejKreguł¦zast¦powaniadeﬁnicyjnego(2)lubte»przyjmuj¡c

obokzało»e«klasycznegorachunkuzda«reguły(7)i(8)bezkonieczno±ci

akceptowaniajakichkolwiekinnychzało»e«.

4Równowa»no±¢systemówzało»eniowychK

Dowiedziemy,»eobydwasposobybudowaniazało»eniowegosystemulo-

gikimodalnejKprzedstawionewparagraﬁe3s¡równowa»ne.

Lemat1 Reguły(7)i(8)s¡wtórnewzgl¦demreguły(6)ideﬁnicji(2)na

grunciezało»eniowegosystemuklasycznegorachunkuzda«.

¬ )zostałowprowadzonedodo-

wodunamocyreguły(7).Wówczasnamocyreguły(6)wolnododowodu

doł¡czy¢wyra»enie(

),zktóregoprzezzastosowaniedeﬁnicji(2)otrzymu-

¬ ).

Załó»myteraz,»epewne(2 )zostałodoł¡czonedodowodunamocy

reguły(8).Wówczasdodowodunale»¡odpowiedniewyra»enia

( ¬

¬ 1 ) , ( ¬

¬ 2 ) ,..., ( ¬

¬ m ) ,

zktórychprzezzastosowaniedeﬁnicji(2)otrzymujemywyra»enia

(2 1 ) , (2 2 ) ,..., (2 m ) ,

którewolnodoł¡czy¢dodowodu,woparciuza±otewyra»enia,namocy

reguły(6),wolnowł¡czy¢dodowoduwyra»enie(

).Toko«czydowód.

(

Dowód:Załó»my,»epewnewyra»enie( ¬

jemywyra»enie( ¬

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika: