Monoidal t-norm logik

Inom matematisk logik är monoidal t-normbaserad logik (eller kort sagt MTL ), logiken för vänsterkontinuerliga t-normer , en av t - normens fuzzy logik . Den tillhör den bredare klassen av substrukturella logiker , eller logik av restgitter ; den utvidgar logiken för kommutativt begränsade integralrestgitter (känd som Höhles monoidala logik, Onos FL _ew , eller intuitionistisk logik utan sammandragning) med axiomet prelinearitet.

Motivering

I suddig logik , snarare än att betrakta påståenden som antingen sanna eller falska, associerar vi varje påstående med ett numeriskt förtroende för det påståendet. Enligt konvention sträcker sig konfidenserna över enhetsintervallet $[0,1]$ , där den maximala konfidensen $1$ motsvarar det klassiska begreppet sann och den minimala konfidensen $0$ motsvarar till det klassiska begreppet falskt.

T-normer är binära funktioner på det reella enhetsintervallet [0, 1], som i fuzzy logik ofta används för att representera en konjunktion connective; om $a,b\in [0,1]$ är de konfidenser vi tillskriver påståendena $A$ respektive $B$ , då använder man en t-norm $*$ för att beräkna konfidensen $a*b$ som tillskrivs den sammansatta satsen ' $A$ och $B$ '. En t-norm $*$ måste uppfylla egenskaperna för

kommutativitet $a*b=b*a$ ,

associativitet $(a*b)*c=a*( b*c)$ ,

monotoni — om $a\leqslant b$ och $c\leqslant d$ så $a*c\leqslant b* d$ ,

och har 1 som identitetselement $1*a=a$ .

Speciellt frånvarande i denna lista är egenskapen idempotens $a*a=a$ ; det närmaste man kommer är att $a*a\leqslant 1*a=a$ . Det kan tyckas konstigt att vara mindre säker på ' $A$ och $A$ ' än i bara $A$ , men vi vill generellt sett tillåta förtroendet ${\ displaystyle a*b}$ i en kombinerad ' $A$ och $B$ ' är mindre än både konfidensen $a$ i $A$ och konfidensen $b$ i $B$ , och sedan ordningen $a*b<a\leqslant b$ genom monotonitet kräver $a*a \leqslant a*b<a$ . Ett annat sätt att uttrycka det är att t-normen bara kan ta hänsyn till konfidenserna som siffror, inte de skäl som kan ligga bakom att tillskriva dessa konfidenser; den kan därför inte behandla ' $A$ och $A$ ' annorlunda än ' $A$ och $B$ , där vi är lika säkra på båda.

Eftersom symbolen $\wedge$ via dess användning i gitterteorin är mycket nära förknippad med egenskapen idempotens, kan det vara användbart att byta till en annan symbol för konjunktion som inte nödvändigtvis är idempotent. I fuzzy logic traditionen använder man ibland $\&$ för denna "starka" konjunktion, men denna artikel följer den substrukturella logiktraditionen att använda $\otimes$ för den starka konjunktionen; alltså $a*b$ är det förtroende vi tillskriver påståendet $A\otimes B$ (läs fortfarande ' $A$ och $B$ ', kanske med 'stark' eller 'multiplikativ' som kvalificering av 'och').

Efter att ha formaliserat konjunktion $\otimes$ , vill man fortsätta med de andra konnektiven. Ett tillvägagångssätt för att göra det är att introducera negation som en ordningsomkastande karta ${\displaystyle [0,1]\longrightarrow [0,1]} ,$ och sedan definiera återstående kopplingar med hjälp av De Morgans lagar , materiell implikation och liknande. Ett problem med att göra det är att de resulterande logikerna kan ha oönskade egenskaper: de kan vara för nära klassisk logik, eller om inte, omvänt, inte stödja förväntade slutledningsregler . Ett alternativ som gör konsekvenserna av olika val mer förutsägbara är att istället fortsätta med implikation $\to$ som det andra konnektivet: detta är totalt sett det vanligaste bindemedlet i axiomatiseringar av logik, och det har närmare kopplingar till de deduktiva aspekterna av logik än de flesta andra kopplingar. En konfidensmotsvarighet $\Rightarrow$ av implikationskonnektivet kan faktiskt definieras direkt som t-normens residuum .

Den logiska länken mellan konjunktion och implikation tillhandahålls av något så grundläggande som slutledningsregeln modus ponens $A,A\to B\vdash B$ : från $A$ och $A\to B$ följer $B$ . I det luddiga logiska fallet som är mer rigoröst skrivet som ${\displaystyle A\otimes (A\to B)\vdash B} ,$ eftersom detta tydliggör att vårt förtroende för premissen(erna) här är att i $A\otimes (A\to B)$ , inte de i $A$ och $A\to B$ separat. Så om $a$ och $b$ är våra konfidenser i $A$ respektive $B$ , då är $a\Rightarrow b$ det eftersträvade konfidensvärdet i $A\to B$ , och $a*(a\Rightarrow b)$ är det kombinerade förtroendet för $A\ ibland (A\till B)$ . Det kräver vi

$a*(a{\mathbin {\Rightarrow }}b)\leqslant b$

eftersom vårt förtroende $b$ för $B$ inte bör vara mindre än vårt förtroende $a*(a\Rightarrow b)$ i påståendet $A\otimes (A\to B)$ från vilken $B$ logiskt följer. Detta begränsar det eftersträvade förtroendet $a\Rightarrow b$ , och en metod för att omvandla $\Rightarrow$ till en binär operation som $*$ skulle vara att göra den så stor som möjligt medan respektera denna gräns:

$a{\mathbin {\Rightarrow }}b\equiv \sup \left\{x\in [0,1]\;{\big |}\;a*x\leqslant b \right\}$ .

Att ta $x=0$ ger ${\displaystyle a*x=a*0\leqslant 1*0=0\leqslant b} ,$ så det högsta är alltid av en icke-tom avgränsad mängd och därmed väldefinierad. För en generell t-norm kvarstår möjligheten att $f_{a}(x)=a*x$ har en hoppdiskontinuitet vid $x= a{\mathbin {\Rightarrow }}b$ , i vilket fall $a*(a{\mathbin {\Rightarrow }}b)$ skulle kunna bli strikt större än $b$ även om $a{\mathbin {\Rightarrow }}b$ definieras som den minsta övre gränsen för $x$ s som uppfyller $a*x\leqslant b$ ; för att förhindra det och få byggarbetet som förväntat kräver vi att t-normen $*$ är vänsterkontinuerlig . Resterna av en vänsterkontinuerlig t-norm kan således karakteriseras som den svagaste funktionen som gör den fuzzy modus ponens giltig, vilket gör den till en lämplig sanningsfunktion för implikation i fuzzy logik.

Mer algebraiskt säger vi att en operation $\Rightarrow$ är en rest av en t-norm $*$ om för alla $a$ , $b$ och ${\ displaystyle c}$ den uppfyller

$a*b\leq c$ om och endast om $a\leq (b{\mathbin {\Rightarrow }}c)$ .

Denna ekvivalens av numeriska jämförelser speglar ekvivalensen av entailments

$A\otimes B\vdash C$ om och endast om $A\vdash B\to C$

som existerar eftersom alla bevis för $C$ från premissen $A\otimes B$ kan konverteras till ett bevis på $B\to C$ från premissen ${\ displaystyle A}$ genom att göra ett extra implikationsintroduktionssteg , och omvänt alla bevis på $B\to C$ från premissen $A$ kan konverteras till ett bevis på $C$ från premissen $A\otimes B$ genom att göra ett extra implikationselimineringssteg . Vänsterkontinuitet hos t-normen är det nödvändiga och tillräckliga villkoret för att detta förhållande mellan en t-normkonjunktion och dess återstående implikation ska hålla.

Sanningsfunktioner för ytterligare propositionella konnektiver kan definieras med hjälp av t-normen och dess residuum, till exempel restnegationen $\neg x=(x{\mathbin {\Rightarrow }}0).$ På detta sätt fungerar den vänsterkontinuerliga t-normen, dess residuum och sanningsfunktionerna för ytterligare propositionella konnektiver (se avsnittet Standardsemantik nedan) bestäm sanningsvärdena för komplexa propositionsformler i [0, 1]. Formler som alltid utvärderas till 1 kallas då tautologier med avseende på den givna vänsterkontinuerliga t-normen $*,$ eller $*{\mbox{-}}$ tautologier. Mängden av alla $*{\mbox{-}}$ tautologier kallas t-normens logik $*,$ eftersom dessa formler representerar lagarna för fuzzy logik (bestämda av t -norm) som håller (till grad 1) oavsett sanningsgraderna för atomformler . Vissa formler är tautologier med avseende på alla vänsterkontinuerliga t-normer: de representerar allmänna lagar för propositionell fuzzy logik som är oberoende av valet av en viss vänsterkontinuerlig t-norm. Dessa formler bildar logiken MTL, som alltså kan karakteriseras som logiken för vänsterkontinuerliga t-normer.

Syntax

Språk

Språket för den propositionella logiken MTL består av ett uträkneligt antal propositionella variabler och följande primitiva logiska kopplingar :

• Implikation $\rightarrow$ ( binär )
• Stark konjunktion $\otimes$ (binär). Tecknet & är en mer traditionell notation för stark konjunktion i litteraturen om fuzzy logic, medan notationen $\otimes$ följer traditionen av substrukturell logik.
• Svag konjunktion ${\displaystyle \wedge } (binär)$ , även kallad gitterkonjunktion (som det alltid realiseras av gitteroperationen meet i algebraisk semantik). Till skillnad från BL och starkare fuzzy logics är svag konjunktion inte definierbar i MTL och måste inkluderas bland primitiva connectives.
• Botten $\bot$ ( nullär — en propositionskonstant ; $0$ eller ${\overline {0}}$ är vanliga alternativa symboler och noll ett vanligt alternativt namn för propositionskonstanten (som konstanter botten och noll för substrukturella logiker sammanfaller i MTL).

Följande är de vanligaste definierade logiska kopplingarna:

• Negation $\neg$ ( unary ), definierad som

$\neg A\equiv A\rightarrow \bot$

• Ekvivalens $\leftrightarrow$ (binär), definierad som

$A\leftrightarrow B\equiv (A\rightarrow B)\wedge (B\rightarrow A)$

I MTL är definitionen ekvivalent med $(A\högerpil B)\otimes (B\högerpil A).$

• (Svag) disjunktion $\vee$ (binär), även kallad gitterdisjunktion (som det alltid realiseras av gitteroperationen för join i algebraisk semantik), definierad som

$A\vee B\equiv ((A\högerpil B)\högerpil B) \wedge ((B\rightarrow A)\rightarrow A)$

• Topp $\top$ (nullär), även kallad en och betecknad med $1$ eller ${\overline {1} }$ (eftersom konstanterna topp och noll för substrukturell logik sammanfaller i MTL), definierad som

$\top \equiv \bot \rightarrow \bot$

Välformade formler för MTL definieras som vanligt i propositionell logik . För att spara parenteser är det vanligt att använda följande prioritetsordning:

• Unära bindemedel (binder närmast)
• Andra binära bindemedel än implikation och ekvivalens
• Implikation och ekvivalens (binder mest löst)

Axiom

Ett avdragssystem i Hilbert-stil för MTL har införts av Esteva och Godo (2001). Dess enda avledningsregel är modus ponens :

från $A$ och $A\rightarrow B$ härleder $B.$

Följande är dess axiomschema :

${\begin{array}{ll }{\rm {(MTL1)}}\colon &(A\högerpil B)\högerpil ((B\högerpil C)\högerpil (A\högerpil C))\\{\rm {(MTL2)}}\kolon &A\otimes B\rightarrow A\\{\rm {(MTL3)}}\colon &A\otimes B\rightarrow B\otimes A\\{\rm {(MTL4a)}}\colon &A\wedge B\högerpil A \\{\rm {(MTL4b)}}\colon &A\wedge B\högerpil B\wedge A\\{\rm {(MTL4c)}}\colon &A\otimes (A\högerpil B)\högerpil A\kil B\\{\rm {(MTL5a)}}\colon &(A\högerpil (B\högerpil C))\högerpil (A\otimes B\högerpil C)\\{\rm {(MTL5b)}}\kolon &(A\otimes B\högerpil C)\högerpil (A\högerpil (B\högerpil C))\\{\rm {(MTL6)}}\kolon &((A\högerpil B)\högerpil C)\högerpil (((B\högerpil A)\högerpil C)\högerpil C)\\{\rm {(MTL7)}}\colon &\bot \rightarrow A\end{array}}$

Den traditionella numreringen av axiom, som ges i den vänstra kolumnen, är härledd från numreringen av axiom i Hájeks grundläggande fuzzy logik BL. Axiomen (MTL4a)–(MTL4c) ersätter delningsaxiomet ( BL4) för BL. Axiomen (MTL5a) och (MTL5b) uttrycker lagen om residual och axiomet (MTL6) motsvarar villkoret prelinearitet. Axiomen (MTL2) och (MTL3) för det ursprungliga axiomatiska systemet visade sig vara redundanta (Chvalovský, 2012) och (Cintula, 2005). Alla andra axiom visade sig vara oberoende (Chvalovský, 2012).

Semantik

Liksom i andra propositionella t-norm fuzzy logics används algebraisk semantik övervägande för MTL , med tre huvudklasser av algebror med avseende på vilka logiken är komplett :

• Allmän semantik , bildad av alla MTL-algebror - det vill säga alla algebror för vilka logiken är sund
• Linjär semantik , bildad av alla linjära MTL-algebror - det vill säga alla MTL-algebror vars gitterordning är linjär
• Standardsemantik , bildad av alla standard MTL-algebror — det vill säga alla MTL-algebror vars gitterredukt är det reella enhetsintervallet [0, 1] med den vanliga ordningen; de bestäms unikt av funktionen som tolkar stark konjunktion, vilket kan vara vilken vänsterkontinuerlig t-norm som helst

Allmän semantik

MTL-algebror

Algebror för vilka logiken MTL är ljud kallas MTL-algebror. De kan karakteriseras som prelinjära kommutativa bundna integralrestgitter. Mer detaljerat är en algebraisk struktur $(L,\wedge ,\vee ,\ast ,\Rightarrow ,0,1)$ en MTL-algebra om

• $(L,\wedge ,\vee ,0,1)$ är ett avgränsat gitter med det övre elementet 0 och det nedre elementet 1
• $(L,\ast ,1)$ är en kommutativ monoid
• $\ast$ och $\Rightarrow$ bildar ett adjoint par , det vill säga $z*x\leq y$ om och endast om ${\ displaystyle z\leq x\Rightarrow y,}$ där $\leq$ är gitterordningen för $(L,\wedge ,\vee ),$ för alla x , y , och z i $L$ , ( restvillkoret )
• $\displaystyle (x\Rightarrow y)\vee (y\Rightarrow x)=1}$ { gäller för alla x och y i L (prelinearitetsvillkoret )

Viktiga exempel på MTL-algebror är standard -MTL-algebror på det reella enhetsintervallet [0, 1]. Ytterligare exempel inkluderar alla booleska algebror , alla linjära Heyting-algebror (båda med $\ast =\wedge$ ), alla MV-algebror , alla BL -algebror, etc. Eftersom residualvillkoret på samma sätt kan uttryckas med identiteter , MTL-algebror bildar en variation .

Tolkning av logiken MTL i MTL-algebror

MTL-kopplingarna tolkas i MTL-algebror enligt följande:

• Stark konjunktion av den monoida operationen $\ast$
• Implikation av operationen $\Rightarrow$ (vilket kallas residuum av $\ast$ )
• Svag konjunktion och svag disjunktion av gitteroperationerna $\wedge$ respektive $\vee ,$ (vanligtvis betecknad med samma symboler som connectives, om ingen förvirring kan uppstå)
• Sanningskonstanterna noll (överst) och en (nederst) med konstanterna 0 och 1
• Ekvivalensanslutningen tolkas av operationen $\Leftrightarrow$ definierad som

$x\Leftrightarrow y\equiv (x\Rightarrow y)\wedge (y\Rightarrow x)$

På grund av prelinearitetsvillkoret är denna definition ekvivalent med en som använder $\ast$ istället för $\wedge ,$ alltså

$x\Leftrightarrow y\equiv (x\Rightarrow y)\ast (y\Högerpil x)$

• Negation tolkas av den definierbara operationen $-x\equiv x\Högerpil 0$

Med denna tolkning av kopplingar, sträcker sig varje utvärdering e _v av propositionella variabler i L unikt till en utvärdering e av alla välformade formler för MTL, genom följande induktiva definition (som generaliserar Tarskis sanningsvillkor ), för alla formler A , B , och valfri propositionsvariabel p :

${\begin{array}{rcl}e(p)&=&e_{\mathrm {v} }(p)\\e(\bot )&= &0\\e(\top )&=&1\\e(A\otimes B)&=&e(A)\ast e(B)\\e(A\högerpil B)&=&e(A)\Högerpil e (B)\\e(A\kil B)&=&e(A)\kil e(B)\\e(A\vee B)&=&e(A)\vee e(B)\\e(A \leftrightarrow B)&=&e(A)\Leftrightarrow e(B)\\e(\neg A)&=&e(A)\Rightarrow 0\end{array}}$

Informellt representerar sanningsvärdet 1 full sanning och sanningsvärdet 0 representerar full falskhet; mellanliggande sanningsvärden representerar mellanliggande grader av sanning. Således anses en formel vara helt sann under en utvärdering e om e ( A ) = 1. En formel A sägs vara giltig i en MTL-algebra L om den är helt sann under alla utvärderingar i L , det vill säga om e ( A ) = 1 för alla utvärderingar e i L . Vissa formler (till exempel p → p ) är giltiga i vilken MTL-algebra som helst; dessa kallas tautologier av MTL.

Begreppet global entailment (eller: global konsekvens ) definieras för MTL enligt följande: en uppsättning formler Γ innebär en formel A (eller: A är en global konsekvens av Γ), i symbolerna $\Gamma \modeller A,$ om för någon utvärdering e i någon MTL-algebra, närhelst e ( B ) = 1 för alla formler B i Γ, då också e ( A ) = 1. Informellt representerar den globala konsekvensrelationen överföringen av full sanning i vilken MTL-algebra som helst av sanningsvärden.

Allmänna sundhets- och fullständighetssatser

Logiken MTL är sund och komplett med avseende på klassen för alla MTL-algebror (Esteva & Godo, 2001):

En formel är bevisbar i MTL om och bara om den är giltig i alla MTL-algebror.

Begreppet MTL-algebra är i själva verket så definierat att MTL-algebra utgör klassen av alla algebror för vilka den logiska MTL är ljud. Dessutom gäller stark fullständighetssatsen :

En formel A är en global konsekvens i MTL av en uppsättning formler Γ om och endast om A kan härledas från Γ i MTL.

Linjär semantik

Liksom algebror för andra fuzzy logiker, har MTL-algebror följande linjära subdirekta nedbrytningsegenskap :

Varje MTL-algebra är en subdirekt produkt av linjärt ordnade MTL-algebra.

(En subdirekt produkt är en subalgebra av den direkta produkten så att alla projektionskartor är surjektiva . En MTL-algebra är linjärt ordnad om dess gitterordning är linjär .)

Till följd av den linjära subdirekta nedbrytningsegenskapen för alla MTL-algebror, gäller fullständighetssatsen med avseende på linjära MTL-algebror (Esteva & Godo, 2001):

• En formel är bevisbar i MTL om och bara om den är giltig i alla linjära MTL-algebror.
• En formel A är härledbar i MTL från en uppsättning formler Γ om och endast om A är en global konsekvens i alla linjära MTL-algebror av Γ.

Standard semantik

Standard kallas de MTL-algebror vars gitterredukt är det reella enhetsintervallet [0, 1]. De bestäms unikt av den verkliga funktionen som tolkar stark konjunktion, som kan vara vilken som helst vänsterkontinuerlig t-norm $\ast$ . Standarden MTL-algebra bestäms av en vänsterkontinuerlig t-norm $\ast$ betecknas vanligtvis med $[0,1]_{\ast }.$ I $[0,1]_{\ast },$ representeras implikationen av resten av $\ ast ,$ svag konjunktion respektive disjunktion med minimum och maximum, och sanningskonstanterna noll respektive ett med de reella talen 0 och 1.

Den logiska MTL är komplett med avseende på standard MTL-algebror; detta faktum uttrycks av standardsatsen för fullständighet (Jenei & Montagna, 2002):

En formel är bevisbar i MTL om och bara om den är giltig i alla standard MTL-algebror.

Eftersom MTL är komplett med avseende på standard MTL-algebror, som bestäms av vänsterkontinuerliga t-normer, hänvisas MTL ofta till som logiken för vänsterkontinuerliga t-normer ( på samma sätt som BL är logiken för kontinuerliga t-normer ).

Bibliografi

• Hájek P., 1998, Metamathematics of Fuzzy Logic . Dordrecht: Kluwer.
• Esteva F. & Godo L., 2001, "Monoidal t-norm based logic: Towards a logic of left-continuous t-norms". Fuzzy Sets and Systems 124 : 271–288.
• Jenei S. & Montagna F., 2002, "Ett bevis på standardfullständighet hos Esteva och Godos monoidala logik MTL". Studia Logica 70 : 184–192.
• Ono, H., 2003, "Substructural logics and rested lattices - an introduction". I FV Hendricks, J. Malinowski (red.): Trends in Logic: 50 Years of Studia Logica, Trends in Logic 20 : 177–212.
• Cintula P., 2005, "Kort anmärkning: Om redundansen av axiom (A3) i BL och MTL". Soft Computing 9 : 942.
• Cintula P., 2006, "Svagt implikativ (fuzzy) logics I: Basic properties". Arkiv för matematisk logik 45 : 673–704.
• Chvalovský K., 2012, " On the Independence of Axioms in BL and MTL ". Fuzzy Sets and Systems 197 : 123–129, doi : 10.1016/j.fss.2011.10.018 .