Questions tagged [natural-deduction]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
9 votes
2 answers
883 views

Why is the Curry-Howard isomorphism?

The Curry-Howard isomorphism is the correspondence between type systems (like for the simply typed lambda calculus) and proof systems (like natural deduction). More precisely, types resemble ...
JoJoModding's user avatar
3 votes
0 answers
100 views

How to develop an effective notation for a partially ordered logic?

I am developing a logic for reasoning about programs in a resource-constrained environment. My starting point is intuitionistic linear logic, but I made the following changes: In intuitionistic ...
isekaijin's user avatar
  • 501
7 votes
3 answers
436 views

Discharged hypotheses in ->Introduction

I have a question about page 9 in Proofs and Types. The given $\rightarrow$Introduction rule says that $A \rightarrow B$ can be deduced from $B$ if the deduction of $B$ contains an arbitrary number ...
brooksbp's user avatar
  • 171
8 votes
2 answers
416 views

About the correspondence of left introduction and elimination of implication in Sequent Calculus and in Natural Deduction resp.

Could anyone give an intuitive (not intutionistic) explanation of the correspondence of left introduction and elimination of implication in Sequent Calculus (SC) and Natural Deduction (ND) ...
day's user avatar
  • 2,795