Rhesymeg osodiadol

Oddi ar Wicipedia
Neidio i: llywio, chwilio

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[golygu]

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\!.
\Omega = \Omega_0 \cup \Omega_1 \cup \ldots \cup \Omega_j \cup \ldots \cup \Omega_m \,.
Yn y dosranniad 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-destyn.
  • Gan ddibynnu ar y cystrawen a defnyddir, gall fod symbolau ychwanegol, cystrawennol, megis "(", a ")", yn angenrheidiol i gwblhau fformwlâu.

Diffinir 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 \Alpha\! yn frawddeg o \mathcal{L}.
  2. Cam (i). Os y mae p yn frawddeg, yna mae ¬p yn frawddeg.
  3. Cam (ii). Os y mae p a q yn frawddegau, yna mae (p \land q), (pq), (pq), a (pq) yn frawddegau.
  4. 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 cychwynol a gelwir yn wirebau pan mae cymhwysiad rhesymegol iddynt.

Enghraifft allweddol. System gyda gwirebau syml[golygu]

Gadewch i \mathcal{L}_1 = \mathcal{L}\ (\Alpha,\ \Omega,\ \Zeta,\ \Iota), lle diffinir \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 â" (↔) 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 dosranniad 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 (pq), didwyther q. Yna, diffinir ab yn ¬ab, ac ab yn ¬(a → ¬b).

Mae'r erthygl hon yn cynnwys term neu dermau sydd efallai wedi eu bathu'n newydd sbon: ol-der, fformwla-iawn-ffurfedig o'r Saesneg "arity, well-formed-formula". Gallwch helpu trwy safoni'r termau.