Porównanie arytmetyki Heytinga i arytmetyki Peano pierwszego rzędu

Obie arytmetyki definiują liczby naturalne wraz z dodawaniem, mnożeniem i zasadą indukcji, różniąc się jedynie systemem logicznym (dla arytmetyki Heytinga jest to logika intuicjonistyczna, a dla arytmetyki Peano - logika klasyczna).

Celem zadania jest formalizacja obu arytmetyk i udowodnienie kilku związków między nimi.

Dane są symbole funkcyjne:

O - arności zero,
S - arności jeden,
*, + - arności dwa.

oraz jeden dwuargumentowy symbol relacyjny =.

Następnie dane są aksjomaty Peano, schemat rekursji i intuicjonistyczne reguły dowodzenia.

Te wszystkie ingrediencje tworzą arytmetykę Heytinga. Aby otrzymać arytmetykę Peano należy dolożyć jeszcze aksjomat wyłączonego środka.

Państwa zadaniem będzie:

formalizacja formuł pierwszego rzędu nad podaną syganturą, używając indeksów de Bruijna do reprezentowania zmiennych.
formalizacja obu arytmetyk, jako system reguł dowodzenia sparametryzowany zbiorem aksjomatów
zdefiniowanie transformacji Friedmana P |Ž P^A
udowodnienie, że dla dowolnej formuły A zachodzi G |-_P P implikuje G^A |-_H P^A.
zakładając, że dla dowolnej formuły A i dowolnej formuły P bez kwantyfikatorów zachodzi |-_H P^A ÜŢ P Ú A, pokazać, że każda formuła S₀¹ (czyli postaci $ x. F(x), gdzie F jest bez kwantyfikatorów) jest dowodliwa w arytmetyce Heytinga wtedy i tylko wtedy gdy jest dowodliwa w arytmetyce Peano.

Poniżej dołączony jest spis reguł naturalnej dedukcji pierwszego rzędu oraz definicja translacji Friedmana.

Reguły naturalnej dedukcji pierwszego rzędu

Sekwenty są postaci G |- A, gdzie G to multizbiór formuł, a A to formuła. Oprócz początkowych reguł Assume i Weak mamy wyłącznie reguły wprowadzania i eliminacji dla poszczególnych operatorów. Reguły wprowadzania mówią jak udowodnić formułę o danym operatorze głównym, a reguły eliminacji -- jak użyć w dowodzie takiej formuły.

G, A |- A

(Assume)

G |- A

G, B |- A

(Assume)

G, A |- B

G |- A Ž B

(Imp-I)

G |- A Ž B G |- A

G |- B

(Imp-E)

G |- A G |- B

G |- A Ů B

(And-I)

G |- A Ů B

G |- A

(And-E-L)

G |- A Ů B

G |- B

(And-E-R)

G |- A

G |- A Ú B

(Or-I-L)

G |- B

G |- A Ú B

(Or-I-R)

G |- A Ú B G, A |- C G, B |- C

G |- C

(Or-E)

G |- ^

G |- A

(False-E)

G |- A x ĎG

G |- " x.A

(Forall-I)

G |- " x.A

G |- A[x \ t]

(Forall-E)

G |- A[x \ t]

G |- $ x.A

(Exists-I)

G |- $ x.A G, A |- B x ĎG,B

G |- B

(Exists-E)

Tłumaczenie Friedmana

Niech A będzie formułą arytmetyki. Przez Ź^A P oznaczamy formułę P Ž A. Dla każdej formuły arytmetyki P definiujemy tłumaczenie P^A w następujący sposób:

^^A	ş	^ Ú A
(t₁=t₂)^A	ş	t₁=t₂ Ú A
(P₁ Ů P₂)^A	ş	Ź^A Ź^A (P₁^A) Ů Ź^A Ź^A (P₂^A)
(P₁ Ú P₂)^A	ş	Ź^A Ź^A (P₁^A) Ú Ź^A Ź^A (P₂^A)
(P₁ Ž P₂)^A	ş	Ź^A Ź^A (P₁^A) Ž Ź^A Ź^A (P₂^A)
(" x.P)^A	ş	Ź^A Ź^A " x.(P^A)
($ x.P)^A	ş	Ź^A Ź^A $ x.(P^A)

Jacek Chrząszcz, 11 kwietnia 2002 ostatnia zmiana: April 18, 2002

This document was translated from L^AT_EX by H^EV^EA.