Dyskusja:Rachunek predykatów pierwszego rzędu

1. Skoro autor powołuje się na W.A.Pogorzelskiego, "Klasyczny rachunek kwantyfikatorów, zarys teorii", to dlaczego nie zaczerpnął stamtąd definicji podstawiania termu za zmienną w formule?
2. Coś jest nie tak z aksjomatyką:
   • Gdzie na przykład jest jakikolwiek aksjomat dotyczący kwantyfikatora szczegółowego?
   • Nie wydaje mi się szczęśliwym pomysł opuszczenia w formalizacji KRK reguły generalizacji: ${\frac {\alpha }{\forall _{x}\alpha }}$.
     Zasadność jej użycia wynika z codziennej praktyki matematycznej. Przecież zapisując jakąś równość (np. prawo przemienności, etc.), czy wręcz całe twierdzenie. Np. ${\textrm {nwd}}(a,n)=1\;\Rightarrow \;a^{\varphi (n)}\equiv 1({\textrm {mod}}\;n)$, zmienne wolne traktujemy jako miejsca, w które możemy wstawiać inne wartości, czyli traktujemy je jako skwantyfikowane ogólnie!. To prowadzi do konkluzji, że dla operatora konsekwencji KRK, zachodzi związek: $Cn(X\cup \{\alpha \})=Cn(X\cup \{\forall _{x}\alpha \})$, co w prostej drodze prowadzi do wyprowadzalności w/w reguły generalizacji w KRK!
3. Definicja spełniania formuły w modelu jest o wiele bardziej przejrzysta jeśli operuje się pojęciem wartościowania zmiennych indywiduowych w uniwersum modelu (por. wspomniany wyżej W.A.Pogorzelski). Szczególnie mętny jest tutaj fragment dotyczący kwantyfikatorów.
4. Trafność formalizacji jakiegokolwiek formalizmu logicznego można ocenić jedynie na podstawie jego semantyki (czyli określeniu, co oznacza, że ze zbioru formuł $X$ wynika logicznie formuła $\alpha$, ew. co oznacza, że zbiór formuł jest spełnialny) i wynikających stąd twierdzeń o pełności. Warto by te informacje tutaj uzupełnić.

--AdamKolany (dyskusja) 09:54, 31 lip 2009 (CEST)

Definicja formalna zmiennej wolnej dla termu

Przy formalnej definicji zmiennej wolnej dla termu w formule jest błąd ponieważ użyto oznaczenia Vf(...) nigdzie nie definiowanego . Wszystko wskazuje, że jest to zbiór zmiennych związanych (ang. bound) ale pomylono się przy wpisywaniu bo litera V jest blisko litery B na klawiaturze a poza tym oba klawisze obsługiwane są tym samym palcem więc łatwo o pomyłkę. Aha! Jeszcze jedno. Dalej jest użyty znaczek & (ampersand) do oznaczenia koniunkcji logicznej co jest zrozumiałe dla programistów a do tego celu przeznaczony jest inny znaczek:∧ -- niepodpisany komentarz użytkownika 00:41, 4 sty 2017‎ (dyskusja)