New answers tagged

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