1302
правки
Изменения
→Больше формальности!
К стандартным аксиомам исчисления предикатов добавим следующие 8 ''нелогических'' аксиом и одну нелогическую схему аксиом.
<tabletex>\begin{cases}(A1) & a = b \rightarrow a' = b' \\(A2) & a = b \rightarrow a = c \rightarrow b = c \\(A3) & a' = b' \rightarrow a = b \\(A4) & \neg a' = 0 \\(A5) & a + b' = (a+b)' \\(A6) & a + 0 = a \\(A7) & a \cdot 0 = a \\(A8) & a \cdot b' = a \cdot b + a \\(A9) & (\psi [x := 0]) \& \forall{x}((\psi) \rightarrow (\psi) [x := x']) \rightarrow (\psi)\\\end{cases}</tex>
<tr class="odd">
<td align="left">(A5)</td>
<td align="left"><tex>a + b' = (a+b)'</tex></td>
</tr>
<tr class="even">
<td align="left">(A6)</td>
<td align="left"><tex>a + 0 = a</tex></td>
</tr>
<tr class="odd">
<td align="left">(A7)</td>
<td align="left"><tex>a \cdot 0 = a</tex></td>
</tr>
<tr class="even">
<td align="left">(A8)</td>
<td align="left"><tex>a \cdot b' = a \cdot b + a</tex></td>
</tr>
<tr class="odd">
<td align="left">(A9)</td>
<td align="left"><tex>(\psi [x := 0]) \& \forall{x}((\psi) \rightarrow (\psi) [x := x']) \rightarrow (\psi)</tex></td>
</tr>
