Rhesymeg osodiadol

Mewn rhesymeg a mathemateg, mae rhesymeg osodiadol (neu galcwlws gosodiadol) yn system ffurfiol lle gellir ffurfio fformwlâu sy'n cynrychioli gosodiadau trwy gyfuno gosodiadau atomaidd gan ddefnyddio cysylltion rhesymegol, a system o reolau prawf ffurfiol sy'n galluogi dangos fod fformwlâu neilltuol yn "theoremau" o fewn y system.

Rhesymeg osodiadol

Math	logical system
Rhan o	rhesymeg, rhesymeg mathemateg
Ffeiliau perthnasol ar Gomin Wicimedia

Mae'r isod yn amlinellu rhesymeg osodiadol safonol. Gellir ffurfio systemau sydd mwy neu lai'n gywerth, ond sy'n amrywio o ran (1) eu hiaith, hynny yw, eu casgliad o symbolau atomaidd a symbolau gweithredyddion, (2) eu set o wirebau, a (3) y set o reolau didwytho.

Disgrifiad cyffredinol o resymeg osodiadol

System ffurfiol, ${\mathcal {L}}={\mathcal {L}}\ (\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I} )$, yw rhesymeg osodiadol, gyda'i fformwlâu wedi eu llunio fel a ganlyn:

• Mae'r set alffa, $\mathrm {A} \!$, yn set feidraidd o elfennau a gelwir yn neu'n newidynnau gosodiadol. O safbwynt cystrawennol, rhain yw elfennau mwyaf sylfaenol yr iaith ffurfiol ${\mathcal {L}}$, ac fe'u celwir yn fformwlâu atomig yn rhinwedd hynny. Yn yr enghreifftiau a ganlyn, y llythrennau p, q, r ac yn y blaen yw elfennau $\mathrm {A} \!$.
• Set feidraidd o elfennau a gelwir yn symbolau gweithredyddion yw'r set omega, $\Omega \!$. Dosrennir $\Omega \!$ yn is-setiau cyd-anghynwysol fel a ganlyn:

$\Omega =\Omega _{0}\cup \Omega _{1}\cup \ldots \cup \Omega _{j}\cup \ldots \cup \Omega _{m}\,.$

Yn y dosraniad hwn, $\Omega _{j}\!$ yw'r set o symbolau gweithredyddion gydag ol-der $j\!$.

Mewn rhai rhesymegau gosodiadol cyffredin, dosrennir $\Omega \!$ fel a ganlyn:

$\Omega _{1}=\{\lnot \}\,,$

$\Omega _{2}\subseteq \{\land ,\lor ,\rightarrow ,\leftrightarrow \}\,.$

Yn aml, caiff gwerth rhesymegol ei drin fel gweithredydd ag ol-der sero, felly:

$\Omega _{0}=\{0,\ 1\}\,.$

Defnyddia rai awduron (~) yn lle (¬), a defnyddia rai (&) yn lle ($\land$). Amrywia nodiant yn fwy fyth o ran y set o werthoedd rhesymegol, gyda symbolau megis {gwir, an-wir}, {F, T}, {0, 1}, ac {$\bot$, $\top$} i'w gweld mewn sawl cyd-destun.

• Gan ddibynnu ar y cystrawen a defnyddir, gall fod symbolau ychwanegol, cystrawennol, megis "(", a ")", yn angenrheidiol i gwblhau fformwlâu.

Diffinnir yr iaith (ffurfiol) ${\mathcal {L}}$ (a gelwir hefyd yn set o fformwlâu, neu'n fformwlwâu-iawn-ffurfedig), yn anwythol neu'n iterus gan y rheolau canlynol:

1. Sylfaen. Mae unrhyw elfen o'r set $\mathrm {A} \!$ yn frawddeg o ${\mathcal {L}}$.
2. Cam (i). os mae p yn frawddeg, yna mae ¬p yn frawddeg.
3. Cam (ii). os mae p a q yn frawddegau, yna mae (p $\land$ q), (p ∨ q), (p → q), a (p ↔ q) yn frawddegau.
4. Cau. Does dim byd arall yn frawddeg.

• Mae'r set zeta, $\mathrm {Z} \!$, yn set feidraidd o reolau trawsffurfio a gelwir yn rheolau didwythiad pan mae cymhwysiad rhesymegol iddynt.
• Mae'r set iota, $\mathrm {I} \!$, yn set feidraidd o bwyntiau cychwynnol a gelwir yn wirebau pan mae cymhwysiad rhesymegol iddynt.

Enghraifft allweddol. System gyda gwirebau syml

Gadewch i ${\mathcal {L}}_{1}={\mathcal {L}}\ (\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I} )$, lle diffinnir $\mathrm {A} ,\ \Omega ,\ \mathrm {Z} ,\ \mathrm {I}$ fel a ganlyn:

• Mae'r set $\mathrm {A} \!$ digon fawr i fodloni anghenion y drafodaeth:

$\mathrm {A} =\{p,q,r,s,t,u\}\,.$

er enghraifft. O'r tri cysylltydd ar gyfer "ac," "neu," ac "ymhlyga," (∧, ∨, a →), gellir cymryd un fel symbol cyntefig, a diffinio'r lleill gan ei ddefnyddio ynghyd â "nacáu" (¬). (Yn wir, gellir diffinio'r cysylltyddion i gyd yn nhermau un gweithredydd. Wrth gwrs, gellir diffinio "yn unfath â" (↔) yn nhermau'r symbolau eraill, gyda a ↔ b wedi'i diffinio'n (a → b) ∧ (b → a).

Mae fabwysiadu (¬) a (→) fel dau weithredydd cyntefig y resymeg osodiadol dan sylw, yn cyfateb i gael y dosraniad canlynol o $\Omega =\Omega _{1}\cup \Omega _{2}$:

$\Omega _{1}=\{\lnot \}\,.$

$\Omega _{2}=\{\rightarrow \}\,.$

Darganfu Jan Łukasiewicz system o wirebau sy'n deillio rhesymeg osodiadol. Y gwirebau yw'r fformwlâu canlynol, gydag unrhyw fformwla dilys wedi mewnosod yn lle'r newidynnau:

• $p\to (q\to p)$

• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$

• $(\neg p\to \neg q)\to (q\to p)$

Modus ponens yw'r rheol didwytho, hynny yw, o p a (p → q), didwyther q. Yna, diffinnir a ∨ b yn ¬a → b, ac a ∧ b yn ¬(a → ¬b).