Q0 (математикалық логика) - Q0 (mathematical logic)

Q0 болып табылады Питер Эндрюс 'тұжырымдамасы жай терілген лямбда калькулясы, және математиканың негізін бірінші ретті логика мен жиын теориясымен салыстыруға болады, бұл формасы жоғары ретті логика логикасымен тығыз байланысты HOL теоремасын дәлелдеуші отбасы.

Теорема дәлелдейтін жүйелер TPS және ETPS Q-ға негізделген0. 2009 жылдың тамызында TPS жоғары деңгейлі теореманы дәлелдейтін жүйелер арасындағы бірінші байқауда жеңіске жетті.[1]

Q аксиомалары0

Жүйеде бес аксиома бар, оларды келесідей айтуға болады:

  

  

  

  

  ℩

(2, 3 және 4 аксиомалар - аксиома схемалары - ұқсас аксиомалардың тектілері. Аксиома 2 және Аксиома 3 индикаторлары тек айнымалылар мен тұрақтылар типтеріне байланысты өзгереді, бірақ Аксиома 4 жағдайлары кез-келген өрнекті алмастыра алады. A және B.)

Жазылды «o«бұл логикалық мәндердің типтік белгісі және жазылған»мен«- бұл жеке (бульдік емес) мәндердің типтік белгісі. Бұлардың реттілігі функциялардың түрлерін білдіреді және әртүрлі функционалдық типтерді ажыратуға арналған жақшаларды қамтуы мүмкін. Жазбаша грек әріптері, мысалы, α және β - типтік таңбалардың синтаксистік айнымалылары. Қалың бас әріптер A, B, және C сияқты WFF үшін синтаксистік айнымалылар және жуан кіші әріптер х, ж айнымалыларға арналған синтаксистік айнымалылар.S барлық еркін көріністерде синтаксистік алмастыруды көрсетеді.

Тек қарабайыр тұрақтылар Q((oα) α), әр түрдегі мүшелердің теңдігін білдіретін α, және (мен (ой))жеке тұлғаларға арналған сипаттама операторын белгілейтін жиынтықтың бірегей элементі, нақты бір адамды қамтиды. symbols таңбалары және жақшалар («[» және «]) - тілдің синтаксисі. Барлық басқа белгілер - олардың құрамына кіретін терминдердің қысқартулары, оның ішінде кванторлар ∀ және ∃.

Аксиомада 4, х тегін болуы керек A жылы B, дегеніміз, ауыстыру еркін айнымалылардың кез-келген көрінісін тудырмайды A ауыстыру нәтижесімен байланысты болу.

Аксиомалар туралы

  • Аксиома 1 деген ойды білдіреді Т және F тек логикалық мәндер болып табылады.
  • Аксиома схемалары 2α және 3αβ функциялардың іргелі қасиеттерін білдіру.
  • Аксиома схемасы 4 λ жазудың табиғатын анықтайды.
  • Аксиома 5 таңдау операторы - бұл жеке адамдарға теңдік функциясына кері деп айтады. (Бір дәлел келтірілген, Q жеке тұлғаны қамтитын жиынтыққа / предикатқа карталар. Жылы Q0, x = y деген аббревиатура болып табылады Qxy, бұл деген аббревиатура болып табылады (Qx) y.)

Жылы Эндрюс 2002, Аксиома 4 ауыстыру процесін бұзатын бес бөлімде жасалған. Мұнда келтірілген аксиома альтернатива ретінде талқыланады және кіші бөліктерден дәлелденеді.

Q-тегі қорытынды0

Q0 қорытынды жасаудың бірыңғай ережесі бар.

Сызғыш. Қайдан C және Aα = Bα бір жағдайды ауыстыру нәтижесін шығару Aα жылы C пайда болуымен Bα, болған жағдайда Aα жылы Cемес (айнымалының пайда болуы) алдында бірден λ.

Қорытынды ережесі R ′ гипотезалар жиынтығынан ой қорытуға мүмкіндік береді H.

Сызғыш'. Егер HAα = Bα,және HC, және Д. алынған Cбір пайда болуын ауыстыру арқылы Aα пайда болуымен Bα, содан кейінHД., егер:

  • Пайда болуы Aα жылы C бірден айнымалының пайда болуы емес λ, және
  • еркін айнымалы жоқ Aα = Bα және мүшесі H байланысты C ауыстырылған кезде Aα.

Ескерту: ауыстыруға шектеу Aα арқылыBα жылы C гипотезада және кез-келген ауыспалылықтың болмауын қамтамасыз етеді Aα = Bαауыстыру аяқталғаннан кейін екеуінде де бірдей мәнге ие бола алады.

Q үшін шегерім теоремасы0 R′ ережесін қолданатын гипотезалардағы дәлелдемелер гипотезасыз және R ережесін қолдана отырып дәлелдеуге болатындығын көрсетеді.

Кейбір ұқсас жүйелерден айырмашылығы Q0 WFF-мен кез-келген тереңдіктегі субэкспрессияны тең өрнекпен ауыстырады. Мысалы, аксиомалар келтірілген:

1. ∃x Px
2. Px ⊃ Qx

және бұл A ⊃ B ≡ (A ≡ A ∧ B), біз санды алып тастамай-ақ жалғастыра аламыз:

3. Px ≡ (Px ∧ Qx) А және В-ға нұсқау
4. ∃x (Px ∧ Qx) 3-жолды пайдаланып 1-жолға ауыстыру ережесі R.

Ескертулер

Әдебиеттер тізімі

  • Эндрюс, Питер Б. (2002). Математикалық логикаға және түр теориясына кіріспе: дәлелдеу арқылы шындыққа (2-ші басылым). Дордрехт, Нидерланды: Kluwer Academic Publishers. ISBN  1-4020-0763-9. Сондай-ақ қараңыз [1]
  • Шіркеу, Алонзо (1940). «Түрлердің қарапайым теориясының тұжырымдамасы» (PDF). Символикалық логика журналы. 5: 56–58. дои:10.2307/2266170.

Әрі қарай оқу