A many sorted natural deduction