Skip to content

Latest commit

 

History

History
173 lines (158 loc) · 3.53 KB

InputData.md

File metadata and controls

173 lines (158 loc) · 3.53 KB

简单定律

同一律

输入

p->p

输出

(  1°)  p->(#327->p)    [l1]
(  2°)  p->((#327->p)->p)       [l1]
(  3°)  (p->((#327->p)->p))->((p->(#327->p))->(p->p))   [l2]
(  4°)  (p->(#327->p))->(p->p)  [MP 2°, 3°]
(  5°)  p->p    [MP 1°, 4°]

否定前件律

输入

!q->(q->p)

输出

(  1°)  !q->(!p->!q)    [l1]
(  2°)  (!p->!q)->(q->p)        [l3]
(  3°)  ((!p->!q)->(q->p))->(!q->((!p->!q)->(q->p)))    [l1]
(  4°)  !q->((!p->!q)->(q->p))  [MP 2°, 3°]
(  5°)  (!q->((!p->!q)->(q->p)))->((!q->(!p->!q))->(!q->(q->p)))        [l2]
(  6°)  (!q->(!p->!q))->(!q->(q->p))    [MP 4°, 5°]
(  7°)  !q->(q->p)      [MP 1°, 6°]

习题

练习3 2.1°

输入

(x1->x2)->((!x1->!x2)->(x2->x1))

输出

(  1°)  (!x1->!x2)->(x2->x1)    [l3]
(  2°)  ((!x1->!x2)->(x2->x1))->((x1->x2)->((!x1->!x2)->(x2->x1)))      [l1]
(  3°)  (x1->x2)->((!x1->!x2)->(x2->x1))        [MP 1°, 2°]

练习3 2.2°

输入

((p->(q->r))->(p->q))->((p->(q->r))->(p->r))

输出

(  1°)  (p->(q->r))->((p->q)->(p->r))   [l2]
(  2°)  ((p->(q->r))->((p->q)->(p->r)))->(((p->(q->r))->(p->q))->((p->(q->r))->(p->r))) [l2]
(  3°)  ((p->(q->r))->(p->q))->((p->(q->r))->(p->r))    [MP 1°, 2°]

练习3 2.3°

输入

p->(q->(p->q))

输出

(  1°)  q->(p->q)       [l1]
(  2°)  (q->(p->q))->(p->(q->(p->q)))   [l1]
(  3°)  p->(q->(p->q))  [MP 1°, 2°]

练习3 2.3°

输入

p->(q->(p->q))

输出

(  1°)  q->(p->q)       [l1]
(  2°)  (q->(p->q))->(p->(q->(p->q)))   [l1]
(  3°)  p->(q->(p->q))  [MP 1°, 2°]

练习3 3.1°

输入

p->p
!p

输出

(  1°)  p->(#327->p)    [l1]
(  2°)  p->((#327->p)->p)       [l1]
(  3°)  (p->((#327->p)->p))->((p->(#327->p))->(p->p))   [l2]
(  4°)  (p->(#327->p))->(p->p)  [MP 2°, 3°]
(  5°)  p->p    [MP 1°, 4°]

练习3 3.2°

输入

p
!!p

输出

(  1°)  #780429->(#780430->#780429)     [l1]
(  2°)  !!p     [known]
(  3°)  !!p->(!!(#780429->(#780430->#780429))->!!p)     [l1]
(  4°)  !!(#780429->(#780430->#780429))->!!p    [MP 2°, 3°]
(  5°)  (!!(#780429->(#780430->#780429))->!!p)->(!p->!(#780429->(#780430->#780429)))    [l3]
(  6°)  !p->!(#780429->(#780430->#780429))      [MP 4°, 5°]
(  7°)  (!p->!(#780429->(#780430->#780429)))->((#780429->(#780430->#780429))->p)        [l3]
(  8°)  (#780429->(#780430->#780429))->p        [MP 6°, 7°]
(  9°)  p       [MP 1°, 8°]

练习3 3.3°

输入

p->r
p->q
!(q->r)->!p

输出

(  1°)  p->q    [known]
(  2°)  !(q->r)->!p     [known]
(  3°)  (!(q->r)->!p)->(p->(q->r))      [l3]
(  4°)  p->(q->r)       [MP 2°, 3°]
(  5°)  (p->(q->r))->((p->q)->(p->r))   [l2]
(  6°)  (p->q)->(p->r)  [MP 4°, 5°]
(  7°)  p->r    [MP 1°, 6°]

练习3 3.4°

输入

q->(p->r)
p->(q->r)

输出

(  1°)  q->(p->q)       [l1]
(  2°)  p->(q->r)       [known]
(  3°)  (p->(q->r))->((p->q)->(p->r))   [l2]
(  4°)  (p->q)->(p->r)  [MP 2°, 3°]
(  5°)  ((p->q)->(p->r))->(q->((p->q)->(p->r))) [l1]
(  6°)  q->((p->q)->(p->r))     [MP 4°, 5°]
(  7°)  (q->((p->q)->(p->r)))->((q->(p->q))->(q->(p->r)))       [l2]
(  8°)  (q->(p->q))->(q->(p->r))        [MP 6°, 7°]
(  9°)  q->(p->r)       [MP 1°, 8°]

练习3 3.5°

输入

p->r
p->q
q->r

输出

(  1°)  p->q    [known]
(  2°)  q->r    [known]
(  3°)  (q->r)->(p->(q->r))     [l1]
(  4°)  p->(q->r)       [MP 2°, 3°]
(  5°)  (p->(q->r))->((p->q)->(p->r))   [l2]
(  6°)  (p->q)->(p->r)  [MP 4°, 5°]
(  7°)  p->r    [MP 1°, 6°]