TWiki> Sandbox Web>TestTopic11 (16 Nov 2009, TWikiGuest)EditAttach
Reflexivity of $=$
$\Gamma\vdash t=t$, where $t$ is a constant symbol or a variable.
Transitivity of $=$
%\Gamma , r=s,s=t\vdash r=t$%, where $r$, $s$, and $t$ are constant symbols or variables.
Substitution
If $\phi$ is a formula according to either of the first two clauses of the definition of a formula, $s$ and $t$ are variables and constant symbols, and $\psi$ is obtained from $\phi$ by replacing some occurrences of $s$ by $t$, then $\Gamma ,s=t,\phi\vdash\psi$.
Thinning
If $\Sigma$ is a set of formulas and $\Gamma\vdash\phi$, then $\Gamma\cup\Sigma\vdash\phi$.
Cut
If $\Gamma\vdash\sigma$ for every $\sigma$ in $\Sigma$ and $\Sigma\vdash\phi$, then $\Gamma\vdash\phi$.

A derivation (or proof) of $\phi$ from $\Gamma$ is a finite sequence of inferences $\Sigma_{i}\vdash\phi_{i}$ such that the last one is $\Gamma\vdash\phi$ and such that each $\Sigma_{i}\vdash\phi_{i}$ is shown to be a legitimate inference using only the rules above and $\Sigma_{j}\vdash\phi_{j}$ for $j<i$. A sentence $\phi$ is derivable from $\Gamma$ or is a theorem of $\Gamma$ if there is a proof of $\phi$ from $\Gamma$ or, equivalently, if $\phi$ is a member of the smallest set $\Sigma$ such that $\Gamma\subseteq\Sigma$ and, for any formula $\sigma$ if $$\Sigma\vdash\sigma$, then $\sigma\in\Sigma$.

-- ShaughanLavine - 04 May 2009
Latex rendering error!! dvi file was not created.

Edit | Attach | Print version | History: r3 < r2 < r1 | Backlinks | Raw View | More topic actions
Topic revision: r3 - 16 Nov 2009 - 09:58:17 - TWikiGuest
 
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback