[Om3] binary vs n-ary relations

[Professor James Davenport]

On Mon, September 29, 2008 12:21 am, Chris Rowley wrote:
>> The use and meaning I can see is formula manipulation. When solving an
>> exercise by formula manipulation, one would use n-ary relation symbols
>> (for example (x+1)^2=(x+1)*(x+1)=x^2+x+x+1=x^2+2x+1).
I claim this is in fact shorthand for a proof (in the sense of Logic 101):
      (x+1)^2=(x+1)*(x+1)              [defn of ^]
      (x+1)*(x+1)=x^2+x+x+1            [generalised distrib]
      (x+1)^2=x^2+x+x+1                [transitivity]
      x^2+x+x+1=x^2+2x+1               [collection]
      (x+1)^2=x^2+2x+1                 [transitivity]


James Davenport
Hebron & Medlock Professor of Information Technology
Formerly RAE Coordinator and Undergraduate Director of Studies, CS Dept
Lecturer on CM30070, 30078, 50209, 50123, 50199
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor
IMU Committee on Electronic Information and Communication