Questions tagged [natural-deduction]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer

Natural deduction with coq assistant prover

I want to mimic natural deduction proofs in coq ; for instance the proof I made for "A /\ B -> B /\ A" is for now ...
  • 123
1 vote
1 answer

Natural deduction vs simply typed lambda calculus

In ND , I have propositions as their own things, but in simply typed lambda calculus, I have propositions associated with proof. The question I want to ask is, how do these two different way of ...