# Is there a semantically complete system of direct-method natural deduction/sequent calculus?

Does anybody know of a system of direct-method natural deduction/sequent calculus, in other words, a system that does not require (or even incorporate) conditional (and indirect) proof method(s) and that is (at least claimed to be) semantically complete (regardless of whether or not it has been established to be syntactically complete)?

I am thinking that the intuitionists might have come up with such systems given their constructivist inclinations, but I am not finding anything.

(I wrestled with whether to post this on the mathematics stack exchange or here. I hope I made the right choice.)

• Intuitionsitic logic is complete without Double Negation, which is equivalent to Proof by contradiction in the form : from not P we have a contra, then conclude with P. But Intuistionistic logic needs Conditional proof. Jan 4 '20 at 11:45
• In the logic community, is it not (sensed to be) somewhat tendentious to claim that a logical system that requires conditional proof is semantically complete given that there is no way to construct a formal proof for the validity of conditional proof (which makes sense as it is a method/technique, not a rule)? A deduction theorem only justifies and defines the use of conditional proof for a given system. It does not prove anything. Indeed, couldn't this be what Irving Copi was on to? After all, he dropped the method(s) of (both) conditional proof (and indirect proof) from his system. Jan 4 '20 at 22:56