Some mixed proposals

[feffemannen]

A few typos and proposed changes. Main changes:

• Using A[t/x] instead of A(t) in the ND-rules for FOL. Then a short comment on that A(t) will do in many contexts.
• Val(t)=t for the term model is used but not proved. Even though the proof isn't very interesting I think it makes sense to state this as a lemma.
• In the section on SOA the last corollary isn't correct. To correct it we need to complicate things a bit. I think it's enough to mention that addition and multiplication are definable. That already indicates that we don't "need" the axioms for addition and multiplication.

[rzach]

Thanks, these are all super useful and well taken. The exception is the stuff about removing the use of the conventions about A(x) and A(t) in the ND chapter. The convention about what A(t) means is explained at the end of the section on substitution. We use that convention practically everywhere after that section. I think it would be odd to do it here...at the very least we'd also have to change it in all the other proof system chapters. I could be persuaded to add a paragraph of explanation that makes explicit what instances of, say, \forall E count as correct though (and also in the other proof system chapters). What do you think? Do you gave strong feelings? Why the proposed change?

[rzach]

I'm thinking something like this paragraph added at the end of the section:

Recall the convention that when $!A$ is !!a{formula} with the !!{variable}~$x$ free, we indicate this by 
writing~$!A(x)$. In the same context, $!A(t)$ then is short for~$\Subst{!A}{t}{x}$.  So we could also write 
the $\Intro\lexists$ rule as $\Subst{!A}{t}{x} / \lexists[x][!A]$.  Note that $t$ may already occur  in~$!A$, say, 
$!A$ might be $P(t,x)$.  Thus, inferring $\lexists[x][\Atom{\Obj P}{t,x}]$ from $\Atom{\Obj P}{t,t}$ is a 
correct application of~$\Intro\lexists$---you may ``replace'' one or more, and not necessarily all, 
occurrences of~$t$ in in the premise by the bound !!{variable}~$x$.  However, the eigenvariable conditions 
in $\Intro\lforall$ and $\Elim\lexists$ require that the !!{constant}~$a$ does not occur in~$!A$. So, you 
cannot correctly infer $\lforall[x][\Atom{\Obj P}{a,x}]$ from $\Atom{\Obj P}{a,a}$ using~$\Intro\lforall$.

How's that?

If that's as good as your proposed change to the quantifier rules, then feel free to make that change and push to update the pull request. That'll save me cherry-picking the other commits from the pull request. You can use git reset <path> to undo the changes to content/first-order-logic/natural-deduction/quantifier-rules.tex and then copy (something like) this plus your last paragraph back into the file.

[feffemannen]

That's completely fine with me. Thanks!

Hopefully I got the revert and new commit correct, please check!

[rzach]

Wait what was wrong with the original TM? (The doubler machine always leaves blanks at the beginning--except if the input is blank, but that's another problem.)

[feffemannen]

It halts in state q_9. And even if you modify it with a transition from q_8 to q_10 and an extra transition from q_10 to q_11 (when reading a stroke) it will still write one stroke too much to the tape.