| 单词 | natural deduction |
| 释义 | natural deductionnatural deductionnatural deductionnatural deduction(logic)In the traditional notation, a horizontal line separatespremises (above) from conclusions (below). Verticalellipsis (dots) stand for a series of applications of therules. "T" is the constant "true" and "F" is the constant"false" (sometimes written with a LaTeX \\perp). "^" is the AND (conjunction) operator, "v" is the inclusiveOR (disjunction) operator and "/" is NOT (negation orcomplement, normally written with a LaTeX \eg). P, Q, P1, P2, etc. stand for propositions such as "Socrateswas a man". P[x] is a proposition possibly containinginstances of the variable x, e.g. "x can fly". A proof (a sequence of applications of the rules) may beenclosed in a box. A boxed proof produces conclusions thatare only valid given the assumptions made inside the box,however, the proof demonstrates certain relationships whichare valid outside the box. For example, the box belowlabelled "Implication introduction" starts by assuming P,which need not be a true proposition so long as it can beused to derive Q. Truth introduction: -T (Truth is free). Binary AND introduction: -----------| . | . || . | . || Q1 | Q2 |-----------Q1 ^ Q2 (If we can derive both Q1 and Q2 then Q1^Q2 is true). N-ary AND introduction: ----------------| . | .. | . || . | .. | . || Q1 | .. | Qn |----------------Q1^..^Qi^..^Qn Other n-ary rules follow the binary versions similarly. Quantified AND introduction: ---------| x . || . || Q[x] |---------For all x . Q[x] (If we can prove Q for arbitrary x then Q is true for all x). Falsity elimination: F-Q (Falsity opens the floodgates). OR elimination: P1 v P2-----------| P1 | P2 || . | . || . | . || Q | Q |-----------Q (Given P1 v P2, if Q follows from both then Q is true). Exists elimination: Exists x . P[x]-----------| x P[x] || . || . || Q |-----------Q (If Q follows from P[x] for arbitrary x and such an x existsthen Q is true). OR introduction 1: P1-------P1 v P2 (If P1 is true then P1 OR anything is true). OR introduction 2: P2-------P1 v P2 (If P2 is true then anything OR P2 is true). Similarsymmetries apply to ^ rules. Exists introduction: P[a]-------------Exists x.P[x] (If P is true for "a" then it is true for all x). AND elimination 1: P1 ^ P2-------P1 (If P1 and P2 are true then P1 is true). For all elimination: For all x . P[x]----------------P[a] (If P is true for all x then it is true for "a"). For all implication introduction: -----------| x P[x] || . || . || Q[x] |-----------For all x . P[x] -> Q[x] (If Q follows from P for arbitrary x then Q follows from P forall x). Implication introduction: -----| P || . || . || Q |-----P -> Q (If Q follows from P then P implies Q). NOT introduction: -----| P || . || . || F |-----/ P (If falsity follows from P then P is false). NOT-NOT: //P---P (If it is not the case that P is not true then P is true). For all implies exists: P[a] For all x . P[x] -> Q[x]-------------------------------Q[a] (If P is true for given "a" and P implies Q for all x then Qis true for a). Implication elimination, modus ponens: P P -> Q----------Q (If P and P implies Q then Q). NOT elimination, contradiction: P /P------F (If P is true and P is not true then false is true). |
| 随便看 |
|
英语词典包含2567994条英英释义在线翻译词条，基本涵盖了全部常用单词的英英翻译及用法，是英语学习的有利工具。