# What will be the notion of a “valid deduction” in the following system?

Consider the Propositional Calculus whose axiom schemes and rule of inference are given below (here $$P,Q$$ and $$S$$ are formula schemes,

$$\color{crimson}{\text{Axiom 1.}}\ P\to (Q\to P)$$

$$\color{crimson}{\text{Axiom 2.}}\ (S\to (P\to Q))\to((S\to P)\to (S\to Q))$$

$$\color{crimson}{\text{Axiom 3.}}\ (\neg Q\to\neg P)\to(P\to Q)$$

$$\color{crimson}{\text{Rule of Inference.}}$$ Modus Ponens.

However, if instead of considering the axioms if we want to use an equivalent version of rules of inferences of the axioms which has a single premise and single conclusion we get the following,

$$\color{crimson}{\text{Rule 1.}}\ \dfrac{P}{Q\to P}$$

$$\color{crimson}{\text{Rule 2.}}\ \dfrac{S\to (P\to Q)}{(S\to P)\to (S\to Q)}$$

$$\color{crimson}{\text{Rule 3.}}\ \dfrac{\neg Q\to\neg P}{P\to Q}$$

$$\color{crimson}{\text{Rule 4.}}$$ Modus Ponens.

Question. My question is the following,

What will be a definition of a valid deduction in this system?

Of course we can say that $$S_1,\ldots,S_n$$ is a proof of $$Q$$ in this system if $$\{S_1,\ldots,S_n\}\vdash Q$$ in the former system. But I am looking for an independent definition. The case of Propositional Calculus, which motivated me to write the question may be considered a special case of a more general question.

Also, I have looked at the pages Natural Deduction and Sequent Calculus but while they are very close to what I want, I am not sure whether they are exactly the thing I am looking for because in this case my rules of inferences are only the above four and nothing else.

• This won't be equivalent. In fact, here, you can't prove anything. In order to be able to prove anything from no assumptions, you either need an axiom, or a notion of conditional proof... rules of inference of this simple form won't do. – spaceisdarkgreen Feb 17 at 5:05
• @spaceisdarkgreen: Indeed. That's why I said "valid deduction" and not a proof. What can be a legitimate notion of "conditional proof" in this case? – user 170039 Feb 17 at 5:07
• Not sure I entirely understand. But one thing that would work would be taking the deduction metatheorem $A\vdash B \implies \vdash A\to B$ as a primative assumption. That gets you into natural deduction territory. – spaceisdarkgreen Feb 17 at 5:10
• No, that isn’t the same thing, any more than your inference rules above are the same thing as the axioms. How do you take $P$ and $P\to Q$ and infer $P\land (P\to Q)$ without a two-premise inference rule? Anyway, although there are probably ideas in the direction you are looking I don’t know any offhand. But what you’re literally asking for seems impossible: in propositional logic an empty set of premises has consequences, and it can’t have any consequences if you have no axioms and only simple rules of inference of the form “from statement 1, infer statement 2.” – spaceisdarkgreen Feb 17 at 5:51
• The reasoning is just the King Lear axiom: “nothing can come from nothing.” – spaceisdarkgreen Feb 17 at 5:54