Dyskusja:Aksjomat klasycznego rachunku predykatów

Z Wikipedii

[edytuj] Czy to nie powinno być zintegrowane?

Czy to hasło nie powinno być zintegrowane jakoś z Rachunek predykatów pierwszego rzędu? Wiem, "zrób to sam", ale w tym przypadku nie za bardzo wyobrażam sobie jaka była intencja w tworzeniu tutejszego hasła jako osobnego bytu. Może tu chodziłoby o przedyskutowanie/wylistowanie różnych opisów "aksjomatów logicznych LPR"? Sugestie???? Stotr 08:17, 23 paź 2007 (CEST)

Ja też nie rozumiem o co chodzi w tym artykule; nie ma początku ani końca. Byłoby dobre, jeśli mamy listę (z wyjaśnieniami) różnych układów aksjomatycznych, tzn aksjomatów i reguł.

Mamy

• układy w stylu Hilberta/Łukasiewicza: kilka aksjomatów, tylko jedna reguła - modus ponens (być może też generalizacja, tak jak w tym artykule). Dowody są ciągami formuł.
• układy w stylu Gentzena: dwie reguły dla każdego spójnika, a jako aksjomaty tylko A→A. Dowody są drzewami formuł.

(Teoria dowodu kocha te układy, bo mają taką własność, że po cut-elimination każda formuła w dowodzie musi być podformułą udowodnionej formuły. O ile wiem, matematycy poza teorią dowodu nie lubią takiego układów.)

• Dedukcja naturalna Jaśkowskiego: stosunkowe bliska do "zwyklej matematyki" -- można wprowadzić dowolne przypuszczenia (?assumptions) w dowód, tyklo trzeba je eliminować później w ciągu dowodu. Dowody są -- hm, nie wiem dokładnie -- ciągami formuł z znakowaniami.
• Dowody na bazie rezolucji, czyli skolemizacji i twierdzenia Herbranda. Bardzo dobry dla komputerami. Nic nie można udowodnić w takich wkładach, tylko obalić. Dowody są ciągami klausul.
• Chyba też inne. Ile książek o logice, tyle aksjomatyzacji...

Alef 01:28, 11 lis 2007 (CET)

Alef, Ty wyraźnie znasz tematykę, ja znam (trochę) język polski. Zacznij może to hasło przerabiać a ja Ci bedę pomagał/przeszkadzał :-). Co? Bo to co Ty proponujesz aby tu mieć wydaje się bardzo dobrym planem. Tylko że tytuł hasła powininen być inny... Może coś w rodzaju Aksjomatyki logik pierwszego rzędu? Stotr 01:58, 11 lis 2007 (CET)