Lohika ng unang orden

Ang lohikang pang-unang orden ay isang sistemang pormal na ginagamit sa matematika, linggwistika, pilosopiya at agham pangkompyuter. Ito ay kilala rin bilang predikadong kalkulus na unang order, ang mas mababang predikadong kalkulus, teoriyang kwantipikasyon at lohikang predikado(isang mas hindi tumpak na termino). Ang lohikang unang order ay itinatangi mula sa lohikang proposisyonal sa paggamit nito ng mga may bilang na variable.

Ang isang teoriya tungkol sa isang paksa ay karaniwang lohikang unang order kasama ng: isang tinukoy na sakop ng diskurso na sumasaklaw sa mga may bilang na variable, may hangganang maraming mga punsiyon na nagmamapa mula sa sakop tungo dito, may hangganang maraming mga predikado na inilarawan sa sakop na ito at isang rekursibong hanay ng mga aksiyom na pinaniniwalaang totoo para sa mga bagay na ito. Minsan, ang teoriya ay nauunawaan sa isang mas pormal na kahulugan na isang hanay lamang ng mga pangungusap sa lohikang unang order. Ang pang-uring "unang-order" ay nagtatangi ng lohikang unang order mula sa lohikang mas mataas na order kung saan ay may mga predikadong mayroong mga predikado o mga punsiyon bilang mga argumento o kung saan ang isa o parehong mga predikadong nagkakwantipika o mga nagkakakwantipikang punsiyon ay pinapayagan. Sa mga teoriyang unang order, ang mga predikado ay kadalasang nauugnay sa mga hanay. Sa pinakahulugang mga teoriyang mas mataas na order, ang mga predikado ay maaaring pakahulugan bilang mga hanay ng mga hanay. Maraming mga sistemang deduktibo para sa lohikang unang order na matunog(ang lahat ng mga mapapatunayang pangungusap ay mapapatunayan). Bagaman ang relasyong kalalabasang lohikal ay isa lamang kalahating mapagpapasyahan, ang labis na pagsulong ay nagawa sa automadong pagpapatunay ng teorema sa lohikang unang order. Ang lohikang unang order ay sumasapat rin sa ilan gmga teoremang metalohikal na gumagawa ritong bukas sa pagsisiyasat sa teoriya ng patunay gaya ng teoremang Löwenheim–Skolem at teorema ng pagiging siksik. Ang lohikang unang order ay may malaking kahalagahan sa mga pundasyon ng matematika dahil ito ang pamantayang lohikang pormal para sa mga sistemang aksiyomatiko. Maraming mga karaniwang sistemang aksiyomatiko gaya ng unang order na aritmetikang Peano at teoriyang aksiomatikong hanay kabilang ang kanonikal na teoriyang hanay na Zermelo–Fraenkel (ZF) ay mapopormalisa bilang mga teoriyang unang order. Gayunpaman, walang teoriyang unang order ang may kalakasan na maliwaran ng bouo at kategorikal ang mga istrukturang may walang hanggang sakop gaya ng mga natural na bilang o linyang real. Ang mga sistemang aksiyomang kategorikal para sa mga istrukturang ito ay makakamit sa mga mas malakas na lohika gaya ng lohikang ikalawang order.

Ang lohika ng unang orden ay pumapayag sa pangangatwiran tungkol sa mga katangian na pinagsasaluhan ng maraming mga bagay sa pamamagitan ng mga variable. Halimbawa, ang pormulang

${\text{Pilosopo}}(a)\to {\text{Iskolar}}(a)\,$

ay nagsasaad na kung ang a ay isang pilosopo, kung gayon ang a ay isang iskolar. Ang simbolong $\to$ ay tumutukoy sa pahayag na kondisyonal. Ang hipotesis ay nasa kaliwa ng pana at ang konklusyon ang nasa kanan. Ang katotohanan ng pormula ay nakasalalay sa kung aling bagay ang tinutukoy ng a at sa mga interpretasyon ng Pilosopo at Iskolar. Ang mga pahayag sa anyong "para sa bawat a, kung ang a ay isang pilosopo kung gayon ang a ay isang iskolar" ay nangangailangan ng parehong paggamit ng mga variable at kwantipikador. Ang pahayag na

$\forall a({\text{Pilosopo}}(a)\to {\text{Iskolar}}(a))\,$

ay nagsasaad na anuman ang kinatawan ng a, kung ang a ay isang pilosopo, kung gayon ang a ay isang iskolar. Dito ang $\forall$ ay pangkalahatang kwantipikador. Upang ipakita na ang pahayag na "kung ang a ay isang pilosopo, kung gayon ang a ay isang iskolar" ay hindi totoo, ipapakita na may isang pilosopong hindi iskolar. Ang kontra pahayag ang eksistensiyal na kwantipikador na $\exists$:

$\exists a({\text{Pilosopo}}(a)\land \lnot {\text{Iskolar}}(a))\,.$

Dito:

• ang $\lnot$ ang operador na negasyon: ang $\lnot {\text{Iskolar}}(a)$ ay totoo kung ang a ay hindi isang iskolar.
• ang $\land$ ang operador na pagsasanib: ang ${\text{Pilosopo}}(a)\land \lnot {\text{Iskolar}}(a)$ ay nagsasaad na ang a ay isang pilosopo at hindi rin isang iskolar.

Bilang karagdagang halimbawa:

• Kung ang x ay isang sasakyang panglupain, kung gayon ito ay may mga gulong

$\forall xSasakyangLupain(x)\to MayGulong(x)$

• May umiiral na kahit isang bagay na may mga gulong at hindi kotse

$\exists xMayGulong(x)\wedge \lnot Kotse(x)$

Ang mga bawat predikadong Pilosopo(a) at Iskolar(a) ay kumukuha lamang ng isang parametro. Ang lohika ng unang orden ay makapaghahayag rin ng mga predikado na may higit sa isang parametro. Halimbawa:

• Ang lahat ng mga ina ay may isang anak

$\forall xIna(x)\to \exists yAnak(y)\wedge MayAnak(x,y)$

Ang saklaw ng mga kwantipikador ang hanay ng mga bagay na magagamit upang sapatan ang mga ito. Sa karagdagan ng pagtukoy ng kahulugan ng mga simbolong predikador, ang interpretasyon ay dapat tumukoy sa isang walang lamang hanay na kilala bilang sakop ng diskurso o uniberso bilang isang saklaw ng mga kwantipikador.