What will be the notion of a "valid deduction" in the following system?

62 Views Asked by At

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.