Tag Info

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