p É < q É p. [p É < f É f] É p. р É [f É f] É р.. s É [p É q] É < s É p É < s É q. [s É < p É q] É < s É p &Eac

p É < q É p

в качестве сокращения для +102 и выражение

[p É < f É f] É p

в качестве другого возможного сокращения пп-формулы, для которой мы выше указали сокращение

р É [f É f] É р.

Соглашение о больших точках можно использовать совместно с предыдущим, а именно соглашением о группировке влево, действующим в тех случаях, когда опущенная левая скобка не заменена, большой точкой. Так, вместо +l03 мы можем использовать каждое из следующих двух возможных сокращений:

s É [p É q] É < s É p É < s É q

[s É < p É q] É < s É p É < s É q

== (конец правки до §12) ==

12. Теоремы исчисления P1.

В качестве первого примера теоремы исчисления P₁ мы докажем +120. р É р . [Закон рефлексивности (материальной) импликации. ]

Читатель, который помнит главную интерпретацию системы P₁ данную в § 10, возможно, сочтет предложенную теорему не только очевидной, но даже более очевидной, чем любая из аксиом. Это верно, но это не делает доказательство теоремы излишним, так как мы хотим удостовериться не просто в истинности предложенной теоремы, а в том, что она следует из наших аксиом по нашим правилам; и не просто в том, что она верна в одной интерпретации, а в том, что она верна во всех правильных интерпретациях.

Доказательством теоремы +120 является следующая последовательность девяти формул:

s É [p É q] É < s É p É < s É q

s É [r É q] É < s É r É < s É q

s É [r É p] É < s É r É < s É p

p É [r É p] É < p É r É < p É p

⇐ Предыдущая 1 2 3 456 7 8 Следующая ⇒