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.

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}\ (\Alpha,\ \Omega,\ \Zeta,\ \Iota), yw **rhesymeg osodiadol**, gyda'i fformwlâu wedi eu llunio fel a ganlyn:

* Mae'r *set alffa*, \Alpha\!, 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 \Alpha\!.
* 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:

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

* Mae'r *set zeta,* \Zeta\!, yn set feidraidd o *reolau trawsffurfio* a gelwir yn  *rheolau didwythiad* pan mae cymhwysiad rhesymegol iddynt.
* Mae'r *set iota,* \Iota\!, 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}\ (\Alpha,\ \Omega,\ \Zeta,\ \Iota), lle diffinnir \Alpha,\ \Omega,\ \Zeta,\ \Iota fel a ganlyn:

* Mae'r set \Alpha \! digon fawr i fodloni anghenion y drafodaeth:

::: \Alpha = \{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 â" (&harr;) 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*).

Categori:Rhesymeg
Categori:Sylfeini mathemateg