Forgóajtó (szimbólum)

Forgóajtó
⊢
◄ ⊞ ⊟ ⊠ ⊡ ⊢ ⊣ ⊤ ⊥ ⊦ ►
Jellemzők
Név jobb tapadás
Unicode U+22A2
HTML kód ⊢ vagy ⊢
UTF-16 0x22A2
URL kód %E2%8A%A2
Mnemonika ⊢
⊢

Forgóajtó  – A matematikai logikában és a számítástechnikában a szimbólumot "forgókapunak" nevezik, mert felülről nézve hasonlít egy tipikus forgókapuhoz . „Tee”-nek is nevezik, és gyakran „ad”, „bizonyít”, „kielégít” vagy „következ”.

A TeX -ben a forgóajtó szimbólum a \vdash parancsból származik . A Unicode -ban a forgóajtó karakterét ( \vdash ) "jobb gombnak" hívják, és az U+22A2 [1] kódhelyen van . Az U+22A6 kódpozíciót érvényesítési jelnek ( \vdash ) hívják. Írógépen a forgóajtó állhat egy függőleges sávból (|) és egy kötőjelből (-). A LaTeX -nek van egy turnstile csomagja, amely sok esetben előállítja ezt a karaktert, és képes az alatta vagy felette lévő karaktereket a megfelelő helyekre elhelyezni. [2]

Jelentése

A forgókapu bináris reláció . Az értelmezése különböző kontextusokban eltérő:

:

olvasható: "Tudom, hogy A igaz".

Ugyanebben a szellemben egy feltételes kijelentés :

így olvasható:

" P -től tudom, hogy Q " azt jelenti, hogy Q a rendszerben P - ből származtatható . A származtatásra való felhasználása szerint, amelyet egy kifejezés követ, anélkül, hogy bármit megelõzne, tételt jelöl, vagyis a kifejezés az üres axiómahalmaz segítségével levezethetõ a szabályokból . Mint ilyen, a kifejezés azt jelenti, hogy Q egy tétel a rendszerben. azt jelenti, hogy S bizonyítható T -ből . [5] Ezt a használatot a propozíciós logikáról szóló cikk mutatja be . A bizonyíthatóság szintaktikai következményét szembe kell állítani a kettős forgókapu szimbólummal jelölt szemantikai következménnyel . Azt mondja, hogy ez a , vagy szemantikai következménye , amikor minden lehetséges kiértékelés igaz is . A propozíciós logika esetében kimutatható, hogy a szemantikai következmény és a származtathatóság ekvivalensek egymással. Vagyis a propozíciós logika egészséges ( implikál ) és teljes ( implikál ). [6]

a G funktorral . [9] Ritkább esetekben a forgókapu ( ), mint a -ban , arra szolgál, hogy jelezze, hogy a G funktor közvetlenül szomszédos az F funktorral . [tíz]

  • Az APL -ben a szimbólumot "right tack"-nek hívják, és az ambivalens jobb identitásfüggvényt jelenti, ahol és , és vannak . A fordított szimbólumot "bal tapadásnak" nevezik, és hasonló bal oldali azonosságot jelent, ahol  van és  van . [11] [12]
  • A kombinatorikában azt jelenti, hogy ez a szám partíciója . [13]
  • A Hewlett-Packard HP-41C és HP-42S sorozatú számológépeiben a FOCAL karakterkészletben található karaktert (a 127-es kódpontban ) "Add Character"-nek hívják, és azt jelzik, hogy a A következő karakterek hozzáadódnak az alfa-regiszterhez, nem pedig a regiszter meglévő tartalmát. Ezt a karaktert (a 148-as kódponton) a HP Roman betűtípus egy módosított változata is támogatja, amelyet más HP számológépekben használnak.
  • A Casio fx-92 College 2D és fx-92+ Speciale College sorozatú számológépeiben [14] a szimbólum a modulus operátort jelenti ; a bemenet megjelenik , ahol Q a hányados és R a maradék . Más CASIO számológépekben (például a belga változatokban - az fx-92B Speciale College és az fx-92B College 2D számológépekben [15] - ahol a decimális elválasztót vessző helyett pont jelöli) a modulo operátort a következővel jelölik .

Lásd még

Jegyzetek

  1. ↑ Unicode szabvány . Letöltve: 2021. május 16. Az eredetiből archiválva : 2011. május 13.
  2. ↑ CTAN Átfogó TEX Archívum Hálózat, Directory - macros/latex/contrib/turnstile . Letöltve: 2021. május 16. Az eredetiből archiválva : 2021. május 17.
  3. ↑ Martin-Lof, 1996 , pp. 6, 15
  4. ↑ 6. fejezet, Formális nyelvelmélet . Letöltve: 2021. május 16. Az eredetiből archiválva : 2018. április 4..
  5. ↑ Troelstra és Schwichtenberg, 2000
  6. ↑ Dirk van Dalen, Logika és struktúra (1980), Springer, ISBN 3-540-20879-8 . Lásd az 1. fejezet 1.5. szakaszát.
  7. ↑ Peter Selinger, Lecture Notes on the Lambda Calculus . Letöltve: 2021. május 16. Az eredetiből archiválva : 2021. május 6..
  8. ↑ Schmidt, 1994
  9. ↑ Adjungint Funktor az nLab-ban . Letöltve: 2021. május 16. Az eredetiből archiválva : 2021. május 13.
  10. ↑ FunctorFact. Functor Fact a Twitteren . [tweet] . Twitter (2016. július 5. )
  11. ↑ Iverson, APL szótár . Letöltve: 2021. május 16. Az eredetiből archiválva : 2020. április 25.
  12. ↑ Iverson, 1987
  13. ↑ Stanley, Richard P. Enumeratív kombinatorika. — 1. - Cambridge: Cambridge University Press, 1999. - Vol. Vol. 2. - 287. o.
  14. ↑ fx-92 Speciale College Mode d'emploi . - CASIO COMPUTER CO., LTD., 2015. - P. 12. Archiválva : 2021. április 16. a Wayback Machine -nél
  15. ↑ Fennmaradó számítások - Casio fx-92B felhasználói kézikönyv [13. oldal | ManualsLib] . www.manualslib.com . Letöltve: 2020. december 24. Az eredetiből archiválva : 2021. május 16.

Linkek