Proposisjonell logikk

Den proposisjonelle (eller enunciative ) logikken er et formelt språk med en enkel syntaktisk struktur , grunnleggende basert på elementære proposisjoner (atomer) og på logiske forbindelser av en sann-funksjonell type, som returnerer sannhetsverdien til en proposisjon basert på sannhetsverdien relatert. klausuler (vanligvis kjent som AND, OR, NOT ...). Semantikken _av proposisjonell logikk definerer betydningen av symboler og enhver proposisjon som respekterer språkets syntaktiske regler, basert på sannhetsverdiene assosiert med atomer. Gitt en tolkning (eller modell) av en proposisjon (generelt av et sett av proposisjoner), det vil si en assosiasjon mellom elementære proposisjoner og representerte realiteter, kan vi generere et uendelig sett med proposisjoner med definert mening angående den virkeligheten. Hver proposisjon refererer derfor til ett eller flere objekter i den representerte virkeligheten (også abstrakt, selvfølgelig) og lar deg beskrive eller resonnere om det objektet, ved å bruke bare de to verdiene "True" og "False".

Syntaks

Definisjonen av setningsstrukturen (eller syntaksen) av proposisjonell logikk er basert på to komponenter:

Alfabet

Alfabetet til proposisjonell logikk består av:

Velformede formler

De "syntaktisk korrekte" uttrykkene for proposisjonell logikk (de som skal representere setninger med mening på en entydig måte) kalles f ormule b en f ormate, kort fbf (ofte i litteraturen finner vi også wff , fra de engelske "well-formed formulas" "), og er definert ved hjelp av følgende rekursive definisjon :

  1. et forslagssymbol er en wff
  2. hvis A er en wff er det også ¬ A
  3. hvis A og B er wffs, så er det ( A B ), ( A B ), ( A → B ) og ( A ↔ B )
  4. ingenting annet er en wff

Eksempler på velformede formler er :

Reglene ovenfor definerer språket for proposisjonell logikk gjennom en generativ grammatikk .

Grammatikken for proposisjonell logikk skrevet i BNF er som følger:

f: = L | IKKE f | (f1 OG f2) | (f1 ELLER f2) | (f1 -> f2) | (f1 <-> f2)

Semantikk

Formlene for proposisjonell logikk kan assosieres med sannhetsverdier ved hjelp av en evalueringsfunksjon :

En evalueringsfunksjon er en funksjon som går fra settet L av velformede formler i settet { V , F } (sant, usant)

v  : L → { V , F }

slik at for hvert par wffs x og y gjelder følgende betingelser:

v (¬ x ) = V hvis v ( x ) = F v (¬ x ) = F hvis v ( x ) = V v ( x y ) = V hvis og bare hvis v ( x ) = V og v ( y ) = V v ( x y ) = V hvis og bare hvis v ( x ) = V eller v ( y ) = V v ( x → y ) = V hvis og bare hvis v ( x ) = F eller v ( y ) = V v ( x ↔ y ) = V hvis og bare hvis v ( x ) = v ( y )

Disse forholdene gjenspeiler betydningen som skal tilskrives symbolene knyttet til de logiske forbindelsene og kan oppsummeres ved hjelp av følgende sannhetstabell :

F. F. V. F. F. V. V.
F. V. F. F. V. F. V.
V. F. V. F. V. F. F.
V. V. F. V. V. V. V.

Det er vist at en evaluering er entydig identifisert av verdiene den antar på symbolene til proposisjoner: verdiene på de mer komplekse formlene der symboler for logiske operatorer vises, kan utledes fra betingelsene ovenfor som definerer en evaluering .

Tilfredsstillelse, tautologier og motsetninger

Følgende definisjoner er viktige:

En velformet formel A sies

Et trivielt eksempel på en tilfredsstillende formel er p , et eksempel på en motstridende formel er ( p ¬ p ), et eksempel på tautologi er ( p ¬ p ).

Problemet med å fastslå om en formel er tilfredsstillende - også kjent som det boolske tilfredshetsproblemet - er et problem som kan avgjøres : det kan løses ved å vurdere alle mulige kombinasjoner av evalueringer på proposisjonelle symboler og beregne den tilsvarende sannhetsverdien til den sammensatte formelen ved å utnytte egenskapene til evalueringsfunksjonen. Cook-Levin-teoremet sier at dette problemet tilhører klassen av NP-komplette problemer .

Definisjonen av tilfredsstillelse kan utvides til (muligens uendelige) sett med velformede formler:

Et sett med wffs S sies å være tilfredsstillende hvis det er en evaluering v som tildeler verdi V til alle formlene til S.

Kompaktitetsteoremet fastslår at et sett med wffs S er tilfredsstillbar hvis og bare hvis hver av dens endelige delmengde er tilfredsstilt.

Med andre termer er det mulig å gi følgende definisjoner. En velformet formel A er:

Bibliografi

Relaterte elementer

Eksterne lenker