1673068206

8.2 Teoria Dowodu

Przyjmujemy sobie pewne zdania za prawdziwe, oraz mamy pewne reguły wyprowadzania nowych zdań. Każdy sobie może taki system wyprowadzania wymyślić¹:

1. Aksjomaty (które są tak naprawdę kombinatorami)

r H (a ->■ 0 —► 7) -»• (a —*• /?) -> (a -► 7)

Ti-c* F a 0

2. reguły wnioskowania:

itp...

mówimy:

\= p - p jest prawdziwa 1- p - p jest dowodliwa

Ustalamy sobie konkretny model i staramy się sprawdzić co jest prawdziwe w tym modelu.

Jeśli coś udowodnię to to jest prawdziwe. Ale jest cała masa rzeczy prawdziwych, których nie mogę udowodnić. Zawsze prawd jest więcej niż to co jesteśmy w stanie wywnioskować w samym systemie.

8.3 Mały wstęp do składni

1. Świat naszych instrukcji wygląda tak:

c "= skip | X := e | if b then ci else C2 | if b then c \ while b do c \ ci; C2

e ::= n | X | e\ ® e2 © ::= + | - | x | div | mod b ■■■■= e\ © e2 | ->b \ 6j a b₂ | h v b₂

10

1

np. formalizacja „Hilbertowska” w whitebooku...