3

I'd really love your help with understanding how to refute/prove this following claims: (even general tips would be fine)

$t1=t2 \vdash _{FOL=}^t s\{t1/x\}=s\{t2/x\}$

$t1=t2 \vdash _{FOL=}^t t1\{s/x\}=t2\{s/x\}$

$t1=t2 \vdash _{FOL=}^v A\{{t1\{{s/x \}/y\}}}=A\{{t2\{{s/x \}/y\}}}$

$t1=t2 \vdash _{FOL=}^t A\{{t1\{{s/x \}/y\}}}=A\{{t2\{{s/x \}/y\}}}$

All of these similar claims are very confusing me- It looks like its all true and I just can't see how to approach it.

Jozef
  • 7,100
  • 2
    How to prove these depends critically on the precise formalization of first-order logic you're working with. Does $\vdash^t$ and $\vdash^v$ mean that different formal systems are being used? – hmakholm left over Monica Aug 03 '13 at 19:24
  • $A \vdash _{FOL=}^t B$ means that for every struct $M$ and assignment $v$ such that $ M,v \models A $ so does $ M,v \models B $. $A \vdash _{FOL=}^v B$ means that for every struct such that for all the assignments under its scope $ M,v \models A $ (OR: $ M \models A $) also this struct implies $ M \models B $. – Jozef Aug 03 '13 at 19:35

1 Answers1

2

The first item is true. You can prove it by induction on terms.

The second is false. A structure and valuation that makes $f(x) = g(x)$ true may not make $f(y) = g(y)$ true. The fourth item should be false for the same reason.

I don't follow the definition of "$A \vdash^v B$" well enough to answer the third item.

Carl Mummert
  • 81,604