Description
Az intuicionista kiválasztási logikákban a Martin-Löf-féle kiválasztási elv term-realizáló alakja megengedhető (admissible). A tanúk nevei az epszilon termek. Felépítettünk egy típusos programozási nyelvet, és egy Curry--Howard--Lambek-megfeleltetés megadásával igazoltuk, hogy ez helyes és teljes a Lawere-féle elsőrendű hiperdoktrínák vékony verziójának egy plusz termválasztó adjungálttal való bővítményére nézve. Igazoltuk, hogy az említett kalkulus egy közbülső logika az intuicionista és a klasszikus között. Végül vázolunk egy szemantikát, amelyben sérülhet a konstruktív kiválasztási séma komputációs tartalma (azaz megjelenhet a tanúvédelem a logikában). Minden igazolt tételt a Rocq bizonyítás asszisztensben formalizáltunk és bizonyítottunk. A kódok nagy részét, szoros emberi felügyelet mellett, a Gemini és a ChatGPT generálta.