How does one prove tautologies using arbitrary ands/ors

Question

One can easily prove $\phi \wedge \psi \iff \psi \wedge \phi$, using truth tables or $\wedge$-introduction/$\wedge$-elimination. But if we want to prove something like $$ \bigwedge_{x \in X} \phi\wedge \psi \iff \big(\bigwedge_{x \in X} \phi\big) \wedge \big(\bigwedge_{x \in X} \psi\big),$$ how do we go about it?

Answer 1

The other answers (currently) have assumed that $X$ is meant to be a finite set, at which point $\bigwedge\limits_{x\in X}\varphi_x$ is essentially $\bigwedge\limits_{i=0}^{|X|}\varphi_i$ which can then in turn be viewed as a syntactic abbreviation for $\varphi_1\land\varphi_2\land\dots\land\varphi_{|X|}$. For the initial abbreviation to be well-defined, we arguably need $\land$ to be associative, commutative, and idempotent which it is.

When $X$ is infinite, we can no longer interpret the above formula as an abbreviation: formulas are usually presumed to be finite by definition. That means if you want to use $\bigwedge\limits_{x\in X}\varphi_x$ as a formula, you need to give rules for $\bigwedge$. Now the most obvious thing to do would be to take the rules for $\land$, namely $\cfrac{A_1\quad A_2}{A_1\land A_2}\land\! I$ and $\cfrac{A_1\land A_2}{A_i}\land\! E_i$ (for $i\in\{1,2\}$) and extend them to the infinitary case. The latter rule is relatively straightforward to extend: $\cfrac{\bigwedge\limits_{x\in X}\varphi_x}{\varphi_y}$ (for $y\in X$). The first rule, though, would need an infinite number of premises e.g. $\cfrac{\varphi_{x_0}\quad\varphi_{x_1}\quad\cdots}{\bigwedge\limits_{x\in X}\varphi_x}$ but this is usually disallowed even for the countable case and starts to become downright silly for the uncountable case. Nevertheless, this is explored in infinitary logic.

For classical logic, a semantics-based approach would suggest that the meaning of $\bigwedge\limits_{x\in X}\varphi_x$ should be $\bigcap\limits_{x\in X}[\![\varphi_x]\!]$. We have $y\in\bigcap\limits_{x\in X}[\![\varphi_x]\!]\iff \forall x.x\in X\to y\in[\![\varphi_x]\!]$. In the special case that $X$ is the universe of discourse, then this is just the interpretation of universal quantification. More generally, if $X=\{x\in D\mid \psi(x)\}$ for some formula $\psi$ of the logic where $D$ is the domain/universe of discourse, then we can completely represent this with the formula: $\forall x.\psi(x)\to\varphi(x,y)$ assuming the family of formulas $\{\varphi_x\}_{x\in X}$ can be represented with a single parameterized formula. From here, we can use the rules for quantifiers and implication to prove your statement. In other logics, universal quantification isn't naturally seen as a potentially infinitary generalization of conjunction, and this approach is not available.

Returning to a syntactic perspective, without taking an approach above, you immediately run into issues. What is $X$? In the context of logic you actually have to spell out what kinds of expressions can take the place of $X$. You could, for example, use a multi-sorted logic with a sort $\mathsf{set}$ to which you could add all the axioms of ZFC, say, and then you could introduce a $\bigwedge$ as a binding form that takes a $\mathsf{set}$ and an expression with a free $\mathsf{set}$-sorted variable. Of course, if you're willing to tack ZFC on to your theories, you can probably just embed your reasoning within the language of ZFC rather than axiomatizing it.

To answer your question, if $X$ is arbitrary, the most natural approach is probably the inifintary logic approach. Infinitary logic is quite non-standard, so if this is what you intended, then it should be stated in the question. If you've never heard of infinitary logic, as should be clear by now, the formulas you are talking about are not formulas of standard predicate logic and so your question doesn't have meaning in that context. This suggests that you may want to think about what you're trying to do differently. Nevertheless, here's how a syntactic argument may look in an infinitary logic. Note, the set theoretic notation is for specifying sets of derivations and is not part of the object language, i.e. the syntax of formulas in the logic.

First, the introduction rule for $\bigwedge$ described before is more formally described as $\cfrac{\{\Gamma\vdash\varphi_x\mid x\in X\}}{\Gamma\vdash\bigwedge\limits_{x\in X}\varphi_x}\bigwedge I$. The elimination rule, $\bigwedge E$, is as above: $\cfrac{\Gamma\vdash\bigwedge\limits_{x\in X}\varphi_x\quad y\in X}{\Gamma\vdash\varphi_y}\bigwedge E$.

$$\cfrac{ \cfrac{\left\{\cfrac{\cfrac{\cfrac{}{\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\vdash\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)}}{\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\vdash\varphi_x\land\psi_x}}{\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\vdash\varphi_x}\ \middle|\ x\in X\right\}} {\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\vdash\bigwedge\limits_{x\in X}\varphi_x}\ \cfrac{\left\{\cfrac{\cfrac{\cfrac{}{\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\vdash\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)}}{\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\vdash\varphi_x\land\psi_x}}{\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\vdash\psi_x}\ \middle|\ x\in X\right\}} {\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\vdash\bigwedge\limits_{x\in X}\psi_x}} {\cfrac{\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\vdash\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x}{\vdash \bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)\to\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x}}$$ and for the other direction $$\cfrac{ \cfrac{\left\{\cfrac{ \cfrac{ \cfrac{ \cfrac{} {\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x\vdash\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x}} {\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x\vdash\bigwedge\limits_{x\in X}\varphi_x}} {\bigwedge\limits_{x\in X}\varphi_x)\land\bigwedge\limits_{x\in X}\psi_x\vdash\varphi_x}\ \cfrac{\cfrac{ \cfrac{} {\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x\vdash\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x}} {\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x\vdash\bigwedge\limits_{x\in X}\psi_x}} {\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x\vdash\psi_x}} {\bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x\vdash\varphi_x\land\psi_x}\ \middle|\ x\in X\right\}}{ \bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x\vdash\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)}} {\vdash \bigwedge\limits_{x\in X}\varphi_x\land\bigwedge\limits_{x\in X}\psi_x\to\bigwedge\limits_{x\in X}(\varphi_x\land\psi_x)}$$

Answer 2

In your special case just notice that a "conjunction of conjunctions" is equivalent to the "conjunction of the conjuctions". This sounds confusing, but it is only to say that the conjunction is distributive with itself; this is not hard to see sice $\varphi\equiv \varphi\wedge\varphi$ and $(\varphi\wedge\psi)\wedge\chi\equiv \varphi\wedge(\psi\wedge\chi)$. Basicly you could prove it by induction on the size of $X$. For $|X|=1$ is trivial. And in the induction step you just enumerate the first $n$ terms and then use the case $n=2$.

Answer 3

You can use conjunction introduction and elimination to show that $\phi$⟺($\phi$$\land$$\phi$). That allows you to replace any instance of ($\phi$$\land$$\phi$) with $\phi$ anywhere ($\phi$$\land$$\phi$) appears within a well-formed formula. You also show that ($\phi$$\land$($\phi$$\land$$\phi$)) ⟺ (($\phi$$\land$$\phi$)$\land$$\phi$). That allows you fix an interpretation of an n-ary conjunction say as being left-associative. For example, $\land$ $\phi$ $\phi$ $\phi$ is a shorthand for (($\phi$$\land$$\phi$)$\land$$\phi$). Finally, you use mathematical induction to show that the result follows.

For the induction step, given that such holds for an n-ary conjunction, for an (n+1)-ary conjunction we have one extra conjunction symbol and $\phi$ at the end and two more parentheses. But, the earlier instance of ($\phi$$\land$$\phi$) can get reduced to $\phi$ by the idempotent equivalence above. This redues the (n+1)-ary conjunction to an n-ary conjunction and consequently the induction step follows.