2

I'm reading Language, Proof and Logic. I'm trying to understand this proof:

enter image description here

"= Intro" and "= Elim" are:

enter image description here

I understand the use of "= Intro" in the proof, but how exactly are we using "= Elim"? What is $p(n)$? I suspect $p(n) := [n=b]$. So we have in the fourth line:

  • $p(b)$ which means $b=b$
  • $b=a$
  • $p(a)$ which means $a=b$

Is that it?

Red Banana
  • 23,956
  • 20
  • 91
  • 192

2 Answers2

3

Almost! The $P(n)$ is a formula that has some number of instances of the variable-free term $n$, and the $P(m)$ is the formula that is the result of replacing zero or more of those $n$'s with $m$'s given that $n = m$

So ... the '$n=m$' claim corresponds to the $b = a$ claim on line 2, meaning that the '$n$' is $b$, and the '$m$' is $a$. The '$P(n)$' is $b = b$ on line 3, and the $P(m)$ is $a=b$ on line 4.

So yes, you correctly identified that the $b=a$ claim was the 'substitution' claim that you applied to the claim $b=b$ ... but it is not quite true that the '$P(n)$' claim is $n = b$.... it is simply $b=b$.

However, I think you were trying to think about it this way:

Let the formula $P(x)$ be the expression $x = b$

Then $P(b)$ is the result of taking formula $P(x)$, and instantiating the free variable $x$ with constant $b$.

So, $P(b)$ is $b = b$

Likewise, $P(a)$ is the result of taking formula $P(x)$, and instantiating the free variable $x$ with constant $a$.

So, $P(a)$ is $ a = b$

Identifying a formula $P(x)$ of which both the 'before' expression $P(n)$ and the 'after' expression $P(m)$ are instances (or in our case $P(a)$ and $P(b)$) is indeed a helpful way to think about $= Elim$. It may also make it a little more clear as to why you don't have to replace all occurrences of some constant in an expression with some other constant.

That is, had we defined $P(x)$ as $x = x$, then $P(b)$ would still have been $b = b$, but $P(a)$ would then have been $a = a$. And if $P(x)$ would have been $b = x$, then $P(a)$ would have been $b = a$.

Perversely, we could even have defined $P(x)$ as $b = b$. Then $P(a)$ would still have been $b = b$. So, if you infer $b = b$ from $b = b$ and $b = a$ using $= Elim$ in the proof-checker software, it should still check out. Try it!

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • Yeah, I thought that $P(m)$ could also represent a "constant" in the same way that there are functions such as $f(x)=1$. But I thought that not putting the variable somewhere would be a mistake or something. – Red Banana Dec 21 '20 at 13:35
  • 1
    @BillyRubina Again, you're right conceptually ... but still don't quite use the notarion correctly. The $n$ In the $P(n)$ expression is a constant, not a variable. Thus, the $n$ corresponds to $a$. Likewise, $P(n)$ is already a specific instance of a general formula ... what I referred to as $P(x)$ in my post. So, $P(n)$ is what you get when plugging in $n$ for $x$ in $P(x)$. Indeed, $P(n)$ corresponds to $P(a)$. Also, $P(m)$ corresponds to $P(b)$. But, as far as the general formula goes, it could indeed work similar to a constant function, e.g. You could have that $P(x)$ is $b=b$. – Bram28 Dec 21 '20 at 13:57
  • This is so odd. So when are "variables" actual variables? – Red Banana Dec 21 '20 at 15:06
  • 1
    @BillyRubina Well, in logic variables are typically letters like $x,y,z$ (near end of alphabet) ... while constants are letters like $a,b,c$ (early in alphabet)... you'll know for certain that are dealing with a variable when a quantifier $\forall$ or $\exists$ appears in front of them ... though I suspect you're only at chapter 2 (I know the book) and haven;t seen those quantifiers yet. Indeed, until part II of the book, you don;t deal with variables at all ... just constants. ... (continued) – Bram28 Dec 21 '20 at 15:11
  • 1
    @BillyRubina Now, confusingly, when a rule like $= \ Elim$ is described, they use letters as well, in this case $m$ and $n$. So, what are they? Well, they are not logical variables ... a logic variable like $x$ is a letter in the alphabet that, in the logic language, is used to denote some arbitrary object from your doamin of objects (e.g. blocks in Tarski's world). Rather, they are 'mathematical variables' in the sense that you can use any constant in its place .. you might call them 'meta-logic variables' or 'linguistics variable': a placeholders that says: you can use any constant here. – Bram28 Dec 21 '20 at 15:13
  • Yes, I'm at chapter 2. – Red Banana Dec 21 '20 at 15:34
  • 1
    Your first sentence claiming that "n" in "P(n)" is a constant is inconsistent with LPL, which said "This rule allows you to introduce, for any name (or complex term) n in use in the proof, the assertion n = n." just before the =Intro rule, and did not say anything in-between that and the =Elim rule. So there is nothing wrong with @BillyRubina's definition of P(n). – user21820 Dec 21 '20 at 19:02
  • 1
    @user21820 You're of course right that the $n$ could be a complex term.... I forgot about that. But still, I believe BillyRubina tried to parse this whole thing as there being some general formula $P(n)$ in which you can substitute $a$ for $n$, as well as $b$ for $n$, resulting in $P(a)$ and $P(b)$ respectively. That is not quite right IMO. I would say a better way to look at this is that $P(n)$ simply corresponds to $P(a)$, and the $P(m)$ to $P(b)$. If there is any general formula of which both are instances, it would be better constructed as some kind of $P(x)$ with $x$ being a variable. – Bram28 Dec 21 '20 at 19:13
  • 1
    Ah, so can you fix your first paragraph concerning constants? Actually I think that @BillyRubina had the right idea. We simply define the predicate $P$ via $P(n) ≡ n=b$, and then we literally have $P(b)$ and $b=a$ and hence can deduce $P(a) ≡ a=b$. – user21820 Dec 22 '20 at 18:46
  • 1
    @user21820 Right, I think I am just splitting hairs here! Yes, Billy had the right idea ... I just disagree that the general formula should have been defined in terms of $n$ since the '$n$' only corresponds to the $a$, and not the $b$... the latter coresponds to $m$, not $n$. And so if you want a general formula I think you should call it $P(x)$ of which both $P(a)/P(n)$ and $P(b)/P(m)$ are instances. But like I said, splitting hairs! – Bram28 Dec 22 '20 at 20:22
  • 1
    Ah okay. Let's have just a little bit more fun splitting hairs then. As I quoted, LPL says that n can be any complex term, so implicitly LPL's description of the =elim rule quantifies over every complex term n. Thus we can treat "n" as bound within the rule description but unbound outside. Hence it makes sense for us to define a predicate using the variable "n" to stand for any term in exactly the same way that LPL uses it. In other words, the =elim rule is applied to the predicate $P$ that I just defined. In any case, please fix the first paragraph. =) – user21820 Dec 23 '20 at 14:34
  • @user21820 OK, I think I see that! Finally fixed that first paragraph too. Thanks for your feedback and analysis! – Bram28 Dec 23 '20 at 15:07
  • Thanks, and welcome! =) – user21820 Dec 23 '20 at 15:11
2

Equality elimination is a rule of substitution: When $n=m$ is given then we may substitute any (some or all) occurrences of $n$, in a statement, for $m$ .

When $P(n)$ is a statement containing some occurrences of $n$, then $P(m)$ is that statement with those occurrences replaced with $m$, and so when we have the equality $n=m$ we may 'eliminate' this to say: $$\begin{array}{l}P(n)\\n=m\\\hline P(m)\end{array}$$

So your proof is using equality elimination to make the inferences that:

$$\begin{array}{l}3.~b=b\\2.~b=a\\\hline4.~a=b\hspace{4ex}{=}\textsf{E 3,2}\end{array}\qquad\begin{array}{l}1.~\operatorname{SameRow}(a,a)\\4.~a=b\\\hline5.~\operatorname{SameRow}(b,a)\hspace{2ex}{=}\textsf{E 1,4}\end{array}$$

Where the equality being 'eliminated' is the second line referenced in the rule, and has the form [original] = [substitute].

The first inference is a common subproof using equality introduction to 'flip' an equality around so we have the required order for the second inference.

So we put this together with the equality introduction to claim:

$$\begin{array}{|l}1.~\operatorname{SameRow}(a,a)\\2.~b=a\\\hline3.~b=b\hspace{12ex}{=}\textsf{I}~\\4.~a=b\hspace{12ex}{=}\textsf{E 3,2 }\\5.~\operatorname{SameRow}(b,a)\hspace{2ex}{=}\textsf{E 1,4}\end{array}$$

Graham Kemp
  • 129,094