The logical law of closed systems of sentences

Question

Consider the usual logical connectors $\wedge, \vee, \supset, \neg$ (i.e., "and", "or", material implication, negation) and the "stroke" $/$ defined as $p / q := (\neg p) \vee (\neg q)$.

In his book "Introduction to Logic: And to the Methodology of Deductive Sciences" (ISBN-10: 048628462X) the author A. Tarski presents on page 176 a section about "Closed systems of sentences" which runs as follows:

There exists a general logical law which permits us in some cases, when we have succeeded in proving several conditional propositions, to infer from the form of these propositions that the corresponding converse propositions may be also considered as proved.

Assume we are given a finite system of implications to which we will give the following schematic form $p \supset q, p' \supset q', p'' \supset q'', ...$

If the antecedents (premisses) exhaust all possible cases, that is, if it is true that $p \vee p' \vee p'' \vee ...$, and if simultaneously their consequents (conclusions) exclude one another (incompatibility) $q/q' \wedge q/q'' \wedge q'/q'' \wedge ...$, then the converse implications are entailed $q \supset p, q' \supset p', q'' \supset p'', ...$

Consider as example the following simple system of sentences: $((p \supset q) \wedge (p' \supset q') \wedge (p'' \supset q'') \wedge (p \vee p' \vee p'') \wedge (q/q') \wedge (q/q'') \wedge (q'/q'')) \supset ((q \supset p) \wedge (q' \supset p') \wedge (q'' \supset p''))$

My question is: How can the general claim in Tarski's book above be proved?

Answer 1

The general statement cannot itself be expressed as a formula in the system, so if we are to prove it at all it must be as a metatheorem, working on the metalevel:

Let $n\ge 1$ be a natural number and let $p_i$ and $q_i$ for $1\le i\le n$ be arbitrary formulas. Then the formula $$ \bigwedge_{1\le i\le n}( p_i \to q_i ) \land \bigvee_{1\le i \le n} p_i \land \bigwedge_{1\le i<j\le n} (q_i \uparrow q_j ) \to \bigwedge_{1\le i\le n}(q_i\to p_i) $$ is a theorem of such-and-such logical system.

Note that the indexed conjunctions and disjunctions such as $\bigwedge_{1\le i\le n}(p_i\to q_i)$ are not part of the formal language; they appear in the metatheorem as a way to describe the actual formal formula that the metatheorem claims is a theorem.

To prove the metatheorem means to argue that when we construct a formula according to the recipe in the metatheorem, we can also find a formal proof of that formula.

This can be done either directly, by describing a procedure for how to write down that formal proof once $n$ and the $p_i$s and $q_i$s are given, or semantically, by arguing that the constructed formula evaluates to true in every valuation/interpretation and then appealing to a completeness theorem for the logic in question.

In both of these cases, the starting point would be an informal argument that the principle works:

Assume everything on the left-hand side; we want to prove that $q_i\to p_i$. So suppose $q_i$ is true. Since the $q_i$s are all mutually exclusive, this means that $q_j$ is false for all $j\ne i$. However $p_j\to q_j$ is assumed, and by contraposition we get that $p_j$ is false for all $j\ne i$. However since $p_1\lor p_2 \lor \cdots \lor p_n$ is also assumed, it must be that $p_i$ is true (it is the only one we haven't just found to be false). So $p_i$, which is what we wanted.

It is straightforward but (extremely) tedious to get from this informal argument to a rigorous description of a formal proof sequence for the constructed sentence, in the style of

....
Line $2612+87n^2+333n+8i$ of the proof is the formula $\neg q_i\to \neg p_i$. This is a valid proof step because of the previous lines $2608+87n^2+333n+8i$ and $2611+87n^2+333n+8i$, by modus ponens.
...

In fact so tedious that nobody ever does it in this level of detail. Instead one either combines a slew of earlier similar metatheorems to build up things step-by-step, or goes to the semantic way instead.

The informal argument is almost word-for-word a valid (but still informal, because we're at the metalevel here) argument about truth values in a particular interpretation. With a few strategic substitutions such as writing "Assume $\mathfrak M\vDash \neg q$" instead of "Assume that $q$ is false", we get an ordinary proof that the constructed formula is true in every interpretation. We can then appeal to the completeness of the logic to conclude that there must be a formal proof of the formula, even though we never see that formal proof in detail.

Answer 2

Tarski example, page 176 (page 167 in the 4th edition, 1994) with three laws can be generalized to any finite case.

In Tarski's example we have :

(i) : $p_1 \lor p_2 \lor p_3$

and :

(ii) : $p_1 \to q_1, p_2 \to q_2, p_3 \to q_3$

and :

(iii) $q_1 \to \lnot q_2, q_1 \to \lnot q_3, q_2 \to \lnot q_3$.

With this conditions, we can easily prove : $q_i \to p_i$, for all $i$ :

1) assume : $q_1$

2) $\lnot q_2$ --- from 1) and (iii)

3) $\lnot p_2$ --- from 2) and (ii) by contraposition

4) $\lnot q_3$ --- from 1) and (iii)

5) $\lnot p_3$ --- from 4) and (ii) by contraposition

6) $p_1$ --- from (i), 3) and 5) by (repetead) Disjunctive Syllogism

7) $q_1 \to p_1$ --- from 1) and 6) by Deduction Theorem.