Nuprl Definition : mFOLRule

Nuprl Definition : mFOLRule_ind

case(v)
andI => andI
impI => impI
allI with var => allI[var]
existsI with var => existsI[var]
orI (left?left) => orI[left]
hyp => hyp
andE @hypnum => andE[hypnum]
orE @hypnum => orE[hypnum]
impE @hypnum => impE[hypnum]
allE @hypnum with var => allE[hypnum; var]
existsE @hypnum with var => existsE[hypnum; var] ==
  let lbl,v1 = v
  in if lbl="andI" then andI
     if lbl="impI" then impI
     if lbl="allI" then allI[v1]
     if lbl="existsI" then existsI[v1]
     if lbl="orI" then orI[v1]
     if lbl="hyp" then hyp
     if lbl="andE" then andE[v1]
     if lbl="orE" then orE[v1]
     if lbl="impE" then impE[v1]
     if lbl="allE" then let hypnum,v2 = v1 in allE[hypnum; v2]
     if lbl="existsE" then let hypnum,v2 = v1 in existsE[hypnum; v2]
     else Ax
     fi

Definitions occuring in Statement : atom_eq: if a=b then c else d fi , spread: spread def, token: "$token", axiom: Ax
Definitions occuring in definition : atom_eq: if a=b then c else d fi , token: "$token", spread: spread def, axiom: Ax
FDL editor aliases : FOLRule_ind

Latex:
case(v) andI => andI impI => impI allI with var => allI[var] existsI with var => existsI[var] orI (left?left) => orI[left] hyp => hyp andE @hypnum => andE[hypnum] orE @hypnum => orE[hypnum] impE @hypnum => impE[hypnum] allE @hypnum with var => allE[hypnum; var] existsE @hypnum with var => existsE[hypnum; var] == let lbl,v1 = v in if lbl="andI" then andI if lbl="impI" then impI if lbl="allI" then allI[v1] if lbl="existsI" then existsI[v1] if lbl="orI" then orI[v1] if lbl="hyp" then hyp if lbl="andE" then andE[v1] if lbl="orE" then orE[v1] if lbl="impE" then impE[v1] if lbl="allE" then let hypnum,v2 = v1 in allE[hypnum; v2] if lbl="existsE" then let hypnum,v2 = v1 in existsE[hypnum; v2] else Ax fi Date html generated: 2016_05_15-PM-10_21_54 Last ObjectModification: 2015_09_23-AM-08_24_15 Theory : minimal-first-order-logic Home Index