Formal proof thought process

Question

I would happy to receive some external input on my thought process to shed light on my confusion.

Consider the proposition

\begin{equation} \exists B\in \mathbb{R}^{n\times n}, AB = I \implies \exists x\in\mathbb{R}^{n\times 1} , Ax = b \end{equation}

which is true since for $Bb \in \mathbb{R^{n\times 1}}$ we have $ABb = I b = b$.

I would like to pick apart how I prove this proposition and see the logical steps/method.

I would equivalently read the proposition as $$ B\in \mathbb{R}^{n\times n} \wedge AB = I \implies x\in\mathbb{R}^{n\times 1} \wedge Ax = b $$

If I now name the constitutents as follows $$ \underbrace{B\in \mathbb{R}^{n\times n} \wedge AB=I}_{=P} \implies \underbrace{x\in\mathbb{R}^{n\times 1}}_{=Q} \wedge\underbrace{Ax = b}_{=R} $$

then we have $$ P \implies Q \wedge R $$

Here is where I am confused and I think there is something that there is something obvious I am missing...

If I now check I proof then I am doing something like this

1. Assume Q
2. Prove $P\wedge Q\implies R$

Is this a reasonable approach?

Answer 1

As I commented, I would rewrite the proposition in a different way in order to make it more explicit.

First of all, it is better if you say where does $b$ belong to (though it is not strictly necessary). Hence, the proposition becomes \begin{equation} \exists B\in \mathbb{R}^{n\times n}, AB = I \implies \exists x\in\mathbb{R}^{n\times 1} , Ax = b\in\mathbb{R}^{n\times 1} \end{equation} Then, we've got something of the form \begin{equation} \exists B\ P(B)\Rightarrow\exists x\exists b Q(x,b) \end{equation} where $P(B)\equiv B\in\mathbb{R}^{n\times n}\land AB = I$ and $Q(x,b)\equiv x\in\mathbb{R}^{n\times 1}\land Ax = b\land b\in\mathbb{R}^{n\times 1}$.

What you're doing in the proof is the following:

1. Assume $\exists B\ P(B)$.
2. Take a particular $B$ such that $P(B)$.
3. Take $b\in\mathbb{R}^{n\times 1}$ (you know it exists) and get $Bb\in\mathbb{R}^{n\times 1}$.
4. $b$ and $x=Bb$ are such that $Q(x,b)$, hence $\exists x\exists bQ(x,b)$, and you're done.

Answer 2

First note that $b$ is a free variable. Typically, such free variables are implicitly universally quantified. So a closed form for the whole formula is:$$\forall n\in\mathbb N.\forall A\in\mathbb R^{n\times n}.\forall b\in\mathbb{R}^{n\times 1}.(\exists B\in\mathbb{R}^{n\times n}.AB=I)\implies\exists x\in\mathbb{R}^{n\times 1}.Ax=b$$ However, I will use the convention that free variables are universally quantified and also use that generally $(\exists y\in Y.P(y))\implies Q$ is logically equivalent to $\forall y\in Y.(P(y)\implies Q)$ to produce the simpler formula: $$AB=I\implies \exists x\in\mathbb{R}^{n\times 1}.Ax=b$$

This is where the informal derivation you briefly give starts. It next assumes $AB=I$ leaving $\exists x\in\mathbb{R}^{n\times 1}.Ax=b$ to be proven. It then chooses $x=Bb$ as a witness for the existential quantifier leaving $ABb=b$ to be proven which it does using the assumption $AB=I$ to produce $Ib=b$ which is true by the definition of $I$.

When you start to formalize the statement, though, you go completely off the rails. You simply drop the quantifiers as if they had no significance. You give no argument for why this is acceptable. As a suggestion, while you can analyze the bounded quantifiers $\forall x\in X.P(x)$ and $\exists x\in X.P(x)$ as $\forall x.x\in X\implies P(x)$ and $\exists x.x\in X\land P(x)$ respectively set-theoretically, it is simpler, clearer, and more general to simply view the bounded quantifiers $\forall x\in X.(\dots)$ and $\exists x\in X.(\dots)$ as primitive. Continuing, even if $P\implies Q\land R$ were the correct propositional structure, it states that we need to prove $Q$ (and $R$) from $P$, so why would we start by assuming $Q$? That's what we're trying to prove. (You could structure a proof of $P\implies Q\land R$ as a proof of $P\land Q \implies R$ and $P\implies Q$ and then combine those, but this is certainly not the obvious thing to do.) You are going to need to grapple with the quantifiers, so there is no reason to hide them behind proposition variables.

Here's a formal natural-deduction-like presentation. To formally describe these I'll use the notation $\Gamma\vdash P$ to mean "$P$ is provable from the statements in $\Gamma$". I'll use a vertical notation such as $\cfrac{\Gamma\vdash P\qquad\Gamma\vdash Q}{\Gamma\vdash P\land Q}$ which means if all of the top claims are true then the bottom is true, and the particular example says "if $P$ can be proven given the statements in $\Gamma$ and so can $Q$, then, given those same statements $P\land Q$ can be proven". These can be stacked vertically corresponding to chains of logic e.g. $\cfrac{\Gamma\vdash P}{\cfrac{\Gamma\vdash Q}{\Gamma\vdash R}}$ means $\cfrac{\Gamma\vdash P}{\Gamma\vdash Q}$ and $\cfrac{\Gamma\vdash Q}{\Gamma\vdash R}$.

Here are the rules we'll use. Implication introduction is $$\cfrac{\Gamma,P\vdash Q}{\Gamma\vdash P\implies Q}$$ Existential introduction is $$\cfrac{\Gamma\vdash P(t)}{\Gamma\vdash\exists x\in X.P(x)}$$ where $t$ is some term in $X$, and equality elimination is $$\cfrac{\Gamma\vdash x = y \qquad\Gamma\vdash P(y)}{\Gamma\vdash P(x)}$$ To start a derivation we have the rule $\cfrac{}{\Gamma,A\vdash A}$. In a natural deduction presentation of predicate logic, these rules (or minor variations on them) are primitive.

The formal derivation corresponding to the informal argument above is: $$\cfrac{\cfrac{}{Ib=b, AB=I\vdash AB=I}\qquad\cfrac{}{Ib=b, AB=I\vdash Ib=b}}{\cfrac{\cfrac{Ib=b, AB=I\vdash ABb=b}{Ib=b, AB=I\vdash \exists x\in\mathbb{R}^{n\times 1}.Ax=b}}{Ib=b\vdash AB=I\implies \exists x\in\mathbb{R}^{n\times 1}.Ax=b}}$$ where we start with the assumption $Ib=b$ to reflect the definition of $I$. (The uses of the rules should be labelled in the above derivation, but in this case it is reasonably clear which rule is being used in each step.) One thing to note about this is that the shape of the theorem we want to prove strongly guides the derivation. For example, the outermost connective at the beginning is an implication, so we start (reading bottom-up) with implication introduction. Then we the outermost connective is existential quantification, so we do an existential introduction. There definitely can be some ambiguity on which rule to use, but there is always only a few rules applicable at a time though they may be applicable in many different ways, e.g. existential introduction requires guessing an arbitrary term $t$ and there are very many wrong choices. Another thing to note is that the formal derivation fairly closely follows the informal derivation which was made without any reference to these rules. If a Hilbert-style proof system had been used, the formal derivation would have been quite a bit more opaque and nothing like the informal derivation. Natural deduction does do a reasonably good job of living up to its name.

Answer 3

I would equivalently read the proposition as $$B\in \mathbb{R}^{n\times n} \wedge AB = I \implies x\in\mathbb{R}^{n\times 1} \wedge Ax = b$$

That's not quite right. You can eliminate the $\exists B$ because $(\exists B, ~S) \to T$ is equivalent to $\forall B,~(S \to T)$ which is equivalent to $S \to T$ leaving $B$ arbitrary.

However, $S \to \exists x,~T$ is equivalent to $\exists x,~S \to T$, and you can't just ignore $\exists x$ because $x$ isn't arbitrary. So you should get

$$B\in \mathbb{R}^{n\times n} \wedge AB = I \implies \exists x ,~ x \in \mathbb{R}^{n\times 1} \wedge Ax = b$$

or

$$\exists x,~ B\in \mathbb{R}^{n\times n} \wedge AB = I \implies \mathbb{R}^{n\times 1} \wedge Ax = b$$

Either would be fine.

$$P \implies (Q \land R)$$ If I now check I proof then I am doing something like this

1. Assume Q
2. Prove $P\wedge Q\implies R$

Is this a reasonable approach?

I'm afraid that won't work. You'd still have $Q$ as an outstanding assumption. $P \to (Q \land R)$ is equivalent to $(P \to Q) \land (P \to R)$. You have to prove both independently. Note that you have chosen $x = Bb$. One you have identified that $x$, both proofs are straightforward.

---

This is what a formal proof in natural deduction would look like. Note that you do have to add the assumption that $b \in \mathbb{R}^{n \times 1}$.

$$\begin{array} {rll} % (1) & \quad b \in \mathbb {R}^{n \times 1} \land \exists B ,~ B \in \mathbb{R}^{n\times n} \land AB = I & \text{Assumption} \\ % (2) & \quad b \in \mathbb {R}^{n \times 1} & \text{And Elimination of 1} \\ % (3) & \quad \exists B ,~ B \in \mathbb{R}^{n\times n} \land AB = I & \text{And Elimination of 1} \\ % (4) & \quad \quad B \in \mathbb{R}^{n\times n} \land AB = I & \text{Assumption} \\ % (5) & \quad \quad AB = I & \text{And Elimination of 4} \\ % (6) & \quad \quad B \in \mathbb{R}^{n\times n} & \text{And Elimination of 4} \\ % (7) & \quad \quad A(Bb) = b & \text{Linear Algebra on 2, 5, 6} \\ % (8) & \quad \quad Bb \in \mathbb {R} ^ {n \times 1} & \text{Linear Algebra from 2 6} \\ % (9) & \quad \quad Bb \in \mathbb {R} ^ {n \times 1} \land A(Bb) = b & \text{And Introduction of 7 8} \\ % (10) & \quad \quad \exists x ~ x \in \mathbb {R} ^ {n \times 1} \land Ax = b & \text{Exists Introduction of 9} \\ % (11) & \quad b \in \mathbb{R}^{n \times 1} \implies \exists x,~ ~ x \in \mathbb {R} ^ {n \times 1} \land Ax = b & \text{Existential Elimination of 3, 4 through 10} \\ % (12) & \bigg(b \in \mathbb {R}^{n \times 1} \land \exists B ,~ B \in \mathbb{R}^{n\times n} \land AB = I\bigg) \implies \bigg(\exists x,~ ~ x \in \mathbb {R} ^ {n \times 1} \land Ax = b \bigg) & \text{Discharge assumption 1} \\ % \end{array}$$