0
$\begingroup$

In mathematical logic, when we write a formula of the metalanguage (such as $A \vdash B$) above an horizontal rule and another formula (such as $\vdash A \to B$), is it the same as writing a meta implication sign $\implies$ between the two formulas?

$\endgroup$
2
  • $\begingroup$ if you already have ⊢ (logical entailment), then ⟹ usually means meta implication ("if then" in the meta language). Inference rules in sequent calculus can be read as meta implication. For example: If A is provable from Γ, then ∅ is provable from Γ, ¬A. So yes. But if your inference rules are in natural deduction, then you shouldn't read it as meta implication $\endgroup$ Apr 18 at 16:18
  • $\begingroup$ $A \vdash B$ in general means "A is derivable form B". If we have it in the upper part of the horizontal, this means that we are working with Sequent Calcus where rules act on derivation instead of formulas. $\endgroup$ Apr 18 at 16:58

2 Answers 2

2
$\begingroup$

The horizontal line is typically used to reflect the definition or use of an inference rule. As a definition it says "If you have something that looks like [this], then you can write down something that look like [that]". As an actual use, it says: "given that we have something that looks like [this], we can and will write down something that look like [that]". For example, we can write something like:

\begin{array}{} P \vdash Q\\ \hline \vdash P \to Q\\ \end{array}

Now, is this the same as writing $P \vdash Q \implies \vdash P \to Q$?

Well, different authors/texts use $\implies$ in different ways, but I would say most will use $\implies$ to mean logical implication. As such, it is a little different from an inference rule in several ways:

  1. An inference rule is purely syntactic. As such, an inference rule wouldn't even have to reflect a logical implication. For example, I could define:

Modus Bogus

\begin{array}{} \Gamma \vdash P\\ \hline \Gamma \vdash Q\\ \end{array}

Now, clearly just because we have $\Gamma \vdash P$ does not imply that $\Gamma \vdash Q$, and so you wouldn't want to write $\Gamma \vdash P \implies \Gamma \vdash Q$. And yet, if I declare this inference rule as an inference rule ... well, then it's an inference rule.

  1. Inference rules are part of a defined formal proof system that contains a limited number of such inference rules, and thus it is unlikely that for every metaimplication there is a corresponding inference rule.

For example, a little work will tell you that $\Gamma \vdash P \land (\neg P \lor Q) \land \neg Q$ implies $\Gamma \vdash R \lor S$, and so we could say that $P \land (\neg P \lor Q) \land \neg Q \implies R \lor S$. But the formal proof system that you are currently considering may not have anything like that defined as an inference rule. So while an inference rule may reflect a metaimplication, not every metaimplication is reflected by an inference rule. So again, they are not the same.

$\endgroup$
2
  • $\begingroup$ Thank you for your answer but this is not what I am asking. As I mentioned in the question, I use $\implies$ as the metaimplication, not as the semantic one. Moreover I am asking about the precise meaning of the horizontal rule, not about the set of inference rules one should use $\endgroup$
    – user1313248
    Apr 18 at 15:42
  • $\begingroup$ @anserin OK, will update my answer $\endgroup$
    – Bram28
    Apr 18 at 15:56
0
$\begingroup$

If $p$ and $q$ are arbitrary statements such that $p \rightarrow q$ is a tautology,then we say that $p$ logically implies $q$ and we write $\implies$ to denote this situation.

So, if some compound statements are showed by means of $\implies$, it is tautology.

$p \implies q$ is true for each $p$ and $q$ value, but $p \rightarrow q$ does not mean that the implication has to be tautology.

$\endgroup$

You must log in to answer this question.