New answers tagged first-order-logic
3
I'm not sure this is exactly what you are looking for, but you might find what you want in Theorem 3.2.1 of Computability Theory by S. Barry Cooper:
All recursive functions are representable in PA.
that is for any recursive function $f$, there exists a binary predicate $F$ in the language of arithmetic such that for any natural numbers $x$ and $y$ we ...
1
Say you tried to solve $f(A, g(A)) = f(B, B)$ after applying $A \to B$ you'd then have $f(A, g(A)) = f(A, A)$ and you'd have to unify $A = g(A)$ as a sub problem.
0
If you say
$\forall x, x': ran\ routes . x<>x'$
You're only saying that the sequences are different. For example
$<London, Berlin, Paris>$ would be different to $<London, Paris, Berlin>$
Instead, you need two quantifiers
$\forall x: ran\ routes . \#x>20$
and
$\forall p,p': Place • p \in ran\ (ran\ routes) \land p' \in ran\ (...
2
Usually in practice we weld the two steps together and just say that from $p$ and $\lnot p$ anything follows, but in formal logic this is a combination of two rules of inference:
$p$ and $\lnot p$ both together entail falsehood $\bot$,
from $\bot$ anything follows.
These are precisely lines 9 and 10 in your proof.
We often take $\lnot p$ to be an ...
Top 50 recent answers are included
