The truth-function conditional, also called the material conditional, is a binary boolean truth function whose values are as you described in the truth table; it is true for all inputs except when the antecedent (left hand side) is true and the consequent (right hand side) is false. The conditional is written with a variety of symbols, e.g., $P \to Q$, $P \supset Q$, and $P \Rightarrow Q$.
There is an inference rule called modus ponens which says that from a conditional $P \to Q$ and $P$, infer $Q$. This can be written in a number of ways, e.g.,
- $P$
- $P \to Q$
- $Q$ by modus ponens from 1 and 2.
or
$$ \begin{array}{c} P \quad P \to Q \\ \hline Q \end{array} $$
Because modus ponens is so important, and because in some axiomatic systems it is the only inference rule, it is sometimes called “the inference rule.” Most of the time, that usage should probably be avoided, because in practice (i.e., outside of those specific axiomatic systems), there are plenty of other inference rules, and modus ponens is just one among many.
Asserting that the conditional $P \to Q$ is true is simply to assert that either:
- a. $P$ is true and $Q$ is true; or
- b. $P$ is false and $Q$ is true; or
- c. $P$ is false and $Q$ is false.
Using the inference rule modus ponens lets us affirm that $Q$ is true, based on the prior assertion that $P \to Q$ is true and that $P$ is true.
Modus ponens is a sound inference rule because whenever all the premises are actually true, then the conclusion is also actually true. To see why this is the case, consider the premises to modus ponens. These are a conditional $P \to Q$ and $P$. If $P \to Q$ is true, then one of the three cases (a, b, c) described above must also be true. $P \to Q$ being true does not, by itself, ensure that $Q$ is true, because there is one case (c) in which $P \to Q$ is true, but $Q$ is false. However, with the additional requirement that $P$ is true, we are restricted to the case (a) in which $Q$ is also true. Thus, if the premises to modus ponens are true, then so is its conclusion.
Now, it's worth considering how this applies to the example that you gave. The example of “all men are mortal, Socrates is man, therefore Socrates is mortal”. It uses first-order reasoning, and is not actually a case of modus ponens, neither premise is a conditional. However, the proof does use _modus ponens_, in that it requires us to make the following inference.
- (Premise) If Socrates is a man then Socrates is mortal.
- (Premise) Socrates is a man.
- (Conclusion) Therefore, Socrates is mortal.
There are two important concepts to consider: soundness and validity. These mean slightly different things for inference rules and for arguments.
An inference rule is sound if whenever its premises are true, then its conclusion is true. As we saw earlier, modus ponens is a sound rule of inference. The term valid is not used concerning inference rules. We do not say that an inference rule is valid or invalid.
An argument is valid if each reasoning step is an application of a sound inference rule. This means that each sentence in the argument must be true if the earlier sentences that it is based on are true. It does not make the claim that those earlier sentence are true, but just that if they are true, then the current sentence is true. An argument is sound if its premises are, in fact, true. If an argument is both sound and valid, then its conclusion must be true.
So, both
- (Premise) If Socrates is a man then Socrates is mortal.
- (Premise) Socrates is a man.
- (Conclusion) Therefore, Socrates is mortal.
and
- (Premise) If Italy is a man then Italy is mortal.
- (Premise) Italy is a man.
- (Conclusion) Therefore, Italy is mortal.
are valid arguments, because they use only valid inference rules (namely, modus ponens). The first argument is sound because both of its premises are true. The second argument is unsound because one of its premises its second premise, “Italy is man,” is not true.
If the conclusion of an argument is not true, it means that the argument is either invalid or unsound. (Of course, it could also be both.)
As I stated in my previous answer, the rule modus ponens is part of the definition of many common proof systems. Let HPC stand for Hilbert's system for classical propositional logic whose only rule of inference is modus ponens and whose axioms are listed here after Frege's. This is a well-defined mathematical object. It is one proof system for classical propositional logic. Literally over a dozen others are mentioned on that page, and those are restricted to Hilbert-style proof systems. There are also many others in the style of natural deduction or the sequent calculus.
In HPC a (formal) proof is either an instance of one of the axioms, or it is a use of the rule modus ponens which combines two other proofs. This produces a binary-tree-like structure whose leaves are instances of axioms. This is the definition of a proof in HPC. A formula of classical propositional logic is proven by HPC if we can build a proof which has that formula as the conclusion (i.e. the root of the tree). This is an example of the syntactic approach to logic. We don't even need to formulate the idea of "truth tables" to completely specify this.
An alternate approach is semantics. Here there are no axioms or rules. Instead, we need to provide a way of interpreting formulas as some mathematical object (in a compositional way, but I won't elaborate on that). There are many possible semantics you could use. One possibility is to use a Boolean algebra, and, in particular, the simplest possible non-trivial Boolean algebra built on a two element set. Any two element set will do. Let's use $\{\mathsf{cat},\mathsf{dog}\}$ for concreteness. With this choice of semantics, formulas with $n$ (distinct) propositional variables become $n$-ary operations on that two element set. Now we define a formula to be "true" if its interpretation is function that constantly has the value $\mathsf{dog}$. Dually from before, we can completely specify this semantics without ever mentioning any notion of formal proof.
Now we can ask the question: are the formulas that HPC proves the same as the formulas that the Boolean algebra semantics calls "true"? The soundness theorem for HPC with respect to this Boolean algebra semantics states that the formulas that HPC proves are "true" in the semantics. The completeness theorem for HPC with respect to this Boolean algebra semantics states that every formula that is "true" in the semantics has a proof in HPC. These (meta-)theorems can be proven either with informal mathematical reasoning or formally within some richer logical framework.
At no point in this do you need to accept the rules or axioms of HPC or agree that the Boolean algebra semantics I gave correctly reflects some philosophical notion of truth. This is no different from studying any other mathematical object. If I'm studying the ring of square matrices, I don't have to reject my prior notions of addition and multiplication and accept matrix addition/multiplication as the One True Meaning of addition and multiplication. I don't need to have a first principles account of how there is no other way of adding and multiplying matrices. (There are other ways of adding and multiplying matrices!) The formulas proven by HPC are the same regardless of one's philosophical stance. The formulas that are "true" with respect to the Boolean algebra semantics are the same regardless of one's philosophical stance. One's philosophical stance simply doesn't come into it.1
The only time I would need to convince you of the axioms/rules of HPC is if I'm making a philosophical claim that they correspond to some philosophical notion of "truth". There are plenty of reasons to study classical propositional logic quite apart from philosophical notions of "truth" such as applications to digital circuits. Similarly, there are plenty of reasons to study intuitionistic logics unrelated to philosophical notions of truth such as extracting computational content from constructive proofs or proving theorems that hold for a much broader and mathematically important class of semantics than classical logics. There are good reasons to study both simultaneously, and there is no cognitive dissonance in doing so.
As to some people calling $(p\land(p\to q))\to q$ "modus ponens", it wouldn't be the first time in mathematics that two distinct but related concepts were given the same name. That said, I think many of the times you see that it is being said by someone who doesn't have (or at least hasn't demonstrated that they have) a clear understanding of the separation between logic and meta-logic. Like your earlier question, if you try to naively formalize the usual informal description of the rule modus ponens but don't take care to separate syntax from semantics and logic from meta-logic, then you readily get the above formula. If you do take care to keep these separate, it is readily apparent that treating the above formula as the formalization of the rule modus ponens is a mish-mash of logic and meta-logic.
Write $\vdash p$ for the meta-logical claim that HPC proves $p$. The typical informal description of the rule modus ponens is: "if $p$ is provable and $p\to q$ is provable, then $q$ is provable". Let me write that a bit more formally. To make the distinction between logic and meta-logic a bit clearer, I'll write $\curlywedge$ and $\leadsto$ for the meta-logical conjunction and implication. The informal "modus ponens" is then more formally: $((\vdash p)\curlywedge(\vdash(p\to q)))\leadsto(\vdash q)$. This has the form $(\varphi\curlywedge\psi)\leadsto \chi$ where $\varphi$, $\psi$, and $\chi$ are atomic propositions in the meta-logic. Saying $(p\land(p\to q))\to q$ is a tautology is via the soundness and completeness theorems equivalent to saying $\vdash ((p\land(p\to q))\to q)$. This is an atomic proposition of the meta-logic. It should be clear now why I speak of a mish-mash. Viewing these two meta-logical propositions as being the same leads to $\to$ being used for both the $\to$ connective of the logic and the meta-logical $\leadsto$.
Still, if someone wants to call $(p\land(p\to q))\to q$ "modus ponens", that's their prerogative. It's no different than saying you are going to call it $A$. If, however, they are claiming it is the formalization of the rule modus ponens, then they are simply wrong.
1 This isn't completely true as one's philosophical stance on truth impacts their informal reasoning. For example, an ultrafinitist might reject the claim that sufficiently large formulas of classical propositional logic can have proofs in HPC or can be shown to be "true" in the Boolean algebra semantics. However, a classical mathematician, an ultrafinitist, and an intuitionist will all agree that $p\lor\neg p$ is provable in HPC and is "true" with respect to the Boolean algebra semantics. They just may not agree that HPC is a good reflection of their (philosophical) notion of "truth".
Best Answer
Note: due to the fact that the example uses $A,B,C$ as schematic letters for formulas, I'll adopt a different letter for the formulation of Leibniz's rule:
Thus, to apply the rule with premise $B \equiv C$, we use as $X$ the formula $A \equiv p$.
The two substitutions are: $X[p := B] = (A \equiv p)[p := B] = A \equiv B$ and $X[p := C] = (A \equiv p)[p := C] = A \equiv C$, respectively.
In conclusion:
$A \equiv B$
$B \equiv C$
$X[p := B] \equiv X[p := C] \text { i.e. } A \equiv B \equiv A \equiv C$ --- from 1) and 2) by Leibniz.
Regarding
the answer is: no. We assume as $X$ the "composite" formula $A \equiv p$, where $p$ is atomic.