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
Mathlogical system Edit this on Wikidata
Rhan orhesymeg, rhesymeg mathemateg Edit this on Wikidata
Tudalen Comin 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 golygu

System ffurfiol,  , yw rhesymeg osodiadol, gyda'i fformwlâu wedi eu llunio fel a ganlyn:

  • Mae'r set alffa,  , yn set feidraidd o elfennau a gelwir yn neu'n newidynnau gosodiadol. O safbwynt cystrawennol, rhain yw elfennau mwyaf sylfaenol yr iaith ffurfiol  , 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  .
  • Set feidraidd o elfennau a gelwir yn symbolau gweithredyddion yw'r set omega,  . Dosrennir   yn is-setiau cyd-anghynwysol fel a ganlyn:
 
Yn y dosraniad hwn,   yw'r set o symbolau gweithredyddion gydag ol-der  .
Mewn rhai rhesymegau gosodiadol cyffredin, dosrennir   fel a ganlyn:
 
 
Yn aml, caiff gwerth rhesymegol ei drin fel gweithredydd ag ol-der sero, felly:
 
Defnyddia rai awduron (~) yn lle (¬), a defnyddia rai (&) yn lle ( ). Amrywia nodiant yn fwy fyth o ran y set o werthoedd rhesymegol, gyda symbolau megis {gwir, an-wir}, {F, T}, {0, 1}, ac { ,  } 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)   (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   yn frawddeg o  .
  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   q), (pq), (pq), a (pq) yn frawddegau.
  4. Cau. Does dim byd arall yn frawddeg.
  • Mae'r set zeta,  , yn set feidraidd o reolau trawsffurfio a gelwir yn rheolau didwythiad pan mae cymhwysiad rhesymegol iddynt.
  • Mae'r set iota,  , yn set feidraidd o bwyntiau cychwynnol a gelwir yn wirebau pan mae cymhwysiad rhesymegol iddynt.

Enghraifft allweddol. System gyda gwirebau syml golygu

Gadewch i  , lle diffinnir   fel a ganlyn:

  • Mae'r set   digon fawr i fodloni anghenion y drafodaeth:
 

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  :

 
 

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:

  •  
  •  
  •  

Modus ponens yw'r rheol didwytho, hynny yw, o p a (pq), didwyther q. Yna, diffinnir 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.