Logika: Rachunek predykatów.
Operacja podstawiania:
(1) xj[xi /t] = { t, gdy i = j; xj, gdy i =/= j
(2) aj[xi /t] = aj
(3) fk(t1 ... tn)[xi /t] = fk(t1[xi/t], ..., tn[xi /t])
(4) Pk(t1, ..., tn)[xi /t] = Pk(t1[xi /t], ..., tn[xi /t])
(5) Jeżeli A ma postać ~B, to A[xi/t] = ~B[xi/t].
(6) Jeżeli A ma postać (B <spójnik> C), gdzie <spójnik> jest jednym ze spójników ^, v, ->, <->, to A[xi/t] <spójnik> C[xi/t]
(7) Jeżeli A ma postać Qxj(B), gdzie Q jest jednym z kwantyfikatorów \-/ lub 3, to:A[xi/t] = { Qxj(B), gdy i = j ; Qxj(B[xi/t] gdy i =/= j
[Definicja znajduje się w Batógu]
x1 x1/0+2 => 0+2x1 x3/0+2 => x1 [pustospełnienie]
+(x1, 2) x1/ pierwiastek z 2 => +(x1[x1/ pierwiastek z 2], 2[[x1/ pierwiastek z 2]) =
= +(pierwiastek z 2 + 2)
\-/x1~(x1 < x2) x2/0
\-/x1~(x1 < x2)[x2/0] = \-/x1~(x1[x2/0x] < x2/[x2/0]) = \-/x1~(x1 < 0)
Jest to funkcja.
Reguły dowodzenia (inferencyjne):
RP: A / A[xi/t] o ile term t jest podstawialny za zmienną x, do formuły A.
RO: A ->B, A / B
O\-/: A -> \-/xi(B) / A ->B
D\-/: A -> B / A -> \-/x1(B) o ile zmienna xi nie jest wolna w formule A.
O3: 3xi(A) -> B / A -> B
D3: A -> B / 3xi(A) -> B o ile zmienna xi nie jest wolna w formule B.
Wszystkie te reguły są niezawodne.
Czemu zastrzeżenia: są one istotne ponieważ gdyby ich nie było, to mogłoby się zdarzyć, że przesłanka byłaby prawdziwa natomiast wniosek byłby fałszywy; np.:
W(x) -> P(x)
[jeżeli x (piotr) jest wysoki, to x (np. piotr) jest popularny]
W(x) -> \-/xP(x)
[jeżeli x (piotr) jest wysoki, to każdy x (piotr) jest popularny]
Dowodzenie KRP przebiega analogicznie do KRZ:
T1. \-/xP1(x) -> 3xP1(x).
1. \-/xP1(x) -> \-/xP1(x) [aksjomat: prawo tożsamości]
2. \-/xP1(x) -> P1(x) [O\-/: 1]
3. 3xP1(x) -> 3xP1(x) [aksjomat: prawo tożsamości]
4. P1(x) -> 3xP1(x) [O3: 3]
5. (2) -> [(4) -> (\-/xP1(x) -> 3xP1(x))] [aksjomat: prawo sylogizmu hipotetycznego]
6. (4) -> (\-/xP1(x) -> 3xP1(x)) [RO: 2,5]
7. \-/xP1(x) -> 3xP1(x) [RO: 4,6]
Dygresja: dowodem jest ciąg formuł, a ni numery po lewej stronie, ani informacje po prawej nie należą do dowodu – mają na celu ułatwienia życia;).
Zauważmy, że rola formuł atomowych w przeprowadzanych dowodach jest znikoma. Istotnie każdą taką formułę można zastąpić dowolną formułą, np. W powyższym dowodzei P1(x) można by zastąpić przez 3y~P3(x,y,z). Stąd dowody też można łatwo przekształcić w dowody metatez (tj. Schematów tez KRP); np.:
\-/x(A) -> 3y(A),
gdzie A jest metazmienną reprezentującą dowolną formułę KRP, a x metazmienną reprezentującą zmienne indywiduowe. Każda taka metateza jest schematem nieskończenie wielu tez KRP.
Podobnie jak w KRZ w dowodach na gruncie KRP możemy używać w charakterze przesłanek nie tylko aksjomatów KRP, lecz również tez wcześniej udowodnionych. Jest tak, gdyż każdy dowód w którym korzystamy z tez uprzednio udowodnionych można przedłużyć w taki sposób, aby jedynynmi przesłankami były aksjomaty.
MT1. \-/x(A) -> A
1. \-/x(A) -> \-/x(A) [aksjomat: pr. Tożsamości]
2. \-/x(A) -> A [O\-/: 1]
MT2. A -> 3x(A)
MT3: \-/x(A) -> 3x(A)
1. MT1
2. MT2
3. (1) -> [(2) -> (\-/x(A) -> 3x(A))] [aksjomat: pr. Sylogizmu hipotetycznego]
4. (2) -> (\-/x(A) -> 3x(A)) [RO: 1,3]
5. \-/x(A) -> 3x(A) [RO: 4,3]
KRP jest nadbudowany nad KRZ. Stąd w dowodach tez KRP możemy stosować wszystkie wtórne reguły dowodzenia z których korzystaliśmy w KRZ, np. Regułę sylogizmu hipotetycznego (RSH). Udowodnijmy jeszcze raz:
MT4. 3x\-/yA(x,y) -> \-/y3xA(x,y)
1. \-/yA(x,y) -> A(x,y) [MT1]
2. A(x,y) -> 3xA(x,y) [MT2]
3. ...
jelonka72