I matematikk kalles uttrykkene " for alt " og " det eksisterer ", som brukes til å formulere matematiske proposisjoner i beregningen av predikater , kvantifiseringer . Symbolene som representerer det formelle språket kalles kvantifiseringsmidler (eller tidligere kvantifiseringsmidler ).
Universell kvantisering ("for alle ..." eller "hva som helst ...") er betegnet med symbolet ∀ (en A bakover ).
Eksempel:
∀ x P ( x )leser
"For alle x P ( x )"og betyr
"Ethvert objekt av det aktuelle domenet har eiendommen P ".Notasjonen "∀" ble først brukt av Gerhard Gentzen i 1933 (utgitt i 1934). Det tyske ordet alle betyr "alt", det foreslår et "symbol ( Zeichen ) gyldig for alle ( für alle )" . Gentzen indikerer at han valgte som "symbol for alt" ( All-Zeichen ) den omvendte A analogt med symbolet "∃" for den eksistensielle kvantifisereren som han tar fra Russell .
Eksistensiell kvantifisering ("det eksisterer en ..." i betydningen "det er minst en ...") er notert med tegnet ∃ (en returnert E). Mer presist,
∃ x P ( x )midler
det eksisterer minst en x slik at P ( x ) (minst ett objekt av det betraktede domenet har egenskapen P )For å uttrykke unikhet i tillegg til eksistensen er tegnet som brukes ∃! (den eksistensielle kvantifiseringen etterfulgt av et utropstegn), mer presist,
∃! x P ( x )midler
det eksisterer en unik x slik at P ( x ), ellers eksisterer det en og bare en x slik at P ( x ) (et objekt av nøyaktig det domene som er vurdert har egenskapen P ).Denne siste kvantifisereren er definert ved å beregne egalitære predikater fra de to foregående tallene (og fra likhet), for eksempel ved
∃! x P ( x ) ≡ ∃ x [ P ( x ) og ∀ y ( P ( y ) ⇒ y = x )].
Notasjonen ∃ ble først brukt av Giuseppe Peano i 1897 i bind II av hans matematikkform med en annen syntaks, og tegnet var direkte knyttet til predikatet (∃ P for vår ∃ x P ( x )). Bertrand Russell er den første som bruker den på dagens måte, som en koblingsoperatør.
Negasjonen av er:
Eller: .Negasjonen av er:
, eller: i klassisk logikk , men ikke i intuisjonistisk logikk .For en formel som er formatert på forhånd , er rekkefølgen på kvantifiseringsmidlene mellom hver blokk med identiske kvantifiserere (derfor blokk med eksistensielle kvantifiseringsmidler eller blokk med universelle kvantifiseringsmidler) irrelevant, formelen forblir den samme. På den annen side gir vekslingen av blokkene til eksistensielle eller universelle kvantifiserere veldig tydelige formler hvis logiske kompleksitet blir observert spesielt i det aritmetiske hierarkiet .
I naturlig deduksjon , Gerhard Gentzen presenterer de to quantifiers som følger:
Innledende regler | Avhendingsregler | |
---|---|---|
for alt | . | |
det finnes |
Hvis vi tar en gruppe svarte katter, kan vi si at uansett hvilken katt vi velger fra denne gruppen, vil den være svart. ( )
Hvis det i en gruppe svarte katter er noen få hvite katter (eller bare en), kan vi si at det er en (eller bare en) hvit katt i denne gruppen.
( )
Symbol | Unicode | Html | Latex | |
---|---|---|---|---|
for alt | ∀ | U + 2200 | & for alle; | \ for alle |
det finnes | ∃ | U + 2203 | &eksistere; | \ eksisterer |
Utskriften av reglene som regulerer de vanlige kvantifiseringsmidlene der eksisterer, og hva som helst som finnes i alle lærebøkene til predikatberegning , en bibliografi som finnes på matematisk logikk .
For en generalisering av disse kvantifisererne kan vi henvende oss til: