Definition:Logical Implication

From ProofWiki
Jump to navigation Jump to search

Definition

In a valid argument, the premises logically imply the conclusion.


If the truth of one statement $p$ can be shown in an argument directly to cause the meaning of another statement $q$ to be true, then $q$ follows from $p$ by logical implication.

We may say:

$p$, therefore $q$ and write $p \vdash q$.
$q$, because $p$ and write $q \dashv p$.


In symbolic logic, the concept of logical consequence occurs in the form of semantic consequence and provable consequence.


In the context of proofs of a conventional mathematical nature on $\mathsf{Pr} \infty \mathsf{fWiki}$, the notation:

$p \leadsto q$

is preferred, where $\leadsto$ can be read as leads to.


Semantic Consequence

Let $\mathscr M$ be a formal semantics for a formal language $\mathcal L$.

Let $\mathcal F$ be a collection of WFFs of $\mathcal L$.


Let $\map {\mathscr M} {\mathcal F}$ be the formal semantics obtained from $\mathscr M$ by retaining only the structures of $\mathscr M$ that are models of $\mathcal F$.

Let $\phi$ be a tautology for $\map {\mathscr M} {\mathcal F}$.


Then $\phi$ is called a semantic consequence of $\mathcal F$, and this is denoted as:

$\mathcal F \models_{\mathscr M} \phi$


That is to say, $\phi$ is a semantic consequence of $\mathcal F$ if and only if, for each $\mathscr M$-structure $\mathcal M$:

$\mathcal M \models_{\mathscr M} \mathcal F$ implies $\mathcal M \models_{\mathscr M} \phi$

where $\models_{\mathscr M}$ is the models relation.


Note in particular that for $\mathcal F = \O$, the notation agrees with the notation for a $\mathscr M$-tautology:

$\models_{\mathscr M} \phi$


The concept naturally generalises to sets of formulas $\mathcal G$ on the right hand side:

$\mathcal F \models_{\mathscr M} \mathcal G$

if and only if $\mathcal F \models_{\mathscr M} \phi$ for every $\phi \in \mathcal G$.


Provable Consequence

Let $\mathscr P$ be a proof system for a formal language $\mathcal L$.

Let $\mathcal F$ be a collection of WFFs of $\mathcal L$.


Denote with $\mathscr P \left({\mathcal F}\right)$ the proof system obtained from $\mathscr P$ by adding all the WFFs from $\mathcal F$ as axioms.

Let $\phi$ be a theorem of $\mathscr P \left({\mathcal F}\right)$.


Then $\phi$ is called a provable consequence of $\mathcal F$, and this is denoted as:

$\mathcal F \vdash_{\mathscr P} \phi$


Note in particular that for $\mathcal F = \varnothing$, this notation agrees with the notation for a $\mathscr P$-theorem:

$\vdash_{\mathscr P} \phi$


Distinction between Logical Implication and Conditional

It is important to understand the difference between:

$A \implies B$: If we assume the truth of $A$, we can deduce the truth of $B$

and:

$A \leadsto B$: $A$ is asserted to be true, therefore it can be deduced that $B$ is true


When $A$ is indeed true, the distinction is less important than when the truth of $A$ is in question, but it is a bad idea to ignore it.


Compare the following:

\((1):\quad\) \(\displaystyle x > y\) \(\implies\) \(\displaystyle \paren {x^2 > x y \text { and } x y > y ^2}\)
\(\displaystyle \) \(\implies\) \(\displaystyle x^2 > y^2\)


\((2):\quad\) \(\displaystyle x\) \(>\) \(\displaystyle y\)
\(\displaystyle \leadsto \ \ \) \(\displaystyle x^2\) \(>\) \(\displaystyle x y\)
\(\, \displaystyle \text { and } \, \) \(\displaystyle x y\) \(>\) \(\displaystyle y^2\)
\(\displaystyle \leadsto \ \ \) \(\displaystyle x^2\) \(>\) \(\displaystyle y^2\)


We note that $(1)$ is a conditional statement of the form:

$A \implies B \implies C$

This can mean either:

$\paren {A \implies B} \implies C$

or:

$A \implies \paren {B \implies C}$

instead of what is actually meant:

$\paren {A \implies B} \text { and } \paren {B \implies C}$


Hence on $\mathsf{Pr} \infty \mathsf{fWiki}$ we commit to using the form $A \leadsto B$ rigorously in our proofs.


The same applies to $\iff$ and $\leadstoandfrom$ for the same reasons.


Also see


Sources