Q0 (математическая логика)

---

Q ₀ — это формулировка простого лямбда-исчисления , предложенная Питером Эндрюсом и обеспечивающая основу для математики, сравнимую с логикой первого порядка и теорией множеств. Это форма логики высшего порядка, тесно связанная с логикой семейства средств доказательства теорем HOL .

Системы доказательства теорем TPS и ETPS основаны на Q ₀ . В августе 2009 года TPS выиграла первое в истории соревнование среди систем доказательства теорем более высокого порядка. ^[1]

${\ Displaystyle (1)}$  ${\ displaystyle g_ {oo} T \ land g_ {oo} F = \ forall x_ {o} \ centerdot g_ {oo} x_ {o}}$

${\ Displaystyle (2 ^ {\ альфа})}$  ${\ displaystyle [x _ {\ alpha} = y _ {\ alpha}] \ supset \ centerdot \, h_ {o \ alpha} x _ {\ alpha} = h_ {o \ alpha} y _ {\ alpha}}$

${\ Displaystyle (3 ^ {\ альфа \ бета})}$  ${\ displaystyle f _ {\ alpha \ beta} = g _ {\ alpha \ beta} = \ forall x _ {\ beta} \ centerdot f _ {\ alpha \ beta} x _ {\ beta} = g _ {\ alpha \ beta} x_ { \бета}}$

${\ Displaystyle (4)}$  ${\ displaystyle [\ lambda \ mathbf {x _ {\ alpha}} \ mathbf {B} _ {\ beta}] \ mathbf {A} _ {\ alpha} = \ mathbf {S} _ {A _ {\ alpha}} ^ {\ mathbf {х} _ {\ альфа}} \ mathbf {B} _ {\ бета}}$

---