Funktory jednoargumentowe (indeks: z / z)

1) Funktor negacji ∼: nie; nieprawda, że; nie jest tak, że

p	∼ p
1	0
0	1

Funktor podwójnej negacji ∼∼: nieprawda, że nie

p	∼∼ p
1	1
0	0

∼∼ p ≡ p

2) Funktor asercji as: jest tak, że; zaiste

p	as(p)
1	1
0	0

Funktor asercji jest równoważny funktorowi podwójnej negacji: as(p) ≡ ∼∼ p

3) Funktor verum vr: jest prawdą, że („uprawdziwiacz”)

p	vr(p)
1	1
0	1

Funktor tworzy zdanie zawsze prawdziwe (tautologiczne); vr(p) ≡ p → p

4) Funktor falsum fl­: jest nieprawdą, że („falsyfikator”)

p	fl(p)
1	0
0	0

Funktor tworzy zdanie zawsze fałszywe (kontrtautologiczne); fl(p) ≡ ∼ (p → p)

fl(p) ≡ ∼ vr(p); vr(p) ≡ ∼ fl(p)

Zestawienie funktorów jednoargumentowych

p	s(p)	∼ p	vr (p	fl(p)
1	1	0	1	0
0	0	1	1	0

Na dowód założeniowy w systemie założeniowym składają się kolejno przeprowadzone rozumowania - kroki dowodowe. Oddziela się je od siebie i podaje jako kolejne, ponumerowane wiersze kolumny tworzącej zapis dowodu. Pierwsze wiersze dowodu tworzą wszystkie wypisane kolejno założenia dowodzonego twierdzenia, którymi są jego poprzedniki (patrz niżej, przykład dowodu założeniowego). Jeżeli dowód jest założeniowym dowodem nie wprost, jako ostatnie założenie dowodu zapisujemy założenie które jest sprzeczne z następnikiem dowodzonego twierdzenia. Kolejnymi wierszami dowodu są wiersze powstałe w oparciu o wyżej wymienione reguły pierwotne lub twierdzenia już wcześniej udowodnione. Po prawej stronie każdego nowo dołączonego wiersza wypisujemy jego podstawę dowodową, tj. te reguły pierwotne (podajemy ich skróty) lub udowodnione twierdzenia, oraz te wcześniejsze wiersze dowodu (podajemy tylko ich numery) w oparciu o które został on wyprowadzony. Jeżeli dowód jest dowodem wprost, to jest on zakończony gdy w kolejnym kroku otrzymamy następnik dowodzonego twierdzenia. Jest on ostatnim wierszem w całej procedurze. Dowód nie wprost kończy się wtedy gdy w toku dowodu dojdziemy do sprzeczności, tj. gdy otrzymamy dwa sprzeczne ze sobą wiersze.

Poniższe przykłady pokazują jak wyglądają założeniowe dowody poszczególnych tautologii rachunku i jak są one zapisywane.

1) Dowód wprost prawa sylogizmu warunkowego

Dowodzone twierdzenie: [ (p _> q) ∧ (q _> r) ] _> (p _> r)

Poprzedniki twierdzenia: (p _> q) ∧ (q _> r), p

Następnik dowodzonego twierdzenia: r

Numer kolejnego wiersza dowodu	Wiersz dowodu	Racja przyjęcia danego wiersza
1.	(p _> q) ∧ (q _> r)	założenie - poprzednik twierdzenia
2.	p	założenie - poprzednik twierdzenia
3.	p _> q	OK: 1
4.	q _> r	OK: 1
5.	q	RO: 3, 2
6	r - quod erat demonstrandum (q.e.d.)	RO: 4, 5

2) Dowód nie wprost prawa transpozycji prostej

Dowodzone twierdzenie: (p _> q) _> (∼ q _> ∼ p)

Dowód

1. p _> q założenie (zał.) - poprzednik twierdzenia

2. ∼ q zał., poprzednik twierdzenia

3. p założenie dowodu nie wprost (z. d. n.)

4. q RO: 1,3

5. sprzeczność między wierszami 2 i 4.

3) Dowód nie wprost prawa transpozycji złożonej

Dowodzone twierdzenie: (r ∧ p _> q) _> [(r ∧ ∼ q) _> ∼ p)]

Dowód

1. r ∧ p _> q zał., poprzednik

2. r ∧ ∼ q zał., poprzednik

3. p z. d. n.

4. r OK: 2

5. ∼ q OK: 2

6. r ∧ p DK: 4,3

7. q RO: 1,6

8. sprzeczność między 7 i 5.

---