Equivalence of Semantic Consequence and Logical Implication

From ProofWiki
Jump to navigation Jump to search


It has been suggested that this page be renamed.
To discuss this page in more detail, feel free to use the talk page.



Work In Progress
In particular: This pertains to classical PC, intuitionistic PC is not sound
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{WIP}} from the code.


Theorem

Let $U = \set {\phi_1, \phi_2, \ldots, \phi_m, \ldots}$ be a countable set of propositional formulas.

Let $\psi$ be a propositional formula.


Then $U \models \psi$ if and only if $U \vdash \psi$.


That is, semantic consequence is equivalent to provable consequence.


Direct Proof

Necessary Condition

This is a statement of the Extended Soundness Theorem for Propositional Tableaus and Boolean Interpretations:

Let $\mathbf H$ be a countable set of propositional formulas.

Let $\mathbf A$ be a propositional formula.


If $\mathbf H \vdash \mathbf A$, then $\mathbf H \models \mathbf A$.


Sufficient Condition

This is the statement of the Extended Completeness Theorem for Propositional Tableaus and Boolean Interpretations.

$\blacksquare$


Comment

There are two things being proved here:

$(1): \quad$ Suppose we have a sequent $\phi_1, \phi_2, \ldots, \phi_m, \ldots \vdash \psi$, the validity of which has been established, for example, by a tableau proof.

The result:

if $\phi_1, \phi_2, \ldots, \phi_m, \ldots \vdash \psi$ then $\set {\phi_1, \phi_2, \ldots, \phi_m, \ldots} \models \psi$

establishes that if all the propositions $\phi_1, \phi_2, \ldots, \phi_m, \ldots$ evaluate to true, then so does $\psi$.

This establishes that propositional logic is sound.


$(2): \quad$ Suppose we have determined that $\set {\phi_1, \phi_2, \ldots, \phi_m, \ldots} \models \psi$.

The result:

if $\set {\phi_1, \phi_2, \ldots, \phi_m, \ldots} \models \psi$ then $\phi_1, \phi_2, \ldots, \phi_m, \ldots \vdash \psi$

establishes that if we can show that there is a model for a proposition, then we will be able to find a tableau proof for it.

This establishes that propositional logic is complete.


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Equivalence_of_Semantic_Consequence_and_Logical_Implication&oldid=451275"