New answers tagged


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 ...


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.


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\ (...


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